Tweak proof methods, some type rules; add HoTT Book examples

7 files changed, 87 insertions, 50 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index 2da7e2f..9b43345 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -26,7 +26,7 @@ text "
 lemma inv_type:
   assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
 unfolding inv_def
-by (rule Equal_elim[where ?x=x and ?y=y]) (simple lem: assms)
+by (rule Equal_elim[where ?x=x and ?y=y]) (simple lems: assms)
   \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close>
 
 text "
@@ -39,7 +39,7 @@ lemma inv_comp:
 unfolding inv_def
 proof
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
-qed (simple lem: assms)
+qed (simple lems: assms)
 
 
 section \<open>Transitivity / Path composition\<close>
@@ -75,18 +75,18 @@ proof
           proof
             fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z"
             show "ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms asm)
-          qed (simple lem: assms)
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm)
+          qed (simple lems: assms)
         qed (rule assms)
-      qed (simple lem: assms 1 2 3)
-    qed (simple lem: assms 1 2)
+      qed (simple lems: assms 1 2 3)
+    qed (simple lems: assms 1 2)
   qed (rule assms)
 qed fact
 
 corollary
   assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
   shows "reqcompose`x`y`p`z`q: x =\<^sub>A z"
-  by (simple lem: assms reqcompose_type)
+  by (simple lems: assms reqcompose_type)
 
 text "
   The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule.
@@ -112,11 +112,11 @@ proof (subst comp)
           proof
             fix u z assume asm: "u: A" "z: A"
             show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms asm)
-          qed (simple lem: assms)
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm)
+          qed (simple lems: assms)
         qed (rule assms)
-      qed (simple lem: assms 1 2 3)
-    qed (simple lem: assms 1 2)
+      qed (simple lems: assms 1 2 3)
+    qed (simple lems: assms 1 2)
   qed (rule assms) }
 
   show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \<equiv> refl(a)"
@@ -134,11 +134,11 @@ proof (subst comp)
             show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
             proof
               show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-              by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 3 4)
-            qed (simple lem: assms 3 4)
+              by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 3 4)
+            qed (simple lems: assms 3 4)
           qed fact
-        qed (simple lem: assms 1 2)
-      qed (simple lem: assms 1) }
+        qed (simple lems: assms 1 2)
+      qed (simple lems: assms 1) }
     
     show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \<equiv> refl(a)"
     proof (subst comp)
@@ -152,10 +152,10 @@ proof (subst comp)
           show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A u \<rightarrow> u =\<^sub>A z"
           proof
             show "\<And>q. q: u =\<^sub>A u \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 2 3)
-          qed (simple lem: assms 2)
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 2 3)
+          qed (simple lems: assms 2)
         qed fact
-      qed (simple lem: assms 1) }
+      qed (simple lems: assms 1) }
       
       show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)"
       proof (subst comp)
@@ -166,8 +166,8 @@ proof (subst comp)
           show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A u \<rightarrow> u =\<^sub>A z"
           proof
             show "\<And>q. q: u =\<^sub>A u \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
-            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 1 2)
-          qed (simple lem: assms 1)
+            by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 1 2)
+          qed (simple lems: assms 1)
         qed fact }
         
         show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)"
@@ -176,21 +176,21 @@ proof (subst comp)
           show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
           proof
             show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a"
-            by (rule Equal_elim[where ?x=a and ?y=a]) (simple lem: assms 1)
-          qed (simple lem: assms 1) }
+            by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms 1)
+          qed (simple lems: assms 1) }
           
           show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)"
           proof (subst comp)
             show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a"
-            by (rule Equal_elim[where ?x=a and ?y=a]) (simple lem: assms)
+            by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms)
             show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)"
             proof
               show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" ..
-            qed (simple lem: assms)
-          qed (simple lem: assms)
+            qed (simple lems: assms)
+          qed (simple lems: assms)
         qed fact
-      qed (simple lem: assms)
-    qed (simple lem: assms)
+      qed (simple lems: assms)
+    qed (simple lems: assms)
   qed fact
 qed fact
 
@@ -210,11 +210,11 @@ lemma eqcompose_type:
   shows "p \<bullet> q: x =\<^sub>A z"
 proof (subst eqcompose_def)
   show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
-qed (simple lem: assms reqcompose_type)
+qed (simple lems: assms reqcompose_type)
 
 lemma eqcompose_comp:
   assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)"
-by (subst eqcompose_def) (simple lem: assms reqcompose_comp)
+by (subst eqcompose_def) (simple lems: assms reqcompose_comp)
 
 
 lemmas EqualProps_rules [intro] = inv_type eqcompose_type
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index e2eb4f1..d7f0821 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -23,7 +23,7 @@ text "
   Can also perform typechecking, and search for elements of a type.
 "
 
-method simple uses lem = (assumption | rule lem | standard)+
+method simple uses lems = (assumption | rule lems | standard)+
 
 
 subsection \<open>Wellformedness checker\<close>
@@ -33,21 +33,21 @@ text "
   The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy.
 "
 
-method wellformed' uses jmt declares wellform =
+method wellformed' uses jdmt declares wellform =
   match wellform in rl: "PROP ?P" \<Rightarrow> \<open>(
-    catch \<open>rule rl[OF jmt]\<close> \<open>fail\<close> |
-    catch \<open>wellformed' jmt: rl[OF jmt]\<close> \<open>fail\<close>
+    catch \<open>rule rl[OF jdmt]\<close> \<open>fail\<close> |
+    catch \<open>wellformed' jdmt: rl[OF jdmt]\<close> \<open>fail\<close>
     )\<close>
 
-method wellformed uses lem =
-  match lem in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jmt: lem\<close>
+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 lem = (simple lem: lem | wellformed lem: lem)+
+method derive uses lems = (simple lems: lems | wellformed lems: lems)+
 
 
 subsection \<open>Substitution and simplification\<close>
diff --git a/Prod.thy b/Prod.thy
index 496bf3e..59c6cc3 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -43,7 +43,7 @@ and
 and
   Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)"
 and
-  Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)"
+  Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)"
 and
   Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f"
 
diff --git a/Proj.thy b/Proj.thy
index 5c05eb2..d5ae6fa 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -20,7 +20,7 @@ text "Typing judgments and computation rules for the dependent and non-dependent
 
 lemma fst_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
-unfolding fst_def by (derive lem: assms)
+unfolding fst_def by (derive lems: assms)
 
 lemma fst_comp:
   assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
@@ -33,14 +33,14 @@ lemma snd_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
 unfolding snd_def
 proof
-  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (derive lem: assms fst_type)
+  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (derive lems: assms fst_type)
   
   fix x y
   assume asm: "x: A" "y: B(x)"
   show "y: B(fst <x,y>)"
   proof (subst fst_comp)
-    show "A: U(i)" by (wellformed lem: assms(1))
-    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" by (wellformed lem: assms(1))
+    show "A: U(i)" by (wellformed lems: assms(1))
+    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" by (wellformed lems: assms(1))
   qed fact+
 qed fact
 
@@ -51,13 +51,13 @@ proof
   show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
   show "a: A" by fact
   show "b: B(a)" by fact
-qed (simple lem: assms)
+qed (simple lems: assms)
 
 
 text "Rule declarations:"
 
 lemmas Proj_types [intro] = fst_type snd_type
-lemmas Proj_comps [intro] = fst_comp snd_comp
+lemmas Proj_comps [comp] = fst_comp snd_comp
 
 
 end
\ No newline at end of file
diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT Book/Ch1.thy
new file mode 100644
index 0000000..84a5cf4
--- /dev/null
+++ b/ex/HoTT Book/Ch1.thy
@@ -0,0 +1,37 @@
+theory Ch1
+  imports "../../HoTT"
+begin
+
+chapter \<open>HoTT Book, Chapter 1\<close>
+
+section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
+
+text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor."
+
+schematic_goal
+  assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
+  shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>"
+
+text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:"
+
+proof (rule Sum_elim[where ?p=p])
+  text "We just need to prove the base case; the rest will be taken care of automatically."
+
+  fix x y assume asm: "x: A" "y: B(x)" show
+    "refl(<x,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>"
+  proof (subst (0 1) comp)
+    text "
+      The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> have appropriate types.
+      The automatic proof methods have trouble picking the appropriate types, so we state them explicitly,
+    "
+    show "x: A" and "y: B(x)" by (fact asm)+
+
+    text "...twice, once each for the substitutions of \<open>fst\<close> and \<open>snd\<close>."
+    show "x: A" and "y: B(x)" by (fact asm)+
+
+  qed (derive lems: assms asm)
+
+qed (derive lems: assms)
+
+
+end
\ No newline at end of file
diff --git a/ex/Methods.thy b/ex/Methods.thy
index b0c5f92..699d620 100644
--- a/ex/Methods.thy
+++ b/ex/Methods.thy
@@ -13,7 +13,7 @@ begin
 lemma
   assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)"
   shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)"
-by (simple lem: assms)
+by (simple lems: assms)
 
 
 lemma
@@ -29,7 +29,7 @@ proof -
     "B: A \<longrightarrow> U(i)" and
     "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
     "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
-  by (derive lem: assms)
+  by (derive lems: assms)
 qed
 
 
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index 60655e5..48d762c 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -33,10 +33,10 @@ text "
 "
 
 schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n"
-apply (subst comp, rule Nat_rules)
-prefer 3 apply (subst comp, rule Nat_rules)
+apply (subst comp)
+prefer 4 apply (subst comp)
 prefer 3 apply (rule Nat_rules)
-prefer 8 apply (rule Nat_rules | assumption)+
+apply (rule Nat_rules | assumption)+
 done
 
 text "
@@ -49,7 +49,7 @@ definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat
 lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by simple
 
 lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
-proof (simple lem: pred_type)
+proof (simple lems: pred_type)
   have *: "pred`0 \<equiv> 0" unfolding pred_def
   proof (subst comp)
     show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple
@@ -75,7 +75,7 @@ qed
 
 theorem
   "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
-by (simple lem: pred_welltyped pred_type pred_props)
+by (simple lems: pred_welltyped pred_type pred_props)
 
 
 end
\ No newline at end of file