--- 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}
--- 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)
--- 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)
--- 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
--- 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
-
--- 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
--- 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]:
--- 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>)"
--- 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
--- 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
--- 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]:
--- 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:
--- 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
--- 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
-
-
--- 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
--- 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:
--- 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>
--- 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)
--- 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)
--- 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]:
--- 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 [] = []" |
--- 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
--- 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)"
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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 *}