--- a/NEWS Wed Mar 04 00:05:20 2009 +0100
+++ b/NEWS Wed Mar 04 10:47:35 2009 +0100
@@ -500,6 +500,9 @@
Suc_Suc_eq ~> nat.inject
Suc_not_Zero Zero_not_Suc ~> nat.distinct
+* The option datatype has been moved to a new theory HOL/Option.thy.
+Renamed option_map to Option.map.
+
* Library/Nat_Infinity: added addition, numeral syntax and more
instantiations for algebraic structures. Removed some duplicate
theorems. Changes in simp rules. INCOMPATIBILITY.
--- a/src/HOL/Bali/Basis.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Mar 04 10:47:35 2009 +0100
@@ -251,8 +251,8 @@
Oex :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
translations
- "! x:A: P" == "! x:o2s A. P"
- "? x:A: P" == "? x:o2s A. P"
+ "! x:A: P" == "! x:CONST Option.set A. P"
+ "? x:A: P" == "? x:CONST Option.set A. P"
section "Special map update"
--- a/src/HOL/Bali/Conform.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/Conform.thy Wed Mar 04 10:47:35 2009 +0100
@@ -102,7 +102,7 @@
constdefs
conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70)
- "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
+ "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map 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/Decl.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/Decl.thy Wed Mar 04 10:47:35 2009 +0100
@@ -801,7 +801,7 @@
"imethds G I
\<equiv> iface_rec (G,I)
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
- (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
+ (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
--- a/src/HOL/Bali/DeclConcepts.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Mar 04 10:47:35 2009 +0100
@@ -1385,7 +1385,7 @@
"imethds G I
\<equiv> iface_rec (G,I)
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
- (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
+ (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
constdefs
@@ -1528,7 +1528,7 @@
lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>
imethds G I = Un_tables ((\<lambda>J. imethds G J)`set (isuperIfs i)) \<oplus>\<oplus>
- (o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
+ (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
apply (unfold imethds_def)
apply (rule iface_rec [THEN trans])
apply auto
--- a/src/HOL/Bali/Example.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/Example.thy Wed Mar 04 10:47:35 2009 +0100
@@ -458,7 +458,7 @@
lemmas methd_rec' = methd_rec [OF _ ws_tprg]
lemma imethds_HasFoo [simp]:
- "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
+ "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
apply (rule trans)
apply (rule imethds_rec')
apply (auto simp add: HasFooInt_def)
--- a/src/HOL/Bali/State.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/State.thy Wed Mar 04 10:47:35 2009 +0100
@@ -146,7 +146,7 @@
fields_table::
"prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table"
"fields_table G C P
- \<equiv> option_map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
+ \<equiv> Option.map 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>
@@ -258,8 +258,8 @@
lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
translations
- "val_this s" == "the (locals s This)"
- "lookup_obj s a'" == "the (heap s (the_Addr a'))"
+ "val_this s" == "CONST the (locals s This)"
+ "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))"
subsection "memory allocation"
@@ -290,7 +290,7 @@
init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
translations
- "init_vals vs" == "CONST option_map default_val \<circ> vs"
+ "init_vals vs" == "CONST Option.map 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)
@@ -315,12 +315,12 @@
lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000)
"lupd vn v \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
- upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
+ upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
"upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
set_locals :: "locals \<Rightarrow> st \<Rightarrow> st"
"set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
-
+
init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
"init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
--- a/src/HOL/Bali/Table.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/Table.thy Wed Mar 04 10:47:35 2009 +0100
@@ -194,7 +194,7 @@
done
lemma Ball_set_tableD:
- "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
+ "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
apply (frule Ball_set_table)
by auto
--- a/src/HOL/Bali/WellForm.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/WellForm.thy Wed Mar 04 10:47:35 2009 +0100
@@ -236,7 +236,7 @@
under (\<lambda> new old. accmodi old \<noteq> Private)
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and>
is_static new = is_static old)) \<and>
- (o2s \<circ> table_of (imethods i)
+ (Option.set \<circ> table_of (imethods i)
hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
@@ -248,7 +248,7 @@
lemma wf_idecl_hidings:
"wf_idecl G (I, i) \<Longrightarrow>
- (\<lambda>s. o2s (table_of (imethods i) s))
+ (\<lambda>s. Option.set (table_of (imethods i) s))
hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))
entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
apply (unfold wf_idecl_def o_def)
@@ -751,7 +751,7 @@
show "\<not>is_static im \<and> accmodi im = Public"
proof -
let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
- let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
+ let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
by (simp add: imethds_rec)
from wf if_I have
@@ -1783,7 +1783,7 @@
by (blast dest: subint1D)
let ?newMethods
- = "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
+ = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
show "?Concl I"
proof (cases "?newMethods sig = {}")
case True
@@ -1864,7 +1864,7 @@
apply (drule (1) wf_prog_idecl)
apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1
[THEN is_acc_ifaceD [THEN conjunct1]]]])
-apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
+apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
sig ={}")
apply force
--- a/src/HOL/Bali/WellType.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Mar 04 10:47:35 2009 +0100
@@ -87,11 +87,11 @@
defs
cmheads_def:
"cmheads G S C
- \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
+ \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
Objectmheads_def:
"Objectmheads G S
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd)))
- ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
+ ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
accObjectmheads_def:
"accObjectmheads G S T
\<equiv> if G\<turnstile>RefT T accessible_in (pid S)
--- a/src/HOL/Datatype.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Datatype.thy Wed Mar 04 10:47:35 2009 +0100
@@ -576,122 +576,4 @@
hide (open) const Suml Sumr Projl Projr
-
-subsection {* The option datatype *}
-
-datatype 'a option = None | Some 'a
-
-lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
- by (induct x) auto
-
-lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
- by (induct x) auto
-
-text{*Although it may appear that both of these equalities are helpful
-only when applied to assumptions, in practice it seems better to give
-them the uniform iff attribute. *}
-
-lemma option_caseE:
- assumes c: "(case x of None => P | Some y => Q y)"
- obtains
- (None) "x = None" and P
- | (Some) y where "x = Some y" and "Q y"
- using c by (cases x) simp_all
-
-lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
- by (rule set_ext, case_tac x) auto
-
-lemma inj_Some [simp]: "inj_on Some A"
- by (rule inj_onI) simp
-
-
-subsubsection {* Operations *}
-
-consts
- the :: "'a option => 'a"
-primrec
- "the (Some x) = x"
-
-consts
- o2s :: "'a option => 'a set"
-primrec
- "o2s None = {}"
- "o2s (Some x) = {x}"
-
-lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
- by simp
-
-declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
-*}
-
-lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
- by (cases xo) auto
-
-lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
- by (cases xo) auto
-
-definition
- option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
-where
- [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
-
-lemma option_map_None [simp, code]: "option_map f None = None"
- by (simp add: option_map_def)
-
-lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
- by (simp add: option_map_def)
-
-lemma option_map_is_None [iff]:
- "(option_map f opt = None) = (opt = None)"
- by (simp add: option_map_def split add: option.split)
-
-lemma option_map_eq_Some [iff]:
- "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
- by (simp add: option_map_def split add: option.split)
-
-lemma option_map_comp:
- "option_map f (option_map g opt) = option_map (f o g) opt"
- by (simp add: option_map_def split add: option.split)
-
-lemma option_map_o_sum_case [simp]:
- "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
- by (rule ext) (simp split: sum.split)
-
-
-subsubsection {* Code generator setup *}
-
-definition
- is_none :: "'a option \<Rightarrow> bool" where
- is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
-
-lemma is_none_code [code]:
- shows "is_none None \<longleftrightarrow> True"
- and "is_none (Some x) \<longleftrightarrow> False"
- unfolding is_none_none [symmetric] by simp_all
-
-hide (open) const is_none
-
-code_type option
- (SML "_ option")
- (OCaml "_ option")
- (Haskell "Maybe _")
-
-code_const None and Some
- (SML "NONE" and "SOME")
- (OCaml "None" and "Some _")
- (Haskell "Nothing" and "Just")
-
-code_instance option :: eq
- (Haskell -)
-
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
- (Haskell infixl 4 "==")
-
-code_reserved SML
- option NONE SOME
-
-code_reserved OCaml
- option None Some
-
end
--- a/src/HOL/Extraction.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Extraction.thy Wed Mar 04 10:47:35 2009 +0100
@@ -6,7 +6,7 @@
header {* Program extraction for HOL *}
theory Extraction
-imports Datatype
+imports Option
uses "Tools/rewrite_hol_proof.ML"
begin
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed Mar 04 10:47:35 2009 +0100
@@ -88,14 +88,14 @@
import_theory option;
type_maps
- option > Datatype.option;
+ option > Option.option;
const_maps
- NONE > Datatype.option.None
- SOME > Datatype.option.Some
- option_case > Datatype.option.option_case
- OPTION_MAP > Datatype.option_map
- THE > Datatype.the
+ NONE > Option.option.None
+ SOME > Option.option.Some
+ option_case > Option.option.option_case
+ OPTION_MAP > Option.map
+ THE > Option.the
IS_SOME > HOL4Compat.IS_SOME
IS_NONE > HOL4Compat.IS_NONE
OPTION_JOIN > HOL4Compat.OPTION_JOIN;
--- a/src/HOL/Import/HOL4Compat.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Wed Mar 04 10:47:35 2009 +0100
@@ -73,7 +73,7 @@
lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
by simp
-lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)"
+lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
by simp
consts
--- a/src/HOL/IsaMakefile Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/IsaMakefile Wed Mar 04 10:47:35 2009 +0100
@@ -127,6 +127,7 @@
Nat.thy \
OrderedGroup.thy \
Orderings.thy \
+ Option.thy \
Plain.thy \
Power.thy \
Predicate.thy \
--- a/src/HOL/Library/AssocList.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Library/AssocList.thy Wed Mar 04 10:47:35 2009 +0100
@@ -429,7 +429,7 @@
subsection {* @{const map_ran} *}
-lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
+lemma map_ran_conv: "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
by (induct al) auto
lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
--- a/src/HOL/Library/RBT.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Library/RBT.thy Wed Mar 04 10:47:35 2009 +0100
@@ -891,7 +891,7 @@
theorem mapwk_isrbt[simp]: "isrbt (mapwithkey f t) = isrbt t"
unfolding isrbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_st mapwk_treec)
-theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = option_map (f x) (map_of t x)"
+theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = Option.map (f x) (map_of t x)"
by (induct t) auto
definition map
@@ -899,7 +899,7 @@
theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
theorem map_isrbt[simp]: "isrbt (map f t) = isrbt t" unfolding map_def by simp
-theorem map_of_map[simp]: "map_of (map f t) = option_map f o map_of t"
+theorem map_of_map[simp]: "map_of (map f t) = Option.map f o map_of t"
by (rule ext) (simp add:map_def)
subsection {* Fold *}
--- a/src/HOL/Map.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Map.thy Wed Mar 04 10:47:35 2009 +0100
@@ -242,17 +242,17 @@
"map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
by (induct xs) auto
-lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
+lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = Option.map f (map_of xs x)"
by (induct xs) auto
-subsection {* @{term [source] option_map} related *}
+subsection {* @{const Option.map} related *}
-lemma option_map_o_empty [simp]: "option_map f o empty = empty"
+lemma option_map_o_empty [simp]: "Option.map 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)"
+ "Option.map f o m(a|->b) = (Option.map f o m)(a|->f b)"
by (rule ext) simp
--- a/src/HOL/MicroJava/BV/Effect.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Wed Mar 04 10:47:35 2009 +0100
@@ -105,7 +105,7 @@
(xcpt_names (i,G,pc,et))"
norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
- "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
+ "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))"
eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"
"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/BV/Opt.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Wed Mar 04 10:47:35 2009 +0100
@@ -286,8 +286,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> Option.map f ox : opt S";
+apply (unfold Option.map_def)
apply (simp split: option.split)
apply blast
done
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Wed Mar 04 10:47:35 2009 +0100
@@ -126,11 +126,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 = Option.map (\<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 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)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Mar 04 10:47:35 2009 +0100
@@ -553,7 +553,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))"
+ (Option.map (\<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")
@@ -675,7 +675,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 Option.map_def nth_append)
apply (case_tac "mt ! pc''")
apply simp+
done
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Wed Mar 04 10:47:35 2009 +0100
@@ -271,7 +271,7 @@
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)"
+ = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
apply (induct xs)
apply simp
apply (simp del: split_paired_All)
@@ -288,13 +288,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))))
+ Option.map (\<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: map_compose [THEN sym] split_iter split_compose del: map_compose)
-apply (rule_tac R="%x y. ((x S) = (option_map (\<lambda>(D, rT, b).
+apply (rule_tac R="%x y. ((x S) = (Option.map (\<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/J/Conform.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Mar 04 10:47:35 2009 +0100
@@ -17,7 +17,7 @@
conf :: "'c prog => aheap => val => ty => bool"
("_,_ |- _ ::<= _" [51,51,51,51] 50)
- "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 (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
("_,_ |- _ [::<=] _" [51,51,51,51] 50)
--- a/src/HOL/MicroJava/J/Exceptions.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy Wed Mar 04 10:47:35 2009 +0100
@@ -21,7 +21,7 @@
cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
translations
- "cname_of hp v" == "fst (the (hp (the_Addr v)))"
+ "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))"
constdefs
--- a/src/HOL/MicroJava/J/State.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/MicroJava/J/State.thy Wed Mar 04 10:47:35 2009 +0100
@@ -41,7 +41,7 @@
"Norm s" == "(None,s)"
"abrupt" => "fst"
"store" => "snd"
- "lookup_obj s a'" == "the (heap s (the_Addr a'))"
+ "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))"
constdefs
--- a/src/HOL/NanoJava/State.thy Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Mar 04 10:47:35 2009 +0100
@@ -33,7 +33,7 @@
constdefs
init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
- "init_vars m == option_map (\<lambda>T. Null) o m"
+ "init_vars m == Option.map (\<lambda>T. Null) o m"
text {* private: *}
types heap = "loc \<rightharpoonup> obj"
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Mar 04 00:05:20 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Mar 04 10:47:35 2009 +0100
@@ -539,7 +539,7 @@
thy
|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
|> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
- |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+ |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
|> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
|> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
@@ -606,7 +606,7 @@
|> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(fs_proof fs_thm_nprod)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
- |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+ |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
end) ak_names thy20;
(******** cp_<ak>_<ai> class instances ********)
@@ -687,7 +687,7 @@
|> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
- |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+ |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
|> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
end) ak_names thy) ak_names thy25;