fix warnings about duplicate simp rules
authorhuffman
Wed Feb 17 08:19:46 2010 -0800 (2010-02-17)
changeset 3516807b3112e464b
parent 35167 eba22d68a0a7
child 35169 31cbcb019003
fix warnings about duplicate simp rules
src/HOLCF/Cfun.thy
src/HOLCF/Deflation.thy
     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.7 -by (simp add: cont_if)
     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: