# HG changeset patch # User haftmann # Date 1190715368 -7200 # Node ID c6674504103f65c716bba8120b88951cfb616eec # Parent 9800a76026291a8c95be28177d9243742d3c9b2d datatype interpretators for size and datatype_realizer diff -r 9800a7602629 -r c6674504103f NEWS --- a/NEWS Tue Sep 25 10:27:43 2007 +0200 +++ b/NEWS Tue Sep 25 12:16:08 2007 +0200 @@ -517,6 +517,11 @@ *** HOL *** +* Internal reorganisation of `size' of datatypes: + - size theorems "foo.size" are no longer subsumed by "foo.simps" (but are still + simplification rules by default!) + - theorems "prod.size" now named "*.size" + * The transitivity reasoner for partial and linear orders is set up for locales `order' and `linorder' generated by the new class package. Previously the reasoner was only set up for axiomatic type classes. Instances of the diff -r 9800a7602629 -r c6674504103f src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Datatype.thy Tue Sep 25 12:16:08 2007 +0200 @@ -9,7 +9,7 @@ header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} theory Datatype -imports Nat Sum_Type +imports Nat begin typedef (Node) @@ -537,52 +537,7 @@ 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" - -lemma size_bool [code func]: - "size (b\bool) = 0" by (cases b) auto - -rep_datatype unit - induction unit_induct - -rep_datatype prod - inject Pair_eq - induction prod_induct - -declare prod.size [noatp] - -lemmas prod_caseI = prod.cases [THEN iffD2, standard] - -lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" - by auto - -lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" - by (auto simp: split_tupled_all) - -lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" - by (induct p) auto - -lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" - by (induct p) auto - -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" - by (simp add: expand_fun_eq) - -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] -declare prod_caseE' [elim!] prod_caseE [elim!] - -lemma prod_case_split [code post]: - "prod_case = split" - by (auto simp add: expand_fun_eq) - -lemmas [code inline] = prod_case_split [symmetric] +subsection {* Representing sums *} rep_datatype sum distinct Inl_not_Inr Inr_not_Inl @@ -637,49 +592,6 @@ hide (open) const Suml Sumr -subsection {* Further cases/induct rules for tuples *} - -lemma prod_cases3 [cases type]: - obtains (fields) a b c where "y = (a, b, c)" - by (cases y, case_tac b) blast - -lemma prod_induct3 [case_names fields, induct type]: - "(!!a b c. P (a, b, c)) ==> P x" - by (cases x) blast - -lemma prod_cases4 [cases type]: - obtains (fields) a b c d where "y = (a, b, c, d)" - by (cases y, case_tac c) blast - -lemma prod_induct4 [case_names fields, induct type]: - "(!!a b c d. P (a, b, c, d)) ==> P x" - by (cases x) blast - -lemma prod_cases5 [cases type]: - obtains (fields) a b c d e where "y = (a, b, c, d, e)" - by (cases y, case_tac d) blast - -lemma prod_induct5 [case_names fields, induct type]: - "(!!a b c d e. P (a, b, c, d, e)) ==> P x" - by (cases x) blast - -lemma prod_cases6 [cases type]: - obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" - by (cases y, case_tac e) blast - -lemma prod_induct6 [case_names fields, induct type]: - "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" - by (cases x) blast - -lemma prod_cases7 [cases type]: - obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" - by (cases y, case_tac f) blast - -lemma prod_induct7 [case_names fields, induct type]: - "(!!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 diff -r 9800a7602629 -r c6674504103f src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/FunDef.thy Tue Sep 25 12:16:08 2007 +0200 @@ -6,7 +6,7 @@ header {* General recursive function definitions *} theory FunDef -imports Datatype Accessible_Part +imports Accessible_Part uses ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/fundef_common.ML") @@ -103,7 +103,7 @@ use "Tools/function_package/auto_term.ML" use "Tools/function_package/fundef_package.ML" -setup FundefPackage.setup +setup {* FundefPackage.setup *} lemma let_cong [fundef_cong]: "M = N \ (\x. x = N \ f x = g x) \ Let M f = Let N g" diff -r 9800a7602629 -r c6674504103f src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Inductive.thy Tue Sep 25 12:16:08 2007 +0200 @@ -6,18 +6,17 @@ header {* Support for inductive sets and types *} theory Inductive -imports FixedPoint Product_Type Sum_Type +imports FixedPoint Sum_Type uses ("Tools/inductive_package.ML") - ("Tools/inductive_set_package.ML") - ("Tools/inductive_realizer.ML") + (*("Tools/inductive_set_package.ML") + ("Tools/inductive_realizer.ML")*) "Tools/dseq.ML" ("Tools/inductive_codegen.ML") ("Tools/datatype_aux.ML") ("Tools/datatype_prop.ML") ("Tools/datatype_rep_proofs.ML") ("Tools/datatype_abs_proofs.ML") - ("Tools/datatype_realizer.ML") ("Tools/datatype_case.ML") ("Tools/datatype_package.ML") ("Tools/datatype_codegen.ML") @@ -108,25 +107,15 @@ use "Tools/datatype_rep_proofs.ML" use "Tools/datatype_abs_proofs.ML" use "Tools/datatype_case.ML" -use "Tools/datatype_realizer.ML" - use "Tools/datatype_package.ML" setup DatatypePackage.setup - +use "Tools/primrec_package.ML" use "Tools/datatype_codegen.ML" setup DatatypeCodegen.setup -use "Tools/inductive_realizer.ML" -setup InductiveRealizer.setup - use "Tools/inductive_codegen.ML" setup InductiveCodegen.setup -use "Tools/primrec_package.ML" - -use "Tools/inductive_set_package.ML" -setup InductiveSetPackage.setup - text{* Lambda-abstractions with pattern matching: *} syntax diff -r 9800a7602629 -r c6674504103f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/IsaMakefile Tue Sep 25 12:16:08 2007 +0200 @@ -123,7 +123,8 @@ Tools/function_package/inductive_wrap.ML \ Tools/function_package/lexicographic_order.ML \ Tools/function_package/mutual.ML \ - Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML \ + Tools/function_package/pattern_split.ML \ + Tools/function_package/size.ML Tools/inductive_codegen.ML \ Tools/inductive_package.ML Tools/inductive_realizer.ML \ Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML \ Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML \ diff -r 9800a7602629 -r c6674504103f src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Main.thy Tue Sep 25 12:16:08 2007 +0200 @@ -5,7 +5,7 @@ header {* Main HOL *} theory Main -imports Map +imports Map begin text {* diff -r 9800a7602629 -r c6674504103f src/HOL/MicroJava/Comp/CorrComp.thy --- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Sep 25 12:16:08 2007 +0200 @@ -118,7 +118,7 @@ apply (rule exec_all_trans) apply (simp only: append_Nil) apply (drule_tac x="[]" in spec) -apply (simp only: list.simps) +apply (simp only: list.simps list.size) apply blast apply (rule exec_instr_in_exec_all) apply auto diff -r 9800a7602629 -r c6674504103f src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Nat.thy Tue Sep 25 12:16:08 2007 +0200 @@ -16,6 +16,7 @@ ("arith_data.ML") "~~/src/Provers/Arith/fast_lin_arith.ML" ("Tools/lin_arith.ML") + ("Tools/function_package/size.ML") begin subsection {* Type @{text ind} *} @@ -111,9 +112,13 @@ text {* size of a datatype value *} +use "Tools/function_package/size.ML" + class size = type + fixes size :: "'a \ nat" +setup Size.setup + rep_datatype nat distinct Suc_not_Zero Zero_not_Suc inject Suc_Suc_eq @@ -1467,10 +1472,16 @@ by intro_classes (auto simp add: inf_nat_def sup_nat_def) -subsection {* Size function *} +subsection {* Size function declarations *} lemma nat_size [simp, code func]: "size (n\nat) = n" -by (induct n) simp_all + by (induct n) simp_all + +lemma size_bool [code func]: + "size (b\bool) = 0" by (cases b) auto + +declare "*.size" [noatp] + subsection {* legacy bindings *} diff -r 9800a7602629 -r c6674504103f src/HOL/PreList.thy --- a/src/HOL/PreList.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/PreList.thy Tue Sep 25 12:16:08 2007 +0200 @@ -25,4 +25,3 @@ setup ResAxioms.setup end - diff -r 9800a7602629 -r c6674504103f src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Product_Type.thy Tue Sep 25 12:16:08 2007 +0200 @@ -7,10 +7,24 @@ header {* Cartesian products *} theory Product_Type -imports Typedef Fun -uses ("Tools/split_rule.ML") +imports Inductive +uses + ("Tools/split_rule.ML") + ("Tools/inductive_set_package.ML") + ("Tools/inductive_realizer.ML") + ("Tools/datatype_realizer.ML") begin +subsection {* @{typ bool} is a datatype *} + +rep_datatype bool + distinct True_not_False False_not_True + induction bool_induct + +declare case_split [cases type: bool] + -- "prefer plain propositional version" + + subsection {* Unit *} typedef unit = "{True}" @@ -18,9 +32,10 @@ show "True : ?unit" .. qed -constdefs +definition Unity :: unit ("'(')") - "() == Abs_unit True" +where + "() = Abs_unit True" lemma unit_eq [noatp]: "u = ()" by (induct u) (simp add: unit_def Unity_def) @@ -32,23 +47,26 @@ ML_setup {* val unit_eq_proc = - let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in - Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"] + let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in + Simplifier.simproc @{theory} "unit_eq" ["x::unit"] (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq) end; Addsimprocs [unit_eq_proc]; *} +lemma unit_induct [noatp,induct type: unit]: "P () ==> P x" + by simp + +rep_datatype unit + induction unit_induct + lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()" by simp lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P" by (rule triv_forall_equality) -lemma unit_induct [noatp,induct type: unit]: "P () ==> P x" - by simp - text {* This rewrite counters the effect of @{text unit_eq_proc} on @{term [source] "%u::unit. f u"}, replacing it by @{term [source] @@ -84,7 +102,6 @@ local - subsubsection {* Definitions *} global @@ -343,6 +360,10 @@ lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x" by fast +rep_datatype prod + inject Pair_eq + induction prod_induct + lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" by fast @@ -765,6 +786,77 @@ setup SplitRule.setup + +lemmas prod_caseI = prod.cases [THEN iffD2, standard] + +lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" + by auto + +lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" + by (auto simp: split_tupled_all) + +lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" + by (induct p) auto + +lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" + by (induct p) auto + +lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" + by (simp add: expand_fun_eq) + +declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] +declare prod_caseE' [elim!] prod_caseE [elim!] + +lemma prod_case_split [code post]: + "prod_case = split" + by (auto simp add: expand_fun_eq) + +lemmas [code inline] = prod_case_split [symmetric] + + +subsection {* Further cases/induct rules for tuples *} + +lemma prod_cases3 [cases type]: + obtains (fields) a b c where "y = (a, b, c)" + by (cases y, case_tac b) blast + +lemma prod_induct3 [case_names fields, induct type]: + "(!!a b c. P (a, b, c)) ==> P x" + by (cases x) blast + +lemma prod_cases4 [cases type]: + obtains (fields) a b c d where "y = (a, b, c, d)" + by (cases y, case_tac c) blast + +lemma prod_induct4 [case_names fields, induct type]: + "(!!a b c d. P (a, b, c, d)) ==> P x" + by (cases x) blast + +lemma prod_cases5 [cases type]: + obtains (fields) a b c d e where "y = (a, b, c, d, e)" + by (cases y, case_tac d) blast + +lemma prod_induct5 [case_names fields, induct type]: + "(!!a b c d e. P (a, b, c, d, e)) ==> P x" + by (cases x) blast + +lemma prod_cases6 [cases type]: + obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" + by (cases y, case_tac e) blast + +lemma prod_induct6 [case_names fields, induct type]: + "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" + by (cases x) blast + +lemma prod_cases7 [cases type]: + obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" + by (cases y, case_tac f) blast + +lemma prod_induct7 [case_names fields, induct type]: + "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" + by (cases x) blast + + subsection {* Further lemmas *} lemma @@ -914,6 +1006,9 @@ end *} + +subsection {* Legacy bindings *} + ML {* val Collect_split = thm "Collect_split"; val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1"; @@ -1011,4 +1106,16 @@ val unit_induct = thm "unit_induct"; *} + +subsection {* Further inductive packages *} + +use "Tools/inductive_realizer.ML" +setup InductiveRealizer.setup + +use "Tools/inductive_set_package.ML" +setup InductiveSetPackage.setup + +use "Tools/datatype_realizer.ML" +setup DatatypeRealizer.setup + end diff -r 9800a7602629 -r c6674504103f src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 25 12:16:08 2007 +0200 @@ -10,8 +10,7 @@ - characteristic equations for primrec combinators - characteristic equations for case combinators - equations for splitting "P (case ...)" expressions - - datatype size function - - "nchotomy" and "case_cong" theorems for TFL + - "nchotomy" and "case_cong" theorems for TFL *) @@ -31,9 +30,6 @@ DatatypeAux.descr list -> (string * sort) list -> thm list list -> thm list list -> thm list -> thm list list -> theory -> (thm * thm) list * theory - val prove_size_thms : bool -> string list -> - DatatypeAux.descr list -> (string * sort) list -> - string list -> thm list -> theory -> thm list * theory val prove_nchotomys : string list -> DatatypeAux.descr list -> (string * sort) list -> thm list -> theory -> thm list * theory val prove_weak_case_congs : string list -> DatatypeAux.descr list -> @@ -381,83 +377,6 @@ |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2)) end; -(******************************* size functions *******************************) - -fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy = - if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => - is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) - (List.concat descr) - then - ([], thy) - else - let - val _ = message "Proving equations for size function ..."; - - val big_name = space_implode "_" new_type_names; - val thy1 = add_path flat_names big_name thy; - - val descr' = flat descr; - val recTs = get_rec_types descr' sorts; - - val Const (size_name, _) = HOLogic.size_const dummyT; - val size_names = replicate (length (hd descr)) size_name @ - map (Sign.full_name thy1) (DatatypeProp.indexify_names - (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)))); - val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names - (map (fn T => name_of_typ T ^ "_size") recTs)); - - fun plus (t1, t2) = - Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; - - fun make_sizefun (_, cargs) = - let - val Ts = map (typ_of_dtyp descr' sorts) cargs; - val k = length (filter is_rec_type cargs); - val t = if k = 0 then HOLogic.zero else - foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.Suc_zero]) - in - foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT) - end; - - val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr'; - val fTs = map fastype_of fs; - - fun instance_size_class tyco thy = - let - val n = Sign.arity_number thy tyco; - in - thy - |> Class.prove_instance (Class.intro_classes_tac []) - [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] [] - |> snd - end - - val (size_def_thms, thy') = - thy1 - |> Theory.add_consts_i (map (fn (s, T) => - (Sign.base_name s, T --> HOLogic.natT, NoSyn)) - (Library.drop (length (hd descr), size_names ~~ recTs))) - |> fold (fn (_, (name, _, _)) => instance_size_class name) descr' - |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) => - (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), - list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))) - (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) - ||> parent_path flat_names; - - val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; - - val size_thms = map (fn t => Goal.prove_global thy' [] [] t - (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) - (DatatypeProp.make_size descr sorts thy') - - in - thy' - |> Theory.add_path big_name - |> PureThy.add_thmss [(("size", size_thms), [])] - ||> Theory.parent_path - |-> (fn thmss => pair (flat thmss)) - end; - fun prove_weak_case_congs new_type_names descr sorts thy = let fun prove_weak_case_cong t = diff -r 9800a7602629 -r c6674504103f src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_aux.ML Tue Sep 25 12:16:08 2007 +0200 @@ -10,8 +10,6 @@ val quiet_mode : bool ref val message : string -> unit - val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a - val add_path : bool -> string -> theory -> theory val parent_path : bool -> theory -> theory @@ -72,9 +70,6 @@ val quiet_mode = ref false; fun message s = if !quiet_mode then () else writeln s; -(* FIXME: move to library ? *) -fun foldl1 f (x::xs) = Library.foldl f (x, xs); - fun add_path flat_names s = if flat_names then I else Theory.add_path s; fun parent_path flat_names = if flat_names then I else Theory.parent_path; @@ -184,6 +179,7 @@ type datatype_info = {index : int, + head_len : int, descr : descr, sorts : (string * sort) list, rec_names : string list, diff -r 9800a7602629 -r c6674504103f src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 25 12:16:08 2007 +0200 @@ -447,35 +447,6 @@ | get_spec thy (tyco, false) = TypecopyPackage.get_spec thy tyco; -fun codetypes_dependency thy = - let - val names = - map (rpair true) (Symtab.keys (DatatypePackage.get_datatypes thy)) - @ map (rpair false) (TypecopyPackage.get_typecopies thy); - fun add_node (name, is_dt) = - let - fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys - | add_tycos _ = I; - val tys = if is_dt then - (maps snd o snd o the o DatatypePackage.get_datatype_spec thy) name - else - [(#typ o the o TypecopyPackage.get_typecopy_info thy) name] - val deps = (filter (AList.defined (op =) names) o maps (fn ty => - add_tycos ty [])) tys; - in - Graph.default_node (name, ()) - #> fold (fn name' => - Graph.default_node (name', ()) - #> Graph.add_edge (name', name) - ) deps - end - in - Graph.empty - |> fold add_node names - |> Graph.strong_conn - |> map (AList.make (the o AList.lookup (op =) names)) - end; - local fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco of SOME _ => get_eq_datatype thy tyco @@ -515,7 +486,6 @@ hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy; in thy - |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy)) |> DatatypePackage.add_interpretator datatype_hook |> TypecopyPackage.add_interpretator typecopy_hook end; diff -r 9800a7602629 -r c6674504103f src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue Sep 25 12:16:08 2007 +0200 @@ -17,6 +17,16 @@ sig include BASIC_DATATYPE_PACKAGE val quiet_mode : bool ref + val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix * + (bstring * typ list * mixfix) list) list -> theory -> + {distinct : thm list list, + inject : thm list list, + exhaustion : thm list, + rec_thms : thm list, + case_thms : thm list list, + split_thms : (thm * thm) list, + induction : thm, + simps : thm list} * theory val add_datatype : bool -> string list -> (string list * bstring * mixfix * (bstring * string list * mixfix) list) list -> theory -> {distinct : thm list list, @@ -26,18 +36,6 @@ case_thms : thm list list, split_thms : (thm * thm) list, induction : thm, - size : thm list, - simps : thm list} * theory - val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix * - (bstring * typ list * mixfix) list) list -> theory -> - {distinct : thm list list, - inject : thm list list, - exhaustion : thm list, - rec_thms : thm list, - case_thms : thm list list, - split_thms : (thm * thm) list, - induction : thm, - size : thm list, simps : thm list} * theory val rep_datatype_i : string list option -> (thm list * attribute list) list list -> (thm list * attribute list) list list -> (thm list * attribute list) -> @@ -49,7 +47,6 @@ case_thms : thm list list, split_thms : (thm * thm) list, induction : thm, - size : thm list, simps : thm list} * theory val rep_datatype : string list option -> (thmref * Attrib.src list) list list -> (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> @@ -60,7 +57,6 @@ case_thms : thm list list, split_thms : (thm * thm) list, induction : thm, - size : thm list, simps : thm list} * theory val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table val get_datatype : theory -> string -> DatatypeAux.datatype_info option @@ -325,12 +321,12 @@ end; -fun add_rules simps case_thms size_thms rec_thms inject distinct +fun add_rules simps case_thms rec_thms inject distinct weak_case_congs cong_att = PureThy.add_thmss [(("simps", simps), []), - (("", flat case_thms @ size_thms @ + (("", flat case_thms @ flat distinct @ rec_thms), [Simplifier.simp_add]), - (("", size_thms @ rec_thms), [RecfunCodegen.add_default]), + (("", rec_thms), [RecfunCodegen.add_default]), (("", flat inject), [iff_add]), (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), (("", weak_case_congs), [cong_att])] @@ -460,11 +456,12 @@ (**** make datatype info ****) -fun make_dt_info descr sorts induct reccomb_names rec_thms +fun make_dt_info head_len descr sorts induct reccomb_names rec_thms (((((((((i, (_, (tname, _, _))), case_name), case_thms), exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) = (tname, {index = i, + head_len = head_len, descr = descr, sorts = sorts, rec_names = reccomb_names, @@ -522,9 +519,9 @@ val specify_consts = gen_specify_consts Sign.add_consts_i; val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic; -structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end); +structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string list; val eq = op = end); -fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator; +fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator (fold interpretator); fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy = @@ -534,10 +531,6 @@ val used = map fst (fold Term.add_tfreesT recTs []); val newTs = Library.take (length (hd descr), recTs); - val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists - (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) - cargs) constrs) descr'; - (**** declare new types and constants ****) val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); @@ -554,9 +547,6 @@ (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int) (1 upto (length descr'))); - val size_names = DatatypeProp.indexify_names - (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))); - val freeT = TFree (Name.variant used "'t", HOLogic.typeS); val case_fn_Ts = map (fn (i, (_, _, constrs)) => map (fn (_, cargs) => @@ -565,22 +555,11 @@ val case_names = map (fn s => (s ^ "_case")) new_type_names; - fun instance_size_class tyco thy = - let - val n = Sign.arity_number thy tyco; - in - thy - |> Class.prove_instance (Class.intro_classes_tac []) - [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] [] - |> snd - end - val thy2' = thy (** new types **) |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)]) types_syntax tyvars - |> fold (fn (_, (name, _, _)) => instance_size_class name) descr' |> add_path flat_names (space_implode "_" new_type_names) (** primrec combinators **) @@ -598,12 +577,6 @@ val thy2 = thy2' - (** size functions **) - - |> (if no_size then I else specify_consts (map (fn (s, T) => - (Sign.base_name s, T --> HOLogic.natT, NoSyn)) - (size_names ~~ Library.drop (length (hd descr), recTs)))) - (** constructors **) |> parent_path flat_names @@ -619,18 +592,15 @@ (**** introduction of axioms ****) val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2; - val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2; val ((([induct], [rec_thms]), inject), thy3) = thy2 |> Theory.add_path (space_implode "_" new_type_names) |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct] ||>> add_axioms "recs" rec_axs [] - ||> (if no_size then I else add_axioms "size" size_axs [] #> snd) ||> Theory.parent_path ||>> add_and_get_axiomss "inject" new_type_names (DatatypeProp.make_injs descr sorts); - val size_thms = if no_size then [] else get_thms thy3 (Name "size"); val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3; @@ -651,27 +621,27 @@ val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10; - val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms) + val dt_infos = map (make_dt_info (length (hd descr)) descr' sorts induct + reccomb_names' rec_thms) ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~ exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); - val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; + val simps = flat (distinct @ inject @ case_thms) @ rec_thms; val split_thms = split ~~ split_asm; val thy12 = thy11 |> add_case_tr' case_names' |> Theory.add_path (space_implode "_" new_type_names) - |> add_rules simps case_thms size_thms rec_thms inject distinct + |> add_rules simps case_thms rec_thms inject distinct weak_case_congs Simplifier.cong_add |> put_dt_infos dt_infos |> add_cases_induct dt_infos induct |> Theory.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd - |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> DatatypeInterpretator.add_those (map fst dt_infos); + |> DatatypeInterpretator.add_those [map fst dt_infos]; in ({distinct = distinct, inject = inject, @@ -680,7 +650,6 @@ case_thms = case_thms, split_thms = split_thms, induction = induct, - size = size_thms, simps = simps}, thy12) end; @@ -711,27 +680,25 @@ descr sorts nchotomys case_thms thy8; val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names descr sorts thy9; - val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names - descr sorts reccomb_names rec_thms thy10; - val dt_infos = map (make_dt_info (flat descr) sorts induct reccomb_names rec_thms) + val dt_infos = map (make_dt_info (length (hd descr)) (flat descr) sorts induct + reccomb_names rec_thms) ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~ casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); - val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; + val simps = flat (distinct @ inject @ case_thms) @ rec_thms; val thy12 = - thy11 + thy10 |> add_case_tr' case_names |> Theory.add_path (space_implode "_" new_type_names) - |> add_rules simps case_thms size_thms rec_thms inject distinct + |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs)) |> put_dt_infos dt_infos |> add_cases_induct dt_infos induct |> Theory.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd - |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> DatatypeInterpretator.add_those (map fst dt_infos); + |> DatatypeInterpretator.add_those [map fst dt_infos]; in ({distinct = distinct, inject = inject, @@ -740,7 +707,6 @@ case_thms = case_thms, split_thms = split_thms, induction = induct, - size = size_thms, simps = simps}, thy12) end; @@ -808,35 +774,32 @@ [descr] sorts nchotomys case_thms thy6; val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names [descr] sorts thy7; - val (size_thms, thy9) = - DatatypeAbsProofs.prove_size_thms false new_type_names - [descr] sorts reccomb_names rec_thms thy8; val ((_, [induction']), thy10) = - thy9 + thy8 |> store_thmss "inject" new_type_names inject ||>> store_thmss "distinct" new_type_names distinct ||> Theory.add_path (space_implode "_" new_type_names) ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])]; - val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms) + val dt_infos = map (make_dt_info (length descr) descr sorts induction' + reccomb_names rec_thms) ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); - val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms; + val simps = flat (distinct @ inject @ case_thms) @ rec_thms; val thy11 = thy10 |> add_case_tr' case_names - |> add_rules simps case_thms size_thms rec_thms inject distinct + |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs)) |> put_dt_infos dt_infos |> add_cases_induct dt_infos induction' |> Theory.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd - |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> DatatypeInterpretator.add_those (map fst dt_infos); + |> DatatypeInterpretator.add_those [map fst dt_infos]; in ({distinct = distinct, inject = inject, @@ -845,7 +808,6 @@ case_thms = case_thms, split_thms = split_thms, induction = induction', - size = size_thms, simps = simps}, thy11) end; diff -r 9800a7602629 -r c6674504103f src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_prop.ML Tue Sep 25 12:16:08 2007 +0200 @@ -24,8 +24,6 @@ (string * sort) list -> theory -> term list list val make_splits : string list -> DatatypeAux.descr list -> (string * sort) list -> theory -> (term * term) list - val make_size : DatatypeAux.descr list -> (string * sort) list -> - theory -> term list val make_weak_case_congs : string list -> DatatypeAux.descr list -> (string * sort) list -> theory -> term list val make_case_congs : string list -> DatatypeAux.descr list -> @@ -61,7 +59,6 @@ in indexify_names (map type_name Ts) end; - (************************* injectivity of constructors ************************) fun make_injs descr sorts = @@ -351,44 +348,6 @@ (make_case_combs new_type_names descr sorts thy "f")) end; - -(******************************* size functions *******************************) - -fun make_size descr sorts thy = - let - val descr' = flat descr; - val recTs = get_rec_types descr' sorts; - - val Const (size_name, _) = HOLogic.size_const dummyT; - val size_names = replicate (length (hd descr)) size_name @ - map (Sign.intern_const thy) (indexify_names - (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)))); - val size_consts = map (fn (s, T) => - Const (s, T --> HOLogic.natT)) (size_names ~~ recTs); - - fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; - - fun make_size_eqn size_const T (cname, cargs) = - let - val recs = filter is_rec_type cargs; - val Ts = map (typ_of_dtyp descr' sorts) cargs; - val recTs = map (typ_of_dtyp descr' sorts) recs; - val tnames = make_tnames Ts; - val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); - val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $ - Free (s, T)) (recs ~~ rec_tnames ~~ recTs); - val t = if ts = [] then HOLogic.zero else - foldl1 plus (ts @ [HOLogic.Suc_zero]) - in - HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $ - list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t)) - end - - in - List.concat (map (fn (((_, (_, _, constrs)), size_const), T) => - map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs)) - end; - (************************* additional rules for TFL ***************************) fun make_weak_case_congs new_type_names descr sorts thy = diff -r 9800a7602629 -r c6674504103f src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Tue Sep 25 10:27:43 2007 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Tue Sep 25 12:16:08 2007 +0200 @@ -8,8 +8,8 @@ signature DATATYPE_REALIZER = sig - val add_dt_realizers: (string * sort) list -> - DatatypeAux.datatype_info list -> theory -> theory + val add_dt_realizers: string list -> theory -> theory + val setup: theory -> theory end; structure DatatypeRealizer : DATATYPE_REALIZER = @@ -40,7 +40,7 @@ fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT); -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) (is, thy) = +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy = let val recTs = get_rec_types descr sorts; val pnames = if length descr = 1 then ["P"] @@ -160,7 +160,7 @@ in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) = +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy = let val cert = cterm_of thy; val rT = TFree ("'P", HOLogic.typeS); @@ -216,11 +216,18 @@ (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy' end; +fun add_dt_realizers names thy = + if !proofs < 2 then thy + else let + val _ = message "Adding realizers for induction and case analysis ..." + val infos = map (DatatypePackage.the_datatype thy) names; + val info :: _ = infos; + in + thy + |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1)) + |> fold_rev (make_casedists (#sorts info)) infos + end; -fun add_dt_realizers sorts infos thy = if !proofs < 2 then thy else - (message "Adding realizers for induction and case analysis ..."; thy - |> curry (Library.foldr (make_ind sorts (hd infos))) - (subsets 0 (length (#descr (hd infos)) - 1)) - |> curry (Library.foldr (make_casedists sorts)) infos); +val setup = DatatypePackage.add_interpretator add_dt_realizers; end;