diff options
Diffstat (limited to 'ex')
-rw-r--r-- | ex/HoTT Book/Ch1.thy | 37 | ||||
-rw-r--r-- | ex/Methods.thy | 4 | ||||
-rw-r--r-- | ex/Synthesis.thy | 10 |
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 |