From def15c3748599d5c05cae164653e85ea03da6be6 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 30 Jan 2019 16:38:38 +0100
Subject: Clean and comment methods file

---
 HoTT_Methods.thy | 75 +++++++++++++++++++++++++-------------------------------
 1 file changed, 34 insertions(+), 41 deletions(-)

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index f0cee6c..99f3446 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -1,80 +1,73 @@
-(*
-Title:  HoTT_Methods.thy
-Author: Joshua Chen
-Date:   2018
+(********
+Isabelle/HoTT: Proof methods
+Jan 2019
 
-Method setup for the HoTT logic.
-*)
+********)
 
 theory HoTT_Methods
 imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 
 begin
 
+section \<open>Substitution and simplification\<close>
 
-section \<open>Handling universes\<close>
+ML_file "~~/src/Tools/misc_legacy.ML"
+ML_file "~~/src/Tools/IsaPlanner/isand.ML"
+ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
+ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
+ML_file "~~/src/Tools/eqsubst.ML"
+\<comment> \<open>Import the @{method subst} method, used for substituting definitional equalities.\<close>
 
-method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
+text \<open>
+Method @{theory_text compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context.
+Premises of the rule(s) applied are added as new subgoals.
+\<close>
 
-method hierarchy = (rule U_hierarchy, provelt)
+method compute declares comp = (subst comp)
 
-method cumulativity declares form = (
-  ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) |
-  ((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
-)
+section \<open>Handling universes\<close>
 
 text \<open>
-Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form
+Methods @{theory_text provelt}, @{theory_text hierarchy}, and @{theory_text cumulativity} prove propositions of the form
+
 \<^item> \<open>n < (Suc (... (Suc n) ...))\<close>,
 \<^item> \<open>U i: U (Suc (... (Suc i) ...))\<close>, and
-\<^item> @{prop "A: U i \<Longrightarrow> A: U j"}, where @{prop "i \<le> j"}
-respectively.
-\<close>
-
-
-section \<open>Deriving typing judgments\<close>
+\<^item> @{prop "A: U i \<Longrightarrow> A: U j"}, where @{prop "i \<le> j"},
 
-method routine uses add = (assumption | rule add | rule)+
-
-text \<open>
-The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier \<open>add\<close>.
+respectively.
 \<close>
 
+method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
 
-section \<open>Substitution and simplification\<close>
+method hierarchy = (rule U_hierarchy, provelt)
 
-ML_file "~~/src/Tools/misc_legacy.ML"
-ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
-ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "~~/src/Tools/eqsubst.ML"
+method cumulativity declares form = (
+  ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) |
+  ((elim U_cumulative | (rule U_cumulative, rule form)), provelt)
+)
 
-\<comment> \<open>Import the @{method subst} method, used for substituting definitional equalities.\<close>
+section \<open>Deriving typing judgments\<close>
 
-method compute declares comp = (subst comp)
+method routine uses add = (assumption | rule add | rule)+
 
 text \<open>
-Method @{method compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context.
-Premises of the rule(s) applied are added as new subgoals.
+The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}.
 \<close>
 
-
 section \<open>Derivation search\<close>
 
 text \<open>
-Combine @{method routine} and @{method compute} to search for derivations of judgments.
-Also handle universes using @{method hierarchy} and @{method cumulativity}.
+The method @{theory_text derive} combines @{method routine} and @{method compute} to search for derivations of judgments.
+It also handles universes using @{method hierarchy} and @{method cumulativity}.
 \<close>
 
 method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
 
-
 section \<open>Induction\<close>
 
 text \<open>
-Placeholder section for the automation of induction, i.e. using the elimination rules.
-At the moment one must directly apply them with \<open>rule X_elim\<close>.
+Placeholder section for the automation of induction, i.e. using the type elimination rules.
+At the moment one must directly apply them with @{method rule} or @{method elim}.
 \<close>
 
-
 end
-- 
cgit v1.2.3