avoid compound fields in datatype info record
authorhaftmann
Mon Sep 28 10:20:21 2009 +0200 (2009-09-28 ago)
changeset 327279072201cd69d
parent 32723 866cebde3fca
child 32728 2c55fc50f670
avoid compound fields in datatype info record
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/old_primrec.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 28 09:47:32 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 28 10:20:21 2009 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4      val (full_new_type_names',thy1) =
     1.5        Datatype.add_datatype config new_type_names' dts'' thy;
     1.6  
     1.7 -    val {descr, inducts = (_, induct), ...} =
     1.8 +    val {descr, induct, ...} =
     1.9        Datatype.the_info thy1 (hd full_new_type_names');
    1.10      fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
    1.11  
     2.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 09:47:32 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 10:20:21 2009 +0200
     2.3 @@ -218,26 +218,28 @@
     2.4  
     2.5  (* arrange data entries *)
     2.6  
     2.7 -fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
     2.8 -    ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
     2.9 -      exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
    2.10 +fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
    2.11 +    ((((((((((i, (_, (tname, _, _))), case_name), case_rewrites),
    2.12 +      exhaust), distinct), inject), (split, split_asm)), nchotomy), case_cong), weak_case_cong) =
    2.13    (tname,
    2.14     {index = i,
    2.15      alt_names = alt_names,
    2.16      descr = descr,
    2.17      sorts = sorts,
    2.18      inject = inject,
    2.19 -    distinct = distinct_thm,
    2.20 +    distinct = distinct,
    2.21 +    induct = induct,
    2.22      inducts = inducts,
    2.23 -    exhaust = exhaust_thm,
    2.24 +    exhaust = exhaust,
    2.25      nchotomy = nchotomy,
    2.26 -    rec_names = reccomb_names,
    2.27 -    rec_rewrites = rec_thms,
    2.28 +    rec_names = rec_names,
    2.29 +    rec_rewrites = rec_rewrites,
    2.30      case_name = case_name,
    2.31 -    case_rewrites = case_thms,
    2.32 +    case_rewrites = case_rewrites,
    2.33      case_cong = case_cong,
    2.34      weak_case_cong = weak_case_cong,
    2.35 -    splits = splits});
    2.36 +    split = split,
    2.37 +    split_asm = split_asm});
    2.38  
    2.39  (* case names *)
    2.40  
    2.41 @@ -320,12 +322,12 @@
    2.42    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    2.43  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    2.44  
    2.45 -fun add_rules simps case_thms rec_thms inject distinct
    2.46 +fun add_rules simps case_rewrites rec_rewrites inject distinct
    2.47                    weak_case_congs cong_att =
    2.48    PureThy.add_thmss [((Binding.name "simps", simps), []),
    2.49 -    ((Binding.empty, flat case_thms @
    2.50 -          flat distinct @ rec_thms), [Simplifier.simp_add]),
    2.51 -    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
    2.52 +    ((Binding.empty, flat case_rewrites @
    2.53 +          flat distinct @ rec_rewrites), [Simplifier.simp_add]),
    2.54 +    ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
    2.55      ((Binding.empty, flat inject), [iff_add]),
    2.56      ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    2.57      ((Binding.empty, weak_case_congs), [cong_att])]
    2.58 @@ -357,29 +359,29 @@
    2.59      val (casedist_thms, thy3) = thy2 |>
    2.60        DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
    2.61          case_names_exhausts;
    2.62 -    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
    2.63 +    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
    2.64        config new_type_names [descr] sorts (get_all thy3) inject distinct
    2.65        (Simplifier.theory_context thy3 dist_ss) induct thy3;
    2.66 -    val ((case_thms, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    2.67 -      config new_type_names [descr] sorts reccomb_names rec_thms thy4;
    2.68 +    val ((case_rewrites, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    2.69 +      config new_type_names [descr] sorts rec_names rec_rewrites thy4;
    2.70      val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
    2.71 -      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy5;
    2.72 +      config new_type_names [descr] sorts inject distinct casedist_thms case_rewrites thy5;
    2.73      val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    2.74        [descr] sorts casedist_thms thy6;
    2.75      val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
    2.76 -      [descr] sorts nchotomys case_thms thy7;
    2.77 +      [descr] sorts nchotomys case_rewrites thy7;
    2.78      val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    2.79        [descr] sorts thy8;
    2.80  
    2.81 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    2.82 -    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct) reccomb_names rec_thms)
    2.83 -      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
    2.84 +    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
    2.85 +    val dt_infos = map (make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites)
    2.86 +      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_rewrites ~~ casedist_thms ~~
    2.87          map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    2.88      val dt_names = map fst dt_infos;
    2.89    in
    2.90      thy9
    2.91      |> add_case_tr' case_names
    2.92 -    |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
    2.93 +    |> add_rules simps case_rewrites rec_rewrites inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
    2.94      |> register dt_infos
    2.95      |> add_cases_induct dt_infos inducts
    2.96      |> Sign.parent_path
    2.97 @@ -492,33 +494,33 @@
    2.98  
    2.99      val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   2.100        sorts induct case_names_exhausts thy2;
   2.101 -    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
   2.102 +    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
   2.103        config new_type_names descr sorts dt_info inject dist_rewrites
   2.104        (Simplifier.theory_context thy3 dist_ss) induct thy3;
   2.105 -    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   2.106 -      config new_type_names descr sorts reccomb_names rec_thms thy4;
   2.107 +    val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   2.108 +      config new_type_names descr sorts rec_names rec_rewrites thy4;
   2.109      val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
   2.110 -      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   2.111 +      descr sorts inject dist_rewrites casedist_thms case_rewrites thy6;
   2.112      val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   2.113        descr sorts casedist_thms thy7;
   2.114      val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   2.115 -      descr sorts nchotomys case_thms thy8;
   2.116 +      descr sorts nchotomys case_rewrites thy8;
   2.117      val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   2.118        descr sorts thy9;
   2.119  
   2.120      val dt_infos = map
   2.121 -      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
   2.122 -      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
   2.123 +      (make_dt_info (SOME new_type_names) (flat descr) sorts induct inducts rec_names rec_rewrites)
   2.124 +      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_rewrites ~~
   2.125          casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   2.126  
   2.127 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   2.128 +    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
   2.129      val dt_names = map fst dt_infos;
   2.130  
   2.131      val thy12 =
   2.132        thy10
   2.133        |> add_case_tr' case_names
   2.134        |> Sign.add_path (space_implode "_" new_type_names)
   2.135 -      |> add_rules simps case_thms rec_thms inject distinct
   2.136 +      |> add_rules simps case_rewrites rec_rewrites inject distinct
   2.137            weak_case_congs (Simplifier.attrib (op addcongs))
   2.138        |> register dt_infos
   2.139        |> add_cases_induct dt_infos inducts
     3.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 09:47:32 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 10:20:21 2009 +0200
     3.3 @@ -193,7 +193,8 @@
     3.4     sorts : (string * sort) list,
     3.5     inject : thm list,
     3.6     distinct : simproc_dist,
     3.7 -   inducts : thm list * thm,
     3.8 +   induct : thm,
     3.9 +   inducts : thm list,
    3.10     exhaust : thm,
    3.11     nchotomy : thm,
    3.12     rec_names : string list,
    3.13 @@ -202,7 +203,8 @@
    3.14     case_rewrites : thm list,
    3.15     case_cong : thm,
    3.16     weak_case_cong : thm,
    3.17 -   splits : thm * thm};
    3.18 +   split : thm,
    3.19 +   split_asm: thm};
    3.20  
    3.21  fun mk_Free s T i = Free (s ^ (string_of_int i), T);
    3.22  
     4.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 28 09:47:32 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 28 10:20:21 2009 +0200
     4.3 @@ -38,7 +38,7 @@
     4.4  
     4.5  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
     4.6  
     4.7 -fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy =
     4.8 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
     4.9    let
    4.10      val recTs = get_rec_types descr sorts;
    4.11      val pnames = if length descr = 1 then ["P"]
     5.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Sep 28 09:47:32 2009 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Sep 28 10:20:21 2009 +0200
     5.3 @@ -389,7 +389,7 @@
     5.4      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
     5.5        let
     5.6          val (_, (tname, _, _)) = hd ds;
     5.7 -        val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname;
     5.8 +        val induct = (#induct o the o Symtab.lookup dt_info) tname;
     5.9  
    5.10          fun mk_ind_concl (i, _) =
    5.11            let
     6.1 --- a/src/HOL/Tools/Function/size.ML	Mon Sep 28 09:47:32 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/size.ML	Mon Sep 28 10:20:21 2009 +0200
     6.3 @@ -59,7 +59,7 @@
     6.4  
     6.5  fun prove_size_thms (info : info) new_type_names thy =
     6.6    let
     6.7 -    val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info;
     6.8 +    val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info;
     6.9      val l = length new_type_names;
    6.10      val alt_names' = (case alt_names of
    6.11        NONE => replicate l NONE | SOME names => map SOME names);
     7.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 28 09:47:32 2009 +0200
     7.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 28 10:20:21 2009 +0200
     7.3 @@ -96,7 +96,7 @@
     7.4                     | TVar((s,i),_) => error ("Free variable: " ^ s)
     7.5        val dt = Datatype.the_info thy ty_str
     7.6      in
     7.7 -      cases_thm_of_induct_thm (snd (#inducts dt))
     7.8 +      cases_thm_of_induct_thm (#induct dt)
     7.9      end;
    7.10  
    7.11  (*
     8.1 --- a/src/HOL/Tools/old_primrec.ML	Mon Sep 28 09:47:32 2009 +0200
     8.2 +++ b/src/HOL/Tools/old_primrec.ML	Mon Sep 28 10:20:21 2009 +0200
     8.3 @@ -230,7 +230,7 @@
     8.4                (tname, dt)::(find_dts dt_info tnames' tnames)
     8.5              else find_dts dt_info tnames' tnames);
     8.6  
     8.7 -fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
     8.8 +fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
     8.9    let
    8.10      fun constrs_of (_, (_, _, cs)) =
    8.11        map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;