src/HOLCF/Deflation.thy
 changeset 40002 c5b5f7a3a3b1 parent 39985 310f98585107 child 40321 d065b195ec89
1.1 --- a/src/HOLCF/Deflation.thy	Mon Oct 11 16:24:44 2010 -0700
1.2 +++ b/src/HOLCF/Deflation.thy	Mon Oct 11 21:35:31 2010 -0700
1.3 @@ -19,7 +19,7 @@
1.4  begin
1.6  lemma below_ID: "d \<sqsubseteq> ID"
1.7 -by (rule below_cfun_ext, simp add: below)
1.8 +by (rule cfun_belowI, simp add: below)
1.10  text {* The set of fixed points is the same as the range. *}
1.12 @@ -36,7 +36,7 @@
1.14  lemma belowI:
1.15    assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
1.16 -proof (rule below_cfun_ext)
1.17 +proof (rule cfun_belowI)
1.18    fix x
1.19    from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
1.20    also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
1.21 @@ -326,7 +326,7 @@
1.22  lemma ep_pair_unique_e_lemma:
1.23    assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
1.24    shows "e1 \<sqsubseteq> e2"
1.25 -proof (rule below_cfun_ext)
1.26 +proof (rule cfun_belowI)
1.27    fix x
1.28    have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
1.29      by (rule ep_pair.e_p_below [OF 1])
1.30 @@ -341,7 +341,7 @@
1.31  lemma ep_pair_unique_p_lemma:
1.32    assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
1.33    shows "p1 \<sqsubseteq> p2"
1.34 -proof (rule below_cfun_ext)
1.35 +proof (rule cfun_belowI)
1.36    fix x
1.37    have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
1.38      by (rule ep_pair.e_p_below [OF 1])
1.39 @@ -414,9 +414,9 @@
1.40    interpret e1p1: ep_pair e1 p1 by fact
1.41    interpret e2p2: ep_pair e2 p2 by fact
1.42    fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
1.43 -    by (simp add: expand_cfun_eq)
1.44 +    by (simp add: cfun_eq_iff)
1.45    fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
1.46 -    apply (rule below_cfun_ext, simp)
1.47 +    apply (rule cfun_belowI, simp)
1.48      apply (rule below_trans [OF e2p2.e_p_below])
1.49      apply (rule monofun_cfun_arg)
1.50      apply (rule e1p1.e_p_below)
1.51 @@ -431,9 +431,9 @@
1.52    interpret d2: deflation d2 by fact
1.53    fix f
1.54    show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
1.55 -    by (simp add: expand_cfun_eq d1.idem d2.idem)
1.56 +    by (simp add: cfun_eq_iff d1.idem d2.idem)
1.57    show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
1.58 -    apply (rule below_cfun_ext, simp)
1.59 +    apply (rule cfun_belowI, simp)
1.60      apply (rule below_trans [OF d2.below])
1.61      apply (rule monofun_cfun_arg)
1.62      apply (rule d1.below)
1.63 @@ -455,7 +455,7 @@
1.64        by (simp add: a b)
1.65    qed
1.66    show "inj_on ?f (range ?h)"
1.67 -  proof (rule inj_onI, rule ext_cfun, clarsimp)
1.68 +  proof (rule inj_onI, rule cfun_eqI, clarsimp)
1.69      fix x f g
1.70      assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
1.71      hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"