author | wenzelm |
Mon, 03 May 2010 14:25:56 +0200 | |
changeset 36610 | bafd82950e24 |
parent 36156 | 6f0a8f6b1671 |
child 37469 | 1436d6f28f17 |
permissions | -rw-r--r-- |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31136
diff
changeset
|
1 |
(* Title: HOL/Tools/typecopy.ML |
20426 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
20855 | 4 |
Introducing copies of types using trivial typedefs; datatype-like abstraction. |
20426 | 5 |
*) |
6 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31136
diff
changeset
|
7 |
signature TYPECOPY = |
20426 | 8 |
sig |
31735 | 9 |
type info = { vs: (string * sort) list, constr: string, typ: typ, |
10 |
inject: thm, proj: string * typ, proj_def: thm } |
|
36150
123f721c9a37
typecopy: observe given sort constraints more precisely;
wenzelm
parents:
35994
diff
changeset
|
11 |
val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
12 |
-> theory -> (string * info) * theory |
25506 | 13 |
val get_info: theory -> string -> info option |
25489 | 14 |
val interpretation: (string -> theory -> theory) -> theory -> theory |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
15 |
val add_default_code: string -> theory -> theory |
20426 | 16 |
val setup: theory -> theory |
17 |
end; |
|
18 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31136
diff
changeset
|
19 |
structure Typecopy: TYPECOPY = |
20426 | 20 |
struct |
21 |
||
22 |
(* theory data *) |
|
23 |
||
24 |
type info = { |
|
25 |
vs: (string * sort) list, |
|
26 |
constr: string, |
|
27 |
typ: typ, |
|
28 |
inject: thm, |
|
29 |
proj: string * typ, |
|
30 |
proj_def: thm |
|
31 |
}; |
|
32 |
||
33522 | 33 |
structure TypecopyData = Theory_Data |
22846 | 34 |
( |
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
35 |
type T = info Symtab.table; |
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
36 |
val empty = Symtab.empty; |
20426 | 37 |
val extend = I; |
33522 | 38 |
fun merge data = Symtab.merge (K true) data; |
22846 | 39 |
); |
40 |
||
25506 | 41 |
val get_info = Symtab.lookup o TypecopyData.get; |
20426 | 42 |
|
43 |
||
25489 | 44 |
(* interpretation of type copies *) |
20426 | 45 |
|
33314 | 46 |
structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =); |
47 |
val interpretation = Typecopy_Interpretation.interpretation; |
|
20426 | 48 |
|
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
49 |
|
31735 | 50 |
(* introducing typecopies *) |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
51 |
|
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
52 |
fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy = |
20426 | 53 |
let |
28664 | 54 |
val ty = Sign.certify_typ thy raw_ty; |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36156
diff
changeset
|
55 |
val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty; |
36156 | 56 |
val vs = map (ProofContext.check_tfree ctxt) raw_vs; |
20426 | 57 |
val tac = Tactic.rtac UNIV_witness 1; |
35994
9cc3df9a606e
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents:
35845
diff
changeset
|
58 |
fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, |
9cc3df9a606e
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents:
35845
diff
changeset
|
59 |
Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... }) |
9cc3df9a606e
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents:
35845
diff
changeset
|
60 |
: Typedef.info) thy = |
20426 | 61 |
let |
62 |
val exists_thm = |
|
63 |
UNIV_I |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35842
diff
changeset
|
64 |
|> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] []; |
20426 | 65 |
val inject' = inject OF [exists_thm, exists_thm]; |
66 |
val proj_def = inverse OF [exists_thm]; |
|
67 |
val info = { |
|
68 |
vs = vs, |
|
69 |
constr = c_abs, |
|
70 |
typ = ty_rep, |
|
71 |
inject = inject', |
|
72 |
proj = (c_rep, ty_abs --> ty_rep), |
|
73 |
proj_def = proj_def |
|
74 |
}; |
|
75 |
in |
|
76 |
thy |
|
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset
|
77 |
|> (TypecopyData.map o Symtab.update_new) (tyco, info) |
33314 | 78 |
|> Typecopy_Interpretation.data tyco |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
79 |
|> pair (tyco, info) |
20426 | 80 |
end |
81 |
in |
|
82 |
thy |
|
36150
123f721c9a37
typecopy: observe given sort constraints more precisely;
wenzelm
parents:
35994
diff
changeset
|
83 |
|> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) |
26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
25864
diff
changeset
|
84 |
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20426
diff
changeset
|
85 |
|-> (fn (tyco, info) => add_info tyco info) |
20426 | 86 |
end; |
87 |
||
88 |
||
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
89 |
(* default code setup *) |
20835 | 90 |
|
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
91 |
fun add_default_code tyco thy = |
25489 | 92 |
let |
32378 | 93 |
val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs, |
35743
c506c029a082
adapted to localized typedef: handle single global interpretation only;
wenzelm
parents:
33553
diff
changeset
|
94 |
typ = ty_rep, ... } = get_info thy tyco; |
c506c029a082
adapted to localized typedef: handle single global interpretation only;
wenzelm
parents:
33553
diff
changeset
|
95 |
(* FIXME handle multiple typedef interpretations (!??) *) |
35994
9cc3df9a606e
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents:
35845
diff
changeset
|
96 |
val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco; |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35842
diff
changeset
|
97 |
val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c)); |
28423 | 98 |
val ty = Type (tyco, map TFree vs); |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
99 |
val proj = Const (proj, ty --> ty_rep); |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
100 |
val (t_x, t_y) = (Free ("x", ty), Free ("y", ty)); |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
101 |
val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT) |
28664 | 102 |
$ t_x $ t_y; |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
103 |
val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y); |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
104 |
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs); |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
105 |
fun tac eq_thm = Class.intro_classes_tac [] |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
106 |
THEN (Simplifier.rewrite_goals_tac |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
107 |
(map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject])) |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
108 |
THEN ALLGOALS (rtac @{thm refl}); |
28664 | 109 |
fun mk_eq_refl thy = @{thm HOL.eq_refl} |
110 |
|> Thm.instantiate |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35842
diff
changeset
|
111 |
([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], []) |
28664 | 112 |
|> AxClass.unoverload thy; |
25489 | 113 |
in |
25506 | 114 |
thy |
28664 | 115 |
|> Code.add_datatype [constr] |
116 |
|> Code.add_eqn proj_eq |
|
33553 | 117 |
|> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq]) |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
118 |
|> `(fn lthy => Syntax.check_term lthy eq) |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
119 |
|-> (fn eq => Specification.definition |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
120 |
(NONE, (Attrib.empty_binding, eq))) |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
121 |
|-> (fn (_, (_, eq_thm)) => |
28664 | 122 |
Class.prove_instantiation_exit_result Morphism.thm |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
123 |
(fn _ => fn eq_thm => tac eq_thm) eq_thm) |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
124 |
|-> (fn eq_thm => Code.add_eqn eq_thm) |
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
125 |
|> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy) |
25489 | 126 |
end; |
20426 | 127 |
|
25489 | 128 |
val setup = |
33314 | 129 |
Typecopy_Interpretation.init |
31136
85d04515abb3
tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents:
31090
diff
changeset
|
130 |
#> interpretation add_default_code |
20426 | 131 |
|
22846 | 132 |
end; |