--- a/NEWS Wed Mar 04 15:32:57 2009 +0100
+++ b/NEWS Wed Mar 04 15:33:07 2009 +0100
@@ -501,7 +501,7 @@
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.
+Renamed option_map to Option.map, and o2s to Option.set.
* Library/Nat_Infinity: added addition, numeral syntax and more
instantiations for algebraic structures. Removed some duplicate
--- a/src/HOL/Library/Code_Index.thy Wed Mar 04 15:32:57 2009 +0100
+++ b/src/HOL/Library/Code_Index.thy Wed Mar 04 15:33:07 2009 +0100
@@ -87,12 +87,14 @@
then show "P k" by simp
qed simp_all
-lemmas [code del] = index.recs index.cases
-
declare index_case [case_names nat, cases type: index]
declare index.induct [case_names nat, induct type: index]
-lemma [code]:
+lemma index_decr [termination_simp]:
+ "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
+ by (cases k) simp
+
+lemma [simp, code]:
"index_size = nat_of"
proof (rule ext)
fix k
@@ -102,7 +104,7 @@
finally show "index_size k = nat_of k" .
qed
-lemma [code]:
+lemma [simp, code]:
"size = nat_of"
proof (rule ext)
fix k
@@ -110,6 +112,8 @@
by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
qed
+lemmas [code del] = index.recs index.cases
+
lemma [code]:
"eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
by (cases k, cases l) (simp add: eq)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Option.thy Wed Mar 04 15:33:07 2009 +0100
@@ -0,0 +1,124 @@
+(* Title: HOL/Option.thy
+ Author: Folklore
+*)
+
+header {* Datatype option *}
+
+theory Option
+imports Datatype
+begin
+
+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 *}
+
+primrec the :: "'a option => 'a" where
+"the (Some x) = x"
+
+primrec set :: "'a option => 'a set" where
+"set None = {}" |
+"set (Some x) = {x}"
+
+lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
+ by simp
+
+declaration {* fn _ =>
+ Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
+*}
+
+lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
+ by (cases xo) auto
+
+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
+ [code del]: "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 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 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 option_map_comp:
+ "map f (map g opt) = map (f o g) opt"
+ by (simp add: map_def split add: option.split)
+
+lemma option_map_o_sum_case [simp]:
+ "map f o sum_case g h = sum_case (map f o g) (map f o h)"
+ by (rule ext) (simp split: sum.split)
+
+
+hide (open) const set map
+
+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/Statespace/state_space.ML Wed Mar 04 15:32:57 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Wed Mar 04 15:33:07 2009 +0100
@@ -611,7 +611,7 @@
Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
| NONE =>
if get_silent (Context.Proof ctxt)
- then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
+ then Syntax.const "StateFun.lookup" $ Syntax.const "undefined" $ Syntax.free n $ s
else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
@@ -637,8 +637,8 @@
| NONE =>
if get_silent (Context.Proof ctxt)
then Syntax.const "StateFun.update"$
- Syntax.const "arbitrary"$Syntax.const "arbitrary"$
- Syntax.free n$(Syntax.const KN $ v)$s
+ Syntax.const "undefined" $ Syntax.const "undefined" $
+ Syntax.free n $ (Syntax.const KN $ v) $ s
else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
end;
--- a/src/HOL/Tools/datatype_package.ML Wed Mar 04 15:32:57 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 04 15:33:07 2009 +0100
@@ -629,14 +629,6 @@
(** a datatype antiquotation **)
-local
-
-val sym_datatype = Pretty.command "datatype";
-val sym_binder = Pretty.str "\\ {\\isacharequal}"; (*FIXME use proper symbol*)
-val sym_sep = Pretty.str "{\\isacharbar}\\ ";
-
-in
-
fun args_datatype (ctxt, args) =
let
val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
@@ -654,26 +646,19 @@
in if member (op =) s " " then Pretty.enclose "(" ")" [p]
else p
end;
- fun pretty_constr (co, []) =
- Syntax.pretty_term ctxt (Const (co, ty))
- | pretty_constr (co, [ty']) =
- (Pretty.block o Pretty.breaks)
- [Syntax.pretty_term ctxt (Const (co, ty' --> ty)),
- pretty_typ_br ty']
- | pretty_constr (co, tys) =
- (Pretty.block o Pretty.breaks)
- (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_br tys);
+ fun pretty_constr (co, tys) =
+ (Pretty.block o Pretty.breaks)
+ (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+ map pretty_typ_br tys);
in
Pretty.block
- (sym_datatype :: Pretty.brk 1 ::
+ (Pretty.command "datatype" :: Pretty.brk 1 ::
Syntax.pretty_typ ctxt ty ::
- sym_binder :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, sym_sep]
+ Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
(map (single o pretty_constr) cos)))
end
-end;
(** package setup **)
--- a/src/Pure/axclass.ML Wed Mar 04 15:32:57 2009 +0100
+++ b/src/Pure/axclass.ML Wed Mar 04 15:33:07 2009 +0100
@@ -234,7 +234,10 @@
val map_inst_params = AxClassData.map o apsnd o apsnd;
fun get_inst_param thy (c, tyco) =
- (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco;
+ case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
+ of SOME c' => c'
+ | NONE => error ("No instance parameter for constant " ^ quote c
+ ^ " on type constructor " ^ quote tyco);
fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))