--- 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
--- 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\<Colon>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
--- 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 \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
--- 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
--- 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 \
--- 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 {*
--- 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
--- 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 \<Rightarrow> 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\<Colon>nat) = n"
-by (induct n) simp_all
+ by (induct n) simp_all
+
+lemma size_bool [code func]:
+ "size (b\<Colon>bool) = 0" by (cases b) auto
+
+declare "*.size" [noatp]
+
subsection {* legacy bindings *}
--- 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
-
--- 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
--- 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 =
--- 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,
--- 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;
--- 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;
--- 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 =
--- 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;