From 8541c7d0748d06676e5eb52d61cf468858d590e2 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 7 Jul 2018 22:59:13 +0200
Subject: Methods added and organized!

---
 HoTT_Methods.thy | 87 ++++++++++++++++++++++++++------------------------------
 1 file changed, 40 insertions(+), 47 deletions(-)

(limited to 'HoTT_Methods.thy')

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 81e2055..1f11230 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -10,11 +10,28 @@ theory HoTT_Methods
     "HOL-Eisbach.Eisbach"
     "HOL-Eisbach.Eisbach_Tools"
     HoTT_Base
-    Prod
 begin
 
 
-section \<open>Method setup\<close>
+text "The methods \<open>simple\<close>, \<open>wellformed\<close>, \<open>derive\<close>, and \<open>simplify\<close> should together should suffice to automatically prove most HoTT theorems.
+We also provide a method
+"
+
+
+section \<open>Setup\<close>
+
+text "Import the \<open>subst\<close> method, used by \<open>simplify\<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"
+
+
+section \<open>Method definitions\<close>
+
+subsection \<open>Simple type rule proof search\<close>
 
 text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas.
 
@@ -23,9 +40,11 @@ Can also perform typechecking, and search for elements of a type."
 method simple uses lems = (assumption | standard | rule lems)+
 
 
-text "Find a proof of any valid typing judgment derivable from a given wellformed judgment."
+subsection \<open>Wellformedness checker\<close>
+
+text "Find a proof of any valid typing judgment derivable from a given wellformed judgment.
+The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy."
 
-\<comment> \<open>\<open>wellform\<close> is declared in HoTT_Base.thy\<close>
 method wellformed uses jdgmt declares wellform =
   match wellform in rl: "PROP ?P" \<Rightarrow> \<open>(
     catch \<open>rule rl[OF jdgmt]\<close> \<open>fail\<close> |
@@ -33,11 +52,11 @@ method wellformed uses jdgmt declares wellform =
     )\<close>
 
 
-text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations.
-\<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments.
-Definitions passed as \<open>unfolds\<close> are unfolded throughout.
+subsection \<open>Derivation search\<close>
 
-Roughly speaking \<open>derive\<close> is more powerful than \<open>simple\<close>, but may fail to find a proof where \<open>simple\<close> does if it reduces too eagerly."
+text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments.
+\<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments.
+Definitions passed as \<open>unfolds\<close> are unfolded throughout."
 
 method derive uses lems unfolds = (
   unfold unfolds |
@@ -46,45 +65,19 @@ method derive uses lems unfolds = (
   )+
 
 
-text "Simplify a function application."
-
-method simplify for expr::Term uses lems = match (expr) in
-  "(\<^bold>\<lambda>x:?A. ?b x)`?a" \<Rightarrow> \<open>
-    print_term "Single application",
-    rule Prod_comp,
-    derive lems: lems
-    \<close> \<bar>
-  "(F`a)`b" for F a b \<Rightarrow> \<open>
-    print_term "Repeated application",
-    simplify "F`a"
-    \<close>
-  
-
-
-text "Verify a function application simplification."
-
-method verify_simp uses lems = (
-  print_term "Attempting simplification",
-  ( rule comp | derive lems: lems | simp add: lems )+
-  | print_fact lems,
-    match conclusion in
-    "F`a`b \<equiv> x" for F a b x \<Rightarrow> \<open>
-      print_term "Chained application",
-      print_term F,
-      print_term a,
-      print_term b,
-      print_term x,
-      match (F) in
-        "\<^bold>\<lambda>x:A. f x" for A f \<Rightarrow> \<open>
-          print_term "Matched abstraction",
-          print_fact Prod_comp[where ?A = A and ?b = f and ?a = a]
-          \<close> \<bar>
-        "?x" \<Rightarrow> \<open>
-          print_term "Constant application",
-          print_fact comp
-          \<close>
-      \<close>
-  )
+subsection \<open>Simplification\<close>
+
+text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> simplify lambda applications and attempt to solve definitional equations.
+
+\<open>rsimplify\<close> can also be used to search for lambda expressions inhabiting given types.
+
+Since these methods use \<open>derive\<close>, it is often (but not always) the case that theorems provable with \<open>derive\<close> are also provable with them.
+(Whether this is the case depends on whether the call to \<open>subst (0) comp\<close> fails.)"
+
+method rsimplify uses lems = (subst (0) comp, derive lems: lems)+
+  \<comment> \<open>\<open>subst\<close> performs an equational rewrite according to some computation rule declared as [comp], after which \<open>derive\<close> attempts to solve any new assumptions that arise.\<close>
+
+method simplify uses lems = (simp add: lems | rsimplify lems: lems)+
 
 
 end
\ No newline at end of file
-- 
cgit v1.2.3