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.5  
     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.9  
    1.10  text {* The set of fixed points is the same as the range. *}
    1.11  
    1.12 @@ -36,7 +36,7 @@
    1.13  
    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))))"