author huffman Wed Feb 17 08:19:46 2010 -0800 (2010-02-17) changeset 35168 07b3112e464b parent 35167 eba22d68a0a7 child 35169 31cbcb019003
fix warnings about duplicate simp rules
 src/HOLCF/Cfun.thy file | annotate | diff | revisions src/HOLCF/Deflation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOLCF/Cfun.thy	Wed Feb 17 08:05:16 2010 -0800
1.2 +++ b/src/HOLCF/Cfun.thy	Wed Feb 17 08:19:46 2010 -0800
1.3 @@ -521,7 +521,7 @@
1.4  text {* results about strictify *}
1.5
1.6  lemma cont_strictify1: "cont (\<lambda>f. if x = \<bottom> then \<bottom> else f\<cdot>x)"
1.8 +by simp
1.9
1.10  lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
1.11  apply (rule monofunI)
```
```     2.1 --- a/src/HOLCF/Deflation.thy	Wed Feb 17 08:05:16 2010 -0800
2.2 +++ b/src/HOLCF/Deflation.thy	Wed Feb 17 08:19:46 2010 -0800
2.3 @@ -316,16 +316,14 @@
2.4  subsection {* Uniqueness of ep-pairs *}
2.5
2.6  lemma ep_pair_unique_e_lemma:
2.7 -  assumes "ep_pair e1 p" and "ep_pair e2 p"
2.8 +  assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
2.9    shows "e1 \<sqsubseteq> e2"
2.10  proof (rule below_cfun_ext)
2.11 -  interpret e1: ep_pair e1 p by fact
2.12 -  interpret e2: ep_pair e2 p by fact
2.13    fix x
2.14    have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
2.15 -    by (rule e1.e_p_below)
2.16 +    by (rule ep_pair.e_p_below [OF 1])
2.17    thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
2.18 -    by (simp only: e2.e_inverse)
2.19 +    by (simp only: ep_pair.e_inverse [OF 2])
2.20  qed
2.21
2.22  lemma ep_pair_unique_e:
2.23 @@ -333,18 +331,16 @@
2.24  by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
2.25
2.26  lemma ep_pair_unique_p_lemma:
2.27 -  assumes "ep_pair e p1" and "ep_pair e p2"
2.28 +  assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
2.29    shows "p1 \<sqsubseteq> p2"
2.30  proof (rule below_cfun_ext)
2.31 -  interpret p1: ep_pair e p1 by fact
2.32 -  interpret p2: ep_pair e p2 by fact
2.33    fix x
2.34    have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
2.35 -    by (rule p1.e_p_below)
2.36 +    by (rule ep_pair.e_p_below [OF 1])
2.37    hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
2.38      by (rule monofun_cfun_arg)
2.39    thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
2.40 -    by (simp only: p2.e_inverse)
2.41 +    by (simp only: ep_pair.e_inverse [OF 2])
2.42  qed
2.43
2.44  lemma ep_pair_unique_p:
```