author | haftmann |
Mon, 05 Jan 2009 15:36:24 +0100 | |
changeset 29358 | efdfe5dfe008 |
parent 29333 | 496b94152b55 |
child 29360 | a5be60c3674e |
permissions | -rw-r--r-- |
29358 | 1 |
(* Title: Pure/Isar/ML |
24218 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
29358 | 4 |
Type classes derived from primitive axclasses and locales - interfaces |
24218 | 5 |
*) |
6 |
||
7 |
signature CLASS = |
|
8 |
sig |
|
29358 | 9 |
include CLASS_TARGET |
10 |
(*FIXME the split in class_target.ML, theory_target.ML and |
|
11 |
ML is artificial*) |
|
12 |
||
26247 | 13 |
val class: bstring -> class list -> Element.context_i list |
26518 | 14 |
-> theory -> string * Proof.context |
26247 | 15 |
val class_cmd: bstring -> xstring list -> Element.context list |
26518 | 16 |
-> theory -> string * Proof.context |
29358 | 17 |
val prove_subclass: tactic -> class -> local_theory -> local_theory |
18 |
val subclass: class -> local_theory -> Proof.state |
|
19 |
val subclass_cmd: xstring -> local_theory -> Proof.state |
|
24218 | 20 |
end; |
21 |
||
22 |
structure Class : CLASS = |
|
23 |
struct |
|
24 |
||
29358 | 25 |
open Class_Target; |
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
26 |
|
29358 | 27 |
(** rule calculation **) |
24589 | 28 |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
29 |
fun calculate_axiom thy sups base_sort assm_axiom param_map class = |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
30 |
case Locale.intros thy class |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
31 |
of (_, []) => assm_axiom |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
32 |
| (_, [intro]) => |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
33 |
let |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
34 |
fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
35 |
(base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
36 |
(Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty), |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
37 |
Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map); |
29358 | 38 |
val axiom_premises = map_filter (fst o rules thy) sups |
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
39 |
@ the_list assm_axiom; |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
40 |
in intro |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
41 |
|> instantiate thy [class] |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
42 |
|> (fn thm => thm OF axiom_premises) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
43 |
|> Drule.standard' |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
44 |
|> Thm.close_derivation |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
45 |
|> SOME |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
46 |
end; |
25024 | 47 |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
48 |
fun calculate_rules thy phi sups base_sort param_map axiom class = |
25062 | 49 |
let |
25711 | 50 |
fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) |
51 |
(base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy) |
|
52 |
(Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty), |
|
53 |
Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map); |
|
54 |
val defs = these_defs thy sups; |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
55 |
val assm_intro = Locale.intros thy class |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
56 |
|> fst |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
57 |
|> map (instantiate thy base_sort) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
58 |
|> map (MetaSimplifier.rewrite_rule defs) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
59 |
|> map Thm.close_derivation |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
60 |
|> try the_single; |
25711 | 61 |
val fixate = Thm.instantiate |
62 |
(map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)), |
|
63 |
(TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], []) |
|
25618 | 64 |
val of_class_sups = if null sups |
25711 | 65 |
then map (fixate o Thm.class_triv thy) base_sort |
29358 | 66 |
else map (fixate o snd o rules thy) sups; |
25683 | 67 |
val locale_dests = map Drule.standard' (Locale.dests thy class); |
25711 | 68 |
val num_trivs = case length locale_dests |
69 |
of 0 => if is_none axiom then 0 else 1 |
|
70 |
| n => n; |
|
71 |
val pred_trivs = if num_trivs = 0 then [] |
|
72 |
else the axiom |
|
73 |
|> Thm.prop_of |
|
74 |
|> (map_types o map_atyps o K) (TFree (Name.aT, base_sort)) |
|
75 |
|> (Thm.assume o Thm.cterm_of thy) |
|
76 |
|> replicate num_trivs; |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
77 |
val axclass_intro = (#intro o AxClass.get_info thy) class; |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
78 |
val of_class = (fixate axclass_intro OF of_class_sups OF locale_dests OF pred_trivs) |
25711 | 79 |
|> Drule.standard' |
26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
26596
diff
changeset
|
80 |
|> Thm.close_derivation; |
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
81 |
in (assm_intro, of_class) end; |
24218 | 82 |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
83 |
fun note_assm_intro class assm_intro thy = |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
84 |
thy |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
85 |
|> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
86 |
|> PureThy.store_thm (AxClass.introN, assm_intro) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
87 |
|> snd |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
88 |
|> Sign.restore_naming thy; |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
89 |
|
24218 | 90 |
|
29358 | 91 |
(** define classes **) |
24218 | 92 |
|
93 |
local |
|
94 |
||
26247 | 95 |
fun gen_class_spec prep_class process_expr thy raw_supclasses raw_elems = |
24218 | 96 |
let |
24748 | 97 |
val supclasses = map (prep_class thy) raw_supclasses; |
98 |
val supsort = Sign.minimize_sort thy supclasses; |
|
25618 | 99 |
val sups = filter (is_class thy) supsort; |
26995 | 100 |
val supparam_names = map fst (these_params thy sups); |
101 |
val _ = if has_duplicates (op =) supparam_names |
|
102 |
then error ("Duplicate parameter(s) in superclasses: " |
|
103 |
^ (commas o map quote o duplicates (op =)) supparam_names) |
|
104 |
else (); |
|
25618 | 105 |
val base_sort = if null sups then supsort else |
26167 | 106 |
foldr1 (Sorts.inter_sort (Sign.classes_of thy)) |
29358 | 107 |
(map (base_sort thy) sups); |
25038 | 108 |
val suplocales = map Locale.Locale sups; |
24748 | 109 |
val supexpr = Locale.Merge suplocales; |
110 |
val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; |
|
29133 | 111 |
val mergeexpr = Locale.Merge suplocales; |
24748 | 112 |
val constrain = Element.Constrains ((map o apsnd o map_atyps) |
26167 | 113 |
(K (TFree (Name.aT, base_sort))) supparams); |
25683 | 114 |
fun fork_syn (Element.Fixes xs) = |
29006 | 115 |
fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs |
25683 | 116 |
#>> Element.Fixes |
117 |
| fork_syn x = pair x; |
|
118 |
fun fork_syntax elems = |
|
119 |
let |
|
120 |
val (elems', global_syntax) = fold_map fork_syn elems []; |
|
26247 | 121 |
in (constrain :: elems', global_syntax) end; |
25683 | 122 |
val (elems, global_syntax) = |
123 |
ProofContext.init thy |
|
124 |
|> Locale.cert_expr supexpr [constrain] |
|
125 |
|> snd |
|
29358 | 126 |
|> begin sups base_sort |
25683 | 127 |
|> process_expr Locale.empty raw_elems |
128 |
|> fst |
|
129 |
|> fork_syntax |
|
130 |
in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end; |
|
24748 | 131 |
|
26247 | 132 |
val read_class_spec = gen_class_spec Sign.intern_class Locale.read_expr; |
133 |
val check_class_spec = gen_class_spec (K I) Locale.cert_expr; |
|
24748 | 134 |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
135 |
fun add_consts bname class base_sort sups supparams global_syntax thy = |
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset
|
136 |
let |
25683 | 137 |
val supconsts = map fst supparams |
26518 | 138 |
|> AList.make (snd o the o AList.lookup (op =) (these_params thy sups)) |
25683 | 139 |
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); |
140 |
val all_params = map fst (Locale.parameters_of thy class); |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
141 |
val raw_params = (snd o chop (length supparams)) all_params; |
25683 | 142 |
fun add_const (v, raw_ty) thy = |
143 |
let |
|
28965 | 144 |
val c = Sign.full_bname thy v; |
25683 | 145 |
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; |
146 |
val ty0 = Type.strip_sorts ty; |
|
147 |
val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; |
|
148 |
val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v; |
|
149 |
in |
|
150 |
thy |
|
28965 | 151 |
|> Sign.declare_const [] ((Binding.name v, ty0), syn) |
25683 | 152 |
|> snd |
153 |
|> pair ((v, ty), (c, ty')) |
|
154 |
end; |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
155 |
in |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
156 |
thy |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
157 |
|> Sign.add_path (Logic.const_of_class bname) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
158 |
|> fold_map add_const raw_params |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
159 |
||> Sign.restore_naming thy |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
160 |
|-> (fn params => pair (supconsts @ (map o apfst) fst params, params)) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
161 |
end; |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
162 |
|
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
163 |
fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy = |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
164 |
let |
25683 | 165 |
fun globalize param_map = map_aterms |
166 |
(fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) |
|
167 |
| t => t); |
|
168 |
val raw_pred = Locale.intros thy class |
|
169 |
|> fst |
|
170 |
|> map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of); |
|
171 |
fun get_axiom thy = case (#axioms o AxClass.get_info thy) class |
|
172 |
of [] => NONE |
|
173 |
| [thm] => SOME thm; |
|
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset
|
174 |
in |
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset
|
175 |
thy |
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
176 |
|> add_consts bname class base_sort sups supparams global_syntax |
25683 | 177 |
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort) |
26518 | 178 |
(map (fst o snd) params) |
28965 | 179 |
[((Binding.name (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)] |
25683 | 180 |
#> snd |
181 |
#> `get_axiom |
|
182 |
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
183 |
#> pair (map (Const o snd) param_map, param_map, params, assm_axiom))) |
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset
|
184 |
end; |
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset
|
185 |
|
26518 | 186 |
fun gen_class prep_spec bname raw_supclasses raw_elems thy = |
24748 | 187 |
let |
28965 | 188 |
val class = Sign.full_bname thy bname; |
25683 | 189 |
val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) = |
26247 | 190 |
prep_spec thy raw_supclasses raw_elems; |
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
191 |
val supconsts = map (apsnd fst o snd) (these_params thy sups); |
24218 | 192 |
in |
193 |
thy |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28739
diff
changeset
|
194 |
|> Locale.add_locale "" bname mergeexpr elems |
25038 | 195 |
|> snd |
25311 | 196 |
|> ProofContext.theory_of |
26518 | 197 |
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax |
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
198 |
|-> (fn (inst, param_map, params, assm_axiom) => |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
199 |
`(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
200 |
#-> (fn axiom => |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
201 |
prove_class_interpretation class inst |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
202 |
(supconsts @ map (pair class o fst o snd) params) (the_list axiom) [] |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
203 |
#-> (fn morphism => |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
204 |
`(fn thy => activate_class_morphism thy class inst morphism) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
205 |
#-> (fn phi => |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
206 |
`(fn thy => calculate_rules thy phi sups base_sort param_map axiom class) |
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
207 |
#-> (fn (assm_intro, of_class) => |
29358 | 208 |
register class sups params base_sort inst |
209 |
morphism axiom assm_intro of_class |
|
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset
|
210 |
#> fold (note_assm_intro class) (the_list assm_intro)))))) |
25268 | 211 |
|> init class |
25038 | 212 |
|> pair class |
24218 | 213 |
end; |
214 |
||
215 |
in |
|
216 |
||
26518 | 217 |
val class_cmd = gen_class read_class_spec; |
218 |
val class = gen_class check_class_spec; |
|
24218 | 219 |
|
220 |
end; (*local*) |
|
221 |
||
222 |
||
29358 | 223 |
(** subclass relations **) |
25462 | 224 |
|
29358 | 225 |
local |
25462 | 226 |
|
29358 | 227 |
fun gen_subclass prep_class do_proof raw_sup lthy = |
25462 | 228 |
let |
29358 | 229 |
val thy = ProofContext.theory_of lthy; |
230 |
val sup = prep_class thy raw_sup; |
|
231 |
val sub = case TheoryTarget.peek lthy |
|
232 |
of {is_class = false, ...} => error "Not a class context" |
|
233 |
| {target, ...} => target; |
|
234 |
val _ = if Sign.subsort thy ([sup], [sub]) |
|
235 |
then error ("Class " ^ Syntax.string_of_sort lthy [sup] |
|
236 |
^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub]) |
|
237 |
else (); |
|
238 |
val sub_params = map fst (these_params thy [sub]); |
|
239 |
val sup_params = map fst (these_params thy [sup]); |
|
240 |
val err_params = subtract (op =) sub_params sup_params; |
|
241 |
val _ = if null err_params then [] else |
|
242 |
error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ |
|
243 |
commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); |
|
244 |
val sublocale_prop = |
|
245 |
Locale.global_asms_of thy sup |
|
246 |
|> maps snd |
|
247 |
|> try the_single |
|
248 |
|> Option.map (ObjectLogic.ensure_propT thy); |
|
249 |
fun after_qed some_thm = |
|
250 |
LocalTheory.theory (prove_subclass_relation (sub, sup) some_thm) |
|
251 |
#> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
|
26238 | 252 |
in |
29358 | 253 |
do_proof after_qed sublocale_prop lthy |
25485 | 254 |
end; |
255 |
||
29358 | 256 |
fun user_proof after_qed NONE = |
257 |
Proof.theorem_i NONE (K (after_qed NONE)) [[]] |
|
258 |
| user_proof after_qed (SOME prop) = |
|
259 |
Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; |
|
25485 | 260 |
|
29358 | 261 |
fun tactic_proof tac after_qed NONE lthy = |
262 |
after_qed NONE lthy |
|
263 |
| tactic_proof tac after_qed (SOME prop) lthy = |
|
264 |
after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop |
|
265 |
(K tac))) lthy; |
|
28666 | 266 |
|
29358 | 267 |
in |
28666 | 268 |
|
29358 | 269 |
val subclass = gen_subclass (K I) user_proof; |
270 |
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); |
|
271 |
val subclass_cmd = gen_subclass Sign.read_class user_proof; |
|
25462 | 272 |
|
29358 | 273 |
end; (*local*) |
274 |
||
25603 | 275 |
|
24218 | 276 |
end; |
25683 | 277 |