aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-07-07 22:59:13 +0200
committerJosh Chen2018-07-07 22:59:13 +0200
commit8541c7d0748d06676e5eb52d61cf468858d590e2 (patch)
tree27ee06b904239c0ba318749a0237a333990b83b2
parent1651beafbe7198a320fe87a926bf23e2ab1b784a (diff)
Methods added and organized!
-rw-r--r--HoTT_Methods.thy87
1 files changed, 40 insertions, 47 deletions
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