From 8833cdf99d3128466d85eb88aeb8e340e07e937c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 23:27:25 +0200
Subject: Reorganize methods

---
 HoTT_Methods.thy | 42 +++++++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 19 deletions(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 4d2174b..32e412b 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -12,23 +12,19 @@ theory HoTT_Methods
 begin
 
 
-section \<open>Method definitions\<close>
-
-subsection \<open>Simple type rule proof search\<close>
+section \<open>Deriving typing judgments\<close>
 
 text "
-  Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas.
-  
-  Can also perform typechecking, and search for elements of a type.
+  \<open>routine\<close> proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas.
 "
 
-method simple uses lems = (assumption | rule lems | standard)+
-
-
-subsection \<open>Wellformedness checker\<close>
+method routine uses lems = (assumption | rule lems | standard)+
 
 text "
-  \<open>wellformed\<close> finds a proof of any valid typing judgment derivable from the judgments passed as \<open>lem\<close>.
+  \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>.
+  If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>.
+  \<open>wellform\<close> is like \<open>wellformed'\<close> but takes multiple judgments.
+
   The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy.
 "
 
@@ -42,14 +38,7 @@ method wellformed uses lems =
   match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close>
 
 
-subsection \<open>Derivation search\<close>
-
-text " Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments."
-
-method derive uses lems = (simple lems: lems | wellformed lems: lems)+
-
-
-subsection \<open>Substitution and simplification\<close>
+section \<open>Substitution and simplification\<close>
 
 text "Import the \<open>subst\<close> method, used for substituting definitional equalities."
 
@@ -64,4 +53,19 @@ text "Perform basic single-step computations:"
 method compute uses lems = (subst lems comp | rule lems comp)
 
 
+section \<open>Derivation search\<close>
+
+text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments."
+
+method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+
+
+
+section \<open>Induction\<close>
+
+text "
+  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>.
+"
+
+
 end
-- 
cgit v1.2.3