src/HOL/Tools/typecopy_package.ML

non left-linear equations for nbe

(*  Title:      HOL/Tools/typecopy_package.ML
    ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen

Introducing copies of types using trivial typedefs; datatype-like abstraction.
*)

signature TYPECOPY_PACKAGE =
sig
  type info = {
    vs: (string * sort) list,
    constr: string,
    typ: typ,
    inject: thm,
    proj: string * typ,
    proj_def: thm
  }
  val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
    -> theory -> (string * info) * theory
  val get_typecopies: theory -> string list
  val get_info: theory -> string -> info option
  val interpretation: (string -> theory -> theory) -> theory -> theory
  val print_typecopies: theory -> unit
  val setup: theory -> theory
end;

structure TypecopyPackage: TYPECOPY_PACKAGE =
struct

(* theory data *)

type info = {
  vs: (string * sort) list,
  constr: string,
  typ: typ,
  inject: thm,
  proj: string * typ,
  proj_def: thm
};

structure TypecopyData = TheoryDataFun
(
  type T = info Symtab.table;
  val empty = Symtab.empty;
  val copy = I;
  val extend = I;
  fun merge _ = Symtab.merge (K true);
);

fun print_typecopies thy =
  let
    val tab = TypecopyData.get thy;
    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
      (Pretty.block o Pretty.breaks) [
        Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
        Pretty.str "=",
        (Pretty.str o Sign.extern_const thy) constr,
        Syntax.pretty_typ_global thy typ,
        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
    in
      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
    end;

val get_typecopies = Symtab.keys o TypecopyData.get;
val get_info = Symtab.lookup o TypecopyData.get;


(* interpretation of type copies *)

structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
val interpretation = TypecopyInterpretation.interpretation;


(* add a type copy *)

local

fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
  let
    val ty = prep_typ thy raw_ty;
    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
    val tac = Tactic.rtac UNIV_witness 1;
    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
      Rep_name = c_rep, Abs_inject = inject,
      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
        let
          val exists_thm =
            UNIV_I
            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
          val inject' = inject OF [exists_thm, exists_thm];
          val proj_def = inverse OF [exists_thm];
          val info = {
            vs = vs,
            constr = c_abs,
            typ = ty_rep,
            inject = inject',
            proj = (c_rep, ty_abs --> ty_rep),
            proj_def = proj_def
          };
        in
          thy
          |> (TypecopyData.map o Symtab.update_new) (tyco, info)
          |> TypecopyInterpretation.data tyco
          |> pair (tyco, info)
        end
  in
    thy
    |> TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
      (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
    |-> (fn (tyco, info) => add_info tyco info)
  end;

in

val add_typecopy = gen_add_typecopy Sign.certify_typ;

end;


(* code generator setup *)

fun add_typecopy_spec tyco thy =
  let
    val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
    val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
    val ty = Type (tyco, map TFree vs');
    val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr);
    fun add_def tyco lthy =
      let
        fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
          $ Free ("x", ty) $ Free ("y", ty);
        val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
        val def' = Syntax.check_term lthy def;
        val ((_, (_, thm)), lthy') = Specification.definition
          (NONE, (Attrib.no_binding, def')) lthy;
        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
      in (thm', lthy') end;
    fun tac thms = Class.intro_classes_tac []
      THEN ALLGOALS (ProofContext.fact_tac thms);
    fun add_eq_thms thy = 
      let
        val eq = inject
          |> Code_Unit.constrain_thm [HOLogic.class_eq]
          |> Simpdata.mk_eq
          |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
        val eq_refl = @{thm HOL.eq_refl}
          |> Thm.instantiate
              ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []);
      in
        thy
        |> Code.add_func eq
        |> Code.add_nonlinear_func eq_refl
      end;
  in
    thy
    |> Code.add_datatype [(constr, ty_constr)]
    |> Code.add_func proj_def
    |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
    |> add_def tyco
    |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
    #> LocalTheory.exit
    #> ProofContext.theory_of
    #> Code.del_func thm
    #> add_eq_thms)
  end;

val setup =
  TypecopyInterpretation.init
  #> interpretation add_typecopy_spec

end;