Made Option a separate theory and renamed option_map to Option.map
authornipkow
Wed Mar 04 10:47:20 2009 +0100 (2009-03-04)
changeset 3023558d147683393
parent 30224 79136ce06bdb
child 30236 e70dae49dc57
Made Option a separate theory and renamed option_map to Option.map
NEWS
src/HOL/Bali/Basis.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
src/HOL/Datatype.thy
src/HOL/Extraction.thy
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/IsaMakefile
src/HOL/Library/AssocList.thy
src/HOL/Library/RBT.thy
src/HOL/Map.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/Opt.thy
src/HOL/MicroJava/Comp/AuxLemmas.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Exceptions.thy
src/HOL/MicroJava/J/State.thy
src/HOL/NanoJava/State.thy
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/NEWS	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/NEWS	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -500,6 +500,9 @@
     1.4      Suc_Suc_eq                  ~> nat.inject
     1.5      Suc_not_Zero Zero_not_Suc   ~> nat.distinct
     1.6  
     1.7 +* The option datatype has been moved to a new theory HOL/Option.thy.
     1.8 +Renamed option_map to Option.map.
     1.9 +
    1.10  * Library/Nat_Infinity: added addition, numeral syntax and more
    1.11  instantiations for algebraic structures.  Removed some duplicate
    1.12  theorems.  Changes in simp rules.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Bali/Basis.thy	Tue Mar 03 17:05:18 2009 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Wed Mar 04 10:47:20 2009 +0100
     2.3 @@ -251,8 +251,8 @@
     2.4    Oex  :: "[pttrn, 'a option, bool] => bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
     2.5  
     2.6  translations
     2.7 -  "! x:A: P"    == "! x:o2s A. P"
     2.8 -  "? x:A: P"    == "? x:o2s A. P"
     2.9 +  "! x:A: P"    == "! x:CONST Option.set A. P"
    2.10 +  "? x:A: P"    == "? x:CONST Option.set A. P"
    2.11  
    2.12  section "Special map update"
    2.13  
     3.1 --- a/src/HOL/Bali/Conform.thy	Tue Mar 03 17:05:18 2009 +0100
     3.2 +++ b/src/HOL/Bali/Conform.thy	Wed Mar 04 10:47:20 2009 +0100
     3.3 @@ -102,7 +102,7 @@
     3.4  constdefs
     3.5  
     3.6    conf  :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"    ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
     3.7 -	   "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"
     3.8 +	   "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"
     3.9  
    3.10  lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
    3.11  by (auto simp: conf_def)
     4.1 --- a/src/HOL/Bali/Decl.thy	Tue Mar 03 17:05:18 2009 +0100
     4.2 +++ b/src/HOL/Bali/Decl.thy	Wed Mar 04 10:47:20 2009 +0100
     4.3 @@ -801,7 +801,7 @@
     4.4  "imethds G I 
     4.5    \<equiv> iface_rec (G,I)  
     4.6                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
     4.7 -                        (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     4.8 +                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     4.9  	
    4.10  
    4.11  
     5.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Mar 03 17:05:18 2009 +0100
     5.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Mar 04 10:47:20 2009 +0100
     5.3 @@ -1385,7 +1385,7 @@
     5.4  "imethds G I 
     5.5    \<equiv> iface_rec (G,I)  
     5.6                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
     5.7 -                        (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     5.8 +                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     5.9  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    5.10  
    5.11  constdefs
    5.12 @@ -1528,7 +1528,7 @@
    5.13  
    5.14  lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>  
    5.15    imethds G I = Un_tables ((\<lambda>J. imethds  G J)`set (isuperIfs i)) \<oplus>\<oplus>  
    5.16 -                      (o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    5.17 +                      (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    5.18  apply (unfold imethds_def)
    5.19  apply (rule iface_rec [THEN trans])
    5.20  apply auto
     6.1 --- a/src/HOL/Bali/Example.thy	Tue Mar 03 17:05:18 2009 +0100
     6.2 +++ b/src/HOL/Bali/Example.thy	Wed Mar 04 10:47:20 2009 +0100
     6.3 @@ -458,7 +458,7 @@
     6.4  lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
     6.5  
     6.6  lemma imethds_HasFoo [simp]: 
     6.7 -  "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
     6.8 +  "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
     6.9  apply (rule trans)
    6.10  apply (rule imethds_rec')
    6.11  apply  (auto simp add: HasFooInt_def)
     7.1 --- a/src/HOL/Bali/State.thy	Tue Mar 03 17:05:18 2009 +0100
     7.2 +++ b/src/HOL/Bali/State.thy	Wed Mar 04 10:47:20 2009 +0100
     7.3 @@ -146,7 +146,7 @@
     7.4    fields_table::
     7.5      "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table"
     7.6   "fields_table G C P 
     7.7 -    \<equiv> option_map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
     7.8 +    \<equiv> Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
     7.9  
    7.10  lemma fields_table_SomeI: 
    7.11  "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
    7.12 @@ -258,8 +258,8 @@
    7.13    lookup_obj   :: "st \<Rightarrow> val \<Rightarrow> obj"
    7.14  
    7.15  translations
    7.16 - "val_this s"       == "the (locals s This)" 
    7.17 - "lookup_obj s a'"  == "the (heap s (the_Addr a'))"
    7.18 + "val_this s"       == "CONST the (locals s This)" 
    7.19 + "lookup_obj s a'"  == "CONST the (heap s (the_Addr a'))"
    7.20  
    7.21  subsection "memory allocation"
    7.22  
    7.23 @@ -290,7 +290,7 @@
    7.24    init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
    7.25  
    7.26  translations
    7.27 - "init_vals vs"    == "CONST option_map default_val \<circ> vs"
    7.28 + "init_vals vs"    == "CONST Option.map default_val \<circ> vs"
    7.29  
    7.30  lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
    7.31  apply (unfold arr_comps_def in_bounds_def)
    7.32 @@ -315,12 +315,12 @@
    7.33    lupd       :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"        ("lupd'(_\<mapsto>_')"[10,10]1000)
    7.34   "lupd vn v   \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
    7.35  
    7.36 -  upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" 
    7.37 +  upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
    7.38   "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
    7.39  
    7.40    set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st"
    7.41   "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
    7.42 -  
    7.43 +
    7.44    init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
    7.45   "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
    7.46  
     8.1 --- a/src/HOL/Bali/Table.thy	Tue Mar 03 17:05:18 2009 +0100
     8.2 +++ b/src/HOL/Bali/Table.thy	Wed Mar 04 10:47:20 2009 +0100
     8.3 @@ -194,7 +194,7 @@
     8.4  done
     8.5  
     8.6  lemma Ball_set_tableD: 
     8.7 -  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
     8.8 +  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
     8.9  apply (frule Ball_set_table)
    8.10  by auto
    8.11  
     9.1 --- a/src/HOL/Bali/WellForm.thy	Tue Mar 03 17:05:18 2009 +0100
     9.2 +++ b/src/HOL/Bali/WellForm.thy	Wed Mar 04 10:47:20 2009 +0100
     9.3 @@ -236,7 +236,7 @@
     9.4            under  (\<lambda> new old. accmodi old \<noteq> Private)
     9.5            entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
     9.6                               is_static new = is_static old)) \<and> 
     9.7 -        (o2s \<circ> table_of (imethods i) 
     9.8 +        (Option.set \<circ> table_of (imethods i) 
     9.9                 hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
    9.10  	       entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
    9.11  
    9.12 @@ -248,7 +248,7 @@
    9.13  
    9.14  lemma wf_idecl_hidings: 
    9.15  "wf_idecl G (I, i) \<Longrightarrow> 
    9.16 -  (\<lambda>s. o2s (table_of (imethods i) s)) 
    9.17 +  (\<lambda>s. Option.set (table_of (imethods i) s)) 
    9.18    hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
    9.19    entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
    9.20  apply (unfold wf_idecl_def o_def)
    9.21 @@ -751,7 +751,7 @@
    9.22      show "\<not>is_static im \<and> accmodi im = Public" 
    9.23      proof -
    9.24        let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
    9.25 -      let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
    9.26 +      let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
    9.27        from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
    9.28  	by (simp add: imethds_rec)
    9.29        from wf if_I have 
    9.30 @@ -1783,7 +1783,7 @@
    9.31        by (blast dest: subint1D)
    9.32  
    9.33      let ?newMethods 
    9.34 -          = "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
    9.35 +          = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
    9.36      show "?Concl I"
    9.37      proof (cases "?newMethods sig = {}")
    9.38        case True
    9.39 @@ -1864,7 +1864,7 @@
    9.40  apply (drule (1) wf_prog_idecl)
    9.41  apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
    9.42                                         [THEN is_acc_ifaceD [THEN conjunct1]]]])
    9.43 -apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
    9.44 +apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
    9.45                    sig ={}")
    9.46  apply   force
    9.47  
    10.1 --- a/src/HOL/Bali/WellType.thy	Tue Mar 03 17:05:18 2009 +0100
    10.2 +++ b/src/HOL/Bali/WellType.thy	Wed Mar 04 10:47:20 2009 +0100
    10.3 @@ -87,11 +87,11 @@
    10.4  defs
    10.5   cmheads_def:
    10.6  "cmheads G S C 
    10.7 -  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
    10.8 +  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
    10.9    Objectmheads_def:
   10.10  "Objectmheads G S  
   10.11    \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
   10.12 -    ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
   10.13 +    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
   10.14    accObjectmheads_def:
   10.15  "accObjectmheads G S T
   10.16     \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
    11.1 --- a/src/HOL/Datatype.thy	Tue Mar 03 17:05:18 2009 +0100
    11.2 +++ b/src/HOL/Datatype.thy	Wed Mar 04 10:47:20 2009 +0100
    11.3 @@ -576,122 +576,4 @@
    11.4  
    11.5  hide (open) const Suml Sumr Projl Projr
    11.6  
    11.7 -
    11.8 -subsection {* The option datatype *}
    11.9 -
   11.10 -datatype 'a option = None | Some 'a
   11.11 -
   11.12 -lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
   11.13 -  by (induct x) auto
   11.14 -
   11.15 -lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
   11.16 -  by (induct x) auto
   11.17 -
   11.18 -text{*Although it may appear that both of these equalities are helpful
   11.19 -only when applied to assumptions, in practice it seems better to give
   11.20 -them the uniform iff attribute. *}
   11.21 -
   11.22 -lemma option_caseE:
   11.23 -  assumes c: "(case x of None => P | Some y => Q y)"
   11.24 -  obtains
   11.25 -    (None) "x = None" and P
   11.26 -  | (Some) y where "x = Some y" and "Q y"
   11.27 -  using c by (cases x) simp_all
   11.28 -
   11.29 -lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
   11.30 -  by (rule set_ext, case_tac x) auto
   11.31 -
   11.32 -lemma inj_Some [simp]: "inj_on Some A"
   11.33 -  by (rule inj_onI) simp
   11.34 -
   11.35 -
   11.36 -subsubsection {* Operations *}
   11.37 -
   11.38 -consts
   11.39 -  the :: "'a option => 'a"
   11.40 -primrec
   11.41 -  "the (Some x) = x"
   11.42 -
   11.43 -consts
   11.44 -  o2s :: "'a option => 'a set"
   11.45 -primrec
   11.46 -  "o2s None = {}"
   11.47 -  "o2s (Some x) = {x}"
   11.48 -
   11.49 -lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   11.50 -  by simp
   11.51 -
   11.52 -declaration {* fn _ =>
   11.53 -  Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
   11.54 -*}
   11.55 -
   11.56 -lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   11.57 -  by (cases xo) auto
   11.58 -
   11.59 -lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   11.60 -  by (cases xo) auto
   11.61 -
   11.62 -definition
   11.63 -  option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
   11.64 -where
   11.65 -  [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
   11.66 -
   11.67 -lemma option_map_None [simp, code]: "option_map f None = None"
   11.68 -  by (simp add: option_map_def)
   11.69 -
   11.70 -lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
   11.71 -  by (simp add: option_map_def)
   11.72 -
   11.73 -lemma option_map_is_None [iff]:
   11.74 -    "(option_map f opt = None) = (opt = None)"
   11.75 -  by (simp add: option_map_def split add: option.split)
   11.76 -
   11.77 -lemma option_map_eq_Some [iff]:
   11.78 -    "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   11.79 -  by (simp add: option_map_def split add: option.split)
   11.80 -
   11.81 -lemma option_map_comp:
   11.82 -    "option_map f (option_map g opt) = option_map (f o g) opt"
   11.83 -  by (simp add: option_map_def split add: option.split)
   11.84 -
   11.85 -lemma option_map_o_sum_case [simp]:
   11.86 -    "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   11.87 -  by (rule ext) (simp split: sum.split)
   11.88 -
   11.89 -
   11.90 -subsubsection {* Code generator setup *}
   11.91 -
   11.92 -definition
   11.93 -  is_none :: "'a option \<Rightarrow> bool" where
   11.94 -  is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
   11.95 -
   11.96 -lemma is_none_code [code]:
   11.97 -  shows "is_none None \<longleftrightarrow> True"
   11.98 -    and "is_none (Some x) \<longleftrightarrow> False"
   11.99 -  unfolding is_none_none [symmetric] by simp_all
  11.100 -
  11.101 -hide (open) const is_none
  11.102 -
  11.103 -code_type option
  11.104 -  (SML "_ option")
  11.105 -  (OCaml "_ option")
  11.106 -  (Haskell "Maybe _")
  11.107 -
  11.108 -code_const None and Some
  11.109 -  (SML "NONE" and "SOME")
  11.110 -  (OCaml "None" and "Some _")
  11.111 -  (Haskell "Nothing" and "Just")
  11.112 -
  11.113 -code_instance option :: eq
  11.114 -  (Haskell -)
  11.115 -
  11.116 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
  11.117 -  (Haskell infixl 4 "==")
  11.118 -
  11.119 -code_reserved SML
  11.120 -  option NONE SOME
  11.121 -
  11.122 -code_reserved OCaml
  11.123 -  option None Some
  11.124 -
  11.125  end
    12.1 --- a/src/HOL/Extraction.thy	Tue Mar 03 17:05:18 2009 +0100
    12.2 +++ b/src/HOL/Extraction.thy	Wed Mar 04 10:47:20 2009 +0100
    12.3 @@ -6,7 +6,7 @@
    12.4  header {* Program extraction for HOL *}
    12.5  
    12.6  theory Extraction
    12.7 -imports Datatype
    12.8 +imports Option
    12.9  uses "Tools/rewrite_hol_proof.ML"
   12.10  begin
   12.11  
    13.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Mar 03 17:05:18 2009 +0100
    13.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Mar 04 10:47:20 2009 +0100
    13.3 @@ -88,14 +88,14 @@
    13.4  import_theory option;
    13.5  
    13.6  type_maps
    13.7 -    option > Datatype.option;
    13.8 +    option > Option.option;
    13.9  
   13.10  const_maps
   13.11 -    NONE        > Datatype.option.None
   13.12 -    SOME        > Datatype.option.Some
   13.13 -    option_case > Datatype.option.option_case
   13.14 -    OPTION_MAP  > Datatype.option_map
   13.15 -    THE         > Datatype.the
   13.16 +    NONE        > Option.option.None
   13.17 +    SOME        > Option.option.Some
   13.18 +    option_case > Option.option.option_case
   13.19 +    OPTION_MAP  > Option.map
   13.20 +    THE         > Option.the
   13.21      IS_SOME     > HOL4Compat.IS_SOME
   13.22      IS_NONE     > HOL4Compat.IS_NONE
   13.23      OPTION_JOIN > HOL4Compat.OPTION_JOIN;
    14.1 --- a/src/HOL/Import/HOL4Compat.thy	Tue Mar 03 17:05:18 2009 +0100
    14.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Mar 04 10:47:20 2009 +0100
    14.3 @@ -73,7 +73,7 @@
    14.4  lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
    14.5    by simp
    14.6  
    14.7 -lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)"
    14.8 +lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
    14.9    by simp
   14.10  
   14.11  consts
    15.1 --- a/src/HOL/IsaMakefile	Tue Mar 03 17:05:18 2009 +0100
    15.2 +++ b/src/HOL/IsaMakefile	Wed Mar 04 10:47:20 2009 +0100
    15.3 @@ -127,6 +127,7 @@
    15.4    Nat.thy \
    15.5    OrderedGroup.thy \
    15.6    Orderings.thy \
    15.7 +  Option.thy \
    15.8    Plain.thy \
    15.9    Power.thy \
   15.10    Predicate.thy \
    16.1 --- a/src/HOL/Library/AssocList.thy	Tue Mar 03 17:05:18 2009 +0100
    16.2 +++ b/src/HOL/Library/AssocList.thy	Wed Mar 04 10:47:20 2009 +0100
    16.3 @@ -429,7 +429,7 @@
    16.4  
    16.5  subsection {* @{const map_ran} *}
    16.6  
    16.7 -lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
    16.8 +lemma map_ran_conv: "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
    16.9    by (induct al) auto
   16.10  
   16.11  lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
    17.1 --- a/src/HOL/Library/RBT.thy	Tue Mar 03 17:05:18 2009 +0100
    17.2 +++ b/src/HOL/Library/RBT.thy	Wed Mar 04 10:47:20 2009 +0100
    17.3 @@ -891,7 +891,7 @@
    17.4  theorem mapwk_isrbt[simp]: "isrbt (mapwithkey f t) = isrbt t" 
    17.5  unfolding isrbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_st mapwk_treec)
    17.6  
    17.7 -theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = option_map (f x) (map_of t x)"
    17.8 +theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = Option.map (f x) (map_of t x)"
    17.9  by (induct t) auto
   17.10  
   17.11  definition map
   17.12 @@ -899,7 +899,7 @@
   17.13  
   17.14  theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
   17.15  theorem map_isrbt[simp]: "isrbt (map f t) = isrbt t" unfolding map_def by simp
   17.16 -theorem map_of_map[simp]: "map_of (map f t) = option_map f o map_of t"
   17.17 +theorem map_of_map[simp]: "map_of (map f t) = Option.map f o map_of t"
   17.18    by (rule ext) (simp add:map_def)
   17.19  
   17.20  subsection {* Fold *}
    18.1 --- a/src/HOL/Map.thy	Tue Mar 03 17:05:18 2009 +0100
    18.2 +++ b/src/HOL/Map.thy	Wed Mar 04 10:47:20 2009 +0100
    18.3 @@ -242,17 +242,17 @@
    18.4    "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
    18.5  by (induct xs) auto
    18.6  
    18.7 -lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
    18.8 +lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = Option.map f (map_of xs x)"
    18.9  by (induct xs) auto
   18.10  
   18.11  
   18.12 -subsection {* @{term [source] option_map} related *}
   18.13 +subsection {* @{const Option.map} related *}
   18.14  
   18.15 -lemma option_map_o_empty [simp]: "option_map f o empty = empty"
   18.16 +lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
   18.17  by (rule ext) simp
   18.18  
   18.19  lemma option_map_o_map_upd [simp]:
   18.20 -  "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   18.21 +  "Option.map f o m(a|->b) = (Option.map f o m)(a|->f b)"
   18.22  by (rule ext) simp
   18.23  
   18.24  
    19.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Tue Mar 03 17:05:18 2009 +0100
    19.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Mar 04 10:47:20 2009 +0100
    19.3 @@ -105,7 +105,7 @@
    19.4         (xcpt_names (i,G,pc,et))"
    19.5  
    19.6    norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
    19.7 -  "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
    19.8 +  "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))"
    19.9  
   19.10    eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"
   19.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)"
    20.1 --- a/src/HOL/MicroJava/BV/Opt.thy	Tue Mar 03 17:05:18 2009 +0100
    20.2 +++ b/src/HOL/MicroJava/BV/Opt.thy	Wed Mar 04 10:47:20 2009 +0100
    20.3 @@ -286,8 +286,8 @@
    20.4  
    20.5  lemma option_map_in_optionI:
    20.6    "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
    20.7 -  \<Longrightarrow> option_map f ox : opt S";
    20.8 -apply (unfold option_map_def)
    20.9 +  \<Longrightarrow> Option.map f ox : opt S";
   20.10 +apply (unfold Option.map_def)
   20.11  apply (simp split: option.split)
   20.12  apply blast
   20.13  done 
    21.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue Mar 03 17:05:18 2009 +0100
    21.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Wed Mar 04 10:47:20 2009 +0100
    21.3 @@ -126,11 +126,11 @@
    21.4  by (induct xs,auto)
    21.5  
    21.6  lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow>
    21.7 -  map_of (map f xs) a = option_map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
    21.8 +  map_of (map f xs) a = Option.map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
    21.9  by (induct xs, auto)
   21.10  
   21.11 -lemma option_map_of [simp]: "(option_map f (map_of xs k) = None) = ((map_of xs k) = None)"
   21.12 -by (simp add: option_map_def split: option.split)
   21.13 +lemma option_map_of [simp]: "(Option.map f (map_of xs k) = None) = ((map_of xs k) = None)"
   21.14 +by (simp add: Option.map_def split: option.split)
   21.15  
   21.16  
   21.17  
    22.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Mar 03 17:05:18 2009 +0100
    22.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Mar 04 10:47:20 2009 +0100
    22.3 @@ -553,7 +553,7 @@
    22.4  
    22.5  lemma match_xctable_offset: "
    22.6    (match_exception_table G cn (pc + n) (offset_xctable n et)) =
    22.7 -  (option_map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
    22.8 +  (Option.map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
    22.9  apply (induct et)
   22.10  apply (simp add: offset_xctable_def)+
   22.11  apply (case_tac "match_exception_entry G cn pc a")
   22.12 @@ -675,7 +675,7 @@
   22.13          in app_jumps_lem)
   22.14    apply (simp add: nth_append)+
   22.15      (* subgoal \<exists> st. mt ! pc'' = Some st *)
   22.16 -  apply (simp add: norm_eff_def option_map_def nth_append)
   22.17 +  apply (simp add: norm_eff_def Option.map_def nth_append)
   22.18    apply (case_tac "mt ! pc''")
   22.19  apply simp+
   22.20  done
    23.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue Mar 03 17:05:18 2009 +0100
    23.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Mar 04 10:47:20 2009 +0100
    23.3 @@ -271,7 +271,7 @@
    23.4  lemma map_of_map_fst: "\<lbrakk> inj f;
    23.5    \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
    23.6    \<Longrightarrow>  map_of (map g xs) k 
    23.7 -  = option_map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
    23.8 +  = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
    23.9  apply (induct xs)
   23.10  apply simp
   23.11  apply (simp del: split_paired_All)
   23.12 @@ -288,13 +288,13 @@
   23.13  
   23.14  lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   23.15    ((method (comp G, C) S) = 
   23.16 -  option_map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
   23.17 +  Option.map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
   23.18               (method (G, C) S))"
   23.19  apply (simp add: method_def)
   23.20  apply (frule wf_subcls1)
   23.21  apply (simp add: comp_class_rec)
   23.22  apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
   23.23 -apply (rule_tac R="%x y. ((x S) = (option_map (\<lambda>(D, rT, b). 
   23.24 +apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
   23.25    (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   23.26    in class_rec_relation)
   23.27  apply assumption
    24.1 --- a/src/HOL/MicroJava/J/Conform.thy	Tue Mar 03 17:05:18 2009 +0100
    24.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Wed Mar 04 10:47:20 2009 +0100
    24.3 @@ -17,7 +17,7 @@
    24.4  
    24.5    conf :: "'c prog => aheap => val => ty => bool" 
    24.6                                     ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
    24.7 - "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    24.8 + "G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    24.9  
   24.10    lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
   24.11                                     ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
    25.1 --- a/src/HOL/MicroJava/J/Exceptions.thy	Tue Mar 03 17:05:18 2009 +0100
    25.2 +++ b/src/HOL/MicroJava/J/Exceptions.thy	Wed Mar 04 10:47:20 2009 +0100
    25.3 @@ -21,7 +21,7 @@
    25.4    cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
    25.5  
    25.6  translations
    25.7 -  "cname_of hp v" == "fst (the (hp (the_Addr v)))"
    25.8 +  "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))"
    25.9  
   25.10  
   25.11  constdefs
    26.1 --- a/src/HOL/MicroJava/J/State.thy	Tue Mar 03 17:05:18 2009 +0100
    26.2 +++ b/src/HOL/MicroJava/J/State.thy	Wed Mar 04 10:47:20 2009 +0100
    26.3 @@ -41,7 +41,7 @@
    26.4    "Norm s" == "(None,s)"
    26.5    "abrupt"     => "fst"
    26.6    "store"      => "snd"
    26.7 - "lookup_obj s a'"  == "the (heap s (the_Addr a'))"
    26.8 + "lookup_obj s a'"  == "CONST the (heap s (the_Addr a'))"
    26.9  
   26.10  
   26.11  constdefs
    27.1 --- a/src/HOL/NanoJava/State.thy	Tue Mar 03 17:05:18 2009 +0100
    27.2 +++ b/src/HOL/NanoJava/State.thy	Wed Mar 04 10:47:20 2009 +0100
    27.3 @@ -33,7 +33,7 @@
    27.4  constdefs
    27.5  
    27.6    init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
    27.7 - "init_vars m == option_map (\<lambda>T. Null) o m"
    27.8 + "init_vars m == Option.map (\<lambda>T. Null) o m"
    27.9    
   27.10  text {* private: *}
   27.11  types	heap   = "loc   \<rightharpoonup> obj"
    28.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 03 17:05:18 2009 +0100
    28.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 04 10:47:20 2009 +0100
    28.3 @@ -539,7 +539,7 @@
    28.4          thy
    28.5          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    28.6          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    28.7 -        |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    28.8 +        |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    28.9          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   28.10          |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   28.11          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   28.12 @@ -606,7 +606,7 @@
   28.13           |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   28.14                                       (fs_proof fs_thm_nprod) 
   28.15           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   28.16 -         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   28.17 +         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   28.18          end) ak_names thy20;
   28.19  
   28.20         (********  cp_<ak>_<ai> class instances  ********)
   28.21 @@ -687,7 +687,7 @@
   28.22           |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   28.23           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   28.24           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   28.25 -         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   28.26 +         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   28.27           |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   28.28          end) ak_names thy) ak_names thy25;
   28.29