--- a/src/HOLCF/ConvexPD.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy Wed Oct 27 13:54:18 2010 -0700
@@ -256,7 +256,7 @@
using convex_unit_Rep_compact_basis [of compact_bot]
by (simp add: inst_convex_pd_pcpo)
-lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma convex_unit_bottom_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
lemma compact_convex_unit: "compact x \<Longrightarrow> compact {x}\<natural>"
--- a/src/HOLCF/Deflation.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Deflation.thy Wed Oct 27 13:54:18 2010 -0700
@@ -392,7 +392,7 @@
finally show "e\<cdot>\<bottom> = \<bottom>" by simp
qed
-lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
--- a/src/HOLCF/Domain.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Domain.thy Wed Oct 27 13:54:18 2010 -0700
@@ -22,25 +22,25 @@
text {* Lemmas for proving nchotomy rule: *}
-lemma ex_one_defined_iff:
+lemma ex_one_bottom_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
by simp
-lemma ex_up_defined_iff:
+lemma ex_up_bottom_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
by (safe, case_tac x, auto)
-lemma ex_sprod_defined_iff:
+lemma ex_sprod_bottom_iff:
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
(\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
by (safe, case_tac y, auto)
-lemma ex_sprod_up_defined_iff:
+lemma ex_sprod_up_bottom_iff:
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
(\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
by (safe, case_tac y, simp, case_tac x, auto)
-lemma ex_ssum_defined_iff:
+lemma ex_ssum_bottom_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
(\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
@@ -49,12 +49,12 @@
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
by auto
-lemmas ex_defined_iffs =
- ex_ssum_defined_iff
- ex_sprod_up_defined_iff
- ex_sprod_defined_iff
- ex_up_defined_iff
- ex_one_defined_iff
+lemmas ex_bottom_iffs =
+ ex_ssum_bottom_iff
+ ex_sprod_up_bottom_iff
+ ex_sprod_bottom_iff
+ ex_up_bottom_iff
+ ex_one_bottom_iff
text {* Rules for turning nchotomy into exhaust: *}
@@ -78,14 +78,14 @@
lemmas con_strict_rules =
sinl_strict sinr_strict spair_strict1 spair_strict2
-lemmas con_defined_iff_rules =
- sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
+lemmas con_bottom_iff_rules =
+ sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
lemmas con_below_iff_rules =
- sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
+ sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
lemmas con_eq_iff_rules =
- sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
+ sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
lemmas sel_strict_rules =
cfcomp2 sscase1 sfst_strict ssnd_strict fup1
@@ -102,8 +102,8 @@
sel_strict_rules sel_app_extra_rules
ssnd_spair sfst_spair up_defined spair_defined
-lemmas sel_defined_iff_rules =
- cfcomp2 sfst_defined_iff ssnd_defined_iff
+lemmas sel_bottom_iff_rules =
+ cfcomp2 sfst_bottom_iff ssnd_bottom_iff
lemmas take_con_rules =
ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
--- a/src/HOLCF/Domain_Aux.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Domain_Aux.thy Wed Oct 27 13:54:18 2010 -0700
@@ -71,14 +71,14 @@
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
-lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (auto elim: abs_defin' intro: abs_strict)
-lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
- by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
+lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
+ by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
- by (simp add: rep_defined_iff)
+ by (simp add: rep_bottom_iff)
lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
proof (unfold compact_def)
--- a/src/HOLCF/Fix.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Fix.thy Wed Oct 27 13:54:18 2010 -0700
@@ -119,7 +119,7 @@
text {* strictness of @{term fix} *}
-lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
+lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
apply (rule iffI)
apply (erule subst)
apply (rule fix_eq [symmetric])
@@ -127,10 +127,10 @@
done
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
text {* @{term fix} applied to identity and constant functions *}
--- a/src/HOLCF/Lift.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Lift.thy Wed Oct 27 13:54:18 2010 -0700
@@ -114,7 +114,7 @@
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
by (erule lift_definedE, simp)
-lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
lemma FLIFT_mono:
--- a/src/HOLCF/LowerPD.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/LowerPD.thy Wed Oct 27 13:54:18 2010 -0700
@@ -229,10 +229,10 @@
using lower_unit_Rep_compact_basis [of compact_bot]
by (simp add: inst_lower_pd_pcpo)
-lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
-lemma lower_plus_strict_iff [simp]:
+lemma lower_plus_bottom_iff [simp]:
"xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
apply safe
apply (rule UU_I, erule subst, rule lower_plus_below1)
--- a/src/HOLCF/Pcpodef.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Pcpodef.thy Wed Oct 27 13:54:18 2010 -0700
@@ -235,7 +235,7 @@
apply (rule type_definition.Abs_inverse [OF type UU_in_A])
done
-theorem typedef_Abs_strict_iff:
+theorem typedef_Abs_bottom_iff:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
@@ -244,7 +244,7 @@
apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
done
-theorem typedef_Rep_strict_iff:
+theorem typedef_Rep_bottom_iff:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
@@ -258,14 +258,14 @@
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
+by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
theorem typedef_Rep_defined:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
+by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
subsection {* Proving a subtype is flat *}
--- a/src/HOLCF/Product_Cpo.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy Wed Oct 27 13:54:18 2010 -0700
@@ -173,7 +173,7 @@
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
by (rule minimal_cprod [THEN UU_I, symmetric])
-lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
unfolding inst_cprod_pcpo by simp
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
--- a/src/HOLCF/Sprod.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Sprod.thy Wed Oct 27 13:54:18 2010 -0700
@@ -80,7 +80,7 @@
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
by (simp add: Rep_sprod_simps)
-lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
+lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
by (simp add: Rep_sprod_simps strict_conv_if)
lemma spair_below_iff:
@@ -136,10 +136,10 @@
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
-lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
+lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
by (cases p, simp_all)
-lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
+lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
by (cases p, simp_all)
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
--- a/src/HOLCF/Ssum.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Ssum.thy Wed Oct 27 13:54:18 2010 -0700
@@ -98,10 +98,10 @@
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
by (simp add: Rep_ssum_simps)
-lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma sinl_bottom_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
using sinl_eq [of "x" "\<bottom>"] by simp
-lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma sinr_bottom_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
using sinr_eq [of "x" "\<bottom>"] by simp
lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Wed Oct 27 13:54:18 2010 -0700
@@ -210,7 +210,7 @@
in (n2, mk_ssumT (t1, t2)) end;
val ct = ctyp_of thy (snd (cons2typ 1 spec'));
val thm1 = instantiate' [SOME ct] [] @{thm exh_start};
- val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
+ val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1;
val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
val y = Free ("y", lhsT);
@@ -279,8 +279,8 @@
val lhs = mk_undef (list_ccomb (con, vs));
val rhss = map mk_undef nonlazy;
val goal = mk_trp (iff_disj (lhs, rhss));
- val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
- val rules = rule1 :: @{thms con_defined_iff_rules};
+ val rule1 = iso_locale RS @{thm iso.abs_bottom_iff};
+ val rules = rule1 :: @{thms con_bottom_iff_rules};
val tacs = [simp_tac (HOL_ss addsimps rules) 1];
in prove thy con_betas goal (K tacs) end;
in
@@ -506,7 +506,7 @@
val goal = Logic.list_implies (assms, concl);
val defs = case_beta :: con_betas;
val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
- val rules2 = @{thms con_defined_iff_rules};
+ val rules2 = @{thms con_bottom_iff_rules};
val rules3 = @{thms cfcomp2 one_case2};
val rules = abs_inverse :: rules1 @ rules2 @ rules3;
val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
@@ -528,7 +528,7 @@
(rep_const : term)
(abs_inv : thm)
(rep_strict : thm)
- (rep_strict_iff : thm)
+ (rep_bottom_iff : thm)
(con_betas : thm list)
(thy : theory)
: thm list * theory =
@@ -637,7 +637,7 @@
(* prove selector definedness rules *)
val sel_defins : thm list =
let
- val rules = rep_strict_iff :: @{thms sel_defined_iff_rules};
+ val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules};
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
fun sel_defin sel =
let
@@ -868,8 +868,8 @@
val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
val rep_strict = iso_locale RS @{thm iso.rep_strict};
val abs_strict = iso_locale RS @{thm iso.abs_strict};
- val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
- val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
+ val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff};
+ val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff};
val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
(* qualify constants and theorems with domain name *)
@@ -908,7 +908,7 @@
map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
in
add_selectors sel_spec rep_const
- abs_iso_thm rep_strict rep_defined_iff con_betas thy
+ abs_iso_thm rep_strict rep_bottom_iff con_betas thy
end;
(* define and prove theorems for discriminator functions *)
--- a/src/HOLCF/Tools/pcpodef.ML Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML Wed Oct 27 13:54:18 2010 -0700
@@ -11,7 +11,7 @@
{ below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
lub: thm, thelub: thm, compact: thm }
type pcpo_info =
- { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+ { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
Rep_defined: thm, Abs_defined: thm }
val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
@@ -48,7 +48,7 @@
lub: thm, thelub: thm, compact: thm }
type pcpo_info =
- { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+ { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
Rep_defined: thm, Abs_defined: thm }
(* building terms *)
@@ -136,8 +136,8 @@
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
val Rep_strict = make @{thm typedef_Rep_strict};
val Abs_strict = make @{thm typedef_Abs_strict};
- val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
- val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
+ val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
+ val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
val Rep_defined = make @{thm typedef_Rep_defined};
val Abs_defined = make @{thm typedef_Abs_defined};
val (_, thy) =
@@ -146,14 +146,14 @@
|> Global_Theory.add_thms
([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []),
((Binding.suffix_name "_strict" Abs_name, Abs_strict), []),
- ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
- ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
+ ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
+ ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
((Binding.suffix_name "_defined" Rep_name, Rep_defined), []),
((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])])
||> Sign.parent_path;
val pcpo_info =
{ Rep_strict = Rep_strict, Abs_strict = Abs_strict,
- Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
+ Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
Rep_defined = Rep_defined, Abs_defined = Abs_defined };
in
(pcpo_info, thy)
--- a/src/HOLCF/Tutorial/Domain_ex.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Tutorial/Domain_ex.thy Wed Oct 27 13:54:18 2010 -0700
@@ -116,8 +116,8 @@
domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
-lemmas tree_abs_defined_iff =
- iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
+lemmas tree_abs_bottom_iff =
+ iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
text {* Rules about ismorphism *}
term tree_rep
--- a/src/HOLCF/UpperPD.thy Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/UpperPD.thy Wed Oct 27 13:54:18 2010 -0700
@@ -233,10 +233,10 @@
lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
by (rule UU_I, rule upper_plus_below2)
-lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
-lemma upper_plus_strict_iff [simp]:
+lemma upper_plus_bottom_iff [simp]:
"xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
apply (rule iffI)
apply (erule rev_mp)