# 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 "(\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 "\i. finite_deflation (approx i)" unfolding approx_def apply (rule bifinite.finite_deflation_p_d_e) @@ -228,7 +228,7 @@ next show "cast\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ '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\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ '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\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ '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\DEFL('a u) = emb oo (prj :: udom \ '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]: "(\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\DEFL('a \ 'b) = emb oo (prj :: udom \ 'a \ '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) = (\x. f\x = g\x)" +lemma cfun_eq_iff: "f = g \ (\x. f\x = g\x)" by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff) -lemma ext_cfun: "(\x. f\x = g\x) \ f = g" -by (simp add: expand_cfun_eq) +lemma cfun_eqI: "(\x. f\x = g\x) \ f = g" +by (simp add: cfun_eq_iff) text {* Extensionality wrt. ordering for continuous functions *} -lemma expand_cfun_below: "f \ g = (\x. f\x \ g\x)" -by (simp add: below_CFun_def expand_fun_below) +lemma cfun_below_iff: "f \ g \ (\x. f\x \ g\x)" +by (simp add: below_CFun_def fun_below_iff) -lemma below_cfun_ext: "(\x. f\x \ g\x) \ f \ g" -by (simp add: expand_cfun_below) +lemma cfun_belowI: "(\x. f\x \ g\x) \ f \ 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 \ g \ f\x \ g\x" -by (simp add: expand_cfun_below) +by (simp add: cfun_below_iff) lemma monofun_cfun_arg: "x \ y \ f\x \ f\y" by (rule monofun_Rep_CFun2 [THEN monofunE]) @@ -258,7 +258,7 @@ lemma ch2ch_LAM [simp]: "\\x. chain (\i. S i x); \i. cont (\x. S i x)\ \ chain (\i. \ 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: "\\x. cont (\y. f x y); \y. monofun (\x. f x y)\ \ monofun (\x. \ 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]: "\ oo f = \" -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\ID\ID = ID" -unfolding expand_cfun_eq by simp +unfolding cfun_eq_iff by simp lemma cfun_map_map: "cfun_map\f1\g1\(cfun_map\f2\g2\p) = cfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\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: "\a b. a \ b \ g a \ g b" assumes below: "\a. f a \ g a" shows "basis_fun f \ 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: "\cont f; cont g; \x. f x \ g x\ \ (\ x. f x) \ (\ x. g x)" -by (simp add: expand_cfun_below) +by (simp add: cfun_below_iff) lemma convex_bind_basis_mono: "t \\ u \ convex_bind_basis t \ convex_bind_basis u" @@ -382,7 +382,7 @@ by (induct xs rule: convex_pd_induct, simp_all) lemma convex_map_ID: "convex_map\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\f\(convex_map\g\xs) = convex_map\(\ x. f\(g\x))\xs" @@ -494,7 +494,7 @@ next show "cast\DEFL('a convex_pd) = emb oo (prj :: udom \ '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\ID\ID = ID" -unfolding expand_cfun_eq by auto +unfolding cfun_eq_iff by auto lemma cprod_map_map: "cprod_map\f1\g1\(cprod_map\f2\g2\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 \ 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: "\x. d\x = x \ f\x = x" shows "d \ f" -proof (rule below_cfun_ext) +proof (rule cfun_belowI) fix x from below have "f\(d\x) \ f\x" by (rule monofun_cfun_arg) also from idem have "f\(d\x) = d\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 \ e2" -proof (rule below_cfun_ext) +proof (rule cfun_belowI) fix x have "e1\(p\(e2\x)) \ e2\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 \ p2" -proof (rule below_cfun_ext) +proof (rule cfun_belowI) fix x have "e\(p1\x) \ 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\e1\p2\(cfun_map\p1\e2\f) = f" - by (simp add: expand_cfun_eq) + by (simp add: cfun_eq_iff) fix g show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ 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\d1\d2\(cfun_map\d1\d2\f) = cfun_map\d1\d2\f" - by (simp add: expand_cfun_eq d1.idem d2.idem) + by (simp add: cfun_eq_iff d1.idem d2.idem) show "cfun_map\d1\d2\f \ 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 (\x. (a\x, b\(f\(a\x)))) = range (\x. (a\x, b\(g\(a\x))))" hence "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\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 \ g) = (\x. f x \ g x)" +lemma fun_below_iff: "f \ g \ (\x. f x \ g x)" by (simp add: below_fun_def) -lemma below_fun_ext: "(\x. f x \ g x) \ f \ g" +lemma fun_belowI: "(\x. f x \ g x) \ f \ 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 \ 'b" show "f \ g \ 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: "\y. monofun (\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: "\y. cont (\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. \x. iterate (Suc j)\f\x = iterate (Suc i)\f\x" by (simp only: iterate_Suc2) hence "MOST i. MOST j. iterate (Suc j)\f = iterate (Suc i)\f" - by (simp only: expand_cfun_eq) + by (simp only: cfun_eq_iff) hence "eventually_constant (\i. iterate (Suc i)\f)" unfolding eventually_constant_MOST_MOST . thus "eventually_constant (\i. iterate i\f)" @@ -587,7 +587,7 @@ apply (simp add: defl_approx_principal fd_take_below) done show lub: "(\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\\ = \" -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\\ = \ \ strictify\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\(sfun_rep\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\ID\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\\ = \" and "g2\\ = \" shows "sfun_map\f1\g1\(sfun_map\f2\g2\p) = sfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\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\DEFL('a \! 'b) = emb oo (prj :: udom \ 'a \! '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 @@ "(\x. f x \ g x) \ (FLIFT x. f x) \ (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 \\ u \ lower_bind_basis t \ 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\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\f\(lower_map\g\xs) = lower_map\(\ x. f\(g\x))\xs" @@ -483,7 +483,7 @@ next show "cast\DEFL('a lower_pd) = emb oo (prj :: udom \ '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 \ 'a) = ID" -by (rule ext_cfun, simp add: beta_coerce) +by (rule cfun_eqI, simp add: beta_coerce) lemma emb_coerce: "DEFL('a) \ DEFL('b) @@ -169,7 +169,7 @@ apply (simp add: emb_prj cast.below) done show "cast\DEFL('a) = emb oo (prj :: udom \ '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 \ cast\t = emb oo d oo prj" lemma isodeflI: "(\x. cast\t\x = emb\(d\(prj\x))) \ 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 \ cast\t = (\ x. emb\(d\(prj\x)))" -unfolding isodefl_def by (simp add: ext_cfun) +unfolding isodefl_def by (simp add: cfun_eqI) lemma isodefl_strict: "isodefl d t \ d\\ = \" unfolding isodefl_def @@ -228,14 +228,14 @@ lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \ 'a) DEFL('a) \ 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\x" in spec) apply simp done lemma isodefl_bottom: "isodefl \ \" -unfolding isodefl_def by (simp add: expand_cfun_eq) +unfolding isodefl_def by (simp add: cfun_eq_iff) lemma adm_isodefl: "cont f \ cont g \ adm (\x. isodefl (f x) (g x))" @@ -263,7 +263,7 @@ assumes DEFL: "DEFL('b) = DEFL('a)" shows "isodefl d t \ isodefl (coerce oo d oo coerce :: 'b \ '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 = \ \ y = \") auto lemma sprod_map_ID: "sprod_map\ID\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: "\f1\\ = \; g1\\ = \\ \ 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 = \") simp_all lemma ssum_map_ID: "ssum_map\ID\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: "\f1\\ = \; g1\\ = \\ \ 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]: "(\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\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\f\(u_map\g\p) = u_map\(\ x. f\(g\x))\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 \\ u \ upper_bind_basis t \ 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\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\f\(upper_map\g\xs) = upper_map\(\ x. f\(g\x))\xs" @@ -478,7 +478,7 @@ next show "cast\DEFL('a upper_pd) = emb oo (prj :: udom \ '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)