rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
authorhuffman
Wed Oct 27 13:54:18 2010 -0700 (2010-10-27)
changeset 40321d065b195ec89
parent 40219 b283680d8044
child 40322 707eb30e8a53
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
src/HOLCF/ConvexPD.thy
src/HOLCF/Deflation.thy
src/HOLCF/Domain.thy
src/HOLCF/Domain_Aux.thy
src/HOLCF/Fix.thy
src/HOLCF/Lift.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Product_Cpo.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tutorial/Domain_ex.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/ConvexPD.thy	Wed Oct 27 11:11:35 2010 -0700
     1.2 +++ b/src/HOLCF/ConvexPD.thy	Wed Oct 27 13:54:18 2010 -0700
     1.3 @@ -256,7 +256,7 @@
     1.4  using convex_unit_Rep_compact_basis [of compact_bot]
     1.5  by (simp add: inst_convex_pd_pcpo)
     1.6  
     1.7 -lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
     1.8 +lemma convex_unit_bottom_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
     1.9  unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
    1.10  
    1.11  lemma compact_convex_unit: "compact x \<Longrightarrow> compact {x}\<natural>"
     2.1 --- a/src/HOLCF/Deflation.thy	Wed Oct 27 11:11:35 2010 -0700
     2.2 +++ b/src/HOLCF/Deflation.thy	Wed Oct 27 13:54:18 2010 -0700
     2.3 @@ -392,7 +392,7 @@
     2.4    finally show "e\<cdot>\<bottom> = \<bottom>" by simp
     2.5  qed
     2.6  
     2.7 -lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
     2.8 +lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
     2.9  by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
    2.10  
    2.11  lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
     3.1 --- a/src/HOLCF/Domain.thy	Wed Oct 27 11:11:35 2010 -0700
     3.2 +++ b/src/HOLCF/Domain.thy	Wed Oct 27 13:54:18 2010 -0700
     3.3 @@ -22,25 +22,25 @@
     3.4  
     3.5  text {* Lemmas for proving nchotomy rule: *}
     3.6  
     3.7 -lemma ex_one_defined_iff:
     3.8 +lemma ex_one_bottom_iff:
     3.9    "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
    3.10  by simp
    3.11  
    3.12 -lemma ex_up_defined_iff:
    3.13 +lemma ex_up_bottom_iff:
    3.14    "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
    3.15  by (safe, case_tac x, auto)
    3.16  
    3.17 -lemma ex_sprod_defined_iff:
    3.18 +lemma ex_sprod_bottom_iff:
    3.19   "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
    3.20    (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
    3.21  by (safe, case_tac y, auto)
    3.22  
    3.23 -lemma ex_sprod_up_defined_iff:
    3.24 +lemma ex_sprod_up_bottom_iff:
    3.25   "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
    3.26    (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
    3.27  by (safe, case_tac y, simp, case_tac x, auto)
    3.28  
    3.29 -lemma ex_ssum_defined_iff:
    3.30 +lemma ex_ssum_bottom_iff:
    3.31   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
    3.32   ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
    3.33    (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
    3.34 @@ -49,12 +49,12 @@
    3.35  lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
    3.36    by auto
    3.37  
    3.38 -lemmas ex_defined_iffs =
    3.39 -   ex_ssum_defined_iff
    3.40 -   ex_sprod_up_defined_iff
    3.41 -   ex_sprod_defined_iff
    3.42 -   ex_up_defined_iff
    3.43 -   ex_one_defined_iff
    3.44 +lemmas ex_bottom_iffs =
    3.45 +   ex_ssum_bottom_iff
    3.46 +   ex_sprod_up_bottom_iff
    3.47 +   ex_sprod_bottom_iff
    3.48 +   ex_up_bottom_iff
    3.49 +   ex_one_bottom_iff
    3.50  
    3.51  text {* Rules for turning nchotomy into exhaust: *}
    3.52  
    3.53 @@ -78,14 +78,14 @@
    3.54  lemmas con_strict_rules =
    3.55    sinl_strict sinr_strict spair_strict1 spair_strict2
    3.56  
    3.57 -lemmas con_defined_iff_rules =
    3.58 -  sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
    3.59 +lemmas con_bottom_iff_rules =
    3.60 +  sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
    3.61  
    3.62  lemmas con_below_iff_rules =
    3.63 -  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
    3.64 +  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
    3.65  
    3.66  lemmas con_eq_iff_rules =
    3.67 -  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
    3.68 +  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
    3.69  
    3.70  lemmas sel_strict_rules =
    3.71    cfcomp2 sscase1 sfst_strict ssnd_strict fup1
    3.72 @@ -102,8 +102,8 @@
    3.73    sel_strict_rules sel_app_extra_rules
    3.74    ssnd_spair sfst_spair up_defined spair_defined
    3.75  
    3.76 -lemmas sel_defined_iff_rules =
    3.77 -  cfcomp2 sfst_defined_iff ssnd_defined_iff
    3.78 +lemmas sel_bottom_iff_rules =
    3.79 +  cfcomp2 sfst_bottom_iff ssnd_bottom_iff
    3.80  
    3.81  lemmas take_con_rules =
    3.82    ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
     4.1 --- a/src/HOLCF/Domain_Aux.thy	Wed Oct 27 11:11:35 2010 -0700
     4.2 +++ b/src/HOLCF/Domain_Aux.thy	Wed Oct 27 13:54:18 2010 -0700
     4.3 @@ -71,14 +71,14 @@
     4.4  lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
     4.5    by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
     4.6  
     4.7 -lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
     4.8 +lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
     4.9    by (auto elim: abs_defin' intro: abs_strict)
    4.10  
    4.11 -lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
    4.12 -  by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
    4.13 +lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
    4.14 +  by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
    4.15  
    4.16  lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
    4.17 -  by (simp add: rep_defined_iff)
    4.18 +  by (simp add: rep_bottom_iff)
    4.19  
    4.20  lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
    4.21  proof (unfold compact_def)
     5.1 --- a/src/HOLCF/Fix.thy	Wed Oct 27 11:11:35 2010 -0700
     5.2 +++ b/src/HOLCF/Fix.thy	Wed Oct 27 13:54:18 2010 -0700
     5.3 @@ -119,7 +119,7 @@
     5.4  
     5.5  text {* strictness of @{term fix} *}
     5.6  
     5.7 -lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
     5.8 +lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
     5.9  apply (rule iffI)
    5.10  apply (erule subst)
    5.11  apply (rule fix_eq [symmetric])
    5.12 @@ -127,10 +127,10 @@
    5.13  done
    5.14  
    5.15  lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
    5.16 -by (simp add: fix_defined_iff)
    5.17 +by (simp add: fix_bottom_iff)
    5.18  
    5.19  lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
    5.20 -by (simp add: fix_defined_iff)
    5.21 +by (simp add: fix_bottom_iff)
    5.22  
    5.23  text {* @{term fix} applied to identity and constant functions *}
    5.24  
     6.1 --- a/src/HOLCF/Lift.thy	Wed Oct 27 11:11:35 2010 -0700
     6.2 +++ b/src/HOLCF/Lift.thy	Wed Oct 27 13:54:18 2010 -0700
     6.3 @@ -114,7 +114,7 @@
     6.4  lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
     6.5  by (erule lift_definedE, simp)
     6.6  
     6.7 -lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
     6.8 +lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
     6.9  by (cases x, simp_all)
    6.10  
    6.11  lemma FLIFT_mono:
     7.1 --- a/src/HOLCF/LowerPD.thy	Wed Oct 27 11:11:35 2010 -0700
     7.2 +++ b/src/HOLCF/LowerPD.thy	Wed Oct 27 13:54:18 2010 -0700
     7.3 @@ -229,10 +229,10 @@
     7.4  using lower_unit_Rep_compact_basis [of compact_bot]
     7.5  by (simp add: inst_lower_pd_pcpo)
     7.6  
     7.7 -lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
     7.8 +lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
     7.9  unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
    7.10  
    7.11 -lemma lower_plus_strict_iff [simp]:
    7.12 +lemma lower_plus_bottom_iff [simp]:
    7.13    "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
    7.14  apply safe
    7.15  apply (rule UU_I, erule subst, rule lower_plus_below1)
     8.1 --- a/src/HOLCF/Pcpodef.thy	Wed Oct 27 11:11:35 2010 -0700
     8.2 +++ b/src/HOLCF/Pcpodef.thy	Wed Oct 27 13:54:18 2010 -0700
     8.3 @@ -235,7 +235,7 @@
     8.4   apply (rule type_definition.Abs_inverse [OF type UU_in_A])
     8.5  done
     8.6  
     8.7 -theorem typedef_Abs_strict_iff:
     8.8 +theorem typedef_Abs_bottom_iff:
     8.9    assumes type: "type_definition Rep Abs A"
    8.10      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    8.11      and UU_in_A: "\<bottom> \<in> A"
    8.12 @@ -244,7 +244,7 @@
    8.13   apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
    8.14  done
    8.15  
    8.16 -theorem typedef_Rep_strict_iff:
    8.17 +theorem typedef_Rep_bottom_iff:
    8.18    assumes type: "type_definition Rep Abs A"
    8.19      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    8.20      and UU_in_A: "\<bottom> \<in> A"
    8.21 @@ -258,14 +258,14 @@
    8.22      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    8.23      and UU_in_A: "\<bottom> \<in> A"
    8.24    shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
    8.25 -by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
    8.26 +by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
    8.27  
    8.28  theorem typedef_Rep_defined:
    8.29    assumes type: "type_definition Rep Abs A"
    8.30      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    8.31      and UU_in_A: "\<bottom> \<in> A"
    8.32    shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
    8.33 -by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
    8.34 +by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
    8.35  
    8.36  subsection {* Proving a subtype is flat *}
    8.37  
     9.1 --- a/src/HOLCF/Product_Cpo.thy	Wed Oct 27 11:11:35 2010 -0700
     9.2 +++ b/src/HOLCF/Product_Cpo.thy	Wed Oct 27 13:54:18 2010 -0700
     9.3 @@ -173,7 +173,7 @@
     9.4  lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
     9.5  by (rule minimal_cprod [THEN UU_I, symmetric])
     9.6  
     9.7 -lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
     9.8 +lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
     9.9  unfolding inst_cprod_pcpo by simp
    9.10  
    9.11  lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
    10.1 --- a/src/HOLCF/Sprod.thy	Wed Oct 27 11:11:35 2010 -0700
    10.2 +++ b/src/HOLCF/Sprod.thy	Wed Oct 27 13:54:18 2010 -0700
    10.3 @@ -80,7 +80,7 @@
    10.4  lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
    10.5  by (simp add: Rep_sprod_simps)
    10.6  
    10.7 -lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
    10.8 +lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
    10.9  by (simp add: Rep_sprod_simps strict_conv_if)
   10.10  
   10.11  lemma spair_below_iff:
   10.12 @@ -136,10 +136,10 @@
   10.13  lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
   10.14  by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
   10.15  
   10.16 -lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
   10.17 +lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
   10.18  by (cases p, simp_all)
   10.19  
   10.20 -lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
   10.21 +lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
   10.22  by (cases p, simp_all)
   10.23  
   10.24  lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
    11.1 --- a/src/HOLCF/Ssum.thy	Wed Oct 27 11:11:35 2010 -0700
    11.2 +++ b/src/HOLCF/Ssum.thy	Wed Oct 27 13:54:18 2010 -0700
    11.3 @@ -98,10 +98,10 @@
    11.4  lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
    11.5  by (simp add: Rep_ssum_simps)
    11.6  
    11.7 -lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
    11.8 +lemma sinl_bottom_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
    11.9  using sinl_eq [of "x" "\<bottom>"] by simp
   11.10  
   11.11 -lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
   11.12 +lemma sinr_bottom_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
   11.13  using sinr_eq [of "x" "\<bottom>"] by simp
   11.14  
   11.15  lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
    12.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Oct 27 11:11:35 2010 -0700
    12.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Oct 27 13:54:18 2010 -0700
    12.3 @@ -210,7 +210,7 @@
    12.4            in (n2, mk_ssumT (t1, t2)) end;
    12.5        val ct = ctyp_of thy (snd (cons2typ 1 spec'));
    12.6        val thm1 = instantiate' [SOME ct] [] @{thm exh_start};
    12.7 -      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
    12.8 +      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1;
    12.9        val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
   12.10  
   12.11        val y = Free ("y", lhsT);
   12.12 @@ -279,8 +279,8 @@
   12.13            val lhs = mk_undef (list_ccomb (con, vs));
   12.14            val rhss = map mk_undef nonlazy;
   12.15            val goal = mk_trp (iff_disj (lhs, rhss));
   12.16 -          val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
   12.17 -          val rules = rule1 :: @{thms con_defined_iff_rules};
   12.18 +          val rule1 = iso_locale RS @{thm iso.abs_bottom_iff};
   12.19 +          val rules = rule1 :: @{thms con_bottom_iff_rules};
   12.20            val tacs = [simp_tac (HOL_ss addsimps rules) 1];
   12.21          in prove thy con_betas goal (K tacs) end;
   12.22      in
   12.23 @@ -506,7 +506,7 @@
   12.24            val goal = Logic.list_implies (assms, concl);
   12.25            val defs = case_beta :: con_betas;
   12.26            val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
   12.27 -          val rules2 = @{thms con_defined_iff_rules};
   12.28 +          val rules2 = @{thms con_bottom_iff_rules};
   12.29            val rules3 = @{thms cfcomp2 one_case2};
   12.30            val rules = abs_inverse :: rules1 @ rules2 @ rules3;
   12.31            val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
   12.32 @@ -528,7 +528,7 @@
   12.33      (rep_const : term)
   12.34      (abs_inv : thm)
   12.35      (rep_strict : thm)
   12.36 -    (rep_strict_iff : thm)
   12.37 +    (rep_bottom_iff : thm)
   12.38      (con_betas : thm list)
   12.39      (thy : theory)
   12.40      : thm list * theory =
   12.41 @@ -637,7 +637,7 @@
   12.42    (* prove selector definedness rules *)
   12.43      val sel_defins : thm list =
   12.44        let
   12.45 -        val rules = rep_strict_iff :: @{thms sel_defined_iff_rules};
   12.46 +        val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules};
   12.47          val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
   12.48          fun sel_defin sel =
   12.49            let
   12.50 @@ -868,8 +868,8 @@
   12.51      val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
   12.52      val rep_strict = iso_locale RS @{thm iso.rep_strict};
   12.53      val abs_strict = iso_locale RS @{thm iso.abs_strict};
   12.54 -    val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
   12.55 -    val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
   12.56 +    val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff};
   12.57 +    val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff};
   12.58      val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
   12.59  
   12.60      (* qualify constants and theorems with domain name *)
   12.61 @@ -908,7 +908,7 @@
   12.62            map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
   12.63        in
   12.64          add_selectors sel_spec rep_const
   12.65 -          abs_iso_thm rep_strict rep_defined_iff con_betas thy
   12.66 +          abs_iso_thm rep_strict rep_bottom_iff con_betas thy
   12.67        end;
   12.68  
   12.69      (* define and prove theorems for discriminator functions *)
    13.1 --- a/src/HOLCF/Tools/pcpodef.ML	Wed Oct 27 11:11:35 2010 -0700
    13.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Wed Oct 27 13:54:18 2010 -0700
    13.3 @@ -11,7 +11,7 @@
    13.4      { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
    13.5        lub: thm, thelub: thm, compact: thm }
    13.6    type pcpo_info =
    13.7 -    { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
    13.8 +    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
    13.9        Rep_defined: thm, Abs_defined: thm }
   13.10  
   13.11    val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
   13.12 @@ -48,7 +48,7 @@
   13.13      lub: thm, thelub: thm, compact: thm }
   13.14  
   13.15  type pcpo_info =
   13.16 -  { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
   13.17 +  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
   13.18      Rep_defined: thm, Abs_defined: thm }
   13.19  
   13.20  (* building terms *)
   13.21 @@ -136,8 +136,8 @@
   13.22      fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
   13.23      val Rep_strict = make @{thm typedef_Rep_strict};
   13.24      val Abs_strict = make @{thm typedef_Abs_strict};
   13.25 -    val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
   13.26 -    val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
   13.27 +    val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
   13.28 +    val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
   13.29      val Rep_defined = make @{thm typedef_Rep_defined};
   13.30      val Abs_defined = make @{thm typedef_Abs_defined};
   13.31      val (_, thy) =
   13.32 @@ -146,14 +146,14 @@
   13.33        |> Global_Theory.add_thms
   13.34          ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
   13.35            ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
   13.36 -          ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
   13.37 -          ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
   13.38 +          ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
   13.39 +          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
   13.40            ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
   13.41            ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
   13.42        ||> Sign.parent_path;
   13.43      val pcpo_info =
   13.44        { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
   13.45 -        Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
   13.46 +        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
   13.47          Rep_defined = Rep_defined, Abs_defined = Abs_defined };
   13.48    in
   13.49      (pcpo_info, thy)
    14.1 --- a/src/HOLCF/Tutorial/Domain_ex.thy	Wed Oct 27 11:11:35 2010 -0700
    14.2 +++ b/src/HOLCF/Tutorial/Domain_ex.thy	Wed Oct 27 13:54:18 2010 -0700
    14.3 @@ -116,8 +116,8 @@
    14.4  
    14.5  domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
    14.6  
    14.7 -lemmas tree_abs_defined_iff =
    14.8 -  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
    14.9 +lemmas tree_abs_bottom_iff =
   14.10 +  iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
   14.11  
   14.12  text {* Rules about ismorphism *}
   14.13  term tree_rep
    15.1 --- a/src/HOLCF/UpperPD.thy	Wed Oct 27 11:11:35 2010 -0700
    15.2 +++ b/src/HOLCF/UpperPD.thy	Wed Oct 27 13:54:18 2010 -0700
    15.3 @@ -233,10 +233,10 @@
    15.4  lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
    15.5  by (rule UU_I, rule upper_plus_below2)
    15.6  
    15.7 -lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
    15.8 +lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
    15.9  unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   15.10  
   15.11 -lemma upper_plus_strict_iff [simp]:
   15.12 +lemma upper_plus_bottom_iff [simp]:
   15.13    "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
   15.14  apply (rule iffI)
   15.15  apply (erule rev_mp)