src/HOL/Tools/Datatype/datatype.ML
changeset 32727 9072201cd69d
parent 32722 ad04cda866be
child 32728 2c55fc50f670
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 09:47:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 10:20:21 2009 +0200
     1.3 @@ -218,26 +218,28 @@
     1.4  
     1.5  (* arrange data entries *)
     1.6  
     1.7 -fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
     1.8 -    ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
     1.9 -      exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
    1.10 +fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
    1.11 +    ((((((((((i, (_, (tname, _, _))), case_name), case_rewrites),
    1.12 +      exhaust), distinct), inject), (split, split_asm)), nchotomy), case_cong), weak_case_cong) =
    1.13    (tname,
    1.14     {index = i,
    1.15      alt_names = alt_names,
    1.16      descr = descr,
    1.17      sorts = sorts,
    1.18      inject = inject,
    1.19 -    distinct = distinct_thm,
    1.20 +    distinct = distinct,
    1.21 +    induct = induct,
    1.22      inducts = inducts,
    1.23 -    exhaust = exhaust_thm,
    1.24 +    exhaust = exhaust,
    1.25      nchotomy = nchotomy,
    1.26 -    rec_names = reccomb_names,
    1.27 -    rec_rewrites = rec_thms,
    1.28 +    rec_names = rec_names,
    1.29 +    rec_rewrites = rec_rewrites,
    1.30      case_name = case_name,
    1.31 -    case_rewrites = case_thms,
    1.32 +    case_rewrites = case_rewrites,
    1.33      case_cong = case_cong,
    1.34      weak_case_cong = weak_case_cong,
    1.35 -    splits = splits});
    1.36 +    split = split,
    1.37 +    split_asm = split_asm});
    1.38  
    1.39  (* case names *)
    1.40  
    1.41 @@ -320,12 +322,12 @@
    1.42    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.43  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    1.44  
    1.45 -fun add_rules simps case_thms rec_thms inject distinct
    1.46 +fun add_rules simps case_rewrites rec_rewrites inject distinct
    1.47                    weak_case_congs cong_att =
    1.48    PureThy.add_thmss [((Binding.name "simps", simps), []),
    1.49 -    ((Binding.empty, flat case_thms @
    1.50 -          flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.51 -    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
    1.52 +    ((Binding.empty, flat case_rewrites @
    1.53 +          flat distinct @ rec_rewrites), [Simplifier.simp_add]),
    1.54 +    ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
    1.55      ((Binding.empty, flat inject), [iff_add]),
    1.56      ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    1.57      ((Binding.empty, weak_case_congs), [cong_att])]
    1.58 @@ -357,29 +359,29 @@
    1.59      val (casedist_thms, thy3) = thy2 |>
    1.60        DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
    1.61          case_names_exhausts;
    1.62 -    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
    1.63 +    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
    1.64        config new_type_names [descr] sorts (get_all thy3) inject distinct
    1.65        (Simplifier.theory_context thy3 dist_ss) induct thy3;
    1.66 -    val ((case_thms, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    1.67 -      config new_type_names [descr] sorts reccomb_names rec_thms thy4;
    1.68 +    val ((case_rewrites, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    1.69 +      config new_type_names [descr] sorts rec_names rec_rewrites thy4;
    1.70      val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
    1.71 -      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy5;
    1.72 +      config new_type_names [descr] sorts inject distinct casedist_thms case_rewrites thy5;
    1.73      val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.74        [descr] sorts casedist_thms thy6;
    1.75      val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
    1.76 -      [descr] sorts nchotomys case_thms thy7;
    1.77 +      [descr] sorts nchotomys case_rewrites thy7;
    1.78      val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    1.79        [descr] sorts thy8;
    1.80  
    1.81 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.82 -    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct) reccomb_names rec_thms)
    1.83 -      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
    1.84 +    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
    1.85 +    val dt_infos = map (make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites)
    1.86 +      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_rewrites ~~ casedist_thms ~~
    1.87          map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.88      val dt_names = map fst dt_infos;
    1.89    in
    1.90      thy9
    1.91      |> add_case_tr' case_names
    1.92 -    |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
    1.93 +    |> add_rules simps case_rewrites rec_rewrites inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
    1.94      |> register dt_infos
    1.95      |> add_cases_induct dt_infos inducts
    1.96      |> Sign.parent_path
    1.97 @@ -492,33 +494,33 @@
    1.98  
    1.99      val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   1.100        sorts induct case_names_exhausts thy2;
   1.101 -    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
   1.102 +    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
   1.103        config new_type_names descr sorts dt_info inject dist_rewrites
   1.104        (Simplifier.theory_context thy3 dist_ss) induct thy3;
   1.105 -    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   1.106 -      config new_type_names descr sorts reccomb_names rec_thms thy4;
   1.107 +    val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   1.108 +      config new_type_names descr sorts rec_names rec_rewrites thy4;
   1.109      val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
   1.110 -      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   1.111 +      descr sorts inject dist_rewrites casedist_thms case_rewrites thy6;
   1.112      val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   1.113        descr sorts casedist_thms thy7;
   1.114      val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   1.115 -      descr sorts nchotomys case_thms thy8;
   1.116 +      descr sorts nchotomys case_rewrites thy8;
   1.117      val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.118        descr sorts thy9;
   1.119  
   1.120      val dt_infos = map
   1.121 -      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
   1.122 -      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
   1.123 +      (make_dt_info (SOME new_type_names) (flat descr) sorts induct inducts rec_names rec_rewrites)
   1.124 +      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_rewrites ~~
   1.125          casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.126  
   1.127 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.128 +    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
   1.129      val dt_names = map fst dt_infos;
   1.130  
   1.131      val thy12 =
   1.132        thy10
   1.133        |> add_case_tr' case_names
   1.134        |> Sign.add_path (space_implode "_" new_type_names)
   1.135 -      |> add_rules simps case_thms rec_thms inject distinct
   1.136 +      |> add_rules simps case_rewrites rec_rewrites inject distinct
   1.137            weak_case_congs (Simplifier.attrib (op addcongs))
   1.138        |> register dt_infos
   1.139        |> add_cases_induct dt_infos inducts