# HG changeset patch
# User huffman
# Date 1286858131 25200
# Node ID c5b5f7a3a3b13bb8de23ee75416608ac0c0bda9e
# Parent  666c3751227c1275687819437aba9773bec0c527
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI

diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Bifinite.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -56,7 +56,7 @@
       unfolding approx_def by (simp add: Y)
     show "(\<Squnion>i. approx i) = ID"
       unfolding approx_def
-      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL expand_cfun_eq)
+      by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff)
     show "\<And>i. finite_deflation (approx i)"
       unfolding approx_def
       apply (rule bifinite.finite_deflation_p_d_e)
@@ -228,7 +228,7 @@
 next
   show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)"
     unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq cfun_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map)
 qed
 
 end
@@ -287,7 +287,7 @@
 next
   show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
     unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq cprod_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map)
 qed
 
 end
@@ -348,7 +348,7 @@
 next
   show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
     unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq sprod_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map)
 qed
 
 end
@@ -405,7 +405,7 @@
 next
   show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
     unfolding emb_u_def prj_u_def defl_u_def cast_u_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq u_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map)
 qed
 
 end
@@ -425,7 +425,7 @@
   by (rule chainI, simp add: FLIFT_mono)
 
 lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
 apply (simp add: contlub_cfun_fun)
 apply (simp add: lift_approx_def)
 apply (case_tac x, simp)
@@ -548,7 +548,7 @@
 next
   show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
     unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq ssum_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map)
 qed
 
 end
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -176,19 +176,19 @@
 
 text {* Extensionality for continuous functions *}
 
-lemma expand_cfun_eq: "(f = g) = (\<forall>x. f\<cdot>x = g\<cdot>x)"
+lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
 by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff)
 
-lemma ext_cfun: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
-by (simp add: expand_cfun_eq)
+lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
+by (simp add: cfun_eq_iff)
 
 text {* Extensionality wrt. ordering for continuous functions *}
 
-lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
-by (simp add: below_CFun_def expand_fun_below)
+lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
+by (simp add: below_CFun_def fun_below_iff)
 
-lemma below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: expand_cfun_below)
+lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: cfun_below_iff)
 
 text {* Congruence for continuous function application *}
 
@@ -233,7 +233,7 @@
 text {* monotonicity of application *}
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: expand_cfun_below)
+by (simp add: cfun_below_iff)
 
 lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
 by (rule monofun_Rep_CFun2 [THEN monofunE])
@@ -258,7 +258,7 @@
 
 lemma ch2ch_LAM [simp]:
   "\<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)"
-by (simp add: chain_def expand_cfun_below)
+by (simp add: chain_def cfun_below_iff)
 
 text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
 
@@ -344,7 +344,7 @@
 lemma cont2mono_LAM:
   "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
     \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
-  unfolding monofun_def expand_cfun_below by simp
+  unfolding monofun_def cfun_below_iff by simp
 
 text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
 
@@ -509,7 +509,7 @@
 by (simp add: cfcomp1)
 
 lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
-by (simp add: expand_cfun_eq)
+by (simp add: cfun_eq_iff)
 
 text {*
   Show that interpretation of (pcpo,@{text "_->_"}) is a category.
@@ -520,13 +520,13 @@
 *}
 
 lemma ID2 [simp]: "f oo ID = f"
-by (rule ext_cfun, simp)
+by (rule cfun_eqI, simp)
 
 lemma ID3 [simp]: "ID oo f = f"
-by (rule ext_cfun, simp)
+by (rule cfun_eqI, simp)
 
 lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
-by (rule ext_cfun, simp)
+by (rule cfun_eqI, simp)
 
 subsection {* Map operator for continuous function space *}
 
@@ -539,12 +539,12 @@
 unfolding cfun_map_def by simp
 
 lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID"
-unfolding expand_cfun_eq by simp
+unfolding cfun_eq_iff by simp
 
 lemma cfun_map_map:
   "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
     cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-by (rule ext_cfun) simp
+by (rule cfun_eqI) simp
 
 subsection {* Strictified functions *}
 
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Completion.thy
--- a/src/HOLCF/Completion.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Completion.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -397,7 +397,7 @@
   assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
   assumes below: "\<And>a. f a \<sqsubseteq> g a"
   shows "basis_fun f \<sqsubseteq> basis_fun g"
- apply (rule below_cfun_ext)
+ apply (rule cfun_belowI)
  apply (simp only: basis_fun_beta f_mono g_mono)
  apply (rule is_lub_thelub_ex)
   apply (rule basis_fun_lemma, erule f_mono)
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -331,7 +331,7 @@
 
 lemma monofun_LAM:
   "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
-by (simp add: expand_cfun_below)
+by (simp add: cfun_below_iff)
 
 lemma convex_bind_basis_mono:
   "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
@@ -382,7 +382,7 @@
 by (induct xs rule: convex_pd_induct, simp_all)
 
 lemma convex_map_ID: "convex_map\<cdot>ID = ID"
-by (simp add: expand_cfun_eq ID_def convex_map_ident)
+by (simp add: cfun_eq_iff ID_def convex_map_ident)
 
 lemma convex_map_map:
   "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
@@ -494,7 +494,7 @@
 next
   show "cast\<cdot>DEFL('a convex_pd) = emb oo (prj :: udom \<rightarrow> 'a convex_pd)"
     unfolding emb_convex_pd_def prj_convex_pd_def defl_convex_pd_def cast_convex_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq convex_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff convex_map_map)
 qed
 
 end
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Cprod.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -51,7 +51,7 @@
 unfolding cprod_map_def by simp
 
 lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding expand_cfun_eq by auto
+unfolding cfun_eq_iff by auto
 
 lemma cprod_map_map:
   "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Deflation.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -19,7 +19,7 @@
 begin
 
 lemma below_ID: "d \<sqsubseteq> ID"
-by (rule below_cfun_ext, simp add: below)
+by (rule cfun_belowI, simp add: below)
 
 text {* The set of fixed points is the same as the range. *}
 
@@ -36,7 +36,7 @@
 
 lemma belowI:
   assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
-proof (rule below_cfun_ext)
+proof (rule cfun_belowI)
   fix x
   from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
@@ -326,7 +326,7 @@
 lemma ep_pair_unique_e_lemma:
   assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
   shows "e1 \<sqsubseteq> e2"
-proof (rule below_cfun_ext)
+proof (rule cfun_belowI)
   fix x
   have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
     by (rule ep_pair.e_p_below [OF 1])
@@ -341,7 +341,7 @@
 lemma ep_pair_unique_p_lemma:
   assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
   shows "p1 \<sqsubseteq> p2"
-proof (rule below_cfun_ext)
+proof (rule cfun_belowI)
   fix x
   have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
     by (rule ep_pair.e_p_below [OF 1])
@@ -414,9 +414,9 @@
   interpret e1p1: ep_pair e1 p1 by fact
   interpret e2p2: ep_pair e2 p2 by fact
   fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f"
-    by (simp add: expand_cfun_eq)
+    by (simp add: cfun_eq_iff)
   fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g"
-    apply (rule below_cfun_ext, simp)
+    apply (rule cfun_belowI, simp)
     apply (rule below_trans [OF e2p2.e_p_below])
     apply (rule monofun_cfun_arg)
     apply (rule e1p1.e_p_below)
@@ -431,9 +431,9 @@
   interpret d2: deflation d2 by fact
   fix f
   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f"
-    by (simp add: expand_cfun_eq d1.idem d2.idem)
+    by (simp add: cfun_eq_iff d1.idem d2.idem)
   show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f"
-    apply (rule below_cfun_ext, simp)
+    apply (rule cfun_belowI, simp)
     apply (rule below_trans [OF d2.below])
     apply (rule monofun_cfun_arg)
     apply (rule d1.below)
@@ -455,7 +455,7 @@
       by (simp add: a b)
   qed
   show "inj_on ?f (range ?h)"
-  proof (rule inj_onI, rule ext_cfun, clarsimp)
+  proof (rule inj_onI, rule cfun_eqI, clarsimp)
     fix x f g
     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))))"
     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))))"
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/FOCUS/Buffer.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -200,7 +200,7 @@
 apply (  rule_tac [2] P="(%x. x:B)" in ssubst)
 prefer 3
 apply (   assumption)
-apply (  rule_tac [2] ext_cfun)
+apply (  rule_tac [2] cfun_eqI)
 apply (  drule_tac [2] spec)
 apply (  drule_tac [2] f="rt" in cfun_arg_cong)
 prefer 2
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Fun_Cpo.thy
--- a/src/HOLCF/Fun_Cpo.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -35,12 +35,10 @@
     unfolding below_fun_def by (fast elim: below_trans)
 qed
 
-text {* make the symbol @{text "<<"} accessible for type fun *}
-
-lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
+lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
 by (simp add: below_fun_def)
 
-lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
 by (simp add: below_fun_def)
 
 subsection {* Full function space is chain complete *}
@@ -71,9 +69,9 @@
   shows "range Y <<| f"
 apply (rule is_lubI)
 apply (rule ub_rangeI)
-apply (rule below_fun_ext)
+apply (rule fun_belowI)
 apply (rule is_ub_lub [OF f])
-apply (rule below_fun_ext)
+apply (rule fun_belowI)
 apply (rule is_lub_lub [OF f])
 apply (erule ub2ub_fun)
 done
@@ -104,7 +102,7 @@
 proof
   fix f g :: "'a \<Rightarrow> 'b"
   show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
-    unfolding expand_fun_below fun_eq_iff
+    unfolding fun_below_iff fun_eq_iff
     by simp
 qed
 
@@ -227,7 +225,7 @@
 lemma mono2mono_lambda:
   assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
 apply (rule monofunI)
-apply (rule below_fun_ext)
+apply (rule fun_belowI)
 apply (erule monofunE [OF f])
 done
 
@@ -235,7 +233,7 @@
   assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
 apply (rule contI2)
 apply (simp add: mono2mono_lambda cont2mono f)
-apply (rule below_fun_ext)
+apply (rule fun_belowI)
 apply (simp add: thelub_fun cont2contlubE [OF f])
 done
 
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/HOLCF.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -15,7 +15,16 @@
 
 ML {* path_add "~~/src/HOLCF/Library" *}
 
-text {* Legacy theorem names *}
+text {* Legacy theorem names deprecated after Isabelle2009-2: *}
+
+lemmas expand_fun_below = fun_below_iff
+lemmas below_fun_ext = fun_belowI
+lemmas expand_cfun_eq = cfun_eq_iff
+lemmas ext_cfun = cfun_eqI
+lemmas expand_cfun_below = cfun_below_iff
+lemmas below_cfun_ext = cfun_belowI
+
+text {* Older legacy theorem names: *}
 
 lemmas sq_ord_less_eq_trans = below_eq_trans
 lemmas sq_ord_eq_less_trans = eq_below_trans
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -240,7 +240,7 @@
   hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
     by (simp only: iterate_Suc2)
   hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
-    by (simp only: expand_cfun_eq)
+    by (simp only: cfun_eq_iff)
   hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
     unfolding eventually_constant_MOST_MOST .
   thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
@@ -587,7 +587,7 @@
     apply (simp add: defl_approx_principal fd_take_below)
     done
   show lub: "(\<Squnion>i. defl_approx i) = ID"
-    apply (rule ext_cfun, rule below_antisym)
+    apply (rule cfun_eqI, rule below_antisym)
     apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
     apply (induct_tac x rule: defl.principal_induct, simp)
     apply (simp add: contlub_cfun_fun chain)
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Library/Stream.thy
--- a/src/HOLCF/Library/Stream.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Library/Stream.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -508,7 +508,7 @@
 by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
 apply (subst sfilter_unfold, auto)
 apply (case_tac "x=UU", auto)
 by (drule stream_exhaust_eq [THEN iffD1], auto)
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Library/Strict_Fun.thy
--- a/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -37,13 +37,13 @@
   unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
 
 lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
-  by (simp add: expand_cfun_eq strictify_conv_if)
+  by (simp add: cfun_eq_iff strictify_conv_if)
 
 lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
   unfolding sfun_abs_def sfun_rep_def
   apply (simp add: cont_Abs_sfun cont_Rep_sfun)
   apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
-  apply (simp add: expand_cfun_eq strictify_conv_if)
+  apply (simp add: cfun_eq_iff strictify_conv_if)
   apply (simp add: Rep_sfun [simplified])
   done
 
@@ -56,7 +56,7 @@
 lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
 apply default
 apply (rule sfun_abs_sfun_rep)
-apply (simp add: expand_cfun_below strictify_conv_if)
+apply (simp add: cfun_below_iff strictify_conv_if)
 done
 
 interpretation sfun: ep_pair sfun_rep sfun_abs
@@ -71,14 +71,14 @@
 
 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
   unfolding sfun_map_def
-  by (simp add: cfun_map_ID expand_cfun_eq)
+  by (simp add: cfun_map_ID cfun_eq_iff)
 
 lemma sfun_map_map:
   assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
   "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
     sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
 unfolding sfun_map_def
-by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map)
+by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
 
 lemma ep_pair_sfun_map:
   assumes 1: "ep_pair e1 p1"
@@ -193,7 +193,7 @@
 next
   show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
     unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
 qed
 
 end
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Lift.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -134,7 +134,7 @@
   "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
 apply (rule monofunE [where f=flift1])
 apply (rule cont2mono [OF cont_flift1])
-apply (simp add: below_fun_ext)
+apply (simp add: fun_below_iff)
 done
 
 lemma cont2cont_flift1 [simp, cont2cont]:
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -323,7 +323,7 @@
 
 lemma lower_bind_basis_mono:
   "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
-unfolding expand_cfun_below
+unfolding cfun_below_iff
 apply (erule lower_le_induct, safe)
 apply (simp add: monofun_cfun)
 apply (simp add: rev_below_trans [OF lower_plus_below1])
@@ -371,7 +371,7 @@
 by (induct xs rule: lower_pd_induct, simp_all)
 
 lemma lower_map_ID: "lower_map\<cdot>ID = ID"
-by (simp add: expand_cfun_eq ID_def lower_map_ident)
+by (simp add: cfun_eq_iff ID_def lower_map_ident)
 
 lemma lower_map_map:
   "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
@@ -483,7 +483,7 @@
 next
   show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)"
     unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq lower_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map)
 qed
 
 end
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Representable.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -45,7 +45,7 @@
 by (simp add: coerce_def)
 
 lemma coerce_eq_ID [simp]: "(coerce :: 'a \<rightarrow> 'a) = ID"
-by (rule ext_cfun, simp add: beta_coerce)
+by (rule cfun_eqI, simp add: beta_coerce)
 
 lemma emb_coerce:
   "DEFL('a) \<sqsubseteq> DEFL('b)
@@ -169,7 +169,7 @@
     apply (simp add: emb_prj cast.below)
     done
   show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
-    by (rule ext_cfun, simp add: defl emb_prj)
+    by (rule cfun_eqI, simp add: defl emb_prj)
 qed
 
 lemma typedef_DEFL:
@@ -201,10 +201,10 @@
   "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
 
 lemma isodeflI: "(\<And>x. cast\<cdot>t\<cdot>x = emb\<cdot>(d\<cdot>(prj\<cdot>x))) \<Longrightarrow> isodefl d t"
-unfolding isodefl_def by (simp add: ext_cfun)
+unfolding isodefl_def by (simp add: cfun_eqI)
 
 lemma cast_isodefl: "isodefl d t \<Longrightarrow> cast\<cdot>t = (\<Lambda> x. emb\<cdot>(d\<cdot>(prj\<cdot>x)))"
-unfolding isodefl_def by (simp add: ext_cfun)
+unfolding isodefl_def by (simp add: cfun_eqI)
 
 lemma isodefl_strict: "isodefl d t \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
 unfolding isodefl_def
@@ -228,14 +228,14 @@
 lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \<rightarrow> 'a) DEFL('a) \<Longrightarrow> d = ID"
 unfolding isodefl_def
 apply (simp add: cast_DEFL)
-apply (simp add: expand_cfun_eq)
+apply (simp add: cfun_eq_iff)
 apply (rule allI)
 apply (drule_tac x="emb\<cdot>x" in spec)
 apply simp
 done
 
 lemma isodefl_bottom: "isodefl \<bottom> \<bottom>"
-unfolding isodefl_def by (simp add: expand_cfun_eq)
+unfolding isodefl_def by (simp add: cfun_eq_iff)
 
 lemma adm_isodefl:
   "cont f \<Longrightarrow> cont g \<Longrightarrow> adm (\<lambda>x. isodefl (f x) (g x))"
@@ -263,7 +263,7 @@
   assumes DEFL: "DEFL('b) = DEFL('a)"
   shows "isodefl d t \<Longrightarrow> isodefl (coerce oo d oo coerce :: 'b \<rightarrow> 'b) t"
 unfolding isodefl_def
-apply (simp add: expand_cfun_eq)
+apply (simp add: cfun_eq_iff)
 apply (simp add: emb_coerce coerce_prj DEFL)
 done
 
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -250,7 +250,7 @@
 by (cases "x = \<bottom> \<or> y = \<bottom>") auto
 
 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
-unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
+unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
 
 lemma sprod_map_map:
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -234,7 +234,7 @@
 by (cases "x = \<bottom>") simp_all
 
 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
-unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
+unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun)
 
 lemma ssum_map_map:
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Universal.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -988,7 +988,7 @@
 done
 
 lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID"
-apply (rule ext_cfun, simp add: contlub_cfun_fun)
+apply (rule cfun_eqI, simp add: contlub_cfun_fun)
 apply (rule below_antisym)
 apply (rule is_lub_thelub)
 apply (simp)
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Up.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -303,7 +303,7 @@
 unfolding u_map_def by simp
 
 lemma u_map_ID: "u_map\<cdot>ID = ID"
-unfolding u_map_def by (simp add: expand_cfun_eq eta_cfun)
+unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun)
 
 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"
 by (induct p) simp_all
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -318,7 +318,7 @@
 
 lemma upper_bind_basis_mono:
   "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
-unfolding expand_cfun_below
+unfolding cfun_below_iff
 apply (erule upper_le_induct, safe)
 apply (simp add: monofun_cfun)
 apply (simp add: below_trans [OF upper_plus_below1])
@@ -366,7 +366,7 @@
 by (induct xs rule: upper_pd_induct, simp_all)
 
 lemma upper_map_ID: "upper_map\<cdot>ID = ID"
-by (simp add: expand_cfun_eq ID_def upper_map_ident)
+by (simp add: cfun_eq_iff ID_def upper_map_ident)
 
 lemma upper_map_map:
   "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
@@ -478,7 +478,7 @@
 next
   show "cast\<cdot>DEFL('a upper_pd) = emb oo (prj :: udom \<rightarrow> 'a upper_pd)"
     unfolding emb_upper_pd_def prj_upper_pd_def defl_upper_pd_def cast_upper_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq upper_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff upper_map_map)
 qed
 
 end
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/ex/Fix2.thy
--- a/src/HOLCF/ex/Fix2.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/ex/Fix2.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -16,7 +16,7 @@
 
 
 lemma lemma1: "fix = gix"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
 apply (rule antisym_less)
 apply (rule fix_least)
 apply (rule gix1_def)
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/ex/Focus_ex.thy
--- a/src/HOLCF/ex/Focus_ex.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/ex/Focus_ex.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -211,7 +211,7 @@
 apply (rule_tac x = "f" in exI)
 apply (erule conjE)+
 apply (erule conjI)
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
 apply (erule_tac x = "x" in allE)
 apply (erule exE)
 apply (erule conjE)+
diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/ex/Hoare.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -417,7 +417,7 @@
 (* ------ the main proof q o p = q ------ *)
 
 theorem hoare_main: "q oo p = q"
-apply (rule ext_cfun)
+apply (rule cfun_eqI)
 apply (subst cfcomp2)
 apply (rule hoare_lemma3 [THEN disjE])
 apply (erule hoare_lemma23)