# HG changeset patch
# User nipkow
# Date 1236160055 -3600
# Node ID e70dae49dc57df4ec78a4af7c97545aedc35fc54
# Parent  7dd251bce291c69ee877d1d53a03c6075bd7bf50# Parent  58d14768339312c4909a905005814ae1a49fd083
merged

diff -r 7dd251bce291 -r e70dae49dc57 NEWS
--- 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.
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/Basis.thy
--- 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"
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/Conform.thy
--- 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)
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/Decl.thy
--- 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))))"
 	
 
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/DeclConcepts.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/Example.thy
--- 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)
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/State.thy
--- 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>)"
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/Table.thy
--- 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
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/WellForm.thy
--- 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
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Bali/WellType.thy
--- 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)
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Datatype.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Extraction.thy
--- 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
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- 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;
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Import/HOL4Compat.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/IsaMakefile
--- 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 \
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Library/AssocList.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"
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Library/RBT.thy
--- 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 *}
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Map.thy
--- 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
 
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/BV/Effect.thy
--- 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)"
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/BV/Opt.thy
--- 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 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- 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)
 
 
 
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/Comp/LemmasComp.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/J/Conform.thy
--- 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)
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/J/Exceptions.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/MicroJava/J/State.thy
--- 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
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/NanoJava/State.thy
--- 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"
diff -r 7dd251bce291 -r e70dae49dc57 src/HOL/Nominal/nominal_atoms.ML
--- 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;