datatype interpretators for size and datatype_realizer
authorhaftmann
Tue Sep 25 12:16:08 2007 +0200 (2007-09-25)
changeset 24699c6674504103f
parent 24698 9800a7602629
child 24700 291665d063e4
datatype interpretators for size and datatype_realizer
NEWS
src/HOL/Datatype.thy
src/HOL/FunDef.thy
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/Nat.thy
src/HOL/PreList.thy
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
     1.1 --- a/NEWS	Tue Sep 25 10:27:43 2007 +0200
     1.2 +++ b/NEWS	Tue Sep 25 12:16:08 2007 +0200
     1.3 @@ -517,6 +517,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Internal reorganisation of `size' of datatypes:
     1.8 +  - size theorems "foo.size" are no longer subsumed by "foo.simps" (but are still
     1.9 +      simplification rules by default!)
    1.10 +  - theorems "prod.size" now named "*.size"
    1.11 +
    1.12  * The transitivity reasoner for partial and linear orders is set up for
    1.13  locales `order' and `linorder' generated by the new class package.  Previously
    1.14  the reasoner was only set up for axiomatic type classes.  Instances of the
     2.1 --- a/src/HOL/Datatype.thy	Tue Sep 25 10:27:43 2007 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Tue Sep 25 12:16:08 2007 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     2.5  
     2.6  theory Datatype
     2.7 -imports Nat Sum_Type
     2.8 +imports Nat
     2.9  begin
    2.10  
    2.11  typedef (Node)
    2.12 @@ -537,52 +537,7 @@
    2.13  
    2.14  section {* Datatypes *}
    2.15  
    2.16 -subsection {* Representing primitive types *}
    2.17 -
    2.18 -rep_datatype bool
    2.19 -  distinct True_not_False False_not_True
    2.20 -  induction bool_induct
    2.21 -
    2.22 -declare case_split [cases type: bool]
    2.23 -  -- "prefer plain propositional version"
    2.24 -
    2.25 -lemma size_bool [code func]:
    2.26 -  "size (b\<Colon>bool) = 0" by (cases b) auto
    2.27 -
    2.28 -rep_datatype unit
    2.29 -  induction unit_induct
    2.30 -
    2.31 -rep_datatype prod
    2.32 -  inject Pair_eq
    2.33 -  induction prod_induct
    2.34 -
    2.35 -declare prod.size [noatp]
    2.36 -
    2.37 -lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    2.38 -
    2.39 -lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
    2.40 -  by auto
    2.41 -
    2.42 -lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
    2.43 -  by (auto simp: split_tupled_all)
    2.44 -
    2.45 -lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
    2.46 -  by (induct p) auto
    2.47 -
    2.48 -lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
    2.49 -  by (induct p) auto
    2.50 -
    2.51 -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
    2.52 -  by (simp add: expand_fun_eq)
    2.53 -
    2.54 -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
    2.55 -declare prod_caseE' [elim!] prod_caseE [elim!]
    2.56 -
    2.57 -lemma prod_case_split [code post]:
    2.58 -  "prod_case = split"
    2.59 -  by (auto simp add: expand_fun_eq)
    2.60 -
    2.61 -lemmas [code inline] = prod_case_split [symmetric]
    2.62 +subsection {* Representing sums *}
    2.63  
    2.64  rep_datatype sum
    2.65    distinct Inl_not_Inr Inr_not_Inl
    2.66 @@ -637,49 +592,6 @@
    2.67  hide (open) const Suml Sumr
    2.68  
    2.69  
    2.70 -subsection {* Further cases/induct rules for tuples *}
    2.71 -
    2.72 -lemma prod_cases3 [cases type]:
    2.73 -  obtains (fields) a b c where "y = (a, b, c)"
    2.74 -  by (cases y, case_tac b) blast
    2.75 -
    2.76 -lemma prod_induct3 [case_names fields, induct type]:
    2.77 -    "(!!a b c. P (a, b, c)) ==> P x"
    2.78 -  by (cases x) blast
    2.79 -
    2.80 -lemma prod_cases4 [cases type]:
    2.81 -  obtains (fields) a b c d where "y = (a, b, c, d)"
    2.82 -  by (cases y, case_tac c) blast
    2.83 -
    2.84 -lemma prod_induct4 [case_names fields, induct type]:
    2.85 -    "(!!a b c d. P (a, b, c, d)) ==> P x"
    2.86 -  by (cases x) blast
    2.87 -
    2.88 -lemma prod_cases5 [cases type]:
    2.89 -  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
    2.90 -  by (cases y, case_tac d) blast
    2.91 -
    2.92 -lemma prod_induct5 [case_names fields, induct type]:
    2.93 -    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    2.94 -  by (cases x) blast
    2.95 -
    2.96 -lemma prod_cases6 [cases type]:
    2.97 -  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
    2.98 -  by (cases y, case_tac e) blast
    2.99 -
   2.100 -lemma prod_induct6 [case_names fields, induct type]:
   2.101 -    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   2.102 -  by (cases x) blast
   2.103 -
   2.104 -lemma prod_cases7 [cases type]:
   2.105 -  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
   2.106 -  by (cases y, case_tac f) blast
   2.107 -
   2.108 -lemma prod_induct7 [case_names fields, induct type]:
   2.109 -    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   2.110 -  by (cases x) blast
   2.111 -
   2.112 -
   2.113  subsection {* The option datatype *}
   2.114  
   2.115  datatype 'a option = None | Some 'a
     3.1 --- a/src/HOL/FunDef.thy	Tue Sep 25 10:27:43 2007 +0200
     3.2 +++ b/src/HOL/FunDef.thy	Tue Sep 25 12:16:08 2007 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* General recursive function definitions *}
     3.5  
     3.6  theory FunDef
     3.7 -imports Datatype Accessible_Part
     3.8 +imports Accessible_Part
     3.9  uses
    3.10    ("Tools/function_package/fundef_lib.ML")
    3.11    ("Tools/function_package/fundef_common.ML")
    3.12 @@ -103,7 +103,7 @@
    3.13  use "Tools/function_package/auto_term.ML"
    3.14  use "Tools/function_package/fundef_package.ML"
    3.15  
    3.16 -setup FundefPackage.setup
    3.17 +setup {* FundefPackage.setup *}
    3.18  
    3.19  lemma let_cong [fundef_cong]:
    3.20    "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
     4.1 --- a/src/HOL/Inductive.thy	Tue Sep 25 10:27:43 2007 +0200
     4.2 +++ b/src/HOL/Inductive.thy	Tue Sep 25 12:16:08 2007 +0200
     4.3 @@ -6,18 +6,17 @@
     4.4  header {* Support for inductive sets and types *}
     4.5  
     4.6  theory Inductive 
     4.7 -imports FixedPoint Product_Type Sum_Type
     4.8 +imports FixedPoint Sum_Type
     4.9  uses
    4.10    ("Tools/inductive_package.ML")
    4.11 -  ("Tools/inductive_set_package.ML")
    4.12 -  ("Tools/inductive_realizer.ML")
    4.13 +  (*("Tools/inductive_set_package.ML")
    4.14 +  ("Tools/inductive_realizer.ML")*)
    4.15    "Tools/dseq.ML"
    4.16    ("Tools/inductive_codegen.ML")
    4.17    ("Tools/datatype_aux.ML")
    4.18    ("Tools/datatype_prop.ML")
    4.19    ("Tools/datatype_rep_proofs.ML")
    4.20    ("Tools/datatype_abs_proofs.ML")
    4.21 -  ("Tools/datatype_realizer.ML")
    4.22    ("Tools/datatype_case.ML")
    4.23    ("Tools/datatype_package.ML")
    4.24    ("Tools/datatype_codegen.ML")
    4.25 @@ -108,25 +107,15 @@
    4.26  use "Tools/datatype_rep_proofs.ML"
    4.27  use "Tools/datatype_abs_proofs.ML"
    4.28  use "Tools/datatype_case.ML"
    4.29 -use "Tools/datatype_realizer.ML"
    4.30 -
    4.31  use "Tools/datatype_package.ML"
    4.32  setup DatatypePackage.setup
    4.33 -
    4.34 +use "Tools/primrec_package.ML"
    4.35  use "Tools/datatype_codegen.ML"
    4.36  setup DatatypeCodegen.setup
    4.37  
    4.38 -use "Tools/inductive_realizer.ML"
    4.39 -setup InductiveRealizer.setup
    4.40 -
    4.41  use "Tools/inductive_codegen.ML"
    4.42  setup InductiveCodegen.setup
    4.43  
    4.44 -use "Tools/primrec_package.ML"
    4.45 -
    4.46 -use "Tools/inductive_set_package.ML"
    4.47 -setup InductiveSetPackage.setup
    4.48 -
    4.49  text{* Lambda-abstractions with pattern matching: *}
    4.50  
    4.51  syntax
     5.1 --- a/src/HOL/IsaMakefile	Tue Sep 25 10:27:43 2007 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Tue Sep 25 12:16:08 2007 +0200
     5.3 @@ -123,7 +123,8 @@
     5.4    Tools/function_package/inductive_wrap.ML				\
     5.5    Tools/function_package/lexicographic_order.ML				\
     5.6    Tools/function_package/mutual.ML					\
     5.7 -  Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML	\
     5.8 +  Tools/function_package/pattern_split.ML	\
     5.9 +  Tools/function_package/size.ML Tools/inductive_codegen.ML	\
    5.10    Tools/inductive_package.ML Tools/inductive_realizer.ML		\
    5.11    Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
    5.12    Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
     6.1 --- a/src/HOL/Main.thy	Tue Sep 25 10:27:43 2007 +0200
     6.2 +++ b/src/HOL/Main.thy	Tue Sep 25 12:16:08 2007 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Main HOL *}
     6.5  
     6.6  theory Main
     6.7 -imports Map 
     6.8 +imports Map
     6.9  begin
    6.10  
    6.11  text {*
     7.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Sep 25 10:27:43 2007 +0200
     7.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Sep 25 12:16:08 2007 +0200
     7.3 @@ -118,7 +118,7 @@
     7.4  apply (rule exec_all_trans)
     7.5  apply (simp only: append_Nil)
     7.6  apply (drule_tac x="[]" in spec)
     7.7 -apply (simp only: list.simps)
     7.8 +apply (simp only: list.simps list.size)
     7.9  apply blast
    7.10  apply (rule exec_instr_in_exec_all)
    7.11  apply auto
     8.1 --- a/src/HOL/Nat.thy	Tue Sep 25 10:27:43 2007 +0200
     8.2 +++ b/src/HOL/Nat.thy	Tue Sep 25 12:16:08 2007 +0200
     8.3 @@ -16,6 +16,7 @@
     8.4    ("arith_data.ML")
     8.5    "~~/src/Provers/Arith/fast_lin_arith.ML"
     8.6    ("Tools/lin_arith.ML")
     8.7 +  ("Tools/function_package/size.ML")
     8.8  begin
     8.9  
    8.10  subsection {* Type @{text ind} *}
    8.11 @@ -111,9 +112,13 @@
    8.12  
    8.13  text {* size of a datatype value *}
    8.14  
    8.15 +use "Tools/function_package/size.ML"
    8.16 +
    8.17  class size = type +
    8.18    fixes size :: "'a \<Rightarrow> nat"
    8.19  
    8.20 +setup Size.setup
    8.21 +
    8.22  rep_datatype nat
    8.23    distinct  Suc_not_Zero Zero_not_Suc
    8.24    inject    Suc_Suc_eq
    8.25 @@ -1467,10 +1472,16 @@
    8.26  by intro_classes (auto simp add: inf_nat_def sup_nat_def)
    8.27  
    8.28  
    8.29 -subsection {* Size function *}
    8.30 +subsection {* Size function declarations *}
    8.31  
    8.32  lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
    8.33 -by (induct n) simp_all
    8.34 +  by (induct n) simp_all
    8.35 +
    8.36 +lemma size_bool [code func]:
    8.37 +  "size (b\<Colon>bool) = 0" by (cases b) auto
    8.38 +
    8.39 +declare "*.size" [noatp]
    8.40 +
    8.41  
    8.42  subsection {* legacy bindings *}
    8.43  
     9.1 --- a/src/HOL/PreList.thy	Tue Sep 25 10:27:43 2007 +0200
     9.2 +++ b/src/HOL/PreList.thy	Tue Sep 25 12:16:08 2007 +0200
     9.3 @@ -25,4 +25,3 @@
     9.4  setup ResAxioms.setup
     9.5  
     9.6  end
     9.7 -
    10.1 --- a/src/HOL/Product_Type.thy	Tue Sep 25 10:27:43 2007 +0200
    10.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 25 12:16:08 2007 +0200
    10.3 @@ -7,10 +7,24 @@
    10.4  header {* Cartesian products *}
    10.5  
    10.6  theory Product_Type
    10.7 -imports Typedef Fun
    10.8 -uses ("Tools/split_rule.ML")
    10.9 +imports Inductive
   10.10 +uses
   10.11 +  ("Tools/split_rule.ML")
   10.12 +  ("Tools/inductive_set_package.ML")
   10.13 +  ("Tools/inductive_realizer.ML")
   10.14 +  ("Tools/datatype_realizer.ML")
   10.15  begin
   10.16  
   10.17 +subsection {* @{typ bool} is a datatype *}
   10.18 +
   10.19 +rep_datatype bool
   10.20 +  distinct True_not_False False_not_True
   10.21 +  induction bool_induct
   10.22 +
   10.23 +declare case_split [cases type: bool]
   10.24 +  -- "prefer plain propositional version"
   10.25 +
   10.26 +
   10.27  subsection {* Unit *}
   10.28  
   10.29  typedef unit = "{True}"
   10.30 @@ -18,9 +32,10 @@
   10.31    show "True : ?unit" ..
   10.32  qed
   10.33  
   10.34 -constdefs
   10.35 +definition
   10.36    Unity :: unit    ("'(')")
   10.37 -  "() == Abs_unit True"
   10.38 +where
   10.39 +  "() = Abs_unit True"
   10.40  
   10.41  lemma unit_eq [noatp]: "u = ()"
   10.42    by (induct u) (simp add: unit_def Unity_def)
   10.43 @@ -32,23 +47,26 @@
   10.44  
   10.45  ML_setup {*
   10.46    val unit_eq_proc =
   10.47 -    let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
   10.48 -      Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"]
   10.49 +    let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
   10.50 +      Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
   10.51        (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
   10.52      end;
   10.53  
   10.54    Addsimprocs [unit_eq_proc];
   10.55  *}
   10.56  
   10.57 +lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
   10.58 +  by simp
   10.59 +
   10.60 +rep_datatype unit
   10.61 +  induction unit_induct
   10.62 +
   10.63  lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
   10.64    by simp
   10.65  
   10.66  lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
   10.67    by (rule triv_forall_equality)
   10.68  
   10.69 -lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
   10.70 -  by simp
   10.71 -
   10.72  text {*
   10.73    This rewrite counters the effect of @{text unit_eq_proc} on @{term
   10.74    [source] "%u::unit. f u"}, replacing it by @{term [source]
   10.75 @@ -84,7 +102,6 @@
   10.76  
   10.77  local
   10.78  
   10.79 -
   10.80  subsubsection {* Definitions *}
   10.81  
   10.82  global
   10.83 @@ -343,6 +360,10 @@
   10.84  lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
   10.85    by fast
   10.86  
   10.87 +rep_datatype prod
   10.88 +  inject Pair_eq
   10.89 +  induction prod_induct
   10.90 +
   10.91  lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
   10.92    by fast
   10.93  
   10.94 @@ -765,6 +786,77 @@
   10.95  setup SplitRule.setup
   10.96  
   10.97  
   10.98 +
   10.99 +lemmas prod_caseI = prod.cases [THEN iffD2, standard]
  10.100 +
  10.101 +lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
  10.102 +  by auto
  10.103 +
  10.104 +lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
  10.105 +  by (auto simp: split_tupled_all)
  10.106 +
  10.107 +lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
  10.108 +  by (induct p) auto
  10.109 +
  10.110 +lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
  10.111 +  by (induct p) auto
  10.112 +
  10.113 +lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
  10.114 +  by (simp add: expand_fun_eq)
  10.115 +
  10.116 +declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
  10.117 +declare prod_caseE' [elim!] prod_caseE [elim!]
  10.118 +
  10.119 +lemma prod_case_split [code post]:
  10.120 +  "prod_case = split"
  10.121 +  by (auto simp add: expand_fun_eq)
  10.122 +
  10.123 +lemmas [code inline] = prod_case_split [symmetric]
  10.124 +
  10.125 +
  10.126 +subsection {* Further cases/induct rules for tuples *}
  10.127 +
  10.128 +lemma prod_cases3 [cases type]:
  10.129 +  obtains (fields) a b c where "y = (a, b, c)"
  10.130 +  by (cases y, case_tac b) blast
  10.131 +
  10.132 +lemma prod_induct3 [case_names fields, induct type]:
  10.133 +    "(!!a b c. P (a, b, c)) ==> P x"
  10.134 +  by (cases x) blast
  10.135 +
  10.136 +lemma prod_cases4 [cases type]:
  10.137 +  obtains (fields) a b c d where "y = (a, b, c, d)"
  10.138 +  by (cases y, case_tac c) blast
  10.139 +
  10.140 +lemma prod_induct4 [case_names fields, induct type]:
  10.141 +    "(!!a b c d. P (a, b, c, d)) ==> P x"
  10.142 +  by (cases x) blast
  10.143 +
  10.144 +lemma prod_cases5 [cases type]:
  10.145 +  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
  10.146 +  by (cases y, case_tac d) blast
  10.147 +
  10.148 +lemma prod_induct5 [case_names fields, induct type]:
  10.149 +    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
  10.150 +  by (cases x) blast
  10.151 +
  10.152 +lemma prod_cases6 [cases type]:
  10.153 +  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
  10.154 +  by (cases y, case_tac e) blast
  10.155 +
  10.156 +lemma prod_induct6 [case_names fields, induct type]:
  10.157 +    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
  10.158 +  by (cases x) blast
  10.159 +
  10.160 +lemma prod_cases7 [cases type]:
  10.161 +  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
  10.162 +  by (cases y, case_tac f) blast
  10.163 +
  10.164 +lemma prod_induct7 [case_names fields, induct type]:
  10.165 +    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
  10.166 +  by (cases x) blast
  10.167 +
  10.168 +
  10.169  subsection {* Further lemmas *}
  10.170  
  10.171  lemma
  10.172 @@ -914,6 +1006,9 @@
  10.173  end
  10.174  *}
  10.175  
  10.176 +
  10.177 +subsection {* Legacy bindings *}
  10.178 +
  10.179  ML {*
  10.180  val Collect_split = thm "Collect_split";
  10.181  val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
  10.182 @@ -1011,4 +1106,16 @@
  10.183  val unit_induct = thm "unit_induct";
  10.184  *}
  10.185  
  10.186 +
  10.187 +subsection {* Further inductive packages *}
  10.188 +
  10.189 +use "Tools/inductive_realizer.ML"
  10.190 +setup InductiveRealizer.setup
  10.191 +
  10.192 +use "Tools/inductive_set_package.ML"
  10.193 +setup InductiveSetPackage.setup
  10.194 +
  10.195 +use "Tools/datatype_realizer.ML"
  10.196 +setup DatatypeRealizer.setup
  10.197 +
  10.198  end
    11.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 25 10:27:43 2007 +0200
    11.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 25 12:16:08 2007 +0200
    11.3 @@ -10,8 +10,7 @@
    11.4   - characteristic equations for primrec combinators
    11.5   - characteristic equations for case combinators
    11.6   - equations for splitting "P (case ...)" expressions
    11.7 - - datatype size function
    11.8 - - "nchotomy" and "case_cong" theorems for TFL
    11.9 +  - "nchotomy" and "case_cong" theorems for TFL
   11.10  
   11.11  *)
   11.12  
   11.13 @@ -31,9 +30,6 @@
   11.14      DatatypeAux.descr list -> (string * sort) list ->
   11.15        thm list list -> thm list list -> thm list -> thm list list -> theory ->
   11.16          (thm * thm) list * theory
   11.17 -  val prove_size_thms : bool -> string list ->
   11.18 -    DatatypeAux.descr list -> (string * sort) list ->
   11.19 -      string list -> thm list -> theory -> thm list * theory
   11.20    val prove_nchotomys : string list -> DatatypeAux.descr list ->
   11.21      (string * sort) list -> thm list -> theory -> thm list * theory
   11.22    val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
   11.23 @@ -381,83 +377,6 @@
   11.24      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   11.25    end;
   11.26  
   11.27 -(******************************* size functions *******************************)
   11.28 -
   11.29 -fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   11.30 -  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   11.31 -    is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
   11.32 -      (List.concat descr)
   11.33 -  then
   11.34 -    ([], thy)
   11.35 -  else
   11.36 -  let
   11.37 -    val _ = message "Proving equations for size function ...";
   11.38 -
   11.39 -    val big_name = space_implode "_" new_type_names;
   11.40 -    val thy1 = add_path flat_names big_name thy;
   11.41 -
   11.42 -    val descr' = flat descr;
   11.43 -    val recTs = get_rec_types descr' sorts;
   11.44 -
   11.45 -    val Const (size_name, _) = HOLogic.size_const dummyT;
   11.46 -    val size_names = replicate (length (hd descr)) size_name @
   11.47 -      map (Sign.full_name thy1) (DatatypeProp.indexify_names
   11.48 -        (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
   11.49 -    val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
   11.50 -      (map (fn T => name_of_typ T ^ "_size") recTs));
   11.51 -
   11.52 -    fun plus (t1, t2) =
   11.53 -      Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   11.54 -
   11.55 -    fun make_sizefun (_, cargs) =
   11.56 -      let
   11.57 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   11.58 -        val k = length (filter is_rec_type cargs);
   11.59 -        val t = if k = 0 then HOLogic.zero else
   11.60 -          foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.Suc_zero])
   11.61 -      in
   11.62 -        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
   11.63 -      end;
   11.64 -
   11.65 -    val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr';
   11.66 -    val fTs = map fastype_of fs;
   11.67 -
   11.68 -    fun instance_size_class tyco thy =
   11.69 -      let
   11.70 -        val n = Sign.arity_number thy tyco;
   11.71 -      in
   11.72 -        thy
   11.73 -        |> Class.prove_instance (Class.intro_classes_tac [])
   11.74 -            [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
   11.75 -        |> snd
   11.76 -      end
   11.77 -
   11.78 -    val (size_def_thms, thy') =
   11.79 -      thy1
   11.80 -      |> Theory.add_consts_i (map (fn (s, T) =>
   11.81 -           (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   11.82 -           (Library.drop (length (hd descr), size_names ~~ recTs)))
   11.83 -      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
   11.84 -      |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) =>
   11.85 -           (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
   11.86 -            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))))
   11.87 -            (size_names ~~ recTs ~~ def_names ~~ reccomb_names))
   11.88 -      ||> parent_path flat_names;
   11.89 -
   11.90 -    val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   11.91 -
   11.92 -    val size_thms = map (fn t => Goal.prove_global thy' [] [] t
   11.93 -      (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))
   11.94 -        (DatatypeProp.make_size descr sorts thy')
   11.95 -
   11.96 -  in
   11.97 -    thy'
   11.98 -    |> Theory.add_path big_name
   11.99 -    |> PureThy.add_thmss [(("size", size_thms), [])]
  11.100 -    ||> Theory.parent_path
  11.101 -    |-> (fn thmss => pair (flat thmss))
  11.102 -  end;
  11.103 -
  11.104  fun prove_weak_case_congs new_type_names descr sorts thy =
  11.105    let
  11.106      fun prove_weak_case_cong t =
    12.1 --- a/src/HOL/Tools/datatype_aux.ML	Tue Sep 25 10:27:43 2007 +0200
    12.2 +++ b/src/HOL/Tools/datatype_aux.ML	Tue Sep 25 12:16:08 2007 +0200
    12.3 @@ -10,8 +10,6 @@
    12.4    val quiet_mode : bool ref
    12.5    val message : string -> unit
    12.6    
    12.7 -  val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
    12.8 -
    12.9    val add_path : bool -> string -> theory -> theory
   12.10    val parent_path : bool -> theory -> theory
   12.11  
   12.12 @@ -72,9 +70,6 @@
   12.13  val quiet_mode = ref false;
   12.14  fun message s = if !quiet_mode then () else writeln s;
   12.15  
   12.16 -(* FIXME: move to library ? *)
   12.17 -fun foldl1 f (x::xs) = Library.foldl f (x, xs);
   12.18 -
   12.19  fun add_path flat_names s = if flat_names then I else Theory.add_path s;
   12.20  fun parent_path flat_names = if flat_names then I else Theory.parent_path;
   12.21  
   12.22 @@ -184,6 +179,7 @@
   12.23  
   12.24  type datatype_info =
   12.25    {index : int,
   12.26 +   head_len : int,
   12.27     descr : descr,
   12.28     sorts : (string * sort) list,
   12.29     rec_names : string list,
    13.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 25 10:27:43 2007 +0200
    13.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 25 12:16:08 2007 +0200
    13.3 @@ -447,35 +447,6 @@
    13.4    | get_spec thy (tyco, false) =
    13.5        TypecopyPackage.get_spec thy tyco;
    13.6  
    13.7 -fun codetypes_dependency thy =
    13.8 -  let
    13.9 -    val names =
   13.10 -      map (rpair true) (Symtab.keys (DatatypePackage.get_datatypes thy))
   13.11 -        @ map (rpair false) (TypecopyPackage.get_typecopies thy);
   13.12 -    fun add_node (name, is_dt) =
   13.13 -      let
   13.14 -        fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
   13.15 -          | add_tycos _ = I;
   13.16 -        val tys = if is_dt then
   13.17 -            (maps snd o snd o the o DatatypePackage.get_datatype_spec thy) name
   13.18 -          else
   13.19 -            [(#typ o the o TypecopyPackage.get_typecopy_info thy) name]
   13.20 -        val deps = (filter (AList.defined (op =) names) o maps (fn ty =>
   13.21 -          add_tycos ty [])) tys;
   13.22 -      in
   13.23 -        Graph.default_node (name, ())
   13.24 -        #> fold (fn name' =>
   13.25 -             Graph.default_node (name', ())
   13.26 -             #> Graph.add_edge (name', name)
   13.27 -           ) deps
   13.28 -      end
   13.29 -  in
   13.30 -    Graph.empty
   13.31 -    |> fold add_node names
   13.32 -    |> Graph.strong_conn
   13.33 -    |> map (AList.make (the o AList.lookup (op =) names))
   13.34 -  end;
   13.35 -
   13.36  local
   13.37    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
   13.38     of SOME _ => get_eq_datatype thy tyco
   13.39 @@ -515,7 +486,6 @@
   13.40        hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
   13.41    in
   13.42      thy
   13.43 -    |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
   13.44      |> DatatypePackage.add_interpretator datatype_hook
   13.45      |> TypecopyPackage.add_interpretator typecopy_hook
   13.46    end;
    14.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 25 10:27:43 2007 +0200
    14.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 25 12:16:08 2007 +0200
    14.3 @@ -17,6 +17,16 @@
    14.4  sig
    14.5    include BASIC_DATATYPE_PACKAGE
    14.6    val quiet_mode : bool ref
    14.7 +  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
    14.8 +    (bstring * typ list * mixfix) list) list -> theory ->
    14.9 +      {distinct : thm list list,
   14.10 +       inject : thm list list,
   14.11 +       exhaustion : thm list,
   14.12 +       rec_thms : thm list,
   14.13 +       case_thms : thm list list,
   14.14 +       split_thms : (thm * thm) list,
   14.15 +       induction : thm,
   14.16 +       simps : thm list} * theory
   14.17    val add_datatype : bool -> string list -> (string list * bstring * mixfix *
   14.18      (bstring * string list * mixfix) list) list -> theory ->
   14.19        {distinct : thm list list,
   14.20 @@ -26,18 +36,6 @@
   14.21         case_thms : thm list list,
   14.22         split_thms : (thm * thm) list,
   14.23         induction : thm,
   14.24 -       size : thm list,
   14.25 -       simps : thm list} * theory
   14.26 -  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
   14.27 -    (bstring * typ list * mixfix) list) list -> theory ->
   14.28 -      {distinct : thm list list,
   14.29 -       inject : thm list list,
   14.30 -       exhaustion : thm list,
   14.31 -       rec_thms : thm list,
   14.32 -       case_thms : thm list list,
   14.33 -       split_thms : (thm * thm) list,
   14.34 -       induction : thm,
   14.35 -       size : thm list,
   14.36         simps : thm list} * theory
   14.37    val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
   14.38      (thm list * attribute list) list list -> (thm list * attribute list) ->
   14.39 @@ -49,7 +47,6 @@
   14.40         case_thms : thm list list,
   14.41         split_thms : (thm * thm) list,
   14.42         induction : thm,
   14.43 -       size : thm list,
   14.44         simps : thm list} * theory
   14.45    val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
   14.46      (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
   14.47 @@ -60,7 +57,6 @@
   14.48         case_thms : thm list list,
   14.49         split_thms : (thm * thm) list,
   14.50         induction : thm,
   14.51 -       size : thm list,
   14.52         simps : thm list} * theory
   14.53    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
   14.54    val get_datatype : theory -> string -> DatatypeAux.datatype_info option
   14.55 @@ -325,12 +321,12 @@
   14.56  
   14.57  end;
   14.58  
   14.59 -fun add_rules simps case_thms size_thms rec_thms inject distinct
   14.60 +fun add_rules simps case_thms rec_thms inject distinct
   14.61                    weak_case_congs cong_att =
   14.62    PureThy.add_thmss [(("simps", simps), []),
   14.63 -    (("", flat case_thms @ size_thms @ 
   14.64 +    (("", flat case_thms @
   14.65            flat distinct @ rec_thms), [Simplifier.simp_add]),
   14.66 -    (("", size_thms @ rec_thms), [RecfunCodegen.add_default]),
   14.67 +    (("", rec_thms), [RecfunCodegen.add_default]),
   14.68      (("", flat inject), [iff_add]),
   14.69      (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
   14.70      (("", weak_case_congs), [cong_att])]
   14.71 @@ -460,11 +456,12 @@
   14.72  
   14.73  (**** make datatype info ****)
   14.74  
   14.75 -fun make_dt_info descr sorts induct reccomb_names rec_thms
   14.76 +fun make_dt_info head_len descr sorts induct reccomb_names rec_thms
   14.77      (((((((((i, (_, (tname, _, _))), case_name), case_thms),
   14.78        exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
   14.79    (tname,
   14.80     {index = i,
   14.81 +    head_len = head_len,
   14.82      descr = descr,
   14.83      sorts = sorts,
   14.84      rec_names = reccomb_names,
   14.85 @@ -522,9 +519,9 @@
   14.86  val specify_consts = gen_specify_consts Sign.add_consts_i;
   14.87  val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
   14.88  
   14.89 -structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
   14.90 +structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string list; val eq = op = end);
   14.91  
   14.92 -fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator;
   14.93 +fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator (fold interpretator);
   14.94  
   14.95  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   14.96      case_names_induct case_names_exhausts thy =
   14.97 @@ -534,10 +531,6 @@
   14.98      val used = map fst (fold Term.add_tfreesT recTs []);
   14.99      val newTs = Library.take (length (hd descr), recTs);
  14.100  
  14.101 -    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
  14.102 -      (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
  14.103 -        cargs) constrs) descr';
  14.104 -
  14.105      (**** declare new types and constants ****)
  14.106  
  14.107      val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
  14.108 @@ -554,9 +547,6 @@
  14.109        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
  14.110          (1 upto (length descr')));
  14.111  
  14.112 -    val size_names = DatatypeProp.indexify_names
  14.113 -      (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
  14.114 -
  14.115      val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
  14.116      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
  14.117        map (fn (_, cargs) =>
  14.118 @@ -565,22 +555,11 @@
  14.119  
  14.120      val case_names = map (fn s => (s ^ "_case")) new_type_names;
  14.121  
  14.122 -    fun instance_size_class tyco thy =
  14.123 -      let
  14.124 -        val n = Sign.arity_number thy tyco;
  14.125 -      in
  14.126 -        thy
  14.127 -        |> Class.prove_instance (Class.intro_classes_tac [])
  14.128 -            [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
  14.129 -        |> snd
  14.130 -      end
  14.131 -
  14.132      val thy2' = thy
  14.133  
  14.134        (** new types **)
  14.135        |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
  14.136             types_syntax tyvars
  14.137 -      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
  14.138        |> add_path flat_names (space_implode "_" new_type_names)
  14.139  
  14.140        (** primrec combinators **)
  14.141 @@ -598,12 +577,6 @@
  14.142  
  14.143      val thy2 = thy2'
  14.144  
  14.145 -      (** size functions **)
  14.146 -
  14.147 -      |> (if no_size then I else specify_consts (map (fn (s, T) =>
  14.148 -        (Sign.base_name s, T --> HOLogic.natT, NoSyn))
  14.149 -          (size_names ~~ Library.drop (length (hd descr), recTs))))
  14.150 -
  14.151        (** constructors **)
  14.152  
  14.153        |> parent_path flat_names
  14.154 @@ -619,18 +592,15 @@
  14.155      (**** introduction of axioms ****)
  14.156  
  14.157      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
  14.158 -    val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
  14.159  
  14.160      val ((([induct], [rec_thms]), inject), thy3) =
  14.161        thy2
  14.162        |> Theory.add_path (space_implode "_" new_type_names)
  14.163        |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
  14.164        ||>> add_axioms "recs" rec_axs []
  14.165 -      ||> (if no_size then I else add_axioms "size" size_axs [] #> snd)
  14.166        ||> Theory.parent_path
  14.167        ||>> add_and_get_axiomss "inject" new_type_names
  14.168              (DatatypeProp.make_injs descr sorts);
  14.169 -    val size_thms = if no_size then [] else get_thms thy3 (Name "size");
  14.170      val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
  14.171        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
  14.172  
  14.173 @@ -651,27 +621,27 @@
  14.174      val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
  14.175        (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
  14.176  
  14.177 -    val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms)
  14.178 +    val dt_infos = map (make_dt_info (length (hd descr)) descr' sorts induct
  14.179 +        reccomb_names' rec_thms)
  14.180        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
  14.181          exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
  14.182            nchotomys ~~ case_congs ~~ weak_case_congs);
  14.183  
  14.184 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
  14.185 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
  14.186      val split_thms = split ~~ split_asm;
  14.187  
  14.188      val thy12 =
  14.189        thy11
  14.190        |> add_case_tr' case_names'
  14.191        |> Theory.add_path (space_implode "_" new_type_names)
  14.192 -      |> add_rules simps case_thms size_thms rec_thms inject distinct
  14.193 +      |> add_rules simps case_thms rec_thms inject distinct
  14.194            weak_case_congs Simplifier.cong_add
  14.195        |> put_dt_infos dt_infos
  14.196        |> add_cases_induct dt_infos induct
  14.197        |> Theory.parent_path
  14.198        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
  14.199        |> snd
  14.200 -      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
  14.201 -      |> DatatypeInterpretator.add_those (map fst dt_infos);
  14.202 +      |> DatatypeInterpretator.add_those [map fst dt_infos];
  14.203    in
  14.204      ({distinct = distinct,
  14.205        inject = inject,
  14.206 @@ -680,7 +650,6 @@
  14.207        case_thms = case_thms,
  14.208        split_thms = split_thms,
  14.209        induction = induct,
  14.210 -      size = size_thms,
  14.211        simps = simps}, thy12)
  14.212    end;
  14.213  
  14.214 @@ -711,27 +680,25 @@
  14.215        descr sorts nchotomys case_thms thy8;
  14.216      val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
  14.217        descr sorts thy9;
  14.218 -    val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
  14.219 -      descr sorts reccomb_names rec_thms thy10;
  14.220  
  14.221 -    val dt_infos = map (make_dt_info (flat descr) sorts induct reccomb_names rec_thms)
  14.222 +    val dt_infos = map (make_dt_info (length (hd descr)) (flat descr) sorts induct
  14.223 +        reccomb_names rec_thms)
  14.224        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
  14.225          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
  14.226  
  14.227 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
  14.228 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
  14.229  
  14.230      val thy12 =
  14.231 -      thy11
  14.232 +      thy10
  14.233        |> add_case_tr' case_names
  14.234        |> Theory.add_path (space_implode "_" new_type_names)
  14.235 -      |> add_rules simps case_thms size_thms rec_thms inject distinct
  14.236 +      |> add_rules simps case_thms rec_thms inject distinct
  14.237            weak_case_congs (Simplifier.attrib (op addcongs))
  14.238        |> put_dt_infos dt_infos
  14.239        |> add_cases_induct dt_infos induct
  14.240        |> Theory.parent_path
  14.241        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
  14.242 -      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
  14.243 -      |> DatatypeInterpretator.add_those (map fst dt_infos);
  14.244 +      |> DatatypeInterpretator.add_those [map fst dt_infos];
  14.245    in
  14.246      ({distinct = distinct,
  14.247        inject = inject,
  14.248 @@ -740,7 +707,6 @@
  14.249        case_thms = case_thms,
  14.250        split_thms = split_thms,
  14.251        induction = induct,
  14.252 -      size = size_thms,
  14.253        simps = simps}, thy12)
  14.254    end;
  14.255  
  14.256 @@ -808,35 +774,32 @@
  14.257        [descr] sorts nchotomys case_thms thy6;
  14.258      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
  14.259        [descr] sorts thy7;
  14.260 -    val (size_thms, thy9) =
  14.261 -      DatatypeAbsProofs.prove_size_thms false new_type_names
  14.262 -        [descr] sorts reccomb_names rec_thms thy8;
  14.263  
  14.264      val ((_, [induction']), thy10) =
  14.265 -      thy9
  14.266 +      thy8
  14.267        |> store_thmss "inject" new_type_names inject
  14.268        ||>> store_thmss "distinct" new_type_names distinct
  14.269        ||> Theory.add_path (space_implode "_" new_type_names)
  14.270        ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
  14.271  
  14.272 -    val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms)
  14.273 +    val dt_infos = map (make_dt_info (length descr) descr sorts induction'
  14.274 +        reccomb_names rec_thms)
  14.275        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
  14.276          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
  14.277  
  14.278 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
  14.279 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
  14.280  
  14.281      val thy11 =
  14.282        thy10
  14.283        |> add_case_tr' case_names
  14.284 -      |> add_rules simps case_thms size_thms rec_thms inject distinct
  14.285 +      |> add_rules simps case_thms rec_thms inject distinct
  14.286             weak_case_congs (Simplifier.attrib (op addcongs))
  14.287        |> put_dt_infos dt_infos
  14.288        |> add_cases_induct dt_infos induction'
  14.289        |> Theory.parent_path
  14.290        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
  14.291        |> snd
  14.292 -      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
  14.293 -      |> DatatypeInterpretator.add_those (map fst dt_infos);
  14.294 +      |> DatatypeInterpretator.add_those [map fst dt_infos];
  14.295    in
  14.296      ({distinct = distinct,
  14.297        inject = inject,
  14.298 @@ -845,7 +808,6 @@
  14.299        case_thms = case_thms,
  14.300        split_thms = split_thms,
  14.301        induction = induction',
  14.302 -      size = size_thms,
  14.303        simps = simps}, thy11)
  14.304    end;
  14.305  
    15.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Sep 25 10:27:43 2007 +0200
    15.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Sep 25 12:16:08 2007 +0200
    15.3 @@ -24,8 +24,6 @@
    15.4      (string * sort) list -> theory -> term list list
    15.5    val make_splits : string list -> DatatypeAux.descr list ->
    15.6      (string * sort) list -> theory -> (term * term) list
    15.7 -  val make_size : DatatypeAux.descr list -> (string * sort) list ->
    15.8 -    theory -> term list
    15.9    val make_weak_case_congs : string list -> DatatypeAux.descr list ->
   15.10      (string * sort) list -> theory -> term list
   15.11    val make_case_congs : string list -> DatatypeAux.descr list ->
   15.12 @@ -61,7 +59,6 @@
   15.13    in indexify_names (map type_name Ts) end;
   15.14  
   15.15  
   15.16 -
   15.17  (************************* injectivity of constructors ************************)
   15.18  
   15.19  fun make_injs descr sorts =
   15.20 @@ -351,44 +348,6 @@
   15.21      (make_case_combs new_type_names descr sorts thy "f"))
   15.22    end;
   15.23  
   15.24 -
   15.25 -(******************************* size functions *******************************)
   15.26 -
   15.27 -fun make_size descr sorts thy =
   15.28 -  let
   15.29 -    val descr' = flat descr;
   15.30 -    val recTs = get_rec_types descr' sorts;
   15.31 -
   15.32 -    val Const (size_name, _) = HOLogic.size_const dummyT;
   15.33 -    val size_names = replicate (length (hd descr)) size_name @
   15.34 -      map (Sign.intern_const thy) (indexify_names
   15.35 -        (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
   15.36 -    val size_consts = map (fn (s, T) =>
   15.37 -      Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
   15.38 -
   15.39 -    fun plus (t1, t2) = Const ("HOL.plus_class.plus", HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   15.40 -
   15.41 -    fun make_size_eqn size_const T (cname, cargs) =
   15.42 -      let
   15.43 -        val recs = filter is_rec_type cargs;
   15.44 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   15.45 -        val recTs = map (typ_of_dtyp descr' sorts) recs;
   15.46 -        val tnames = make_tnames Ts;
   15.47 -        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   15.48 -        val ts = map (fn ((r, s), T) => nth size_consts (dest_DtRec r) $
   15.49 -          Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
   15.50 -        val t = if ts = [] then HOLogic.zero else
   15.51 -          foldl1 plus (ts @ [HOLogic.Suc_zero])
   15.52 -      in
   15.53 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
   15.54 -          list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
   15.55 -      end
   15.56 -
   15.57 -  in
   15.58 -    List.concat (map (fn (((_, (_, _, constrs)), size_const), T) =>
   15.59 -      map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs))
   15.60 -  end;
   15.61 -
   15.62  (************************* additional rules for TFL ***************************)
   15.63  
   15.64  fun make_weak_case_congs new_type_names descr sorts thy =
    16.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 10:27:43 2007 +0200
    16.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 12:16:08 2007 +0200
    16.3 @@ -8,8 +8,8 @@
    16.4  
    16.5  signature DATATYPE_REALIZER =
    16.6  sig
    16.7 -  val add_dt_realizers: (string * sort) list ->
    16.8 -    DatatypeAux.datatype_info list -> theory -> theory
    16.9 +  val add_dt_realizers: string list -> theory -> theory
   16.10 +  val setup: theory -> theory
   16.11  end;
   16.12  
   16.13  structure DatatypeRealizer : DATATYPE_REALIZER =
   16.14 @@ -40,7 +40,7 @@
   16.15  
   16.16  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
   16.17  
   16.18 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) (is, thy) =
   16.19 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
   16.20    let
   16.21      val recTs = get_rec_types descr sorts;
   16.22      val pnames = if length descr = 1 then ["P"]
   16.23 @@ -160,7 +160,7 @@
   16.24    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
   16.25  
   16.26  
   16.27 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
   16.28 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
   16.29    let
   16.30      val cert = cterm_of thy;
   16.31      val rT = TFree ("'P", HOLogic.typeS);
   16.32 @@ -216,11 +216,18 @@
   16.33       (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
   16.34    end;
   16.35  
   16.36 +fun add_dt_realizers names thy =
   16.37 +  if !proofs < 2 then thy
   16.38 +  else let
   16.39 +    val _ = message "Adding realizers for induction and case analysis ..."
   16.40 +    val infos = map (DatatypePackage.the_datatype thy) names;
   16.41 +    val info :: _ = infos;
   16.42 +  in
   16.43 +    thy
   16.44 +    |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
   16.45 +    |> fold_rev (make_casedists (#sorts info)) infos
   16.46 +  end;
   16.47  
   16.48 -fun add_dt_realizers sorts infos thy = if !proofs < 2 then thy else
   16.49 -  (message "Adding realizers for induction and case analysis ..."; thy
   16.50 -   |> curry (Library.foldr (make_ind sorts (hd infos)))
   16.51 -     (subsets 0 (length (#descr (hd infos)) - 1))
   16.52 -   |> curry (Library.foldr (make_casedists sorts)) infos);
   16.53 +val setup = DatatypePackage.add_interpretator add_dt_realizers;
   16.54  
   16.55  end;