From 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 08:59:16 +0200 Subject: Go back to higher-order application notation --- EqualProps.thy | 85 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 43 insertions(+), 42 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index c114d37..708eb33 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -14,7 +14,7 @@ begin section \Symmetry / Path inverse\ -definition inv :: "Term \ Term" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. refl(x)) p" +definition inv :: "Term \ Term" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. (refl x)) p" text " In the proof below we begin by using path induction on \p\ with the application of \rule Equal_elim\, 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\: y =\<^sub>A x" + assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\: y =\<^sub>A x" unfolding inv_def by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ @@ -33,7 +33,7 @@ text " " lemma inv_comp: - assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" + assumes "A : U i " and "a : A" shows "(refl a)\ \ refl a" unfolding inv_def proof compute show "\x. x: A \ refl x: x =\<^sub>A x" .. @@ -46,14 +46,14 @@ text " Raw composition function, of type \\x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)\ polymorphic over the type \A\. " -definition rpathcomp :: Term where "rpathcomp \ \<^bold>\_ _ p. ind\<^sub>= (\_. \<^bold>\_ q. ind\<^sub>= (\x. refl(x)) q) p" +definition rpathcomp :: Term where "rpathcomp \ \<^bold>\_ _ p. ind\<^sub>= (\_. \<^bold>\_ q. ind\<^sub>= (\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: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ 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) \ refl(a)" + assumes "A: U i" and "a: A" + shows "rpathcomp`a`a`(refl a)`a`(refl a) \ refl a" unfolding rpathcomp_def proof compute - { fix x assume 1: "x: A" + fix x assume 1: "x: A" show "\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ 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>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \ refl(a)" + next show "(\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \ refl a" proof compute - { fix y assume 1: "y: A" + fix y assume 1: "y: A" show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: a =\<^sub>A y \ (\z:A. y =\<^sub>A z \ 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>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" + next show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \ 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>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. a =\<^sub>A z \ 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>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" + next show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \ refl a" proof compute - { fix u assume 1: "u: A" + fix u assume 1: "u: A" show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" proof fix z assume 2: "z: A" @@ -165,22 +165,22 @@ proof compute show "\q. q: u =\<^sub>A z \ 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>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" + next show "(\<^bold>\z q. ind\<^sub>= refl q)`a`(refl a) \ refl a" proof compute - { fix a assume 1: "a: A" + fix a assume 1: "a: A" show "\<^bold>\q. ind\<^sub>= refl q: a =\<^sub>A a \ a =\<^sub>A a" proof show "\q. q: a =\<^sub>A a \ 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>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" + next show "(\<^bold>\q. ind\<^sub>= refl q)`(refl a) \ refl a" proof compute show "\p. p: a =\<^sub>A a \ 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)) \ refl(a)" + show "ind\<^sub>= refl (refl a) \ refl a" proof compute show "\x. x: A \ 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] \ Term" (infixl "\" 120) where pathcomp_def: "\ - A: U(i); + A: U i; x: A; y: A; z: A; p: x =\<^sub>A y; q: y =\<^sub>A z \ \ p \ q \ 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 \ 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) \ refl(a) \ refl(a)" + assumes "A : U i" and "a : A" shows "(refl a) \ (refl a) \ refl a" by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) @@ -223,44 +223,45 @@ lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp section \Higher groupoid structure of types\ 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>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] p \ refl(y)" and - "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] refl(x) \ p" + "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] p \ (refl y)" and + "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \ p" proof - - show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] p \ refl(y)" + show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] p \ (refl y)" by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] refl x \ p" + show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] (refl x) \ 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>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] refl(y)" and - "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] refl(x)" + "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] (refl y)" and + "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] (refl x)" proof - - show "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] refl(y)" + show "ind\<^sub>= (\u. refl (refl u)) p: p\ \ 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>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] refl(x)" + show "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[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>= (\u. refl (refl u)) p: p\\ =[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) - +\ \Continue by substituting \refl x \ q = q\ etc.\ +sorry end -- cgit v1.2.3