--- a/src/HOL/Bali/Basis.thy Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Aug 07 09:38:44 2007 +0200
@@ -238,7 +238,7 @@
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
translations
- "option"<= (type) "Datatype.option"
+ "option"<= (type) "Option.option"
"list" <= (type) "List.list"
"sum3" <= (type) "Basis.sum3"
--- a/src/HOL/Datatype.thy Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/Datatype.thy Tue Aug 07 09:38:44 2007 +0200
@@ -529,30 +529,19 @@
subsection {* Finishing the datatype package setup *}
-text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
setup "DatatypeCodegen.setup_hooks"
+text {* hides popular names *}
+hide (open) type node item
hide (open) const Push Node Atom Leaf Numb Lim Split Case
-hide (open) type node item
section {* Datatypes *}
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"
-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"
@@ -573,10 +562,11 @@
declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
declare prod_caseE' [elim!] prod_caseE [elim!]
-rep_datatype sum
- distinct Inl_not_Inr Inr_not_Inl
- inject Inl_eq Inr_eq
- induction sum_induct
+lemma prod_case_split [code post]:
+ "prod_case = split"
+ by (auto simp add: expand_fun_eq)
+
+lemmas [code inline] = prod_case_split [symmetric]
lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
by (rule ext) (simp split: sum.split)
@@ -665,118 +655,4 @@
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
by (cases x) blast
-
-subsection {* The option type *}
-
-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)"
- [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)
-
-
-subsubsection {* Code generator setup *}
-
-definition
- is_none :: "'a option \<Rightarrow> bool" where
- is_none_none [normal 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
-
-lemma split_is_prod_case [code inline]:
- "split = prod_case"
- by (simp add: expand_fun_eq split_def prod.cases)
-
-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
--- a/src/HOL/Extraction.thy Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/Extraction.thy Tue Aug 07 09:38:44 2007 +0200
@@ -6,7 +6,7 @@
header {* Program extraction for HOL *}
theory Extraction
-imports Datatype
+imports Datatype Option
uses "Tools/rewrite_hol_proof.ML"
begin
--- a/src/HOL/FunDef.thy Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/FunDef.thy Tue Aug 07 09:38:44 2007 +0200
@@ -6,7 +6,7 @@
header {* General recursive function definitions *}
theory FunDef
-imports Datatype Accessible_Part
+imports Datatype Option Accessible_Part
uses
("Tools/function_package/fundef_lib.ML")
("Tools/function_package/fundef_common.ML")
--- a/src/HOL/IsaMakefile Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 07 09:38:44 2007 +0200
@@ -82,13 +82,13 @@
$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
$(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML $(SRC)/Tools/Metis/metis.ML\
- $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \
+ $(SRC)/Tools/nbe.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \
Accessible_Part.thy Arith_Tools.thy Datatype.thy \
Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy \
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 OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
+ Numeral.thy Option.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 \
--- a/src/HOL/Nat.thy Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/Nat.thy Tue Aug 07 09:38:44 2007 +0200
@@ -68,7 +68,7 @@
less_def: "m < n == (m, n) : pred_nat^+"
le_def: "m \<le> (n::nat) == ~ (n < m)" ..
-lemmas [code func del] = less_def le_def
+lemmas [code func del] = Zero_nat_def One_nat_def less_def le_def
text {* Induction *}
@@ -114,7 +114,24 @@
class size = type +
fixes size :: "'a \<Rightarrow> nat"
-text {* @{typ nat} is a datatype *}
+text {* now we are ready to re-invent primitive types
+ -- dependency on class size is hardwired into datatype package *}
+
+rep_datatype bool
+ distinct True_not_False False_not_True
+ induction bool_induct
+
+rep_datatype unit
+ induction unit_induct
+
+rep_datatype prod
+ inject Pair_eq
+ induction prod_induct
+
+rep_datatype sum
+ distinct Inl_not_Inr Inr_not_Inl
+ inject Inl_eq Inr_eq
+ induction sum_induct
rep_datatype nat
distinct Suc_not_Zero Zero_not_Suc
@@ -130,7 +147,6 @@
lemmas nat_case_0 = nat.cases(1)
and nat_case_Suc = nat.cases(2)
-
lemma n_not_Suc_n: "n \<noteq> Suc n"
by (induct n) simp_all
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Aug 07 09:38:44 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 ("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])
@@ -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 ("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 ********)
@@ -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 ("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)
|> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
end) ak_names thy) ak_names thy25;
--- a/src/HOL/Product_Type.thy Tue Aug 07 09:38:43 2007 +0200
+++ b/src/HOL/Product_Type.thy Tue Aug 07 09:38:44 2007 +0200
@@ -104,9 +104,9 @@
Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)"
fst_def: "fst p == THE a. EX b. p = Pair a b"
snd_def: "snd p == THE b. EX a. p = Pair a b"
- split_def [code func]: "split == (%c p. c (fst p) (snd p))"
- curry_def [code func]: "curry == (%c x y. c (Pair x y))"
- prod_fun_def [code func]: "prod_fun f g == split (%x y. Pair (f x) (g y))"
+ split_def: "split == (%c p. c (fst p) (snd p))"
+ curry_def: "curry == (%c x y. c (Pair x y))"
+ prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
Sigma_def [code func]: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
abbreviation
@@ -337,7 +337,7 @@
lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
by (simp add: curry_def)
-lemma curry_conv [simp]: "curry f a b = f (a,b)"
+lemma curry_conv [simp, code func]: "curry f a b = f (a,b)"
by (simp add: curry_def)
lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
@@ -346,7 +346,7 @@
lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
by fast
-lemma split_conv [simp]: "split c (a, b) = c a b"
+lemma split_conv [simp, code func]: "split c (a, b) = c a b"
by (simp add: split_def)
lemmas split = split_conv -- {* for backwards compatibility *}
@@ -569,7 +569,7 @@
functions.
*}
-lemma prod_fun [simp]: "prod_fun f g (a, b) = (f a, g b)"
+lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
by (simp add: prod_fun_def)
lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
@@ -754,6 +754,8 @@
internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
"internal_split == split"
+lemmas [code func del] = internal_split_def
+
lemma internal_split_conv: "internal_split c (a, b) = c a b"
by (simp only: internal_split_def split_conv)
@@ -908,7 +910,6 @@
Codegen.add_codegen "let_codegen" let_codegen
#> Codegen.add_codegen "split_codegen" split_codegen
- #> CodegenPackage.add_appconst ("Let", CodegenPackage.appgen_let)
end
*}