diff options
| -rw-r--r-- | EqualProps.thy | 58 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 14 | ||||
| -rw-r--r-- | Prod.thy | 2 | ||||
| -rw-r--r-- | Proj.thy | 12 | ||||
| -rw-r--r-- | ex/HoTT Book/Ch1.thy | 37 | ||||
| -rw-r--r-- | ex/Methods.thy | 4 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 10 |
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> @@ -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" @@ -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 |