From 8833cdf99d3128466d85eb88aeb8e340e07e937c Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 18 Aug 2018 23:27:25 +0200 Subject: Reorganize methods --- EqualProps.thy | 66 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 33 insertions(+), 33 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index 8b83c5b..a1d4c45 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -24,7 +24,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 lems: assms) +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.\ text " @@ -35,9 +35,9 @@ text " lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" unfolding inv_def -proof +proof compute show "\x. x: A \ refl x: x =\<^sub>A x" .. -qed (simple lems: assms) +qed (routine lems: assms) section \Transitivity / Path composition\ @@ -72,18 +72,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 lems: assms asm) - qed (simple lems: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) + qed (routine lems: assms) qed (rule assms) - qed (simple lems: assms 1 2 3) - qed (simple lems: assms 1 2) + qed (routine lems: assms 1 2 3) + qed (routine 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 "rpathcomp`x`y`p`z`q: x =\<^sub>A z" - by (simple lems: assms rpathcomp_type) + by (routine lems: assms rpathcomp_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. @@ -109,11 +109,11 @@ proof compute 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 lems: assms asm) - qed (simple lems: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) + qed (routine lems: assms) qed (rule assms) - qed (simple lems: assms 1 2 3) - qed (simple lems: assms 1 2) + qed (routine lems: assms 1 2 3) + qed (routine 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)" @@ -131,11 +131,11 @@ proof compute 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 lems: assms 3 4) - qed (simple lems: assms 3 4) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4) + qed (routine lems: assms 3 4) qed fact - qed (simple lems: assms 1 2) - qed (simple lems: assms 1) } + qed (routine lems: assms 1 2) + 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)" proof compute @@ -149,10 +149,10 @@ proof compute 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 lems: assms 2 3) - qed (simple lems: assms 2 3) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) + qed (routine lems: assms 2 3) qed fact - qed (simple 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)" proof compute @@ -163,8 +163,8 @@ proof compute 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 lems: assms 1 2) - qed (simple lems: assms 1 2) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) + qed (routine lems: assms 1 2) qed fact } show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" @@ -173,21 +173,21 @@ proof compute 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 lems: assms 1) - qed (simple lems: assms 1) } + by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) + qed (routine lems: assms 1) } 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]) (simple lems: assms) + by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms) show "ind\<^sub>= refl (refl(a)) \ refl(a)" - proof + proof compute show "\x. x: A \ refl(x): x =\<^sub>A x" .. - qed (simple lems: assms) - qed (simple lems: assms) + qed (routine lems: assms) + qed (routine lems: assms) qed fact - qed (simple lems: assms) - qed (simple lems: assms) + qed (routine lems: assms) + qed (routine lems: assms) qed fact qed fact @@ -207,15 +207,15 @@ lemma pathcomp_type: 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+ -qed (simple lems: assms rpathcomp_type) +qed (routine lems: assms rpathcomp_type) lemma pathcomp_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" -by (subst pathcomp_def) (simple lems: assms rpathcomp_comp) +by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) -lemmas EqualProps_rules [intro] = inv_type pathcomp_type -lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp +lemmas EqualProps_type [intro] = inv_type pathcomp_type +lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp end -- cgit v1.2.3