3 files changed, 44 insertions, 7 deletions
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