src/HOL/Tools/Datatype/datatype.ML
changeset 32720 fc32e6771749
parent 32719 36cae240b46c
child 32721 a5fcc7960681
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:34:50 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:43:47 2009 +0200
     1.3 @@ -347,61 +347,55 @@
     1.4  
     1.5  (** declare existing type as datatype **)
     1.6  
     1.7 -fun prove_rep_datatype (config : config) dt_names alt_names descr sorts induct inject half_distinct thy =
     1.8 +fun prove_rep_datatype (config : config) dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
     1.9    let
    1.10 -
    1.11 -    val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
    1.12 -
    1.13 +    val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
    1.14      val new_type_names = map Long_Name.base_name (the_default dt_names alt_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 (((inject, distinct), [induct]), thy2) =
    1.18 +      thy1
    1.19 +      |> store_thmss "inject" new_type_names raw_inject
    1.20 +      ||>> store_thmss "distinct" new_type_names raw_distinct
    1.21 +      ||> Sign.add_path (space_implode "_" new_type_names)
    1.22 +      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
    1.23  
    1.24      val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.25 -
    1.26 -    val (casedist_thms, thy2) = thy |>
    1.27 +    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.28 +    val (casedist_thms, thy3) = thy2 |>
    1.29        DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
    1.30          case_names_exhausts;
    1.31 -    val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
    1.32 -      config new_type_names [descr] sorts (get_all thy) inject distinct
    1.33 -      (Simplifier.theory_context thy2 dist_ss) induct thy2;
    1.34 -    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
    1.35 -      config new_type_names [descr] sorts reccomb_names rec_thms thy3;
    1.36 -    val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
    1.37 -      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
    1.38 -    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.39 -      [descr] sorts casedist_thms thy5;
    1.40 -    val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
    1.41 -      [descr] sorts nchotomys case_thms thy6;
    1.42 -    val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    1.43 -      [descr] sorts thy7;
    1.44 +    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
    1.45 +      config new_type_names [descr] sorts (get_all thy3) inject distinct
    1.46 +      (Simplifier.theory_context thy3 dist_ss) induct thy3;
    1.47 +    val ((case_thms, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
    1.48 +      config new_type_names [descr] sorts reccomb_names rec_thms thy4;
    1.49 +    val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
    1.50 +      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy5;
    1.51 +    val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.52 +      [descr] sorts casedist_thms thy6;
    1.53 +    val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
    1.54 +      [descr] sorts nchotomys case_thms thy7;
    1.55 +    val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    1.56 +      [descr] sorts thy8;
    1.57  
    1.58 -    val ((_, [induct']), thy10) =
    1.59 -      thy8
    1.60 -      |> store_thmss "inject" new_type_names inject
    1.61 -      ||>> store_thmss "distinct" new_type_names distinct
    1.62 -      ||> Sign.add_path (space_implode "_" new_type_names)
    1.63 -      ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
    1.64 -    val inducts = Project_Rule.projections (ProofContext.init thy10) induct';
    1.65 -
    1.66 -    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct') reccomb_names rec_thms)
    1.67 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.68 +    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct) reccomb_names rec_thms)
    1.69        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
    1.70          map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.71 -
    1.72 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.73      val dt_names = map fst dt_infos;
    1.74 -
    1.75 -    val thy11 =
    1.76 -      thy10
    1.77 -      |> add_case_tr' case_names
    1.78 -      |> add_rules simps case_thms rec_thms inject distinct
    1.79 -           weak_case_congs (Simplifier.attrib (op addcongs))
    1.80 -      |> register dt_infos
    1.81 -      |> add_cases_induct dt_infos inducts
    1.82 -      |> Sign.parent_path
    1.83 -      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.84 -      |> snd
    1.85 -      |> DatatypeInterpretation.data (config, dt_names);
    1.86 -  in (dt_names, thy11) end;
    1.87 +  in
    1.88 +    thy9
    1.89 +    |> add_case_tr' case_names
    1.90 +    |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
    1.91 +    |> register dt_infos
    1.92 +    |> add_cases_induct dt_infos inducts
    1.93 +    |> Sign.parent_path
    1.94 +    |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.95 +    |> snd
    1.96 +    |> DatatypeInterpretation.data (config, dt_names)
    1.97 +    |> pair dt_names
    1.98 +  end;
    1.99  
   1.100  fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   1.101    let