src/HOLCF/Deflation.thy
changeset 35168 07b3112e464b
parent 33503 3496616b2171
child 35794 8cd7134275cc
     1.1 --- a/src/HOLCF/Deflation.thy	Wed Feb 17 08:05:16 2010 -0800
     1.2 +++ b/src/HOLCF/Deflation.thy	Wed Feb 17 08:19:46 2010 -0800
     1.3 @@ -316,16 +316,14 @@
     1.4  subsection {* Uniqueness of ep-pairs *}
     1.5  
     1.6  lemma ep_pair_unique_e_lemma:
     1.7 -  assumes "ep_pair e1 p" and "ep_pair e2 p"
     1.8 +  assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
     1.9    shows "e1 \<sqsubseteq> e2"
    1.10  proof (rule below_cfun_ext)
    1.11 -  interpret e1: ep_pair e1 p by fact
    1.12 -  interpret e2: ep_pair e2 p by fact
    1.13    fix x
    1.14    have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
    1.15 -    by (rule e1.e_p_below)
    1.16 +    by (rule ep_pair.e_p_below [OF 1])
    1.17    thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
    1.18 -    by (simp only: e2.e_inverse)
    1.19 +    by (simp only: ep_pair.e_inverse [OF 2])
    1.20  qed
    1.21  
    1.22  lemma ep_pair_unique_e:
    1.23 @@ -333,18 +331,16 @@
    1.24  by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
    1.25  
    1.26  lemma ep_pair_unique_p_lemma:
    1.27 -  assumes "ep_pair e p1" and "ep_pair e p2"
    1.28 +  assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
    1.29    shows "p1 \<sqsubseteq> p2"
    1.30  proof (rule below_cfun_ext)
    1.31 -  interpret p1: ep_pair e p1 by fact
    1.32 -  interpret p2: ep_pair e p2 by fact
    1.33    fix x
    1.34    have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
    1.35 -    by (rule p1.e_p_below)
    1.36 +    by (rule ep_pair.e_p_below [OF 1])
    1.37    hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
    1.38      by (rule monofun_cfun_arg)
    1.39    thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
    1.40 -    by (simp only: p2.e_inverse)
    1.41 +    by (simp only: ep_pair.e_inverse [OF 2])
    1.42  qed
    1.43  
    1.44  lemma ep_pair_unique_p: