shared code between rep_datatype and datatype
authorhaftmann
Mon Sep 28 14:48:30 2009 +0200 (2009-09-28)
changeset 327291441cf4ddc1a
parent 32728 2c55fc50f670
child 32730 3958b45b29e4
shared code between rep_datatype and datatype
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 10:51:12 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 14:48:30 2009 +0200
     1.3 @@ -216,31 +216,6 @@
     1.4         | dups => error ("Inconsistent sort constraints for " ^ commas dups))
     1.5    end;
     1.6  
     1.7 -(* arrange data entries *)
     1.8 -
     1.9 -fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
    1.10 -    ((((((((((i, (_, (tname, _, _))), case_name), case_rewrites),
    1.11 -      exhaust), distinct), inject), (split, split_asm)), nchotomy), case_cong), weak_case_cong) =
    1.12 -  (tname,
    1.13 -   {index = i,
    1.14 -    alt_names = alt_names,
    1.15 -    descr = descr,
    1.16 -    sorts = sorts,
    1.17 -    inject = inject,
    1.18 -    distinct = distinct,
    1.19 -    induct = induct,
    1.20 -    inducts = inducts,
    1.21 -    exhaust = exhaust,
    1.22 -    nchotomy = nchotomy,
    1.23 -    rec_names = rec_names,
    1.24 -    rec_rewrites = rec_rewrites,
    1.25 -    case_name = case_name,
    1.26 -    case_rewrites = case_rewrites,
    1.27 -    case_cong = case_cong,
    1.28 -    weak_case_cong = weak_case_cong,
    1.29 -    split = split,
    1.30 -    split_asm = split_asm});
    1.31 -
    1.32  (* case names *)
    1.33  
    1.34  local
    1.35 @@ -322,6 +297,29 @@
    1.36    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.37  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    1.38  
    1.39 +fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
    1.40 +    (index, (((((((((((_, (tname, _, _))), inject), distinct),
    1.41 +      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
    1.42 +  (tname,
    1.43 +   {index = index,
    1.44 +    alt_names = alt_names,
    1.45 +    descr = descr,
    1.46 +    sorts = sorts,
    1.47 +    inject = inject,
    1.48 +    distinct = distinct,
    1.49 +    induct = induct,
    1.50 +    inducts = inducts,
    1.51 +    exhaust = exhaust,
    1.52 +    nchotomy = nchotomy,
    1.53 +    rec_names = rec_names,
    1.54 +    rec_rewrites = rec_rewrites,
    1.55 +    case_name = case_name,
    1.56 +    case_rewrites = case_rewrites,
    1.57 +    case_cong = case_cong,
    1.58 +    weak_case_cong = weak_case_cong,
    1.59 +    split = split,
    1.60 +    split_asm = split_asm});
    1.61 +
    1.62  fun add_rules simps case_rewrites rec_rewrites inject distinct
    1.63                    weak_case_congs cong_att =
    1.64    PureThy.add_thmss [((Binding.name "simps", simps), []),
    1.65 @@ -350,38 +348,39 @@
    1.66  fun derive_datatype_props config dt_names alt_names descr sorts
    1.67      induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
    1.68    let
    1.69 -    val thy2 = thy1 |> Theory.checkpoint
    1.70 +    val thy2 = thy1 |> Theory.checkpoint;
    1.71      val flat_descr = flat descr;
    1.72      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.73      val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
    1.74 +
    1.75      val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.76 -
    1.77 -    val (casedist_thms, thy3) = thy2 |>
    1.78 -      DatatypeAbsProofs.prove_casedist_thms config new_type_names descr sorts induct
    1.79 -        (mk_case_names_exhausts flat_descr dt_names);
    1.80 -    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
    1.81 -      config new_type_names descr sorts (get_all thy3) inject distinct_rewrites
    1.82 -      (Simplifier.theory_context thy3 dist_ss) induct thy3;
    1.83 -    val ((case_rewrites, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    1.84 -      config new_type_names descr sorts rec_names rec_rewrites thy4;
    1.85 -    val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
    1.86 -      config new_type_names descr sorts inject distinct_rewrites casedist_thms case_rewrites thy5;
    1.87 -    val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.88 -      descr sorts casedist_thms thy6;
    1.89 -    val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
    1.90 -      descr sorts nchotomys case_rewrites thy7;
    1.91 -    val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    1.92 -      descr sorts thy8;
    1.93 +    val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
    1.94 +      descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
    1.95 +    val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.96 +      descr sorts exhaust thy3;
    1.97 +    val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
    1.98 +      config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
    1.99 +      inject distinct_rewrites (Simplifier.theory_context thy4 dist_ss) induct thy4;
   1.100 +    val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   1.101 +      config new_type_names descr sorts rec_names rec_rewrites thy5;
   1.102 +    val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
   1.103 +      descr sorts nchotomys case_rewrites thy6;
   1.104 +    val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.105 +      descr sorts thy7;
   1.106 +    val (split_thms, thy9) = DatatypeAbsProofs.prove_split_thms
   1.107 +      config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
   1.108  
   1.109      val simps = flat (distinct_rules @ inject @ case_rewrites) @ rec_rewrites;
   1.110 -    val dt_infos = map (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
   1.111 -      ((0 upto length descr - 1) ~~ flat_descr ~~ case_names ~~ case_rewrites ~~ casedist_thms ~~
   1.112 -        distinct_entry ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.113 +    val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
   1.114 +      (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
   1.115 +        case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ split_thms);
   1.116      val dt_names = map fst dt_infos;
   1.117    in
   1.118      thy9
   1.119      |> add_case_tr' case_names
   1.120 -    |> add_rules simps case_rewrites rec_rewrites inject distinct_rules weak_case_congs (Simplifier.attrib (op addcongs))
   1.121 +    |> Sign.add_path (space_implode "_" new_type_names)
   1.122 +    |> add_rules simps case_rewrites rec_rewrites inject distinct_rules
   1.123 +         weak_case_congs (Simplifier.attrib (op addcongs))
   1.124      |> register dt_infos
   1.125      |> add_cases_induct dt_infos inducts
   1.126      |> Sign.parent_path
   1.127 @@ -394,7 +393,7 @@
   1.128  
   1.129  (** declare existing type as datatype **)
   1.130  
   1.131 -fun prove_rep_datatype config dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
   1.132 +fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
   1.133    let
   1.134      val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
   1.135      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
   1.136 @@ -403,7 +402,8 @@
   1.137        |> store_thmss "inject" new_type_names raw_inject
   1.138        ||>> store_thmss "distinct" new_type_names raw_distinct
   1.139        ||> Sign.add_path (space_implode "_" new_type_names)
   1.140 -      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])];
   1.141 +      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
   1.142 +      ||> Sign.restore_naming thy1;
   1.143    in
   1.144      thy2
   1.145      |> derive_datatype_props config dt_names alt_names [descr] sorts
   1.146 @@ -461,12 +461,12 @@
   1.147  
   1.148      fun after_qed' raw_thms =
   1.149        let
   1.150 -        val [[[induct]], injs, half_distincts] =
   1.151 +        val [[[raw_induct]], raw_inject, half_distinct] =
   1.152            unflat rules (map Drule.zero_var_indexes_list raw_thms);
   1.153              (*FIXME somehow dubious*)
   1.154        in
   1.155          ProofContext.theory_result
   1.156 -          (prove_rep_datatype config dt_names alt_names descr vs induct injs half_distincts)
   1.157 +          (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
   1.158          #-> after_qed
   1.159        end;
   1.160    in
   1.161 @@ -481,52 +481,6 @@
   1.162  
   1.163  (** definitional introduction of datatypes **)
   1.164  
   1.165 -fun add_datatype_def config dt_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   1.166 -  let
   1.167 -    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   1.168 -    val flat_descr = flat descr;
   1.169 -    val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
   1.170 -      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   1.171 -        types_syntax constr_syntax (mk_case_names_induct flat_descr);
   1.172 -
   1.173 -    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
   1.174 -    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   1.175 -      sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
   1.176 -    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
   1.177 -      config new_type_names descr sorts dt_info inject dist_rewrites
   1.178 -      (Simplifier.theory_context thy3 dist_ss) induct thy3;
   1.179 -    val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   1.180 -      config new_type_names descr sorts rec_names rec_rewrites thy4;
   1.181 -    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
   1.182 -      descr sorts inject dist_rewrites casedist_thms case_rewrites thy6;
   1.183 -    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   1.184 -      descr sorts casedist_thms thy7;
   1.185 -    val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   1.186 -      descr sorts nchotomys case_rewrites thy8;
   1.187 -    val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.188 -      descr sorts thy9;
   1.189 -
   1.190 -    val dt_infos = map
   1.191 -      (make_dt_info (SOME new_type_names) flat_descr sorts induct inducts rec_names rec_rewrites)
   1.192 -      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_rewrites ~~
   1.193 -        casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.194 -
   1.195 -    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
   1.196 -    val dt_names = map fst dt_infos;
   1.197 -
   1.198 -    val thy12 =
   1.199 -      thy10
   1.200 -      |> add_case_tr' case_names
   1.201 -      |> Sign.add_path (space_implode "_" new_type_names)
   1.202 -      |> add_rules simps case_rewrites rec_rewrites inject distinct
   1.203 -          weak_case_congs (Simplifier.attrib (op addcongs))
   1.204 -      |> register dt_infos
   1.205 -      |> add_cases_induct dt_infos inducts
   1.206 -      |> Sign.parent_path
   1.207 -      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   1.208 -      |> DatatypeInterpretation.data (config, map fst dt_infos);
   1.209 -  in (dt_names, thy12) end;
   1.210 -
   1.211  fun gen_add_datatype prep_typ config new_type_names dts thy =
   1.212    let
   1.213      val _ = Theory.requires thy "Datatype" "datatype definitions";
   1.214 @@ -588,8 +542,14 @@
   1.215      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   1.216        if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   1.217        else raise exn;
   1.218 +
   1.219 +    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   1.220 +    val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
   1.221 +      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   1.222 +        types_syntax constr_syntax (mk_case_names_induct (flat descr));
   1.223    in
   1.224 -    add_datatype_def config dt_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
   1.225 +    derive_datatype_props config dt_names (SOME new_type_names) descr sorts
   1.226 +      induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'
   1.227    end;
   1.228  
   1.229  val add_datatype = gen_add_datatype cert_typ;
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Sep 28 10:51:12 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Sep 28 14:48:30 2009 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4      attribute list -> theory -> thm list * theory
     2.5    val prove_primrec_thms : config -> string list ->
     2.6      descr list -> (string * sort) list ->
     2.7 -      info Symtab.table -> thm list list -> thm list list ->
     2.8 +      (string -> thm list) -> thm list list -> thm list list ->
     2.9          simpset -> thm -> theory -> (string list * thm list) * theory
    2.10    val prove_case_thms : config -> string list ->
    2.11      descr list -> (string * sort) list ->
    2.12 @@ -88,7 +88,7 @@
    2.13  (*************************** primrec combinators ******************************)
    2.14  
    2.15  fun prove_primrec_thms (config : config) new_type_names descr sorts
    2.16 -    (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    2.17 +    injects_of constr_inject dist_rewrites dist_ss induct thy =
    2.18    let
    2.19      val _ = message config "Constructing primrec combinators ...";
    2.20  
    2.21 @@ -174,11 +174,11 @@
    2.22  
    2.23          val inject = map (fn r => r RS iffD1)
    2.24            (if i < length newTs then List.nth (constr_inject, i)
    2.25 -            else #inject (the (Symtab.lookup dt_info tname)));
    2.26 +            else injects_of tname);
    2.27  
    2.28          fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
    2.29            let
    2.30 -            val k = length (List.filter is_rec_type cargs)
    2.31 +            val k = length (filter is_rec_type cargs)
    2.32  
    2.33            in (EVERY [DETERM tac,
    2.34                  REPEAT (etac ex1E 1), rtac ex1I 1,