diff options
| author | Josh Chen | 2018-07-06 10:48:41 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-07-06 10:48:41 +0200 |
| commit | 76deb7ae15fa00b5498ab43db020a0364499251e (patch) | |
| tree | 706d25614154cf3767e1ad9e905a6074b620809a /EqualProps.thy | |
| parent | b65450369f992171f166a53e9cab408819cd987f (diff) | |
Added attributes to type elimination rules, not sure if these will actually be needed or useful later. Added [comp] attribute to be used by simplification met methods.
Diffstat (limited to 'EqualProps.thy')
| -rw-r--r-- | EqualProps.thy | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 8960a90..2807587 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -66,27 +66,6 @@ lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" -proof (unfold rcompose_def) - show "(\<^bold>\<lambda>p:a =[A] a. - lambda (a =[A] a) - (op ` - ((\<^bold>\<lambda>x:A. - \<^bold>\<lambda>y:A. - lambda (x =[A] y) - (indEqual[A] - (\<lambda>x y _. \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z) - (\<lambda>x. \<^bold>\<lambda>z:A. - lambda (x =[A] z) - (indEqual[A] (\<lambda>x z _. x =[A] z) refl x z)) - x y)) ` - a ` - a ` - p ` - a))) ` - refl(a) ` - refl(a) \<equiv> - refl(a)" - sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close> |