proper qualified naming;
authorwenzelm
Mon Aug 31 20:56:24 2015 +0200 (2015-08-31)
changeset 610686cb92c2a5ece
parent 61067 180a20d4ae53
child 61069 aefe89038dd2
proper qualified naming;
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Library/Mapping.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Aug 31 20:55:22 2015 +0200
     1.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Aug 31 20:56:24 2015 +0200
     1.3 @@ -1608,14 +1608,14 @@
     1.4                (\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
     1.5        unfolding support_def by auto
     1.6      from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
     1.7 -      unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def these_def by force+
     1.8 +      unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def by force+
     1.9      moreover hence "finite (fg ` Field t - {rs.const})" using *
    1.10        unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
    1.11 -      by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff these_def)
    1.12 +      by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff Option.these_def)
    1.13      ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
    1.14        by (subst **) (auto intro!: finite_cartesian_product)
    1.15      with * show "?g \<in> FinFunc r (s *o t)"
    1.16 -      unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def these_def
    1.17 +      unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def
    1.18          support_def rs.zero_oexp[OF Field] by (auto elim!: finite_subset[rotated])
    1.19    qed
    1.20  qed
     2.1 --- a/src/HOL/Library/Mapping.thy	Mon Aug 31 20:55:22 2015 +0200
     2.2 +++ b/src/HOL/Library/Mapping.thy	Mon Aug 31 20:56:24 2015 +0200
     2.3 @@ -40,12 +40,12 @@
     2.4  
     2.5  lemma is_none_parametric [transfer_rule]:
     2.6    "(rel_option A ===> HOL.eq) Option.is_none Option.is_none"
     2.7 -  by (auto simp add: is_none_def rel_fun_def rel_option_iff split: option.split)
     2.8 +  by (auto simp add: Option.is_none_def rel_fun_def rel_option_iff split: option.split)
     2.9  
    2.10  lemma dom_parametric:
    2.11    assumes [transfer_rule]: "bi_total A"
    2.12    shows "((A ===> rel_option B) ===> rel_set A) dom dom" 
    2.13 -  unfolding dom_def [abs_def] is_none_def [symmetric] by transfer_prover
    2.14 +  unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
    2.15  
    2.16  lemma map_of_parametric [transfer_rule]:
    2.17    assumes [transfer_rule]: "bi_unique R1"
    2.18 @@ -223,7 +223,7 @@
    2.19  
    2.20  lemma keys_is_none_rep [code_unfold]:
    2.21    "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
    2.22 -  by transfer (auto simp add: is_none_def)
    2.23 +  by transfer (auto simp add: Option.is_none_def)
    2.24  
    2.25  lemma update_update:
    2.26    "update k v (update k w m) = update k v m"
     3.1 --- a/src/HOL/Option.thy	Mon Aug 31 20:55:22 2015 +0200
     3.2 +++ b/src/HOL/Option.thy	Mon Aug 31 20:56:24 2015 +0200
     3.3 @@ -118,7 +118,11 @@
     3.4      | _ \<Rightarrow> False)"
     3.5    by (auto split: prod.split option.split)
     3.6  
     3.7 -definition is_none :: "'a option \<Rightarrow> bool"
     3.8 +
     3.9 +context
    3.10 +begin
    3.11 +
    3.12 +qualified definition is_none :: "'a option \<Rightarrow> bool"
    3.13    where [code_post]: "is_none x \<longleftrightarrow> x = None"
    3.14  
    3.15  lemma is_none_simps [simp]:
    3.16 @@ -148,7 +152,7 @@
    3.17    by (auto simp add: is_none_def)
    3.18  
    3.19  
    3.20 -primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
    3.21 +qualified primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
    3.22  where
    3.23    bind_lzero: "bind None f = None"
    3.24  | bind_lunit: "bind (Some x) f = f x"
    3.25 @@ -165,7 +169,7 @@
    3.26  lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
    3.27    by (cases x) auto
    3.28  
    3.29 -lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
    3.30 +qualified lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
    3.31    by (cases x) auto
    3.32  
    3.33  lemma bind_split: "P (bind m f) \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m = Some v \<longrightarrow> P (f v))"
    3.34 @@ -192,10 +196,16 @@
    3.35  
    3.36  lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
    3.37    by simp
    3.38 +
    3.39 +end
    3.40 +
    3.41  setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
    3.42  
    3.43  
    3.44 -definition these :: "'a option set \<Rightarrow> 'a set"
    3.45 +context
    3.46 +begin
    3.47 +
    3.48 +qualified definition these :: "'a option set \<Rightarrow> 'a set"
    3.49    where "these A = the ` {x \<in> A. x \<noteq> None}"
    3.50  
    3.51  lemma these_empty [simp]: "these {} = {}"
    3.52 @@ -233,8 +243,7 @@
    3.53  lemma these_not_empty_eq: "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
    3.54    by (auto simp add: these_empty_eq)
    3.55  
    3.56 -hide_const (open) bind these
    3.57 -hide_fact (open) bind_cong
    3.58 +end
    3.59  
    3.60  
    3.61  subsection \<open>Transfer rules for the Transfer package\<close>
    3.62 @@ -251,7 +260,7 @@
    3.63  
    3.64  lemma pred_option_parametric [transfer_rule]:
    3.65    "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
    3.66 -  by (rule rel_funI)+ (auto simp add: rel_option_unfold is_none_def dest: rel_funD)
    3.67 +  by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)
    3.68  
    3.69  end
    3.70  
    3.71 @@ -269,11 +278,9 @@
    3.72  subsubsection \<open>Code generator setup\<close>
    3.73  
    3.74  lemma equal_None_code_unfold [code_unfold]:
    3.75 -  "HOL.equal x None \<longleftrightarrow> is_none x"
    3.76 -  "HOL.equal None = is_none"
    3.77 -  by (auto simp add: equal is_none_def)
    3.78 -
    3.79 -hide_const (open) is_none
    3.80 +  "HOL.equal x None \<longleftrightarrow> Option.is_none x"
    3.81 +  "HOL.equal None = Option.is_none"
    3.82 +  by (auto simp add: equal Option.is_none_def)
    3.83  
    3.84  code_printing
    3.85    type_constructor option \<rightharpoonup>