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:
```