src/HOL/Tools/Datatype/datatype.ML
changeset 32728 2c55fc50f670
parent 32727 9072201cd69d
child 32729 1441cf4ddc1a
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 10:20:21 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 10:51:12 2009 +0200
     1.3 @@ -347,41 +347,41 @@
     1.4      |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
     1.5    end;
     1.6  
     1.7 -fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy1 =
     1.8 +fun derive_datatype_props config dt_names alt_names descr sorts
     1.9 +    induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
    1.10    let
    1.11      val thy2 = thy1 |> Theory.checkpoint
    1.12 +    val flat_descr = flat descr;
    1.13      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.14 -    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.15 -    val (case_names_induct, case_names_exhausts) =
    1.16 -      (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
    1.17 +    val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
    1.18      val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.19  
    1.20      val (casedist_thms, thy3) = thy2 |>
    1.21 -      DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
    1.22 -        case_names_exhausts;
    1.23 +      DatatypeAbsProofs.prove_casedist_thms config new_type_names descr sorts induct
    1.24 +        (mk_case_names_exhausts flat_descr dt_names);
    1.25      val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
    1.26 -      config new_type_names [descr] sorts (get_all thy3) inject distinct
    1.27 +      config new_type_names descr sorts (get_all thy3) inject distinct_rewrites
    1.28        (Simplifier.theory_context thy3 dist_ss) induct thy3;
    1.29      val ((case_rewrites, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    1.30 -      config new_type_names [descr] sorts rec_names rec_rewrites thy4;
    1.31 +      config new_type_names descr sorts rec_names rec_rewrites thy4;
    1.32      val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
    1.33 -      config new_type_names [descr] sorts inject distinct casedist_thms case_rewrites thy5;
    1.34 +      config new_type_names descr sorts inject distinct_rewrites casedist_thms case_rewrites thy5;
    1.35      val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.36 -      [descr] sorts casedist_thms thy6;
    1.37 +      descr sorts casedist_thms thy6;
    1.38      val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
    1.39 -      [descr] sorts nchotomys case_rewrites thy7;
    1.40 +      descr sorts nchotomys case_rewrites thy7;
    1.41      val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    1.42 -      [descr] sorts thy8;
    1.43 +      descr sorts thy8;
    1.44  
    1.45 -    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
    1.46 -    val dt_infos = map (make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites)
    1.47 -      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_rewrites ~~ casedist_thms ~~
    1.48 -        map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.49 +    val simps = flat (distinct_rules @ inject @ case_rewrites) @ rec_rewrites;
    1.50 +    val dt_infos = map (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
    1.51 +      ((0 upto length descr - 1) ~~ flat_descr ~~ case_names ~~ case_rewrites ~~ casedist_thms ~~
    1.52 +        distinct_entry ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.53      val dt_names = map fst dt_infos;
    1.54    in
    1.55      thy9
    1.56      |> add_case_tr' case_names
    1.57 -    |> add_rules simps case_rewrites rec_rewrites inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
    1.58 +    |> add_rules simps case_rewrites rec_rewrites inject distinct_rules weak_case_congs (Simplifier.attrib (op addcongs))
    1.59      |> register dt_infos
    1.60      |> add_cases_induct dt_infos inducts
    1.61      |> Sign.parent_path
    1.62 @@ -398,17 +398,16 @@
    1.63    let
    1.64      val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
    1.65      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.66 -    val (case_names_induct, case_names_exhausts) =
    1.67 -      (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
    1.68      val (((inject, distinct), [induct]), thy2) =
    1.69        thy1
    1.70        |> store_thmss "inject" new_type_names raw_inject
    1.71        ||>> store_thmss "distinct" new_type_names raw_distinct
    1.72        ||> Sign.add_path (space_implode "_" new_type_names)
    1.73 -      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
    1.74 +      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])];
    1.75    in
    1.76      thy2
    1.77 -    |> derive_datatype_props config dt_names alt_names descr sorts induct inject distinct
    1.78 +    |> derive_datatype_props config dt_names alt_names [descr] sorts
    1.79 +         induct inject (distinct, distinct, map FewConstrs distinct)
    1.80   end;
    1.81  
    1.82  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
    1.83 @@ -482,18 +481,17 @@
    1.84  
    1.85  (** definitional introduction of datatypes **)
    1.86  
    1.87 -fun add_datatype_def config new_type_names descr sorts types_syntax constr_syntax dt_info
    1.88 -    case_names_induct case_names_exhausts thy =
    1.89 +fun add_datatype_def config dt_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
    1.90    let
    1.91 -    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.92 -
    1.93 +    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
    1.94 +    val flat_descr = flat descr;
    1.95      val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
    1.96        DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
    1.97 -        types_syntax constr_syntax case_names_induct;
    1.98 -    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.99 +        types_syntax constr_syntax (mk_case_names_induct flat_descr);
   1.100  
   1.101 +    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
   1.102      val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   1.103 -      sorts induct case_names_exhausts thy2;
   1.104 +      sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
   1.105      val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
   1.106        config new_type_names descr sorts dt_info inject dist_rewrites
   1.107        (Simplifier.theory_context thy3 dist_ss) induct thy3;
   1.108 @@ -509,7 +507,7 @@
   1.109        descr sorts thy9;
   1.110  
   1.111      val dt_infos = map
   1.112 -      (make_dt_info (SOME new_type_names) (flat descr) sorts induct inducts rec_names rec_rewrites)
   1.113 +      (make_dt_info (SOME new_type_names) flat_descr sorts induct inducts rec_names rec_rewrites)
   1.114        ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_rewrites ~~
   1.115          casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.116  
   1.117 @@ -534,7 +532,6 @@
   1.118      val _ = Theory.requires thy "Datatype" "datatype definitions";
   1.119  
   1.120      (* this theory is used just for parsing *)
   1.121 -
   1.122      val tmp_thy = thy |>
   1.123        Theory.copy |>
   1.124        Sign.add_types (map (fn (tvs, tname, mx, _) =>
   1.125 @@ -549,6 +546,7 @@
   1.126            | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
   1.127                " : " ^ commas dups))
   1.128        end) dts);
   1.129 +    val dt_names = map fst new_dts;
   1.130  
   1.131      val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
   1.132        [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   1.133 @@ -590,14 +588,8 @@
   1.134      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   1.135        if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   1.136        else raise exn;
   1.137 -
   1.138 -    val descr' = flat descr;
   1.139 -    val case_names_induct = mk_case_names_induct descr';
   1.140 -    val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   1.141    in
   1.142 -    add_datatype_def
   1.143 -      config new_type_names descr sorts types_syntax constr_syntax dt_info
   1.144 -      case_names_induct case_names_exhausts thy
   1.145 +    add_datatype_def config dt_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
   1.146    end;
   1.147  
   1.148  val add_datatype = gen_add_datatype cert_typ;