diff options
author | Josh Chen | 2018-08-15 12:42:52 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-15 12:42:52 +0200 |
commit | 257561ff4036d0eb5b51e649f2590b61e08d6fc5 (patch) | |
tree | 0ad6273546ea73a3d2b6104de100f0dca2f7dea5 /EqualProps.thy | |
parent | f4f468878fc0459a806b02cdf8921af6fcac2759 (diff) |
Basic compute method
Diffstat (limited to '')
-rw-r--r-- | EqualProps.thy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 9b43345..2a13ed2 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -96,7 +96,7 @@ lemma reqcompose_comp: assumes "A: U(i)" and "a: A" shows "reqcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" unfolding reqcompose_def -proof (subst comp) +proof compute { 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 @@ -120,7 +120,7 @@ proof (subst comp) 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)" - proof (subst comp) + proof compute { 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 @@ -141,7 +141,7 @@ proof (subst comp) 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) + proof compute { fix p assume 1: "p: a =\<^sub>A a" show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A a \<rightarrow> a =\<^sub>A z" proof (rule Equal_elim[where ?x=a and ?y=a]) @@ -158,7 +158,7 @@ proof (subst comp) 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) + proof compute { fix u assume 1: "u: A" show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A u\<rightarrow> u =\<^sub>A z" proof @@ -171,7 +171,7 @@ proof (subst comp) qed fact } show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)" - proof (subst comp) + proof compute { fix a assume 1: "a: A" show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" proof @@ -180,7 +180,7 @@ proof (subst comp) qed (simple lems: assms 1) } show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)" - proof (subst comp) + 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]) (simple lems: assms) show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)" |