--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/typecopy.ML Fri Jun 19 17:23:21 2009 +0200
@@ -0,0 +1,157 @@
+(* Title: HOL/Tools/typecopy.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Introducing copies of types using trivial typedefs; datatype-like abstraction.
+*)
+
+signature TYPECOPY =
+sig
+ type info = {
+ vs: (string * sort) list,
+ constr: string,
+ typ: typ,
+ inject: thm,
+ proj: string * typ,
+ proj_def: thm
+ }
+ val typecopy: binding * string list -> typ -> (binding * binding) 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 add_default_code: string -> theory -> theory
+ val print_typecopies: theory -> unit
+ val setup: theory -> theory
+end;
+
+structure Typecopy: TYPECOPY =
+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;
+
+
+(* declaring typecopies *)
+
+fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
+ let
+ val ty = Sign.certify_typ thy raw_ty;
+ val vs =
+ AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT 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, ... } : Typedef.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
+ |> Typedef.add_typedef 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;
+
+
+(* default code setup *)
+
+fun add_default_code tyco thy =
+ let
+ val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
+ typ = ty_rep, ... } = get_info thy tyco;
+ val SOME { Rep_inject = proj_inject, ... } = Typedef.get_info thy tyco;
+ val constr = (constr_name, Logic.unvarifyT (Sign.the_const_type thy constr_name));
+ val vs = (map dest_TFree o snd o dest_Type) (Type (tyco, map TFree raw_vs));
+ val ty = Type (tyco, map TFree vs);
+ val proj = Const (proj, ty --> ty_rep);
+ val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
+ val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+ $ t_x $ t_y;
+ val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
+ val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
+ fun tac eq_thm = Class.intro_classes_tac []
+ THEN (Simplifier.rewrite_goals_tac
+ (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
+ THEN ALLGOALS (rtac @{thm refl});
+ fun mk_eq_refl thy = @{thm HOL.eq_refl}
+ |> Thm.instantiate
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
+ |> AxClass.unoverload thy;
+ in
+ thy
+ |> Code.add_datatype [constr]
+ |> Code.add_eqn proj_eq
+ |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition
+ (NONE, (Attrib.empty_binding, eq)))
+ |-> (fn (_, (_, eq_thm)) =>
+ Class.prove_instantiation_exit_result Morphism.thm
+ (fn _ => fn eq_thm => tac eq_thm) eq_thm)
+ |-> (fn eq_thm => Code.add_eqn eq_thm)
+ |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
+ end;
+
+val setup =
+ TypecopyInterpretation.init
+ #> interpretation add_default_code
+
+end;