# HG changeset patch
# User wenzelm
# Date 1441047384 -7200
# Node ID 6cb92c2a5ece5ad3bd5c1384a35ace47d718cf82
# Parent  180a20d4ae539332e8bef02a82d16fa9d5ad9ce8
proper qualified naming;

diff -r 180a20d4ae53 -r 6cb92c2a5ece src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- 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
diff -r 180a20d4ae53 -r 6cb92c2a5ece src/HOL/Library/Mapping.thy
--- 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"
diff -r 180a20d4ae53 -r 6cb92c2a5ece src/HOL/Option.thy
--- 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>