src/HOL/Tools/datatype_package.ML
changeset 24699 c6674504103f
parent 24626 85eceef2edc7
child 24711 e8bba7723858
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 25 10:27:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 25 12:16:08 2007 +0200
     1.3 @@ -17,6 +17,16 @@
     1.4  sig
     1.5    include BASIC_DATATYPE_PACKAGE
     1.6    val quiet_mode : bool ref
     1.7 +  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
     1.8 +    (bstring * typ list * mixfix) list) list -> theory ->
     1.9 +      {distinct : thm list list,
    1.10 +       inject : thm list list,
    1.11 +       exhaustion : thm list,
    1.12 +       rec_thms : thm list,
    1.13 +       case_thms : thm list list,
    1.14 +       split_thms : (thm * thm) list,
    1.15 +       induction : thm,
    1.16 +       simps : thm list} * theory
    1.17    val add_datatype : bool -> string list -> (string list * bstring * mixfix *
    1.18      (bstring * string list * mixfix) list) list -> theory ->
    1.19        {distinct : thm list list,
    1.20 @@ -26,18 +36,6 @@
    1.21         case_thms : thm list list,
    1.22         split_thms : (thm * thm) list,
    1.23         induction : thm,
    1.24 -       size : thm list,
    1.25 -       simps : thm list} * theory
    1.26 -  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
    1.27 -    (bstring * typ list * mixfix) list) list -> theory ->
    1.28 -      {distinct : thm list list,
    1.29 -       inject : thm list list,
    1.30 -       exhaustion : thm list,
    1.31 -       rec_thms : thm list,
    1.32 -       case_thms : thm list list,
    1.33 -       split_thms : (thm * thm) list,
    1.34 -       induction : thm,
    1.35 -       size : thm list,
    1.36         simps : thm list} * theory
    1.37    val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
    1.38      (thm list * attribute list) list list -> (thm list * attribute list) ->
    1.39 @@ -49,7 +47,6 @@
    1.40         case_thms : thm list list,
    1.41         split_thms : (thm * thm) list,
    1.42         induction : thm,
    1.43 -       size : thm list,
    1.44         simps : thm list} * theory
    1.45    val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
    1.46      (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
    1.47 @@ -60,7 +57,6 @@
    1.48         case_thms : thm list list,
    1.49         split_thms : (thm * thm) list,
    1.50         induction : thm,
    1.51 -       size : thm list,
    1.52         simps : thm list} * theory
    1.53    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
    1.54    val get_datatype : theory -> string -> DatatypeAux.datatype_info option
    1.55 @@ -325,12 +321,12 @@
    1.56  
    1.57  end;
    1.58  
    1.59 -fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.60 +fun add_rules simps case_thms rec_thms inject distinct
    1.61                    weak_case_congs cong_att =
    1.62    PureThy.add_thmss [(("simps", simps), []),
    1.63 -    (("", flat case_thms @ size_thms @ 
    1.64 +    (("", flat case_thms @
    1.65            flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.66 -    (("", size_thms @ rec_thms), [RecfunCodegen.add_default]),
    1.67 +    (("", rec_thms), [RecfunCodegen.add_default]),
    1.68      (("", flat inject), [iff_add]),
    1.69      (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    1.70      (("", weak_case_congs), [cong_att])]
    1.71 @@ -460,11 +456,12 @@
    1.72  
    1.73  (**** make datatype info ****)
    1.74  
    1.75 -fun make_dt_info descr sorts induct reccomb_names rec_thms
    1.76 +fun make_dt_info head_len descr sorts induct reccomb_names rec_thms
    1.77      (((((((((i, (_, (tname, _, _))), case_name), case_thms),
    1.78        exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
    1.79    (tname,
    1.80     {index = i,
    1.81 +    head_len = head_len,
    1.82      descr = descr,
    1.83      sorts = sorts,
    1.84      rec_names = reccomb_names,
    1.85 @@ -522,9 +519,9 @@
    1.86  val specify_consts = gen_specify_consts Sign.add_consts_i;
    1.87  val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
    1.88  
    1.89 -structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
    1.90 +structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string list; val eq = op = end);
    1.91  
    1.92 -fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator;
    1.93 +fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator (fold interpretator);
    1.94  
    1.95  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.96      case_names_induct case_names_exhausts thy =
    1.97 @@ -534,10 +531,6 @@
    1.98      val used = map fst (fold Term.add_tfreesT recTs []);
    1.99      val newTs = Library.take (length (hd descr), recTs);
   1.100  
   1.101 -    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   1.102 -      (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
   1.103 -        cargs) constrs) descr';
   1.104 -
   1.105      (**** declare new types and constants ****)
   1.106  
   1.107      val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   1.108 @@ -554,9 +547,6 @@
   1.109        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   1.110          (1 upto (length descr')));
   1.111  
   1.112 -    val size_names = DatatypeProp.indexify_names
   1.113 -      (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
   1.114 -
   1.115      val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
   1.116      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   1.117        map (fn (_, cargs) =>
   1.118 @@ -565,22 +555,11 @@
   1.119  
   1.120      val case_names = map (fn s => (s ^ "_case")) new_type_names;
   1.121  
   1.122 -    fun instance_size_class tyco thy =
   1.123 -      let
   1.124 -        val n = Sign.arity_number thy tyco;
   1.125 -      in
   1.126 -        thy
   1.127 -        |> Class.prove_instance (Class.intro_classes_tac [])
   1.128 -            [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
   1.129 -        |> snd
   1.130 -      end
   1.131 -
   1.132      val thy2' = thy
   1.133  
   1.134        (** new types **)
   1.135        |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
   1.136             types_syntax tyvars
   1.137 -      |> fold (fn (_, (name, _, _)) => instance_size_class name) descr'
   1.138        |> add_path flat_names (space_implode "_" new_type_names)
   1.139  
   1.140        (** primrec combinators **)
   1.141 @@ -598,12 +577,6 @@
   1.142  
   1.143      val thy2 = thy2'
   1.144  
   1.145 -      (** size functions **)
   1.146 -
   1.147 -      |> (if no_size then I else specify_consts (map (fn (s, T) =>
   1.148 -        (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.149 -          (size_names ~~ Library.drop (length (hd descr), recTs))))
   1.150 -
   1.151        (** constructors **)
   1.152  
   1.153        |> parent_path flat_names
   1.154 @@ -619,18 +592,15 @@
   1.155      (**** introduction of axioms ****)
   1.156  
   1.157      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
   1.158 -    val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
   1.159  
   1.160      val ((([induct], [rec_thms]), inject), thy3) =
   1.161        thy2
   1.162        |> Theory.add_path (space_implode "_" new_type_names)
   1.163        |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
   1.164        ||>> add_axioms "recs" rec_axs []
   1.165 -      ||> (if no_size then I else add_axioms "size" size_axs [] #> snd)
   1.166        ||> Theory.parent_path
   1.167        ||>> add_and_get_axiomss "inject" new_type_names
   1.168              (DatatypeProp.make_injs descr sorts);
   1.169 -    val size_thms = if no_size then [] else get_thms thy3 (Name "size");
   1.170      val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
   1.171        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   1.172  
   1.173 @@ -651,27 +621,27 @@
   1.174      val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
   1.175        (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
   1.176  
   1.177 -    val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms)
   1.178 +    val dt_infos = map (make_dt_info (length (hd descr)) descr' sorts induct
   1.179 +        reccomb_names' rec_thms)
   1.180        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
   1.181          exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
   1.182            nchotomys ~~ case_congs ~~ weak_case_congs);
   1.183  
   1.184 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.185 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.186      val split_thms = split ~~ split_asm;
   1.187  
   1.188      val thy12 =
   1.189        thy11
   1.190        |> add_case_tr' case_names'
   1.191        |> Theory.add_path (space_implode "_" new_type_names)
   1.192 -      |> add_rules simps case_thms size_thms rec_thms inject distinct
   1.193 +      |> add_rules simps case_thms rec_thms inject distinct
   1.194            weak_case_congs Simplifier.cong_add
   1.195        |> put_dt_infos dt_infos
   1.196        |> add_cases_induct dt_infos induct
   1.197        |> Theory.parent_path
   1.198        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   1.199        |> snd
   1.200 -      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
   1.201 -      |> DatatypeInterpretator.add_those (map fst dt_infos);
   1.202 +      |> DatatypeInterpretator.add_those [map fst dt_infos];
   1.203    in
   1.204      ({distinct = distinct,
   1.205        inject = inject,
   1.206 @@ -680,7 +650,6 @@
   1.207        case_thms = case_thms,
   1.208        split_thms = split_thms,
   1.209        induction = induct,
   1.210 -      size = size_thms,
   1.211        simps = simps}, thy12)
   1.212    end;
   1.213  
   1.214 @@ -711,27 +680,25 @@
   1.215        descr sorts nchotomys case_thms thy8;
   1.216      val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.217        descr sorts thy9;
   1.218 -    val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
   1.219 -      descr sorts reccomb_names rec_thms thy10;
   1.220  
   1.221 -    val dt_infos = map (make_dt_info (flat descr) sorts induct reccomb_names rec_thms)
   1.222 +    val dt_infos = map (make_dt_info (length (hd descr)) (flat descr) sorts induct
   1.223 +        reccomb_names rec_thms)
   1.224        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   1.225          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.226  
   1.227 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.228 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.229  
   1.230      val thy12 =
   1.231 -      thy11
   1.232 +      thy10
   1.233        |> add_case_tr' case_names
   1.234        |> Theory.add_path (space_implode "_" new_type_names)
   1.235 -      |> add_rules simps case_thms size_thms rec_thms inject distinct
   1.236 +      |> add_rules simps case_thms rec_thms inject distinct
   1.237            weak_case_congs (Simplifier.attrib (op addcongs))
   1.238        |> put_dt_infos dt_infos
   1.239        |> add_cases_induct dt_infos induct
   1.240        |> Theory.parent_path
   1.241        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   1.242 -      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
   1.243 -      |> DatatypeInterpretator.add_those (map fst dt_infos);
   1.244 +      |> DatatypeInterpretator.add_those [map fst dt_infos];
   1.245    in
   1.246      ({distinct = distinct,
   1.247        inject = inject,
   1.248 @@ -740,7 +707,6 @@
   1.249        case_thms = case_thms,
   1.250        split_thms = split_thms,
   1.251        induction = induct,
   1.252 -      size = size_thms,
   1.253        simps = simps}, thy12)
   1.254    end;
   1.255  
   1.256 @@ -808,35 +774,32 @@
   1.257        [descr] sorts nchotomys case_thms thy6;
   1.258      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.259        [descr] sorts thy7;
   1.260 -    val (size_thms, thy9) =
   1.261 -      DatatypeAbsProofs.prove_size_thms false new_type_names
   1.262 -        [descr] sorts reccomb_names rec_thms thy8;
   1.263  
   1.264      val ((_, [induction']), thy10) =
   1.265 -      thy9
   1.266 +      thy8
   1.267        |> store_thmss "inject" new_type_names inject
   1.268        ||>> store_thmss "distinct" new_type_names distinct
   1.269        ||> Theory.add_path (space_implode "_" new_type_names)
   1.270        ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
   1.271  
   1.272 -    val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms)
   1.273 +    val dt_infos = map (make_dt_info (length descr) descr sorts induction'
   1.274 +        reccomb_names rec_thms)
   1.275        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
   1.276          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.277  
   1.278 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.279 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.280  
   1.281      val thy11 =
   1.282        thy10
   1.283        |> add_case_tr' case_names
   1.284 -      |> add_rules simps case_thms size_thms rec_thms inject distinct
   1.285 +      |> add_rules simps case_thms rec_thms inject distinct
   1.286             weak_case_congs (Simplifier.attrib (op addcongs))
   1.287        |> put_dt_infos dt_infos
   1.288        |> add_cases_induct dt_infos induction'
   1.289        |> Theory.parent_path
   1.290        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   1.291        |> snd
   1.292 -      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
   1.293 -      |> DatatypeInterpretator.add_those (map fst dt_infos);
   1.294 +      |> DatatypeInterpretator.add_those [map fst dt_infos];
   1.295    in
   1.296      ({distinct = distinct,
   1.297        inject = inject,
   1.298 @@ -845,7 +808,6 @@
   1.299        case_thms = case_thms,
   1.300        split_thms = split_thms,
   1.301        induction = induction',
   1.302 -      size = size_thms,
   1.303        simps = simps}, thy11)
   1.304    end;
   1.305