diff options
Diffstat (limited to '')
-rw-r--r-- | EqualProps.thy | 85 |
1 files changed, 43 insertions, 42 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index c114d37..708eb33 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -14,7 +14,7 @@ begin section \<open>Symmetry / Path inverse\<close> -definition inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl(x)) p" +definition inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p" text " In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use. @@ -22,7 +22,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" + 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]) (routine 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> @@ -33,7 +33,7 @@ text " " lemma inv_comp: - assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)" + assumes "A : U i " and "a : A" shows "(refl a)\<inverse> \<equiv> refl a" unfolding inv_def proof compute show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. @@ -46,14 +46,14 @@ text " Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. " -definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" +definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: " lemma rpathcomp_type: - assumes "A: U(i)" + assumes "A: U i" shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" unfolding rpathcomp_def proof @@ -81,7 +81,7 @@ proof qed fact corollary - assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" by (routine lems: assms rpathcomp_type) @@ -90,11 +90,11 @@ text " " lemma rpathcomp_comp: - assumes "A: U(i)" and "a: A" - shows "rpathcomp`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" + assumes "A: U i" and "a: A" + shows "rpathcomp`a`a`(refl a)`a`(refl a) \<equiv> refl a" unfolding rpathcomp_def proof compute - { fix x assume 1: "x: A" + fix x assume 1: "x: A" show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" proof fix y assume 2: "y: A" @@ -114,11 +114,11 @@ proof compute qed (rule assms) qed (routine lems: assms 1 2 3) qed (routine lems: assms 1 2) - qed (rule assms) } + 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)" + next 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" proof compute - { fix y assume 1: "y: A" + fix y assume 1: "y: A" show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)" proof fix p assume 2: "p: a =\<^sub>A y" @@ -135,11 +135,11 @@ proof compute qed (routine lems: assms 3 4) qed fact qed (routine lems: assms 1 2) - qed (routine lems: assms 1) } + qed (routine 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)" + next 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 compute - { fix p assume 1: "p: a =\<^sub>A a" + fix p assume 1: "p: a =\<^sub>A a" show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A z \<rightarrow> a =\<^sub>A z" proof (rule Equal_elim[where ?x=a and ?y=a]) fix u assume 2: "u: A" @@ -152,11 +152,11 @@ proof compute by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) qed (routine lems: assms 2 3) qed fact - qed (routine lems: assms 1) } + qed (routine lems: assms 1) - show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)" + next show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \<equiv> refl a" proof compute - { fix u assume 1: "u: A" + fix u assume 1: "u: A" show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" proof fix z assume 2: "z: A" @@ -165,22 +165,22 @@ proof compute 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]) (routine lems: assms 1 2) qed (routine lems: assms 1 2) - qed fact } + qed fact - show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)" + next show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`(refl a) \<equiv> refl a" proof compute - { fix a assume 1: "a: A" + fix a assume 1: "a: A" 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]) (routine lems: assms 1) - qed (routine lems: assms 1) } + qed (routine lems: assms 1) - show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)" + next show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`(refl a) \<equiv> refl a" proof compute 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]) (routine lems: assms) - show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)" + show "ind\<^sub>= refl (refl a) \<equiv> refl a" proof compute show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" .. qed (routine lems: assms) @@ -196,23 +196,23 @@ text "The raw object lambda term is cumbersome to use, so we define a simpler co axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 120) where pathcomp_def: "\<lbrakk> - A: U(i); + A: U i; x: A; y: A; z: A; p: x =\<^sub>A y; q: y =\<^sub>A z \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q" lemma pathcomp_type: - assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "p \<bullet> q: x =\<^sub>A z" proof (subst pathcomp_def) - show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ + show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ qed (routine lems: assms rpathcomp_type) lemma pathcomp_comp: - assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)" + assumes "A : U i" and "a : A" shows "(refl a) \<bullet> (refl a) \<equiv> refl a" by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) @@ -223,44 +223,45 @@ lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp section \<open>Higher groupoid structure of types\<close> lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" shows - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> refl(y)" and - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] refl(x) \<bullet> p" + "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> (refl y)" and + "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \<bullet> p" proof - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> refl(y)" + show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> (refl y)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] refl x \<bullet> p" + show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] (refl x) \<bullet> p" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ qed lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" shows - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] refl(y)" and - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] refl(x)" + "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" and + "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)" proof - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] refl(y)" + show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] refl(x)" + show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ qed lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" shows "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse>\<inverse> =[x =\<^sub>A y] p" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms) +text "Next we construct a proof term of associativity of path composition." schematic_goal assumes - "A: U(i)" + "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" shows @@ -268,8 +269,8 @@ schematic_goal apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) apply (rule assms)+ -apply (subst pathcomp_comp) - +\<comment> \<open>Continue by substituting \<open>refl x \<bullet> q = q\<close> etc.\<close> +sorry end |