merged 'Option.map' and 'Option.map_option'
authorblanchet
Fri Feb 14 07:53:46 2014 +0100 (2014-02-14)
changeset 55466786edc984c98
parent 55465 0d31c0546286
child 55467 a5c9002bc54d
merged 'Option.map' and 'Option.map_option'
src/Doc/Main/Main_Doc.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/State.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Fun_Def.thy
src/HOL/HOLCF/Library/Option_Cpo.thy
src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy
src/HOL/IMP/Abs_State.thy
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/AList.thy
src/HOL/Library/Code_Binary_Nat.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Lifting_Option.thy
src/HOL/Limited_Sequence.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/Comp/AuxLemmas.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/DFA/Opt.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/NanoJava/State.thy
src/HOL/Option.thy
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -484,7 +484,7 @@
     1.4  
     1.5  \begin{tabular}{@ {} l @ {~::~} l @ {}}
     1.6  @{const Option.the} & @{typeof Option.the}\\
     1.7 -@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
     1.8 +@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
     1.9  @{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
    1.10  @{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
    1.11  \end{tabular}
     2.1 --- a/src/HOL/Bali/Conform.thy	Fri Feb 14 07:53:45 2014 +0100
     2.2 +++ b/src/HOL/Bali/Conform.thy	Fri Feb 14 07:53:46 2014 +0100
     2.3 @@ -97,7 +97,7 @@
     2.4  section "value conformance"
     2.5  
     2.6  definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
     2.7 -  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)"
     2.8 +  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)"
     2.9  
    2.10  lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
    2.11  by (auto simp: conf_def)
     3.1 --- a/src/HOL/Bali/State.thy	Fri Feb 14 07:53:45 2014 +0100
     3.2 +++ b/src/HOL/Bali/State.thy	Fri Feb 14 07:53:46 2014 +0100
     3.3 @@ -143,7 +143,7 @@
     3.4  definition
     3.5    fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
     3.6    "fields_table G C P =
     3.7 -    Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
     3.8 +    map_option type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
     3.9  
    3.10  lemma fields_table_SomeI: 
    3.11  "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
    3.12 @@ -283,7 +283,7 @@
    3.13  subsection "initialization"
    3.14  
    3.15  abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
    3.16 -  where "init_vals vs == Option.map default_val \<circ> vs"
    3.17 +  where "init_vals vs == map_option default_val \<circ> vs"
    3.18  
    3.19  lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
    3.20  apply (unfold arr_comps_def in_bounds_def)
     4.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Feb 14 07:53:45 2014 +0100
     4.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Feb 14 07:53:46 2014 +0100
     4.3 @@ -1429,7 +1429,7 @@
     4.4              by (auto elim!: finite_subset[rotated])
     4.5            from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding underS_def by auto
     4.6            with f inj have neq: "?f h \<noteq> ?f g"
     4.7 -            unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
     4.8 +            unfolding fun_eq_iff inj_on_def rt.oexp_def map_option_case FinFunc_def Func_def Let_def
     4.9              by simp metis
    4.10            moreover
    4.11            with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
     5.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Feb 14 07:53:45 2014 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Feb 14 07:53:46 2014 +0100
     5.3 @@ -3589,4 +3589,3 @@
     5.4  *}
     5.5  
     5.6  end
     5.7 -
     6.1 --- a/src/HOL/Fun_Def.thy	Fri Feb 14 07:53:45 2014 +0100
     6.2 +++ b/src/HOL/Fun_Def.thy	Fri Feb 14 07:53:46 2014 +0100
     6.3 @@ -146,7 +146,7 @@
     6.4  
     6.5  lemmas [fundef_cong] =
     6.6    if_cong image_cong INT_cong UN_cong
     6.7 -  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
     6.8 +  bex_cong ball_cong imp_cong map_option_cong Option.bind_cong
     6.9  
    6.10  lemma split_cong [fundef_cong]:
    6.11    "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
     7.1 --- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Fri Feb 14 07:53:45 2014 +0100
     7.2 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Fri Feb 14 07:53:46 2014 +0100
     7.3 @@ -151,11 +151,11 @@
     7.4  
     7.5  text {* Continuity rule for map. *}
     7.6  
     7.7 -lemma cont2cont_option_map [simp, cont2cont]:
     7.8 +lemma cont2cont_map_option [simp, cont2cont]:
     7.9    assumes f: "cont (\<lambda>(x, y). f x y)"
    7.10    assumes g: "cont (\<lambda>x. g x)"
    7.11 -  shows "cont (\<lambda>x. Option.map (\<lambda>y. f x y) (g x))"
    7.12 -using assms by (simp add: prod_cont_iff Option.map_def)
    7.13 +  shows "cont (\<lambda>x. map_option (\<lambda>y. f x y) (g x))"
    7.14 +using assms by (simp add: prod_cont_iff map_option_case)
    7.15  
    7.16  subsection {* Compactness and chain-finiteness *}
    7.17  
    7.18 @@ -262,10 +262,10 @@
    7.19  by (rule liftdefl_option_def)
    7.20  
    7.21  abbreviation option_map
    7.22 -  where "option_map f \<equiv> Abs_cfun (Option.map (Rep_cfun f))"
    7.23 +  where "option_map f \<equiv> Abs_cfun (map_option (Rep_cfun f))"
    7.24  
    7.25  lemma option_map_ID [domain_map_ID]: "option_map ID = ID"
    7.26 -by (simp add: ID_def cfun_eq_iff Option.map.identity id_def)
    7.27 +by (simp add: ID_def cfun_eq_iff option.map_id[unfolded id_def] id_def)
    7.28  
    7.29  lemma deflation_option_map [domain_deflation]:
    7.30    "deflation d \<Longrightarrow> deflation (option_map d)"
    7.31 @@ -275,7 +275,7 @@
    7.32  done
    7.33  
    7.34  lemma encode_option_option_map:
    7.35 -  "encode_option\<cdot>(Option.map (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
    7.36 +  "encode_option\<cdot>(map_option (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
    7.37  by (induct x, simp_all add: decode_option_def encode_option_def)
    7.38  
    7.39  lemma isodefl_option [domain_isodefl]:
     8.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Fri Feb 14 07:53:45 2014 +0100
     8.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Fri Feb 14 07:53:46 2014 +0100
     8.3 @@ -19,8 +19,8 @@
     8.4  
     8.5  definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
     8.6  
     8.7 -definition "show_acom = map_acom (Option.map show_st)"
     8.8 -definition "show_acom_opt = Option.map show_acom"
     8.9 +definition "show_acom = map_acom (map_option show_st)"
    8.10 +definition "show_acom_opt = map_option show_acom"
    8.11  
    8.12  definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
    8.13  
     9.1 --- a/src/HOL/IMP/Abs_State.thy	Fri Feb 14 07:53:45 2014 +0100
     9.2 +++ b/src/HOL/IMP/Abs_State.thy	Fri Feb 14 07:53:46 2014 +0100
     9.3 @@ -33,8 +33,8 @@
     9.4  definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
     9.5  "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
     9.6  
     9.7 -definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
     9.8 -definition "show_acom_opt = Option.map show_acom"
     9.9 +definition "show_acom C = map_acom (map_option (show_st (vars(strip C)))) C"
    9.10 +definition "show_acom_opt = map_option show_acom"
    9.11  
    9.12  lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    9.13  by transfer auto
    10.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Fri Feb 14 07:53:45 2014 +0100
    10.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Fri Feb 14 07:53:46 2014 +0100
    10.3 @@ -252,7 +252,7 @@
    10.4    "length ([] :: 'A list) = id 0 \<and> (\<forall>(h\<Colon>'A) t. length (h # t) = Suc (length t))"
    10.5    by simp
    10.6  
    10.7 -lemma MAP[import_const MAP : List.map]:
    10.8 +lemma MAP[import_const MAP : List.list.map]:
    10.9    "(\<forall>f\<Colon>'A \<Rightarrow> 'B. map f [] = []) \<and>
   10.10         (\<forall>(f\<Colon>'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
   10.11    by simp
    11.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Feb 14 07:53:45 2014 +0100
    11.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Feb 14 07:53:46 2014 +0100
    11.3 @@ -140,7 +140,7 @@
    11.4  
    11.5  lemma map_code [code]:
    11.6    "map f xq =
    11.7 -    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
    11.8 +    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
    11.9    by (simp_all add: lazy_sequence_eq_iff split: list.splits)
   11.10  
   11.11  definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
   11.12 @@ -167,7 +167,7 @@
   11.13  
   11.14  definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
   11.15  where
   11.16 -  "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
   11.17 +  "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
   11.18    
   11.19  function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
   11.20  where
   11.21 @@ -301,21 +301,21 @@
   11.22  
   11.23  definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
   11.24  where
   11.25 -  "hb_map f xq = map (Option.map f) xq"
   11.26 +  "hb_map f xq = map (map_option f) xq"
   11.27  
   11.28  lemma hb_map_code [code]:
   11.29    "hb_map f xq =
   11.30 -    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
   11.31 -  using map_code [of "Option.map f" xq] by (simp add: hb_map_def)
   11.32 +    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
   11.33 +  using map_code [of "map_option f" xq] by (simp add: hb_map_def)
   11.34  
   11.35  definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
   11.36  where
   11.37    "hb_flat xqq = lazy_sequence_of_list (concat
   11.38 -    (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)))"
   11.39 +    (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)))"
   11.40  
   11.41  lemma list_of_lazy_sequence_hb_flat [simp]:
   11.42    "list_of_lazy_sequence (hb_flat xqq) =
   11.43 -    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))"
   11.44 +    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))"
   11.45    by (simp add: hb_flat_def)
   11.46  
   11.47  lemma hb_flat_code [code]:
    12.1 --- a/src/HOL/Library/AList.thy	Fri Feb 14 07:53:45 2014 +0100
    12.2 +++ b/src/HOL/Library/AList.thy	Fri Feb 14 07:53:46 2014 +0100
    12.3 @@ -399,7 +399,7 @@
    12.4    by (simp add: map_ran_def image_image split_def)
    12.5    
    12.6  lemma map_ran_conv:
    12.7 -  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
    12.8 +  "map_of (map_ran f al) k = map_option (f k) (map_of al k)"
    12.9    by (induct al) auto
   12.10  
   12.11  lemma distinct_map_ran:
    13.1 --- a/src/HOL/Library/Code_Binary_Nat.thy	Fri Feb 14 07:53:45 2014 +0100
    13.2 +++ b/src/HOL/Library/Code_Binary_Nat.thy	Fri Feb 14 07:53:46 2014 +0100
    13.3 @@ -68,9 +68,9 @@
    13.4    "sub (Num.Bit1 m) Num.One = Some (nat_of_num (Num.Bit0 m))"
    13.5    "sub Num.One (Num.Bit0 n) = None"
    13.6    "sub Num.One (Num.Bit1 n) = None"
    13.7 -  "sub (Num.Bit0 m) (Num.Bit0 n) = Option.map dup (sub m n)"
    13.8 -  "sub (Num.Bit1 m) (Num.Bit1 n) = Option.map dup (sub m n)"
    13.9 -  "sub (Num.Bit1 m) (Num.Bit0 n) = Option.map (\<lambda>q. dup q + 1) (sub m n)"
   13.10 +  "sub (Num.Bit0 m) (Num.Bit0 n) = map_option dup (sub m n)"
   13.11 +  "sub (Num.Bit1 m) (Num.Bit1 n) = map_option dup (sub m n)"
   13.12 +  "sub (Num.Bit1 m) (Num.Bit0 n) = map_option (\<lambda>q. dup q + 1) (sub m n)"
   13.13    "sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
   13.14       | Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
   13.15    apply (auto simp add: nat_of_num_numeral
    14.1 --- a/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:45 2014 +0100
    14.2 +++ b/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:46 2014 +0100
    14.3 @@ -65,7 +65,7 @@
    14.4  
    14.5  lemma map_transfer: 
    14.6    "((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) 
    14.7 -    (\<lambda>f g m. (Option.map g \<circ> m \<circ> f)) (\<lambda>f g m. (Option.map g \<circ> m \<circ> f))"
    14.8 +    (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
    14.9  by transfer_prover
   14.10  
   14.11  lemma map_entry_transfer:
   14.12 @@ -105,13 +105,13 @@
   14.13    "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_transfer .
   14.14  
   14.15  lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
   14.16 -  "\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" parametric map_transfer .
   14.17 +  "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_transfer .
   14.18  
   14.19  
   14.20  subsection {* Functorial structure *}
   14.21  
   14.22  enriched_type map: map
   14.23 -  by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
   14.24 +  by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
   14.25  
   14.26  
   14.27  subsection {* Derived operations *}
   14.28 @@ -367,5 +367,3 @@
   14.29    replace default map_entry map_default tabulate bulkload map of_alist
   14.30  
   14.31  end
   14.32 -
   14.33 -
    15.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Feb 14 07:53:45 2014 +0100
    15.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Feb 14 07:53:46 2014 +0100
    15.3 @@ -11,20 +11,16 @@
    15.4  subsection {* Rules for the Quotient package *}
    15.5  
    15.6  lemma option_rel_map1:
    15.7 -  "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
    15.8 +  "option_rel R (map_option f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
    15.9    by (simp add: option_rel_def split: option.split)
   15.10  
   15.11  lemma option_rel_map2:
   15.12 -  "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
   15.13 +  "option_rel R x (map_option f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
   15.14    by (simp add: option_rel_def split: option.split)
   15.15  
   15.16 -lemma option_map_id [id_simps]:
   15.17 -  "Option.map id = id"
   15.18 -  by (simp add: id_def Option.map.identity fun_eq_iff)
   15.19 -
   15.20 -lemma option_rel_eq [id_simps]:
   15.21 -  "option_rel (op =) = (op =)"
   15.22 -  by (simp add: option_rel_def fun_eq_iff split: option.split)
   15.23 +declare
   15.24 +  map_option.id [id_simps]
   15.25 +  option_rel_eq [id_simps]
   15.26  
   15.27  lemma option_symp:
   15.28    "symp R \<Longrightarrow> symp (option_rel R)"
   15.29 @@ -40,9 +36,9 @@
   15.30  
   15.31  lemma option_quotient [quot_thm]:
   15.32    assumes "Quotient3 R Abs Rep"
   15.33 -  shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
   15.34 +  shows "Quotient3 (option_rel R) (map_option Abs) (map_option Rep)"
   15.35    apply (rule Quotient3I)
   15.36 -  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])
   15.37 +  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])
   15.38    using Quotient3_rel [OF assms]
   15.39    apply (simp add: option_rel_def split: option.split)
   15.40    done
   15.41 @@ -61,12 +57,12 @@
   15.42  
   15.43  lemma option_None_prs [quot_preserve]:
   15.44    assumes q: "Quotient3 R Abs Rep"
   15.45 -  shows "Option.map Abs None = None"
   15.46 +  shows "map_option Abs None = None"
   15.47    by simp
   15.48  
   15.49  lemma option_Some_prs [quot_preserve]:
   15.50    assumes q: "Quotient3 R Abs Rep"
   15.51 -  shows "(Rep ---> Option.map Abs) Some = Some"
   15.52 +  shows "(Rep ---> map_option Abs) Some = Some"
   15.53    apply(simp add: fun_eq_iff)
   15.54    apply(simp add: Quotient3_abs_rep[OF q])
   15.55    done
    16.1 --- a/src/HOL/Library/RBT.thy	Fri Feb 14 07:53:45 2014 +0100
    16.2 +++ b/src/HOL/Library/RBT.thy	Fri Feb 14 07:53:46 2014 +0100
    16.3 @@ -127,11 +127,11 @@
    16.4    by transfer (rule rbt_lookup_rbt_bulkload)
    16.5  
    16.6  lemma lookup_map_entry [simp]:
    16.7 -  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
    16.8 +  "lookup (map_entry k f t) = (lookup t)(k := map_option f (lookup t k))"
    16.9    by transfer (rule rbt_lookup_rbt_map_entry)
   16.10  
   16.11  lemma lookup_map [simp]:
   16.12 -  "lookup (map f t) k = Option.map (f k) (lookup t k)"
   16.13 +  "lookup (map f t) k = map_option (f k) (lookup t k)"
   16.14    by transfer (rule rbt_lookup_map)
   16.15  
   16.16  lemma fold_fold:
    17.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Feb 14 07:53:45 2014 +0100
    17.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Feb 14 07:53:46 2014 +0100
    17.3 @@ -1025,7 +1025,7 @@
    17.4  end
    17.5  
    17.6  theorem (in linorder) rbt_lookup_rbt_map_entry:
    17.7 -  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := Option.map f (rbt_lookup t k))"
    17.8 +  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := map_option f (rbt_lookup t k))"
    17.9    by (induct t) (auto split: option.splits simp add: fun_eq_iff)
   17.10  
   17.11  subsection {* Mapping all entries *}
   17.12 @@ -1053,7 +1053,7 @@
   17.13  
   17.14  end
   17.15  
   17.16 -theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = Option.map (f x) (rbt_lookup t x)"
   17.17 +theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
   17.18    apply(induct t)
   17.19    apply auto
   17.20    apply(subgoal_tac "x = a")
   17.21 @@ -1855,9 +1855,9 @@
   17.22  lemma map_of_sinter_with:
   17.23    "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   17.24    \<Longrightarrow> map_of (sinter_with f xs ys) k = 
   17.25 -  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> Option.map (f k v) (map_of ys k))"
   17.26 +  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> map_option (f k v) (map_of ys k))"
   17.27  apply(induct f xs ys rule: sinter_with.induct)
   17.28 -apply(auto simp add: sorted_Cons Option.map_def split: option.splits dest: map_of_SomeD bspec)
   17.29 +apply(auto simp add: sorted_Cons map_option_case split: option.splits dest: map_of_SomeD bspec)
   17.30  done
   17.31  
   17.32  end
   17.33 @@ -1866,11 +1866,11 @@
   17.34  by(induct xs)(auto 4 3 simp add: map_add_def intro!: ext split: option.split intro: rev_image_eqI)
   17.35  
   17.36  lemma map_map_filter: 
   17.37 -  "map f (List.map_filter g xs) = List.map_filter (Option.map f \<circ> g) xs"
   17.38 +  "map f (List.map_filter g xs) = List.map_filter (map_option f \<circ> g) xs"
   17.39  by(auto simp add: List.map_filter_def)
   17.40  
   17.41 -lemma map_filter_option_map_const: 
   17.42 -  "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)"
   17.43 +lemma map_filter_map_option_const: 
   17.44 +  "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)"
   17.45  by(auto simp add: map_filter_def filter_map o_def)
   17.46  
   17.47  lemma set_map_filter: "set (List.map_filter P xs) = the ` (P ` set xs - {None})"
   17.48 @@ -1897,8 +1897,8 @@
   17.49    "rbt_inter_with_key f t1 t2 =
   17.50    (case RBT_Impl.compare_height t1 t1 t2 t2 
   17.51     of compare.EQ \<Rightarrow> rbtreeify (sinter_with f (entries t1) (entries t2))
   17.52 -    | 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))
   17.53 -    | 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)))"
   17.54 +    | 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))
   17.55 +    | 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)))"
   17.56  
   17.57  definition rbt_inter_with where
   17.58    "rbt_inter_with f = rbt_inter_with_key (\<lambda>_. f)"
   17.59 @@ -1971,7 +1971,7 @@
   17.60  
   17.61  lemma rbt_interwk_is_rbt [simp]:
   17.62    "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with_key f t1 t2)"
   17.63 -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)
   17.64 +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)
   17.65  
   17.66  lemma rbt_interw_is_rbt:
   17.67    "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with f t1 t2)"
   17.68 @@ -1987,7 +1987,7 @@
   17.69    (case rbt_lookup t1 k of None \<Rightarrow> None 
   17.70     | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> None
   17.71                 | Some w \<Rightarrow> Some (f k v w))"
   17.72 -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)
   17.73 +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)
   17.74  
   17.75  lemma rbt_lookup_rbt_inter:
   17.76    "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>
    18.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Feb 14 07:53:45 2014 +0100
    18.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Feb 14 07:53:46 2014 +0100
    18.3 @@ -85,7 +85,7 @@
    18.4  assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
    18.5  assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
    18.6  assumes Initial: "P s"
    18.7 -shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
    18.8 +shows "map_option f (while_option b c s) = while_option b' c' (f s)"
    18.9  unfolding while_option_def
   18.10  proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
   18.11    fix k
   18.12 @@ -188,7 +188,7 @@
   18.13  
   18.14  lemma while_option_commute:
   18.15    assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
   18.16 -  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
   18.17 +  shows "map_option f (while_option b c s) = while_option b' c' (f s)"
   18.18  by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
   18.19    (auto simp add: assms)
   18.20  
    19.1 --- a/src/HOL/Lifting_Option.thy	Fri Feb 14 07:53:45 2014 +0100
    19.2 +++ b/src/HOL/Lifting_Option.thy	Fri Feb 14 07:53:46 2014 +0100
    19.3 @@ -83,8 +83,8 @@
    19.4  
    19.5  lemma Quotient_option[quot_map]:
    19.6    assumes "Quotient R Abs Rep T"
    19.7 -  shows "Quotient (option_rel R) (Option.map Abs)
    19.8 -    (Option.map Rep) (option_rel T)"
    19.9 +  shows "Quotient (option_rel R) (map_option Abs)
   19.10 +    (map_option Rep) (option_rel T)"
   19.11    using assms unfolding Quotient_alt_def option_rel_def
   19.12    by (simp split: option.split)
   19.13  
   19.14 @@ -104,9 +104,9 @@
   19.15    "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
   19.16    unfolding fun_rel_def split_option_all by simp
   19.17  
   19.18 -lemma option_map_transfer [transfer_rule]:
   19.19 -  "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
   19.20 -  unfolding Option.map_def by transfer_prover
   19.21 +lemma map_option_transfer [transfer_rule]:
   19.22 +  "((A ===> B) ===> option_rel A ===> option_rel B) map_option map_option"
   19.23 +  unfolding map_option_case[abs_def] by transfer_prover
   19.24  
   19.25  lemma option_bind_transfer [transfer_rule]:
   19.26    "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
    20.1 --- a/src/HOL/Limited_Sequence.thy	Fri Feb 14 07:53:45 2014 +0100
    20.2 +++ b/src/HOL/Limited_Sequence.thy	Fri Feb 14 07:53:46 2014 +0100
    20.3 @@ -27,11 +27,11 @@
    20.4  where
    20.5    "yield f i pol = (case eval f i pol of
    20.6      None \<Rightarrow> None
    20.7 -  | Some s \<Rightarrow> (Option.map \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
    20.8 +  | Some s \<Rightarrow> (map_option \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
    20.9  
   20.10  definition map_seq :: "('a \<Rightarrow> 'b dseq) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b dseq"
   20.11  where
   20.12 -  "map_seq f xq i pol = Option.map Lazy_Sequence.flat
   20.13 +  "map_seq f xq i pol = map_option Lazy_Sequence.flat
   20.14      (Lazy_Sequence.those (Lazy_Sequence.map (\<lambda>x. f x i pol) xq))"
   20.15  
   20.16  lemma map_seq_code [code]:
    21.1 --- a/src/HOL/List.thy	Fri Feb 14 07:53:45 2014 +0100
    21.2 +++ b/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
    21.3 @@ -182,7 +182,7 @@
    21.4  "those [] = Some []" |
    21.5  "those (x # xs) = (case x of
    21.6    None \<Rightarrow> None
    21.7 -| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
    21.8 +| Some y \<Rightarrow> map_option (Cons y) (those xs))"
    21.9  
   21.10  primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   21.11  "remove1 x [] = []" |
    22.1 --- a/src/HOL/Map.thy	Fri Feb 14 07:53:45 2014 +0100
    22.2 +++ b/src/HOL/Map.thy	Fri Feb 14 07:53:46 2014 +0100
    22.3 @@ -242,21 +242,21 @@
    22.4  by (induct xs) auto
    22.5  
    22.6  lemma map_of_map:
    22.7 -  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
    22.8 +  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
    22.9    by (induct xs) (auto simp add: fun_eq_iff)
   22.10  
   22.11 -lemma dom_option_map:
   22.12 -  "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
   22.13 +lemma dom_map_option:
   22.14 +  "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
   22.15    by (simp add: dom_def)
   22.16  
   22.17  
   22.18 -subsection {* @{const Option.map} related *}
   22.19 +subsection {* @{const map_option} related *}
   22.20  
   22.21 -lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
   22.22 +lemma map_option_o_empty [simp]: "map_option f o empty = empty"
   22.23  by (rule ext) simp
   22.24  
   22.25 -lemma option_map_o_map_upd [simp]:
   22.26 -  "Option.map f o m(a|->b) = (Option.map f o m)(a|->f b)"
   22.27 +lemma map_option_o_map_upd [simp]:
   22.28 +  "map_option f o m(a|->b) = (map_option f o m)(a|->f b)"
   22.29  by (rule ext) simp
   22.30  
   22.31  
    23.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Fri Feb 14 07:53:45 2014 +0100
    23.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Fri Feb 14 07:53:46 2014 +0100
    23.3 @@ -95,7 +95,7 @@
    23.4         (xcpt_names (i,G,pc,et))"
    23.5  
    23.6  definition norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option" where
    23.7 -  "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))"
    23.8 +  "norm_eff i G == map_option (\<lambda>s. eff' (i,G,s))"
    23.9  
   23.10  definition eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type" where
   23.11    "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)"
    24.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Fri Feb 14 07:53:45 2014 +0100
    24.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Fri Feb 14 07:53:46 2014 +0100
    24.3 @@ -119,11 +119,11 @@
    24.4  by (induct xs,auto)
    24.5  
    24.6  lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow>
    24.7 -  map_of (map f xs) a = Option.map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
    24.8 +  map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
    24.9  by (induct xs, auto)
   24.10  
   24.11 -lemma option_map_of [simp]: "(Option.map f (map_of xs k) = None) = ((map_of xs k) = None)"
   24.12 -by (simp add: Option.map_def split: option.split)
   24.13 +lemma map_option_map_of [simp]: "(map_option f (map_of xs k) = None) = ((map_of xs k) = None)"
   24.14 +by (simp add: map_option_case split: option.split)
   24.15  
   24.16  
   24.17  
    25.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Feb 14 07:53:45 2014 +0100
    25.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Feb 14 07:53:46 2014 +0100
    25.3 @@ -551,7 +551,7 @@
    25.4  
    25.5  lemma match_xctable_offset: "
    25.6    (match_exception_table G cn (pc + n) (offset_xctable n et)) =
    25.7 -  (Option.map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
    25.8 +  (map_option (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
    25.9  apply (induct et)
   25.10  apply (simp add: offset_xctable_def)+
   25.11  apply (case_tac "match_exception_entry G cn pc a")
   25.12 @@ -672,7 +672,7 @@
   25.13          in app_jumps_lem)
   25.14    apply (simp add: nth_append)+
   25.15      (* subgoal \<exists> st. mt ! pc'' = Some st *)
   25.16 -  apply (simp add: norm_eff_def Option.map_def nth_append)
   25.17 +  apply (simp add: norm_eff_def map_option_case nth_append)
   25.18    apply (case_tac "mt ! pc''")
   25.19  apply simp+
   25.20  done
    26.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Feb 14 07:53:45 2014 +0100
    26.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Feb 14 07:53:46 2014 +0100
    26.3 @@ -273,13 +273,13 @@
    26.4    "mtd_mb == snd o snd"
    26.5  
    26.6  lemma map_of_map:
    26.7 -  "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = Option.map f (map_of xs k)"
    26.8 +  "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = map_option f (map_of xs k)"
    26.9    by (simp add: map_of_map)
   26.10  
   26.11  lemma map_of_map_fst: "\<lbrakk> inj f;
   26.12    \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
   26.13    \<Longrightarrow>  map_of (map g xs) k 
   26.14 -  = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
   26.15 +  = map_option (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
   26.16  apply (induct xs)
   26.17  apply simp
   26.18  apply simp
   26.19 @@ -295,13 +295,13 @@
   26.20  
   26.21  lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   26.22    ((method (comp G, C) S) = 
   26.23 -  Option.map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
   26.24 +  map_option (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
   26.25               (method (G, C) S))"
   26.26  apply (simp add: method_def)
   26.27  apply (frule wf_subcls1)
   26.28  apply (simp add: comp_class_rec)
   26.29  apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
   26.30 -apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
   26.31 +apply (rule_tac R="%x y. ((x S) = (map_option (\<lambda>(D, rT, b). 
   26.32    (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   26.33    in class_rec_relation)
   26.34  apply assumption
    27.1 --- a/src/HOL/MicroJava/DFA/Opt.thy	Fri Feb 14 07:53:45 2014 +0100
    27.2 +++ b/src/HOL/MicroJava/DFA/Opt.thy	Fri Feb 14 07:53:46 2014 +0100
    27.3 @@ -282,8 +282,8 @@
    27.4  
    27.5  lemma option_map_in_optionI:
    27.6    "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
    27.7 -  \<Longrightarrow> Option.map f ox : opt S";
    27.8 -apply (unfold Option.map_def)
    27.9 +  \<Longrightarrow> map_option f ox : opt S";
   27.10 +apply (unfold map_option_case)
   27.11  apply (simp split: option.split)
   27.12  apply blast
   27.13  done 
    28.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Feb 14 07:53:45 2014 +0100
    28.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Fri Feb 14 07:53:46 2014 +0100
    28.3 @@ -14,7 +14,7 @@
    28.4  
    28.5  definition conf :: "'c prog => aheap => val => ty => bool" 
    28.6                                     ("_,_ |- _ ::<= _"  [51,51,51,51] 50) where
    28.7 - "G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    28.8 + "G,h|-v::<=T == \<exists>T'. typeof (map_option obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    28.9  
   28.10  definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
   28.11                                     ("_,_ |- _ [::<=] _" [51,51,51,51] 50) where
    29.1 --- a/src/HOL/NanoJava/State.thy	Fri Feb 14 07:53:45 2014 +0100
    29.2 +++ b/src/HOL/NanoJava/State.thy	Fri Feb 14 07:53:46 2014 +0100
    29.3 @@ -28,7 +28,7 @@
    29.4    (type) "obj"    \<leftharpoondown> (type) "cname \<times> fields"
    29.5  
    29.6  definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
    29.7 - "init_vars m == Option.map (\<lambda>T. Null) o m"
    29.8 + "init_vars m == map_option (\<lambda>T. Null) o m"
    29.9    
   29.10  text {* private: *}
   29.11  type_synonym heap = "loc   \<rightharpoonup> obj"
    30.1 --- a/src/HOL/Option.thy	Fri Feb 14 07:53:45 2014 +0100
    30.2 +++ b/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
    30.3 @@ -80,53 +80,43 @@
    30.4  lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
    30.5    by (cases xo) auto
    30.6  
    30.7 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option" where
    30.8 -  "map = (%f y. case y of None => None | Some x => Some (f x))"
    30.9 -
   30.10 -lemma option_map_None [simp, code]: "map f None = None"
   30.11 -  by (simp add: map_def)
   30.12 +lemma map_option_case: "map_option f y = (case y of None => None | Some x => Some (f x))"
   30.13 +  by (auto split: option.split)
   30.14  
   30.15 -lemma option_map_Some [simp, code]: "map f (Some x) = Some (f x)"
   30.16 -  by (simp add: map_def)
   30.17 -
   30.18 -lemma option_map_is_None [iff]:
   30.19 -    "(map f opt = None) = (opt = None)"
   30.20 -  by (simp add: map_def split add: option.split)
   30.21 +lemma map_option_is_None [iff]:
   30.22 +    "(map_option f opt = None) = (opt = None)"
   30.23 +  by (simp add: map_option_case split add: option.split)
   30.24  
   30.25 -lemma option_map_eq_Some [iff]:
   30.26 -    "(map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   30.27 -  by (simp add: map_def split add: option.split)
   30.28 +lemma map_option_eq_Some [iff]:
   30.29 +    "(map_option f xo = Some y) = (EX z. xo = Some z & f z = y)"
   30.30 +  by (simp add: map_option_case split add: option.split)
   30.31  
   30.32 -lemma option_map_comp:
   30.33 -    "map f (map g opt) = map (f o g) opt"
   30.34 -  by (simp add: map_def split add: option.split)
   30.35 +lemma map_option_o_case_sum [simp]:
   30.36 +    "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
   30.37 +  by (rule o_case_sum)
   30.38  
   30.39 -lemma option_map_o_case_sum [simp]:
   30.40 -    "map f o case_sum g h = case_sum (map f o g) (map f o h)"
   30.41 -  by (rule ext) (simp split: sum.split)
   30.42 -
   30.43 -lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y"
   30.44 +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"
   30.45  by (cases x) auto
   30.46  
   30.47 -enriched_type map: Option.map proof -
   30.48 +enriched_type map_option: map_option proof -
   30.49    fix f g
   30.50 -  show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
   30.51 +  show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
   30.52    proof
   30.53      fix x
   30.54 -    show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
   30.55 +    show "(map_option f \<circ> map_option g) x= map_option (f \<circ> g) x"
   30.56        by (cases x) simp_all
   30.57    qed
   30.58  next
   30.59 -  show "Option.map id = id"
   30.60 +  show "map_option id = id"
   30.61    proof
   30.62      fix x
   30.63 -    show "Option.map id x = id x"
   30.64 +    show "map_option id x = id x"
   30.65        by (cases x) simp_all
   30.66    qed
   30.67  qed
   30.68  
   30.69 -lemma case_option_map [simp]:
   30.70 -  "case_option g h (Option.map f x) = case_option g (h \<circ> f) x"
   30.71 +lemma case_map_option [simp]:
   30.72 +  "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
   30.73    by (cases x) simp_all
   30.74  
   30.75  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
   30.76 @@ -192,8 +182,8 @@
   30.77    "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
   30.78    by (auto simp add: these_empty_eq)
   30.79  
   30.80 -hide_const (open) set map bind these
   30.81 -hide_fact (open) map_cong bind_cong
   30.82 +hide_const (open) set bind these
   30.83 +hide_fact (open) bind_cong
   30.84  
   30.85  
   30.86  subsubsection {* Interaction with finite sets *}