--- a/src/HOL/Bali/Basis.thy Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/Bali/Basis.thy Thu Aug 09 15:52:42 2007 +0200
@@ -236,7 +236,7 @@
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
translations
- "option"<= (type) "Option.option"
+ "option"<= (type) "Datatype.option"
"list" <= (type) "List.list"
"sum3" <= (type) "Basis.sum3"
--- a/src/HOL/Bali/Table.thy Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/Bali/Table.thy Thu Aug 09 15:52:42 2007 +0200
@@ -44,7 +44,7 @@
translations
"table_of" == "map_of"
- (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Option.option"
+ (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
(type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
(* ### To map *)
--- a/src/HOL/Datatype.thy Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/Datatype.thy Thu Aug 09 15:52:42 2007 +0200
@@ -539,9 +539,23 @@
subsection {* Representing primitive types *}
+rep_datatype bool
+ distinct True_not_False False_not_True
+ induction bool_induct
+
declare case_split [cases type: bool]
-- "prefer plain propositional version"
+lemma size_bool [code func]:
+ "size (b\<Colon>bool) = 0" by (cases b) auto
+
+rep_datatype unit
+ induction unit_induct
+
+rep_datatype prod
+ inject Pair_eq
+ induction prod_induct
+
lemmas prod_caseI = prod.cases [THEN iffD2, standard]
lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
@@ -568,6 +582,14 @@
lemmas [code inline] = prod_case_split [symmetric]
+rep_datatype sum
+ distinct Inl_not_Inr Inr_not_Inl
+ inject Inl_eq Inr_eq
+ induction sum_induct
+
+lemma size_sum [code func]:
+ "size (x \<Colon> 'a + 'b) = 0" by (cases x) auto
+
lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
by (rule ext) (simp split: sum.split)
@@ -655,4 +677,125 @@
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
by (cases x) blast
+
+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
+
+
+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
+
+ML_setup {* change_claset (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
+
+
+constdefs
+ option_map :: "('a => 'b) => ('a option => 'b option)"
+ "option_map == %f y. case y of None => None | Some x => Some (f x)"
+
+lemmas [code func del] = option_map_def
+
+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 "op = \<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
+
+code_modulename SML
+ Datatype Nat
+
+code_modulename OCaml
+ Datatype Nat
+
+code_modulename Haskell
+ Datatype Nat
+
end
--- a/src/HOL/Extraction.thy Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/Extraction.thy Thu Aug 09 15:52:42 2007 +0200
@@ -6,7 +6,7 @@
header {* Program extraction for HOL *}
theory Extraction
-imports Datatype Option
+imports Datatype
uses "Tools/rewrite_hol_proof.ML"
begin
--- a/src/HOL/Finite_Set.thy Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/Finite_Set.thy Thu Aug 09 15:52:42 2007 +0200
@@ -7,7 +7,7 @@
header {* Finite sets *}
theory Finite_Set
-imports IntDef Divides Option
+imports IntDef Divides
begin
subsection {* Definition and basic properties *}
--- a/src/HOL/FunDef.thy Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/FunDef.thy Thu Aug 09 15:52:42 2007 +0200
@@ -6,7 +6,7 @@
header {* General recursive function definitions *}
theory FunDef
-imports Datatype Option Accessible_Part
+imports Datatype Accessible_Part
uses
("Tools/function_package/fundef_lib.ML")
("Tools/function_package/fundef_common.ML")
--- a/src/HOL/IsaMakefile Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/IsaMakefile Thu Aug 09 15:52:42 2007 +0200
@@ -88,7 +88,7 @@
Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy \
Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \
Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \
- Numeral.thy Option.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
+ Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \
Record.thy Refute.thy Relation.thy Relation_Power.thy \
Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \
@@ -223,7 +223,7 @@
Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
Library/SCT_Examples.thy Library/sct.ML \
Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \
- Library/Pretty_Char.thy Library/Pretty_Char_chr.thy
+ Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy
@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
@@ -648,7 +648,7 @@
ex/BT.thy ex/BinEx.thy ex/CTL.thy \
ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \
ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
- ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
+ ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Aug 09 15:52:38 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Aug 09 15:52:42 2007 +0200
@@ -456,7 +456,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 ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+ |> AxClass.prove_arity ("Datatype.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])
@@ -524,7 +524,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 ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+ |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
end) ak_names thy20;
(******** cp_<ak>_<ai> class instances ********)
@@ -607,7 +607,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 ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+ |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
|> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
|> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
end) ak_names thy) ak_names thy25;
--- a/src/HOL/Option.thy Thu Aug 09 15:52:38 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(* Title: HOL/Datatype.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* The option datatype *}
-
-theory Option
-imports Datatype
-begin
-
-subsection {* Type declaration *}
-
-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
-
-
-subsection {* 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
-
-ML_setup {* change_claset (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
-
-
-constdefs
- option_map :: "('a => 'b) => ('a option => 'b option)"
- [code func 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)
-
-
-subsection {* 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 "op = \<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