--- a/src/HOL/Tools/typecopy.ML Tue Aug 17 15:29:41 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(* 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, typ: typ, constr: string, proj: string,
- constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
- val typecopy: binding * (string * sort) list -> typ -> binding -> binding
- -> theory -> (string * info) * theory
- val get_info: theory -> string -> info option
- val add_default_code: string -> theory -> theory
-end;
-
-structure Typecopy: TYPECOPY =
-struct
-
-(* theory data *)
-
-type info = {
- vs: (string * sort) list,
- typ: typ,
- constr: string,
- proj: string,
- constr_inject: thm,
- proj_inject: thm,
- constr_proj: thm,
- proj_constr: thm
-};
-
-structure Typecopy_Data = Theory_Data
-(
- type T = info Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data = Symtab.merge (K true) data;
-);
-
-val get_info = Symtab.lookup o Typecopy_Data.get;
-
-
-(* default code setup *)
-
-fun add_default_code tyco thy =
- let
- val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
- get_info thy tyco;
- val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
- 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_global ty)], [])
- |> AxClass.unoverload thy;
- in
- thy
- |> Code.add_datatype [constr]
- |> Code.add_eqn proj_constr
- |> Class.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;
-
-
-(* introducing typecopies *)
-
-fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
- { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
- let
- val exists_thm =
- UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
- val constr_inject = Abs_inject OF [exists_thm, exists_thm];
- val proj_constr = Abs_inverse OF [exists_thm];
- val info = {
- vs = vs,
- typ = rep_type,
- constr = Abs_name,
- proj = Rep_name,
- constr_inject = constr_inject,
- proj_inject = Rep_inject,
- constr_proj = Rep_inverse,
- proj_constr = proj_constr
- };
- in
- thy
- |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
- |> add_default_code tyco
- |> Quickcheck_Record.ensure_random_typecopy tyco vs Abs_name rep_type
- |> pair (tyco, info)
- end
-
-fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
- let
- val ty = Sign.certify_typ thy raw_ty;
- val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
- val vs = map (ProofContext.check_tfree ctxt) raw_vs;
- val tac = Tactic.rtac UNIV_witness 1;
- in
- thy
- |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
- (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
- |-> (fn (tyco, info) => add_info tyco vs info)
- end;
-
-end;