# HG changeset patch
# User blanchet
# Date 1392360826 -3600
# Node ID 786edc984c9841326132670aad16e9b5b884c913
# Parent  0d31c05462863dc5e047899576c7467d30e47aeb
merged 'Option.map' and 'Option.map_option'

diff -r 0d31c0546286 -r 786edc984c98 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -484,7 +484,7 @@
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
 @{const Option.the} & @{typeof Option.the}\\
-@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
+@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
 @{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
 @{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
 \end{tabular}
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Bali/Conform.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -97,7 +97,7 @@
 section "value conformance"
 
 definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
-  where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
+  where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. map_option obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
 
 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: conf_def)
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Bali/State.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -143,7 +143,7 @@
 definition
   fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
   "fields_table G C P =
-    Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
+    map_option type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
 
 lemma fields_table_SomeI: 
 "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
@@ -283,7 +283,7 @@
 subsection "initialization"
 
 abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
-  where "init_vals vs == Option.map default_val \<circ> vs"
+  where "init_vals vs == map_option default_val \<circ> vs"
 
 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
 apply (unfold arr_comps_def in_bounds_def)
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -1429,7 +1429,7 @@
             by (auto elim!: finite_subset[rotated])
           from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding underS_def by auto
           with f inj have neq: "?f h \<noteq> ?f g"
-            unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
+            unfolding fun_eq_iff inj_on_def rt.oexp_def map_option_case FinFunc_def Func_def Let_def
             by simp metis
           moreover
           with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -3589,4 +3589,3 @@
 *}
 
 end
-
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Fun_Def.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -146,7 +146,7 @@
 
 lemmas [fundef_cong] =
   if_cong image_cong INT_cong UN_cong
-  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
+  bex_cong ball_cong imp_cong map_option_cong Option.bind_cong
 
 lemma split_cong [fundef_cong]:
   "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/HOLCF/Library/Option_Cpo.thy
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -151,11 +151,11 @@
 
 text {* Continuity rule for map. *}
 
-lemma cont2cont_option_map [simp, cont2cont]:
+lemma cont2cont_map_option [simp, cont2cont]:
   assumes f: "cont (\<lambda>(x, y). f x y)"
   assumes g: "cont (\<lambda>x. g x)"
-  shows "cont (\<lambda>x. Option.map (\<lambda>y. f x y) (g x))"
-using assms by (simp add: prod_cont_iff Option.map_def)
+  shows "cont (\<lambda>x. map_option (\<lambda>y. f x y) (g x))"
+using assms by (simp add: prod_cont_iff map_option_case)
 
 subsection {* Compactness and chain-finiteness *}
 
@@ -262,10 +262,10 @@
 by (rule liftdefl_option_def)
 
 abbreviation option_map
-  where "option_map f \<equiv> Abs_cfun (Option.map (Rep_cfun f))"
+  where "option_map f \<equiv> Abs_cfun (map_option (Rep_cfun f))"
 
 lemma option_map_ID [domain_map_ID]: "option_map ID = ID"
-by (simp add: ID_def cfun_eq_iff Option.map.identity id_def)
+by (simp add: ID_def cfun_eq_iff option.map_id[unfolded id_def] id_def)
 
 lemma deflation_option_map [domain_deflation]:
   "deflation d \<Longrightarrow> deflation (option_map d)"
@@ -275,7 +275,7 @@
 done
 
 lemma encode_option_option_map:
-  "encode_option\<cdot>(Option.map (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
+  "encode_option\<cdot>(map_option (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
 by (induct x, simp_all add: decode_option_def encode_option_def)
 
 lemma isodefl_option [domain_isodefl]:
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -19,8 +19,8 @@
 
 definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
 
-definition "show_acom = map_acom (Option.map show_st)"
-definition "show_acom_opt = Option.map show_acom"
+definition "show_acom = map_acom (map_option show_st)"
+definition "show_acom_opt = map_option show_acom"
 
 definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
 
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -33,8 +33,8 @@
 definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
 "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
 
-definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
-definition "show_acom_opt = Option.map show_acom"
+definition "show_acom C = map_acom (map_option (show_st (vars(strip C)))) C"
+definition "show_acom_opt = map_option show_acom"
 
 lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
 by transfer auto
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -252,7 +252,7 @@
   "length ([] :: 'A list) = id 0 \<and> (\<forall>(h\<Colon>'A) t. length (h # t) = Suc (length t))"
   by simp
 
-lemma MAP[import_const MAP : List.map]:
+lemma MAP[import_const MAP : List.list.map]:
   "(\<forall>f\<Colon>'A \<Rightarrow> 'B. map f [] = []) \<and>
        (\<forall>(f\<Colon>'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
   by simp
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Lazy_Sequence.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -140,7 +140,7 @@
 
 lemma map_code [code]:
   "map f xq =
-    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
+    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
 
 definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
@@ -167,7 +167,7 @@
 
 definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
 where
-  "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
+  "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
   
 function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
 where
@@ -301,21 +301,21 @@
 
 definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
 where
-  "hb_map f xq = map (Option.map f) xq"
+  "hb_map f xq = map (map_option f) xq"
 
 lemma hb_map_code [code]:
   "hb_map f xq =
-    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
-  using map_code [of "Option.map f" xq] by (simp add: hb_map_def)
+    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
+  using map_code [of "map_option f" xq] by (simp add: hb_map_def)
 
 definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
 where
   "hb_flat xqq = lazy_sequence_of_list (concat
-    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
+    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
 
 lemma list_of_lazy_sequence_hb_flat [simp]:
   "list_of_lazy_sequence (hb_flat xqq) =
-    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
+    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
   by (simp add: hb_flat_def)
 
 lemma hb_flat_code [code]:
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/AList.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -399,7 +399,7 @@
   by (simp add: map_ran_def image_image split_def)
   
 lemma map_ran_conv:
-  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
+  "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
   by (induct al) auto
 
 lemma distinct_map_ran:
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -68,9 +68,9 @@
   "sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))"
   "sub Num.One (Num.Bit0 n) = None"
   "sub Num.One (Num.Bit1 n) = None"
-  "sub (Num.Bit0 m) (Num.Bit0 n) = Option.map dup (sub m n)"
-  "sub (Num.Bit1 m) (Num.Bit1 n) = Option.map dup (sub m n)"
-  "sub (Num.Bit1 m) (Num.Bit0 n) = Option.map (\<lambda>q. dup q + 1) (sub m n)"
+  "sub (Num.Bit0 m) (Num.Bit0 n) = map_option dup (sub m n)"
+  "sub (Num.Bit1 m) (Num.Bit1 n) = map_option dup (sub m n)"
+  "sub (Num.Bit1 m) (Num.Bit0 n) = map_option (\<lambda>q. dup q + 1) (sub m n)"
   "sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
      | Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
   apply (auto simp add: nat_of_num_numeral
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -65,7 +65,7 @@
 
 lemma map_transfer: 
   "((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) 
-    (\<lambda>f g m. (Option.map g \<circ> m \<circ> f)) (\<lambda>f g m. (Option.map g \<circ> m \<circ> f))"
+    (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
 by transfer_prover
 
 lemma map_entry_transfer:
@@ -105,13 +105,13 @@
   "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_transfer .
 
 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
-  "\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" parametric map_transfer .
+  "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_transfer .
 
 
 subsection {* Functorial structure *}
 
 enriched_type map: map
-  by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
+  by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
 
 
 subsection {* Derived operations *}
@@ -367,5 +367,3 @@
   replace default map_entry map_default tabulate bulkload map of_alist
 
 end
-
-
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -11,20 +11,16 @@
 subsection {* Rules for the Quotient package *}
 
 lemma option_rel_map1:
-  "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
+  "option_rel R (map_option f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
   by (simp add: option_rel_def split: option.split)
 
 lemma option_rel_map2:
-  "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
+  "option_rel R x (map_option f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
   by (simp add: option_rel_def split: option.split)
 
-lemma option_map_id [id_simps]:
-  "Option.map id = id"
-  by (simp add: id_def Option.map.identity fun_eq_iff)
-
-lemma option_rel_eq [id_simps]:
-  "option_rel (op =) = (op =)"
-  by (simp add: option_rel_def fun_eq_iff split: option.split)
+declare
+  map_option.id [id_simps]
+  option_rel_eq [id_simps]
 
 lemma option_symp:
   "symp R \<Longrightarrow> symp (option_rel R)"
@@ -40,9 +36,9 @@
 
 lemma option_quotient [quot_thm]:
   assumes "Quotient3 R Abs Rep"
-  shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
+  shows "Quotient3 (option_rel R) (map_option Abs) (map_option Rep)"
   apply (rule Quotient3I)
-  apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
+  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
   using Quotient3_rel [OF assms]
   apply (simp add: option_rel_def split: option.split)
   done
@@ -61,12 +57,12 @@
 
 lemma option_None_prs [quot_preserve]:
   assumes q: "Quotient3 R Abs Rep"
-  shows "Option.map Abs None = None"
+  shows "map_option Abs None = None"
   by simp
 
 lemma option_Some_prs [quot_preserve]:
   assumes q: "Quotient3 R Abs Rep"
-  shows "(Rep ---> Option.map Abs) Some = Some"
+  shows "(Rep ---> map_option Abs) Some = Some"
   apply(simp add: fun_eq_iff)
   apply(simp add: Quotient3_abs_rep[OF q])
   done
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -127,11 +127,11 @@
   by transfer (rule rbt_lookup_rbt_bulkload)
 
 lemma lookup_map_entry [simp]:
-  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
+  "lookup (map_entry k f t) = (lookup t)(k := map_option f (lookup t k))"
   by transfer (rule rbt_lookup_rbt_map_entry)
 
 lemma lookup_map [simp]:
-  "lookup (map f t) k = Option.map (f k) (lookup t k)"
+  "lookup (map f t) k = map_option (f k) (lookup t k)"
   by transfer (rule rbt_lookup_map)
 
 lemma fold_fold:
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -1025,7 +1025,7 @@
 end
 
 theorem (in linorder) rbt_lookup_rbt_map_entry:
-  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := Option.map f (rbt_lookup t k))"
+  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := map_option f (rbt_lookup t k))"
   by (induct t) (auto split: option.splits simp add: fun_eq_iff)
 
 subsection {* Mapping all entries *}
@@ -1053,7 +1053,7 @@
 
 end
 
-theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = Option.map (f x) (rbt_lookup t x)"
+theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
   apply(induct t)
   apply auto
   apply(subgoal_tac "x = a")
@@ -1855,9 +1855,9 @@
 lemma map_of_sinter_with:
   "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   \<Longrightarrow> map_of (sinter_with f xs ys) k = 
-  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> Option.map (f k v) (map_of ys k))"
+  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> map_option (f k v) (map_of ys k))"
 apply(induct f xs ys rule: sinter_with.induct)
-apply(auto simp add: sorted_Cons Option.map_def split: option.splits dest: map_of_SomeD bspec)
+apply(auto simp add: sorted_Cons map_option_case split: option.splits dest: map_of_SomeD bspec)
 done
 
 end
@@ -1866,11 +1866,11 @@
 by(induct xs)(auto 4 3 simp add: map_add_def intro!: ext split: option.split intro: rev_image_eqI)
 
 lemma map_map_filter: 
-  "map f (List.map_filter g xs) = List.map_filter (Option.map f \<circ> g) xs"
+  "map f (List.map_filter g xs) = List.map_filter (map_option f \<circ> g) xs"
 by(auto simp add: List.map_filter_def)
 
-lemma map_filter_option_map_const: 
-  "List.map_filter (\<lambda>x. Option.map (\<lambda>y. f x) (g (f x))) xs = filter (\<lambda>x. g x \<noteq> None) (map f xs)"
+lemma map_filter_map_option_const: 
+  "List.map_filter (\<lambda>x. map_option (\<lambda>y. f x) (g (f x))) xs = filter (\<lambda>x. g x \<noteq> None) (map f xs)"
 by(auto simp add: map_filter_def filter_map o_def)
 
 lemma set_map_filter: "set (List.map_filter P xs) = the ` (P ` set xs - {None})"
@@ -1897,8 +1897,8 @@
   "rbt_inter_with_key f t1 t2 =
   (case RBT_Impl.compare_height t1 t1 t2 t2 
    of compare.EQ \<Rightarrow> rbtreeify (sinter_with f (entries t1) (entries t2))
-    | compare.LT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). Option.map (\<lambda>w. (k, f k v w)) (rbt_lookup t2 k)) (entries t1))
-    | compare.GT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). Option.map (\<lambda>w. (k, f k w v)) (rbt_lookup t1 k)) (entries t2)))"
+    | compare.LT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). map_option (\<lambda>w. (k, f k v w)) (rbt_lookup t2 k)) (entries t1))
+    | compare.GT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). map_option (\<lambda>w. (k, f k w v)) (rbt_lookup t1 k)) (entries t2)))"
 
 definition rbt_inter_with where
   "rbt_inter_with f = rbt_inter_with_key (\<lambda>_. f)"
@@ -1971,7 +1971,7 @@
 
 lemma rbt_interwk_is_rbt [simp]:
   "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with_key f t1 t2)"
-by(auto simp add: rbt_inter_with_key_def Let_def map_map_filter split_def o_def option_map_comp map_filter_option_map_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries intro: is_rbt_rbtreeify split: compare.split)
+by(auto simp add: rbt_inter_with_key_def Let_def map_map_filter split_def o_def option.map_comp map_filter_map_option_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries intro: is_rbt_rbtreeify split: compare.split)
 
 lemma rbt_interw_is_rbt:
   "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with f t1 t2)"
@@ -1987,7 +1987,7 @@
   (case rbt_lookup t1 k of None \<Rightarrow> None 
    | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> None
                | Some w \<Rightarrow> Some (f k v w))"
-by(auto 4 3 simp add: rbt_inter_with_key_def Let_def map_of_entries[symmetric] rbt_lookup_rbtreeify map_map_filter split_def o_def option_map_comp map_filter_option_map_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries map_of_sinter_with map_of_eq_None_iff set_map_filter split: option.split compare.split intro: rev_image_eqI dest: rbt_sorted_entries_right_unique)
+by(auto 4 3 simp add: rbt_inter_with_key_def Let_def map_of_entries[symmetric] rbt_lookup_rbtreeify map_map_filter split_def o_def option.map_comp map_filter_map_option_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries map_of_sinter_with map_of_eq_None_iff set_map_filter split: option.split compare.split intro: rev_image_eqI dest: rbt_sorted_entries_right_unique)
 
 lemma rbt_lookup_rbt_inter:
   "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -85,7 +85,7 @@
 assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
 assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
 assumes Initial: "P s"
-shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
+shows "map_option f (while_option b c s) = while_option b' c' (f s)"
 unfolding while_option_def
 proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
   fix k
@@ -188,7 +188,7 @@
 
 lemma while_option_commute:
   assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
-  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
+  shows "map_option f (while_option b c s) = while_option b' c' (f s)"
 by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
   (auto simp add: assms)
 
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Lifting_Option.thy
--- a/src/HOL/Lifting_Option.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -83,8 +83,8 @@
 
 lemma Quotient_option[quot_map]:
   assumes "Quotient R Abs Rep T"
-  shows "Quotient (option_rel R) (Option.map Abs)
-    (Option.map Rep) (option_rel T)"
+  shows "Quotient (option_rel R) (map_option Abs)
+    (map_option Rep) (option_rel T)"
   using assms unfolding Quotient_alt_def option_rel_def
   by (simp split: option.split)
 
@@ -104,9 +104,9 @@
   "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
   unfolding fun_rel_def split_option_all by simp
 
-lemma option_map_transfer [transfer_rule]:
-  "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
-  unfolding Option.map_def by transfer_prover
+lemma map_option_transfer [transfer_rule]:
+  "((A ===> B) ===> option_rel A ===> option_rel B) map_option map_option"
+  unfolding map_option_case[abs_def] by transfer_prover
 
 lemma option_bind_transfer [transfer_rule]:
   "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Limited_Sequence.thy
--- a/src/HOL/Limited_Sequence.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Limited_Sequence.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -27,11 +27,11 @@
 where
   "yield f i pol = (case eval f i pol of
     None \<Rightarrow> None
-  | Some s \<Rightarrow> (Option.map \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
+  | Some s \<Rightarrow> (map_option \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
 
 definition map_seq :: "('a \<Rightarrow> 'b dseq) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b dseq"
 where
-  "map_seq f xq i pol = Option.map Lazy_Sequence.flat
+  "map_seq f xq i pol = map_option Lazy_Sequence.flat
     (Lazy_Sequence.those (Lazy_Sequence.map (\<lambda>x. f x i pol) xq))"
 
 lemma map_seq_code [code]:
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -182,7 +182,7 @@
 "those [] = Some []" |
 "those (x # xs) = (case x of
   None \<Rightarrow> None
-| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
+| Some y \<Rightarrow> map_option (Cons y) (those xs))"
 
 primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "remove1 x [] = []" |
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Map.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -242,21 +242,21 @@
 by (induct xs) auto
 
 lemma map_of_map:
-  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
+  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
   by (induct xs) (auto simp add: fun_eq_iff)
 
-lemma dom_option_map:
-  "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
+lemma dom_map_option:
+  "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
   by (simp add: dom_def)
 
 
-subsection {* @{const Option.map} related *}
+subsection {* @{const map_option} related *}
 
-lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
+lemma map_option_o_empty [simp]: "map_option f o empty = empty"
 by (rule ext) simp
 
-lemma option_map_o_map_upd [simp]:
-  "Option.map f o m(a|->b) = (Option.map f o m)(a|->f b)"
+lemma map_option_o_map_upd [simp]:
+  "map_option f o m(a|->b) = (map_option f o m)(a|->f b)"
 by (rule ext) simp
 
 
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -95,7 +95,7 @@
        (xcpt_names (i,G,pc,et))"
 
 definition norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option" where
-  "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))"
+  "norm_eff i G == map_option (\<lambda>s. eff' (i,G,s))"
 
 definition eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type" where
   "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -119,11 +119,11 @@
 by (induct xs,auto)
 
 lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow>
-  map_of (map f xs) a = Option.map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
+  map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
 by (induct xs, auto)
 
-lemma option_map_of [simp]: "(Option.map f (map_of xs k) = None) = ((map_of xs k) = None)"
-by (simp add: Option.map_def split: option.split)
+lemma map_option_map_of [simp]: "(map_option f (map_of xs k) = None) = ((map_of xs k) = None)"
+by (simp add: map_option_case split: option.split)
 
 
 
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -551,7 +551,7 @@
 
 lemma match_xctable_offset: "
   (match_exception_table G cn (pc + n) (offset_xctable n et)) =
-  (Option.map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
+  (map_option (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
 apply (induct et)
 apply (simp add: offset_xctable_def)+
 apply (case_tac "match_exception_entry G cn pc a")
@@ -672,7 +672,7 @@
         in app_jumps_lem)
   apply (simp add: nth_append)+
     (* subgoal \<exists> st. mt ! pc'' = Some st *)
-  apply (simp add: norm_eff_def Option.map_def nth_append)
+  apply (simp add: norm_eff_def map_option_case nth_append)
   apply (case_tac "mt ! pc''")
 apply simp+
 done
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -273,13 +273,13 @@
   "mtd_mb == snd o snd"
 
 lemma map_of_map:
-  "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = Option.map f (map_of xs k)"
+  "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = map_option f (map_of xs k)"
   by (simp add: map_of_map)
 
 lemma map_of_map_fst: "\<lbrakk> inj f;
   \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
   \<Longrightarrow>  map_of (map g xs) k 
-  = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
+  = map_option (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
 apply (induct xs)
 apply simp
 apply simp
@@ -295,13 +295,13 @@
 
 lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   ((method (comp G, C) S) = 
-  Option.map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
+  map_option (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
              (method (G, C) S))"
 apply (simp add: method_def)
 apply (frule wf_subcls1)
 apply (simp add: comp_class_rec)
 apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
-apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
+apply (rule_tac R="%x y. ((x S) = (map_option (\<lambda>(D, rT, b). 
   (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   in class_rec_relation)
 apply assumption
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/DFA/Opt.thy
--- a/src/HOL/MicroJava/DFA/Opt.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Opt.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -282,8 +282,8 @@
 
 lemma option_map_in_optionI:
   "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
-  \<Longrightarrow> Option.map f ox : opt S";
-apply (unfold Option.map_def)
+  \<Longrightarrow> map_option f ox : opt S";
+apply (unfold map_option_case)
 apply (simp split: option.split)
 apply blast
 done 
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -14,7 +14,7 @@
 
 definition conf :: "'c prog => aheap => val => ty => bool" 
                                    ("_,_ |- _ ::<= _"  [51,51,51,51] 50) where
- "G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
+ "G,h|-v::<=T == \<exists>T'. typeof (map_option obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
 
 definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
                                    ("_,_ |- _ [::<=] _" [51,51,51,51] 50) where
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/NanoJava/State.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -28,7 +28,7 @@
   (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"
 
 definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
- "init_vars m == Option.map (\<lambda>T. Null) o m"
+ "init_vars m == map_option (\<lambda>T. Null) o m"
   
 text {* private: *}
 type_synonym heap = "loc   \<rightharpoonup> obj"
diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -80,53 +80,43 @@
 lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
   by (cases xo) auto
 
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option" where
-  "map = (%f y. case y of None => None | Some x => Some (f x))"
-
-lemma option_map_None [simp, code]: "map f None = None"
-  by (simp add: map_def)
+lemma map_option_case: "map_option f y = (case y of None => None | Some x => Some (f x))"
+  by (auto split: option.split)
 
-lemma option_map_Some [simp, code]: "map f (Some x) = Some (f x)"
-  by (simp add: map_def)
-
-lemma option_map_is_None [iff]:
-    "(map f opt = None) = (opt = None)"
-  by (simp add: map_def split add: option.split)
+lemma map_option_is_None [iff]:
+    "(map_option f opt = None) = (opt = None)"
+  by (simp add: map_option_case split add: option.split)
 
-lemma option_map_eq_Some [iff]:
-    "(map f xo = Some y) = (EX z. xo = Some z & f z = y)"
-  by (simp add: map_def split add: option.split)
+lemma map_option_eq_Some [iff]:
+    "(map_option f xo = Some y) = (EX z. xo = Some z & f z = y)"
+  by (simp add: map_option_case split add: option.split)
 
-lemma option_map_comp:
-    "map f (map g opt) = map (f o g) opt"
-  by (simp add: map_def split add: option.split)
+lemma map_option_o_case_sum [simp]:
+    "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
+  by (rule o_case_sum)
 
-lemma option_map_o_case_sum [simp]:
-    "map f o case_sum g h = case_sum (map f o g) (map f o h)"
-  by (rule ext) (simp split: sum.split)
-
-lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y"
+lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
 by (cases x) auto
 
-enriched_type map: Option.map proof -
+enriched_type map_option: map_option proof -
   fix f g
-  show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
+  show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
   proof
     fix x
-    show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
+    show "(map_option f \<circ> map_option g) x= map_option (f \<circ> g) x"
       by (cases x) simp_all
   qed
 next
-  show "Option.map id = id"
+  show "map_option id = id"
   proof
     fix x
-    show "Option.map id x = id x"
+    show "map_option id x = id x"
       by (cases x) simp_all
   qed
 qed
 
-lemma case_option_map [simp]:
-  "case_option g h (Option.map f x) = case_option g (h \<circ> f) x"
+lemma case_map_option [simp]:
+  "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
   by (cases x) simp_all
 
 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
@@ -192,8 +182,8 @@
   "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
   by (auto simp add: these_empty_eq)
 
-hide_const (open) set map bind these
-hide_fact (open) map_cong bind_cong
+hide_const (open) set bind these
+hide_fact (open) bind_cong
 
 
 subsubsection {* Interaction with finite sets *}