src/HOL/Tools/datatype_package.ML
changeset 19008 14c1b2f5dda4
parent 18988 d6e5fa2ba8b8
child 19046 bc5c6c9b114e
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Feb 10 02:22:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Feb 10 09:09:07 2006 +0100
     1.3 @@ -70,6 +70,7 @@
     1.4    val get_datatype_case_consts : theory -> string list
     1.5    val get_case_const_data : theory -> string -> (string * int) list option
     1.6    val get_all_datatype_cons : theory -> (string * string) list
     1.7 +  val get_eq_equations: theory -> string -> thm list
     1.8    val constrs_of : theory -> string -> term list option
     1.9    val case_const_of : theory -> string -> term option
    1.10    val weak_case_congs_of : theory -> thm list
    1.11 @@ -159,6 +160,32 @@
    1.12      (fn (co, _) => cons (co, dtco))
    1.13        ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
    1.14  
    1.15 +fun get_eq_equations thy dtco =
    1.16 +  case get_datatype thy dtco
    1.17 +   of SOME (vars, cos) =>
    1.18 +        let
    1.19 +          fun co_inject thm =
    1.20 +            ((fst o dest_Const o fst o strip_comb o fst o HOLogic.dest_eq o fst
    1.21 +              o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm, thm RS HOL.eq_reflection);
    1.22 +          val inject = (map co_inject o #inject o the o datatype_info thy) dtco;
    1.23 +          fun mk_refl co =
    1.24 +            let
    1.25 +              fun infer t =
    1.26 +                (fst o Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) (K NONE) (K NONE) [] true)
    1.27 +                  ([t], Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vars))
    1.28 +              val t = (Thm.cterm_of thy o infer) (Const (co, dummyT));
    1.29 +            in
    1.30 +              HOL.refl 
    1.31 +              |> Drule.instantiate' [(SOME o Thm.ctyp_of_term) t] [SOME t]
    1.32 +              |> (fn thm => thm RS Eq_TrueI)
    1.33 +            end;
    1.34 +          fun get_eq co =
    1.35 +           case AList.lookup (op =) inject co
    1.36 +            of SOME eq => eq
    1.37 +             | NONE => mk_refl co;
    1.38 +        in map (get_eq o fst) cos end
    1.39 +   | NONE => [];
    1.40 +
    1.41  fun find_tname var Bi =
    1.42    let val frees = map dest_Free (term_frees Bi)
    1.43        val params = rename_wrt_term Bi (Logic.strip_params Bi);