# HG changeset patch # User haftmann # Date 1186472324 -7200 # Node ID 8dfd5dd65d82c4aed9702979697d4c243b6376eb # Parent 09027ee4eeaa108ba5969236222d7956ae566439 split off theory Option for benefit of code generator diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/Bali/Basis.thy --- 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" diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/Datatype.thy --- 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 \ bool" where - is_none_none [normal post, symmetric, code inline]: "is_none x \ x = None" - -lemma is_none_code [code]: - shows "is_none None \ True" - and "is_none (Some x) \ 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 = \ 'a\eq option \ 'a option \ bool" - (Haskell infixl 4 "==") - -code_reserved SML - option NONE SOME - -code_reserved OCaml - option None Some - end diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/Extraction.thy --- 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 diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/FunDef.thy --- 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") diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/IsaMakefile --- 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 \ diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/Nat.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 \ (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 \ 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 \ Suc n" by (induct n) simp_all diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/Nominal/nominal_atoms.ML --- 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__ 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; diff -r 09027ee4eeaa -r 8dfd5dd65d82 src/HOL/Product_Type.thy --- 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 *}