src/HOL/Tools/datatype_rep_proofs.ML
changeset 8436 8a87fa482baf
parent 8305 93aa21ec5494
child 8479 5d327a46dc61
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Mar 13 13:22:31 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Mar 13 13:24:12 2000 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     1.5      string list -> (int * (string * DatatypeAux.dtyp list *
     1.6        (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.7 -        (string * mixfix) list -> (string * mixfix) list list -> theory ->
     1.8 -          theory * thm list list * thm list list * thm list list *
     1.9 +        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    1.10 +          -> theory -> theory * thm list list * thm list list * thm list list *
    1.11              DatatypeAux.simproc_dist list * thm
    1.12  end;
    1.13  
    1.14 @@ -42,7 +42,7 @@
    1.15  (******************************************************************************)
    1.16  
    1.17  fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    1.18 -      new_type_names descr sorts types_syntax constr_syntax thy =
    1.19 +      new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    1.20    let
    1.21      val Datatype_thy = theory "Datatype";
    1.22      val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
    1.23 @@ -231,12 +231,11 @@
    1.24          val def_name = (Sign.base_name cname) ^ "_def";
    1.25          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.26            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
    1.27 -        val thy' = thy |>
    1.28 +        val (thy', [def_thm]) = thy |>
    1.29            Theory.add_consts_i [(cname', constrT, mx)] |>
    1.30            (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
    1.31  
    1.32 -      in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
    1.33 -      end;
    1.34 +      in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    1.35  
    1.36      (* constructor definitions for datatype *)
    1.37  
    1.38 @@ -382,8 +381,7 @@
    1.39          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    1.40            equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
    1.41              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
    1.42 -        val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    1.43 -        val def_thms = map (get_thm thy') (map fst defs);
    1.44 +        val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    1.45  
    1.46          (* prove characteristic equations *)
    1.47  
    1.48 @@ -580,8 +578,8 @@
    1.49        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
    1.50  
    1.51      val thy6 = thy5 |> parent_path flat_names |>
    1.52 -      store_thmss "inject" new_type_names constr_inject |>
    1.53 -      store_thmss "distinct" new_type_names distinct_thms;
    1.54 +      (#1 o store_thmss "inject" new_type_names constr_inject) |>
    1.55 +      (#1 o store_thmss "distinct" new_type_names distinct_thms);
    1.56  
    1.57      (*************************** induction theorem ****************************)
    1.58  
    1.59 @@ -638,12 +636,12 @@
    1.60                rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
    1.61                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    1.62  
    1.63 -    val thy7 = thy6 |>
    1.64 +    val (thy7, [dt_induct']) = thy6 |>
    1.65        Theory.add_path big_name |>
    1.66 -      PureThy.add_thms [(("induct", dt_induct), [])] |>
    1.67 +      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.68        Theory.parent_path;
    1.69  
    1.70 -  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
    1.71 +  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
    1.72    end;
    1.73  
    1.74  end;