--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Mon Aug 31 20:55:22 2015 +0200
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Mon Aug 31 20:56:24 2015 +0200
@@ -1608,14 +1608,14 @@
(\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
unfolding support_def by auto
from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
- unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def these_def by force+
+ unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def by force+
moreover hence "finite (fg ` Field t - {rs.const})" using *
unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
- by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff these_def)
+ by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff Option.these_def)
ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
by (subst **) (auto intro!: finite_cartesian_product)
with * show "?g \<in> FinFunc r (s *o t)"
- unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def these_def
+ unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def
support_def rs.zero_oexp[OF Field] by (auto elim!: finite_subset[rotated])
qed
qed
--- a/src/HOL/Library/Mapping.thy Mon Aug 31 20:55:22 2015 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Aug 31 20:56:24 2015 +0200
@@ -40,12 +40,12 @@
lemma is_none_parametric [transfer_rule]:
"(rel_option A ===> HOL.eq) Option.is_none Option.is_none"
- by (auto simp add: is_none_def rel_fun_def rel_option_iff split: option.split)
+ by (auto simp add: Option.is_none_def rel_fun_def rel_option_iff split: option.split)
lemma dom_parametric:
assumes [transfer_rule]: "bi_total A"
shows "((A ===> rel_option B) ===> rel_set A) dom dom"
- unfolding dom_def [abs_def] is_none_def [symmetric] by transfer_prover
+ unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
lemma map_of_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_unique R1"
@@ -223,7 +223,7 @@
lemma keys_is_none_rep [code_unfold]:
"k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
- by transfer (auto simp add: is_none_def)
+ by transfer (auto simp add: Option.is_none_def)
lemma update_update:
"update k v (update k w m) = update k v m"
--- a/src/HOL/Option.thy Mon Aug 31 20:55:22 2015 +0200
+++ b/src/HOL/Option.thy Mon Aug 31 20:56:24 2015 +0200
@@ -118,7 +118,11 @@
| _ \<Rightarrow> False)"
by (auto split: prod.split option.split)
-definition is_none :: "'a option \<Rightarrow> bool"
+
+context
+begin
+
+qualified definition is_none :: "'a option \<Rightarrow> bool"
where [code_post]: "is_none x \<longleftrightarrow> x = None"
lemma is_none_simps [simp]:
@@ -148,7 +152,7 @@
by (auto simp add: is_none_def)
-primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
+qualified primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
where
bind_lzero: "bind None f = None"
| bind_lunit: "bind (Some x) f = f x"
@@ -165,7 +169,7 @@
lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
by (cases x) auto
-lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
+qualified lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
by (cases x) auto
lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))"
@@ -192,10 +196,16 @@
lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
by simp
+
+end
+
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
-definition these :: "'a option set \<Rightarrow> 'a set"
+context
+begin
+
+qualified definition these :: "'a option set \<Rightarrow> 'a set"
where "these A = the ` {x \<in> A. x \<noteq> None}"
lemma these_empty [simp]: "these {} = {}"
@@ -233,8 +243,7 @@
lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
by (auto simp add: these_empty_eq)
-hide_const (open) bind these
-hide_fact (open) bind_cong
+end
subsection \<open>Transfer rules for the Transfer package\<close>
@@ -251,7 +260,7 @@
lemma pred_option_parametric [transfer_rule]:
"((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
- by (rule rel_funI)+ (auto simp add: rel_option_unfold is_none_def dest: rel_funD)
+ by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)
end
@@ -269,11 +278,9 @@
subsubsection \<open>Code generator setup\<close>
lemma equal_None_code_unfold [code_unfold]:
- "HOL.equal x None \<longleftrightarrow> is_none x"
- "HOL.equal None = is_none"
- by (auto simp add: equal is_none_def)
-
-hide_const (open) is_none
+ "HOL.equal x None \<longleftrightarrow> Option.is_none x"
+ "HOL.equal None = Option.is_none"
+ by (auto simp add: equal Option.is_none_def)
code_printing
type_constructor option \<rightharpoonup>