src/HOL/Tools/datatype_codegen.ML
changeset 21546 268b6bed0cc8
parent 21516 c2a116a2c4fd
child 21565 bd28361f4c5b
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Nov 27 13:42:30 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Nov 27 13:42:33 2006 +0100
     1.3 @@ -406,6 +406,8 @@
     1.4  local
     1.5    val not_sym = thm "HOL.not_sym";
     1.6    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     1.7 +  val refl = thm "refl";
     1.8 +  val eqTrueI = thm "eqTrueI";
     1.9  in
    1.10  
    1.11  fun get_eq_datatype thy dtco =
    1.12 @@ -416,11 +418,10 @@
    1.13          val ct' = Thm.cterm_of thy
    1.14            (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
    1.15          val cty' = Thm.ctyp_of_term ct';
    1.16 -        val refl = Thm.prop_of HOL.refl;
    1.17          val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
    1.18            (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
    1.19 -          refl NONE;
    1.20 -      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    1.21 +          (Thm.prop_of refl) NONE;
    1.22 +      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end;
    1.23      val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    1.24      val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    1.25      val ctxt = ProofContext.init thy;
    1.26 @@ -498,11 +499,26 @@
    1.27    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    1.28     of SOME _ => get_eq_datatype thy tyco
    1.29      | NONE => [TypecopyPackage.get_eq thy tyco];
    1.30 +  fun constrain_op_eq_thms thy thms =
    1.31 +    let
    1.32 +      fun add_eq (Const ("op =", ty)) =
    1.33 +            fold (insert (eq_fst (op =)))
    1.34 +              (Term.add_tvarsT ty [])
    1.35 +        | add_eq _ =
    1.36 +            I
    1.37 +      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    1.38 +      val instT = map (fn (v_i, sort) =>
    1.39 +        (Thm.ctyp_of thy (TVar (v_i, sort)),
    1.40 +           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
    1.41 +    in
    1.42 +      thms
    1.43 +      |> map (Thm.instantiate (instT, []))
    1.44 +    end;
    1.45  in
    1.46    fun get_eq thy tyco =
    1.47      get_eq_thms thy tyco
    1.48      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
    1.49 -    |> HOL.constrain_op_eq_thms thy
    1.50 +    |> constrain_op_eq_thms thy
    1.51  end;
    1.52  
    1.53  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list