new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
authorhuffman
Mon Oct 11 21:35:31 2010 -0700 (2010-10-11)
changeset 40002c5b5f7a3a3b1
parent 40001 666c3751227c
child 40003 427106657e04
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
src/HOLCF/Bifinite.thy
src/HOLCF/Cfun.thy
src/HOLCF/Completion.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cprod.thy
src/HOLCF/Deflation.thy
src/HOLCF/FOCUS/Buffer.thy
src/HOLCF/Fun_Cpo.thy
src/HOLCF/HOLCF.thy
src/HOLCF/Library/Defl_Bifinite.thy
src/HOLCF/Library/Stream.thy
src/HOLCF/Library/Strict_Fun.thy
src/HOLCF/Lift.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Representable.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Universal.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
src/HOLCF/ex/Fix2.thy
src/HOLCF/ex/Focus_ex.thy
src/HOLCF/ex/Hoare.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Mon Oct 11 16:24:44 2010 -0700
     1.2 +++ b/src/HOLCF/Bifinite.thy	Mon Oct 11 21:35:31 2010 -0700
     1.3 @@ -56,7 +56,7 @@
     1.4        unfolding approx_def by (simp add: Y)
     1.5      show "(\<Squnion>i. approx i) = ID"
     1.6        unfolding approx_def
     1.7 -      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq)
     1.8 +      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
     1.9      show "\<And>i. finite_deflation (approx i)"
    1.10        unfolding approx_def
    1.11        apply (rule bifinite.finite_deflation_p_d_e)
    1.12 @@ -228,7 +228,7 @@
    1.13  next
    1.14    show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
    1.15      unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
    1.16 -    by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map)
    1.17 +    by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map)
    1.18  qed
    1.19  
    1.20  end
    1.21 @@ -287,7 +287,7 @@
    1.22  next
    1.23    show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
    1.24      unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
    1.25 -    by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map)
    1.26 +    by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
    1.27  qed
    1.28  
    1.29  end
    1.30 @@ -348,7 +348,7 @@
    1.31  next
    1.32    show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    1.33      unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
    1.34 -    by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map)
    1.35 +    by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
    1.36  qed
    1.37  
    1.38  end
    1.39 @@ -405,7 +405,7 @@
    1.40  next
    1.41    show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
    1.42      unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
    1.43 -    by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map)
    1.44 +    by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map)
    1.45  qed
    1.46  
    1.47  end
    1.48 @@ -425,7 +425,7 @@
    1.49    by (rule chainI, simp add: FLIFT_mono)
    1.50  
    1.51  lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
    1.52 -apply (rule ext_cfun)
    1.53 +apply (rule cfun_eqI)
    1.54  apply (simp add: contlub_cfun_fun)
    1.55  apply (simp add: lift_approx_def)
    1.56  apply (case_tac x, simp)
    1.57 @@ -548,7 +548,7 @@
    1.58  next
    1.59    show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
    1.60      unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
    1.61 -    by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map)
    1.62 +    by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
    1.63  qed
    1.64  
    1.65  end
     2.1 --- a/src/HOLCF/Cfun.thy	Mon Oct 11 16:24:44 2010 -0700
     2.2 +++ b/src/HOLCF/Cfun.thy	Mon Oct 11 21:35:31 2010 -0700
     2.3 @@ -176,19 +176,19 @@
     2.4  
     2.5  text {* Extensionality for continuous functions *}
     2.6  
     2.7 -lemma expand_cfun_eq: "(f = g) = (\<forall>x. f\<cdot>x = g\<cdot>x)"
     2.8 +lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
     2.9  by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff)
    2.10  
    2.11 -lemma ext_cfun: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
    2.12 -by (simp add: expand_cfun_eq)
    2.13 +lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
    2.14 +by (simp add: cfun_eq_iff)
    2.15  
    2.16  text {* Extensionality wrt. ordering for continuous functions *}
    2.17  
    2.18 -lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
    2.19 -by (simp add: below_CFun_def expand_fun_below)
    2.20 +lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
    2.21 +by (simp add: below_CFun_def fun_below_iff)
    2.22  
    2.23 -lemma below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
    2.24 -by (simp add: expand_cfun_below)
    2.25 +lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
    2.26 +by (simp add: cfun_below_iff)
    2.27  
    2.28  text {* Congruence for continuous function application *}
    2.29  
    2.30 @@ -233,7 +233,7 @@
    2.31  text {* monotonicity of application *}
    2.32  
    2.33  lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
    2.34 -by (simp add: expand_cfun_below)
    2.35 +by (simp add: cfun_below_iff)
    2.36  
    2.37  lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
    2.38  by (rule monofun_Rep_CFun2 [THEN monofunE])
    2.39 @@ -258,7 +258,7 @@
    2.40  
    2.41  lemma ch2ch_LAM [simp]:
    2.42    "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
    2.43 -by (simp add: chain_def expand_cfun_below)
    2.44 +by (simp add: chain_def cfun_below_iff)
    2.45  
    2.46  text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
    2.47  
    2.48 @@ -344,7 +344,7 @@
    2.49  lemma cont2mono_LAM:
    2.50    "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
    2.51      \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
    2.52 -  unfolding monofun_def expand_cfun_below by simp
    2.53 +  unfolding monofun_def cfun_below_iff by simp
    2.54  
    2.55  text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
    2.56  
    2.57 @@ -509,7 +509,7 @@
    2.58  by (simp add: cfcomp1)
    2.59  
    2.60  lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
    2.61 -by (simp add: expand_cfun_eq)
    2.62 +by (simp add: cfun_eq_iff)
    2.63  
    2.64  text {*
    2.65    Show that interpretation of (pcpo,@{text "_->_"}) is a category.
    2.66 @@ -520,13 +520,13 @@
    2.67  *}
    2.68  
    2.69  lemma ID2 [simp]: "f oo ID = f"
    2.70 -by (rule ext_cfun, simp)
    2.71 +by (rule cfun_eqI, simp)
    2.72  
    2.73  lemma ID3 [simp]: "ID oo f = f"
    2.74 -by (rule ext_cfun, simp)
    2.75 +by (rule cfun_eqI, simp)
    2.76  
    2.77  lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
    2.78 -by (rule ext_cfun, simp)
    2.79 +by (rule cfun_eqI, simp)
    2.80  
    2.81  subsection {* Map operator for continuous function space *}
    2.82  
    2.83 @@ -539,12 +539,12 @@
    2.84  unfolding cfun_map_def by simp
    2.85  
    2.86  lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
    2.87 -unfolding expand_cfun_eq by simp
    2.88 +unfolding cfun_eq_iff by simp
    2.89  
    2.90  lemma cfun_map_map:
    2.91    "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
    2.92      cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    2.93 -by (rule ext_cfun) simp
    2.94 +by (rule cfun_eqI) simp
    2.95  
    2.96  subsection {* Strictified functions *}
    2.97  
     3.1 --- a/src/HOLCF/Completion.thy	Mon Oct 11 16:24:44 2010 -0700
     3.2 +++ b/src/HOLCF/Completion.thy	Mon Oct 11 21:35:31 2010 -0700
     3.3 @@ -397,7 +397,7 @@
     3.4    assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
     3.5    assumes below: "\<And>a. f a \<sqsubseteq> g a"
     3.6    shows "basis_fun f \<sqsubseteq> basis_fun g"
     3.7 - apply (rule below_cfun_ext)
     3.8 + apply (rule cfun_belowI)
     3.9   apply (simp only: basis_fun_beta f_mono g_mono)
    3.10   apply (rule is_lub_thelub_ex)
    3.11    apply (rule basis_fun_lemma, erule f_mono)
     4.1 --- a/src/HOLCF/ConvexPD.thy	Mon Oct 11 16:24:44 2010 -0700
     4.2 +++ b/src/HOLCF/ConvexPD.thy	Mon Oct 11 21:35:31 2010 -0700
     4.3 @@ -331,7 +331,7 @@
     4.4  
     4.5  lemma monofun_LAM:
     4.6    "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
     4.7 -by (simp add: expand_cfun_below)
     4.8 +by (simp add: cfun_below_iff)
     4.9  
    4.10  lemma convex_bind_basis_mono:
    4.11    "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
    4.12 @@ -382,7 +382,7 @@
    4.13  by (induct xs rule: convex_pd_induct, simp_all)
    4.14  
    4.15  lemma convex_map_ID: "convex_map\<cdot>ID = ID"
    4.16 -by (simp add: expand_cfun_eq ID_def convex_map_ident)
    4.17 +by (simp add: cfun_eq_iff ID_def convex_map_ident)
    4.18  
    4.19  lemma convex_map_map:
    4.20    "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
    4.21 @@ -494,7 +494,7 @@
    4.22  next
    4.23    show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
    4.24      unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
    4.25 -    by (simp add: cast_DEFL oo_def expand_cfun_eq convex_map_map)
    4.26 +    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
    4.27  qed
    4.28  
    4.29  end
     5.1 --- a/src/HOLCF/Cprod.thy	Mon Oct 11 16:24:44 2010 -0700
     5.2 +++ b/src/HOLCF/Cprod.thy	Mon Oct 11 21:35:31 2010 -0700
     5.3 @@ -51,7 +51,7 @@
     5.4  unfolding cprod_map_def by simp
     5.5  
     5.6  lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
     5.7 -unfolding expand_cfun_eq by auto
     5.8 +unfolding cfun_eq_iff by auto
     5.9  
    5.10  lemma cprod_map_map:
    5.11    "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
     6.1 --- a/src/HOLCF/Deflation.thy	Mon Oct 11 16:24:44 2010 -0700
     6.2 +++ b/src/HOLCF/Deflation.thy	Mon Oct 11 21:35:31 2010 -0700
     6.3 @@ -19,7 +19,7 @@
     6.4  begin
     6.5  
     6.6  lemma below_ID: "d \<sqsubseteq> ID"
     6.7 -by (rule below_cfun_ext, simp add: below)
     6.8 +by (rule cfun_belowI, simp add: below)
     6.9  
    6.10  text {* The set of fixed points is the same as the range. *}
    6.11  
    6.12 @@ -36,7 +36,7 @@
    6.13  
    6.14  lemma belowI:
    6.15    assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
    6.16 -proof (rule below_cfun_ext)
    6.17 +proof (rule cfun_belowI)
    6.18    fix x
    6.19    from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
    6.20    also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
    6.21 @@ -326,7 +326,7 @@
    6.22  lemma ep_pair_unique_e_lemma:
    6.23    assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
    6.24    shows "e1 \<sqsubseteq> e2"
    6.25 -proof (rule below_cfun_ext)
    6.26 +proof (rule cfun_belowI)
    6.27    fix x
    6.28    have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
    6.29      by (rule ep_pair.e_p_below [OF 1])
    6.30 @@ -341,7 +341,7 @@
    6.31  lemma ep_pair_unique_p_lemma:
    6.32    assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
    6.33    shows "p1 \<sqsubseteq> p2"
    6.34 -proof (rule below_cfun_ext)
    6.35 +proof (rule cfun_belowI)
    6.36    fix x
    6.37    have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
    6.38      by (rule ep_pair.e_p_below [OF 1])
    6.39 @@ -414,9 +414,9 @@
    6.40    interpret e1p1: ep_pair e1 p1 by fact
    6.41    interpret e2p2: ep_pair e2 p2 by fact
    6.42    fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
    6.43 -    by (simp add: expand_cfun_eq)
    6.44 +    by (simp add: cfun_eq_iff)
    6.45    fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
    6.46 -    apply (rule below_cfun_ext, simp)
    6.47 +    apply (rule cfun_belowI, simp)
    6.48      apply (rule below_trans [OF e2p2.e_p_below])
    6.49      apply (rule monofun_cfun_arg)
    6.50      apply (rule e1p1.e_p_below)
    6.51 @@ -431,9 +431,9 @@
    6.52    interpret d2: deflation d2 by fact
    6.53    fix f
    6.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"
    6.55 -    by (simp add: expand_cfun_eq d1.idem d2.idem)
    6.56 +    by (simp add: cfun_eq_iff d1.idem d2.idem)
    6.57    show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
    6.58 -    apply (rule below_cfun_ext, simp)
    6.59 +    apply (rule cfun_belowI, simp)
    6.60      apply (rule below_trans [OF d2.below])
    6.61      apply (rule monofun_cfun_arg)
    6.62      apply (rule d1.below)
    6.63 @@ -455,7 +455,7 @@
    6.64        by (simp add: a b)
    6.65    qed
    6.66    show "inj_on ?f (range ?h)"
    6.67 -  proof (rule inj_onI, rule ext_cfun, clarsimp)
    6.68 +  proof (rule inj_onI, rule cfun_eqI, clarsimp)
    6.69      fix x f g
    6.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))))"
    6.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))))"
     7.1 --- a/src/HOLCF/FOCUS/Buffer.thy	Mon Oct 11 16:24:44 2010 -0700
     7.2 +++ b/src/HOLCF/FOCUS/Buffer.thy	Mon Oct 11 21:35:31 2010 -0700
     7.3 @@ -200,7 +200,7 @@
     7.4  apply (  rule_tac [2] P="(%x. x:B)" in ssubst)
     7.5  prefer 3
     7.6  apply (   assumption)
     7.7 -apply (  rule_tac [2] ext_cfun)
     7.8 +apply (  rule_tac [2] cfun_eqI)
     7.9  apply (  drule_tac [2] spec)
    7.10  apply (  drule_tac [2] f="rt" in cfun_arg_cong)
    7.11  prefer 2
     8.1 --- a/src/HOLCF/Fun_Cpo.thy	Mon Oct 11 16:24:44 2010 -0700
     8.2 +++ b/src/HOLCF/Fun_Cpo.thy	Mon Oct 11 21:35:31 2010 -0700
     8.3 @@ -35,12 +35,10 @@
     8.4      unfolding below_fun_def by (fast elim: below_trans)
     8.5  qed
     8.6  
     8.7 -text {* make the symbol @{text "<<"} accessible for type fun *}
     8.8 -
     8.9 -lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
    8.10 +lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
    8.11  by (simp add: below_fun_def)
    8.12  
    8.13 -lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    8.14 +lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    8.15  by (simp add: below_fun_def)
    8.16  
    8.17  subsection {* Full function space is chain complete *}
    8.18 @@ -71,9 +69,9 @@
    8.19    shows "range Y <<| f"
    8.20  apply (rule is_lubI)
    8.21  apply (rule ub_rangeI)
    8.22 -apply (rule below_fun_ext)
    8.23 +apply (rule fun_belowI)
    8.24  apply (rule is_ub_lub [OF f])
    8.25 -apply (rule below_fun_ext)
    8.26 +apply (rule fun_belowI)
    8.27  apply (rule is_lub_lub [OF f])
    8.28  apply (erule ub2ub_fun)
    8.29  done
    8.30 @@ -104,7 +102,7 @@
    8.31  proof
    8.32    fix f g :: "'a \<Rightarrow> 'b"
    8.33    show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
    8.34 -    unfolding expand_fun_below fun_eq_iff
    8.35 +    unfolding fun_below_iff fun_eq_iff
    8.36      by simp
    8.37  qed
    8.38  
    8.39 @@ -227,7 +225,7 @@
    8.40  lemma mono2mono_lambda:
    8.41    assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
    8.42  apply (rule monofunI)
    8.43 -apply (rule below_fun_ext)
    8.44 +apply (rule fun_belowI)
    8.45  apply (erule monofunE [OF f])
    8.46  done
    8.47  
    8.48 @@ -235,7 +233,7 @@
    8.49    assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
    8.50  apply (rule contI2)
    8.51  apply (simp add: mono2mono_lambda cont2mono f)
    8.52 -apply (rule below_fun_ext)
    8.53 +apply (rule fun_belowI)
    8.54  apply (simp add: thelub_fun cont2contlubE [OF f])
    8.55  done
    8.56  
     9.1 --- a/src/HOLCF/HOLCF.thy	Mon Oct 11 16:24:44 2010 -0700
     9.2 +++ b/src/HOLCF/HOLCF.thy	Mon Oct 11 21:35:31 2010 -0700
     9.3 @@ -15,7 +15,16 @@
     9.4  
     9.5  ML {* path_add "~~/src/HOLCF/Library" *}
     9.6  
     9.7 -text {* Legacy theorem names *}
     9.8 +text {* Legacy theorem names deprecated after Isabelle2009-2: *}
     9.9 +
    9.10 +lemmas expand_fun_below = fun_below_iff
    9.11 +lemmas below_fun_ext = fun_belowI
    9.12 +lemmas expand_cfun_eq = cfun_eq_iff
    9.13 +lemmas ext_cfun = cfun_eqI
    9.14 +lemmas expand_cfun_below = cfun_below_iff
    9.15 +lemmas below_cfun_ext = cfun_belowI
    9.16 +
    9.17 +text {* Older legacy theorem names: *}
    9.18  
    9.19  lemmas sq_ord_less_eq_trans = below_eq_trans
    9.20  lemmas sq_ord_eq_less_trans = eq_below_trans
    10.1 --- a/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 16:24:44 2010 -0700
    10.2 +++ b/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 21:35:31 2010 -0700
    10.3 @@ -240,7 +240,7 @@
    10.4    hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
    10.5      by (simp only: iterate_Suc2)
    10.6    hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
    10.7 -    by (simp only: expand_cfun_eq)
    10.8 +    by (simp only: cfun_eq_iff)
    10.9    hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
   10.10      unfolding eventually_constant_MOST_MOST .
   10.11    thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
   10.12 @@ -587,7 +587,7 @@
   10.13      apply (simp add: defl_approx_principal fd_take_below)
   10.14      done
   10.15    show lub: "(\<Squnion>i. defl_approx i) = ID"
   10.16 -    apply (rule ext_cfun, rule below_antisym)
   10.17 +    apply (rule cfun_eqI, rule below_antisym)
   10.18      apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
   10.19      apply (induct_tac x rule: defl.principal_induct, simp)
   10.20      apply (simp add: contlub_cfun_fun chain)
    11.1 --- a/src/HOLCF/Library/Stream.thy	Mon Oct 11 16:24:44 2010 -0700
    11.2 +++ b/src/HOLCF/Library/Stream.thy	Mon Oct 11 21:35:31 2010 -0700
    11.3 @@ -508,7 +508,7 @@
    11.4  by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
    11.5  
    11.6  lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
    11.7 -apply (rule ext_cfun)
    11.8 +apply (rule cfun_eqI)
    11.9  apply (subst sfilter_unfold, auto)
   11.10  apply (case_tac "x=UU", auto)
   11.11  by (drule stream_exhaust_eq [THEN iffD1], auto)
    12.1 --- a/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 16:24:44 2010 -0700
    12.2 +++ b/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 21:35:31 2010 -0700
    12.3 @@ -37,13 +37,13 @@
    12.4    unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
    12.5  
    12.6  lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
    12.7 -  by (simp add: expand_cfun_eq strictify_conv_if)
    12.8 +  by (simp add: cfun_eq_iff strictify_conv_if)
    12.9  
   12.10  lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
   12.11    unfolding sfun_abs_def sfun_rep_def
   12.12    apply (simp add: cont_Abs_sfun cont_Rep_sfun)
   12.13    apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
   12.14 -  apply (simp add: expand_cfun_eq strictify_conv_if)
   12.15 +  apply (simp add: cfun_eq_iff strictify_conv_if)
   12.16    apply (simp add: Rep_sfun [simplified])
   12.17    done
   12.18  
   12.19 @@ -56,7 +56,7 @@
   12.20  lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
   12.21  apply default
   12.22  apply (rule sfun_abs_sfun_rep)
   12.23 -apply (simp add: expand_cfun_below strictify_conv_if)
   12.24 +apply (simp add: cfun_below_iff strictify_conv_if)
   12.25  done
   12.26  
   12.27  interpretation sfun: ep_pair sfun_rep sfun_abs
   12.28 @@ -71,14 +71,14 @@
   12.29  
   12.30  lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
   12.31    unfolding sfun_map_def
   12.32 -  by (simp add: cfun_map_ID expand_cfun_eq)
   12.33 +  by (simp add: cfun_map_ID cfun_eq_iff)
   12.34  
   12.35  lemma sfun_map_map:
   12.36    assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
   12.37    "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
   12.38      sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
   12.39  unfolding sfun_map_def
   12.40 -by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map)
   12.41 +by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
   12.42  
   12.43  lemma ep_pair_sfun_map:
   12.44    assumes 1: "ep_pair e1 p1"
   12.45 @@ -193,7 +193,7 @@
   12.46  next
   12.47    show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
   12.48      unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
   12.49 -    by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
   12.50 +    by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
   12.51  qed
   12.52  
   12.53  end
    13.1 --- a/src/HOLCF/Lift.thy	Mon Oct 11 16:24:44 2010 -0700
    13.2 +++ b/src/HOLCF/Lift.thy	Mon Oct 11 21:35:31 2010 -0700
    13.3 @@ -134,7 +134,7 @@
    13.4    "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
    13.5  apply (rule monofunE [where f=flift1])
    13.6  apply (rule cont2mono [OF cont_flift1])
    13.7 -apply (simp add: below_fun_ext)
    13.8 +apply (simp add: fun_below_iff)
    13.9  done
   13.10  
   13.11  lemma cont2cont_flift1 [simp, cont2cont]:
    14.1 --- a/src/HOLCF/LowerPD.thy	Mon Oct 11 16:24:44 2010 -0700
    14.2 +++ b/src/HOLCF/LowerPD.thy	Mon Oct 11 21:35:31 2010 -0700
    14.3 @@ -323,7 +323,7 @@
    14.4  
    14.5  lemma lower_bind_basis_mono:
    14.6    "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
    14.7 -unfolding expand_cfun_below
    14.8 +unfolding cfun_below_iff
    14.9  apply (erule lower_le_induct, safe)
   14.10  apply (simp add: monofun_cfun)
   14.11  apply (simp add: rev_below_trans [OF lower_plus_below1])
   14.12 @@ -371,7 +371,7 @@
   14.13  by (induct xs rule: lower_pd_induct, simp_all)
   14.14  
   14.15  lemma lower_map_ID: "lower_map\<cdot>ID = ID"
   14.16 -by (simp add: expand_cfun_eq ID_def lower_map_ident)
   14.17 +by (simp add: cfun_eq_iff ID_def lower_map_ident)
   14.18  
   14.19  lemma lower_map_map:
   14.20    "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   14.21 @@ -483,7 +483,7 @@
   14.22  next
   14.23    show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
   14.24      unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
   14.25 -    by (simp add: cast_DEFL oo_def expand_cfun_eq lower_map_map)
   14.26 +    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
   14.27  qed
   14.28  
   14.29  end
    15.1 --- a/src/HOLCF/Representable.thy	Mon Oct 11 16:24:44 2010 -0700
    15.2 +++ b/src/HOLCF/Representable.thy	Mon Oct 11 21:35:31 2010 -0700
    15.3 @@ -45,7 +45,7 @@
    15.4  by (simp add: coerce_def)
    15.5  
    15.6  lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
    15.7 -by (rule ext_cfun, simp add: beta_coerce)
    15.8 +by (rule cfun_eqI, simp add: beta_coerce)
    15.9  
   15.10  lemma emb_coerce:
   15.11    "DEFL('a) \<sqsubseteq> DEFL('b)
   15.12 @@ -169,7 +169,7 @@
   15.13      apply (simp add: emb_prj cast.below)
   15.14      done
   15.15    show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
   15.16 -    by (rule ext_cfun, simp add: defl emb_prj)
   15.17 +    by (rule cfun_eqI, simp add: defl emb_prj)
   15.18  qed
   15.19  
   15.20  lemma typedef_DEFL:
   15.21 @@ -201,10 +201,10 @@
   15.22    "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
   15.23  
   15.24  lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
   15.25 -unfolding isodefl_def by (simp add: ext_cfun)
   15.26 +unfolding isodefl_def by (simp add: cfun_eqI)
   15.27  
   15.28  lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
   15.29 -unfolding isodefl_def by (simp add: ext_cfun)
   15.30 +unfolding isodefl_def by (simp add: cfun_eqI)
   15.31  
   15.32  lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
   15.33  unfolding isodefl_def
   15.34 @@ -228,14 +228,14 @@
   15.35  lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
   15.36  unfolding isodefl_def
   15.37  apply (simp add: cast_DEFL)
   15.38 -apply (simp add: expand_cfun_eq)
   15.39 +apply (simp add: cfun_eq_iff)
   15.40  apply (rule allI)
   15.41  apply (drule_tac x="emb\<cdot>x" in spec)
   15.42  apply simp
   15.43  done
   15.44  
   15.45  lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
   15.46 -unfolding isodefl_def by (simp add: expand_cfun_eq)
   15.47 +unfolding isodefl_def by (simp add: cfun_eq_iff)
   15.48  
   15.49  lemma adm_isodefl:
   15.50    "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
   15.51 @@ -263,7 +263,7 @@
   15.52    assumes DEFL: "DEFL('b) = DEFL('a)"
   15.53    shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
   15.54  unfolding isodefl_def
   15.55 -apply (simp add: expand_cfun_eq)
   15.56 +apply (simp add: cfun_eq_iff)
   15.57  apply (simp add: emb_coerce coerce_prj DEFL)
   15.58  done
   15.59  
    16.1 --- a/src/HOLCF/Sprod.thy	Mon Oct 11 16:24:44 2010 -0700
    16.2 +++ b/src/HOLCF/Sprod.thy	Mon Oct 11 21:35:31 2010 -0700
    16.3 @@ -250,7 +250,7 @@
    16.4  by (cases "x = \<bottom> \<or> y = \<bottom>") auto
    16.5  
    16.6  lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
    16.7 -unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
    16.8 +unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
    16.9  
   16.10  lemma sprod_map_map:
   16.11    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    17.1 --- a/src/HOLCF/Ssum.thy	Mon Oct 11 16:24:44 2010 -0700
    17.2 +++ b/src/HOLCF/Ssum.thy	Mon Oct 11 21:35:31 2010 -0700
    17.3 @@ -234,7 +234,7 @@
    17.4  by (cases "x = \<bottom>") simp_all
    17.5  
    17.6  lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
    17.7 -unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
    17.8 +unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
    17.9  
   17.10  lemma ssum_map_map:
   17.11    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    18.1 --- a/src/HOLCF/Universal.thy	Mon Oct 11 16:24:44 2010 -0700
    18.2 +++ b/src/HOLCF/Universal.thy	Mon Oct 11 21:35:31 2010 -0700
    18.3 @@ -988,7 +988,7 @@
    18.4  done
    18.5  
    18.6  lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID"
    18.7 -apply (rule ext_cfun, simp add: contlub_cfun_fun)
    18.8 +apply (rule cfun_eqI, simp add: contlub_cfun_fun)
    18.9  apply (rule below_antisym)
   18.10  apply (rule is_lub_thelub)
   18.11  apply (simp)
    19.1 --- a/src/HOLCF/Up.thy	Mon Oct 11 16:24:44 2010 -0700
    19.2 +++ b/src/HOLCF/Up.thy	Mon Oct 11 21:35:31 2010 -0700
    19.3 @@ -303,7 +303,7 @@
    19.4  unfolding u_map_def by simp
    19.5  
    19.6  lemma u_map_ID: "u_map\<cdot>ID = ID"
    19.7 -unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
    19.8 +unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
    19.9  
   19.10  lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
   19.11  by (induct p) simp_all
    20.1 --- a/src/HOLCF/UpperPD.thy	Mon Oct 11 16:24:44 2010 -0700
    20.2 +++ b/src/HOLCF/UpperPD.thy	Mon Oct 11 21:35:31 2010 -0700
    20.3 @@ -318,7 +318,7 @@
    20.4  
    20.5  lemma upper_bind_basis_mono:
    20.6    "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
    20.7 -unfolding expand_cfun_below
    20.8 +unfolding cfun_below_iff
    20.9  apply (erule upper_le_induct, safe)
   20.10  apply (simp add: monofun_cfun)
   20.11  apply (simp add: below_trans [OF upper_plus_below1])
   20.12 @@ -366,7 +366,7 @@
   20.13  by (induct xs rule: upper_pd_induct, simp_all)
   20.14  
   20.15  lemma upper_map_ID: "upper_map\<cdot>ID = ID"
   20.16 -by (simp add: expand_cfun_eq ID_def upper_map_ident)
   20.17 +by (simp add: cfun_eq_iff ID_def upper_map_ident)
   20.18  
   20.19  lemma upper_map_map:
   20.20    "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
   20.21 @@ -478,7 +478,7 @@
   20.22  next
   20.23    show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
   20.24      unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
   20.25 -    by (simp add: cast_DEFL oo_def expand_cfun_eq upper_map_map)
   20.26 +    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
   20.27  qed
   20.28  
   20.29  end
    21.1 --- a/src/HOLCF/ex/Fix2.thy	Mon Oct 11 16:24:44 2010 -0700
    21.2 +++ b/src/HOLCF/ex/Fix2.thy	Mon Oct 11 21:35:31 2010 -0700
    21.3 @@ -16,7 +16,7 @@
    21.4  
    21.5  
    21.6  lemma lemma1: "fix = gix"
    21.7 -apply (rule ext_cfun)
    21.8 +apply (rule cfun_eqI)
    21.9  apply (rule antisym_less)
   21.10  apply (rule fix_least)
   21.11  apply (rule gix1_def)
    22.1 --- a/src/HOLCF/ex/Focus_ex.thy	Mon Oct 11 16:24:44 2010 -0700
    22.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Mon Oct 11 21:35:31 2010 -0700
    22.3 @@ -211,7 +211,7 @@
    22.4  apply (rule_tac x = "f" in exI)
    22.5  apply (erule conjE)+
    22.6  apply (erule conjI)
    22.7 -apply (rule ext_cfun)
    22.8 +apply (rule cfun_eqI)
    22.9  apply (erule_tac x = "x" in allE)
   22.10  apply (erule exE)
   22.11  apply (erule conjE)+
    23.1 --- a/src/HOLCF/ex/Hoare.thy	Mon Oct 11 16:24:44 2010 -0700
    23.2 +++ b/src/HOLCF/ex/Hoare.thy	Mon Oct 11 21:35:31 2010 -0700
    23.3 @@ -417,7 +417,7 @@
    23.4  (* ------ the main proof q o p = q ------ *)
    23.5  
    23.6  theorem hoare_main: "q oo p = q"
    23.7 -apply (rule ext_cfun)
    23.8 +apply (rule cfun_eqI)
    23.9  apply (subst cfcomp2)
   23.10  apply (rule hoare_lemma3 [THEN disjE])
   23.11  apply (erule hoare_lemma23)