From f4f468878fc0459a806b02cdf8921af6fcac2759 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 15 Aug 2018 11:47:30 +0200 Subject: Tweak proof methods, some type rules; add HoTT Book examples --- EqualProps.thy | 58 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'EqualProps.thy') 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\: 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) \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ text " @@ -39,7 +39,7 @@ lemma inv_comp: unfolding inv_def proof show "\x. x: A \ refl x: x =\<^sub>A x" .. -qed (simple lem: assms) +qed (simple lems: assms) section \Transitivity / Path composition\ @@ -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 \`\ 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 "\q. q: u =\<^sub>A z \ 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>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \ refl(a)" @@ -134,11 +134,11 @@ proof (subst comp) show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" proof 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]) (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>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" proof (subst comp) @@ -152,10 +152,10 @@ proof (subst comp) show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A u \ u =\<^sub>A z" proof show "\q. q: u =\<^sub>A u \ 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>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" proof (subst comp) @@ -166,8 +166,8 @@ proof (subst comp) show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A u \ u =\<^sub>A z" proof show "\q. q: u =\<^sub>A u \ 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>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" @@ -176,21 +176,21 @@ proof (subst comp) 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]) (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>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" proof (subst comp) 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]) (simple lem: assms) + by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms) show "ind\<^sub>= refl (refl(a)) \ refl(a)" proof show "\x. x: A \ 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 \ 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) \ refl(a) \ 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 -- cgit v1.2.3