haftmann@29358
|
1 |
(* Title: Pure/Isar/ML
|
haftmann@24218
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@24218
|
3 |
|
haftmann@29575
|
4 |
Type classes derived from primitive axclasses and locales - interfaces.
|
haftmann@24218
|
5 |
*)
|
haftmann@24218
|
6 |
|
haftmann@24218
|
7 |
signature CLASS =
|
haftmann@24218
|
8 |
sig
|
haftmann@29358
|
9 |
include CLASS_TARGET
|
haftmann@29437
|
10 |
(*FIXME the split into class_target.ML, theory_target.ML and
|
haftmann@29437
|
11 |
class.ML is artificial*)
|
haftmann@29358
|
12 |
|
haftmann@26247
|
13 |
val class: bstring -> class list -> Element.context_i list
|
haftmann@29378
|
14 |
-> theory -> string * local_theory
|
haftmann@26247
|
15 |
val class_cmd: bstring -> xstring list -> Element.context list
|
haftmann@29378
|
16 |
-> theory -> string * local_theory
|
haftmann@29358
|
17 |
val prove_subclass: tactic -> class -> local_theory -> local_theory
|
haftmann@29358
|
18 |
val subclass: class -> local_theory -> Proof.state
|
haftmann@29358
|
19 |
val subclass_cmd: xstring -> local_theory -> Proof.state
|
haftmann@24218
|
20 |
end;
|
haftmann@24218
|
21 |
|
haftmann@24218
|
22 |
structure Class : CLASS =
|
haftmann@24218
|
23 |
struct
|
haftmann@24218
|
24 |
|
haftmann@29358
|
25 |
open Class_Target;
|
haftmann@29133
|
26 |
|
haftmann@29665
|
27 |
(** class definitions **)
|
haftmann@24218
|
28 |
|
haftmann@24218
|
29 |
local
|
haftmann@24218
|
30 |
|
haftmann@29665
|
31 |
(* calculating class-related rules including canonical interpretation *)
|
haftmann@29665
|
32 |
|
haftmann@29547
|
33 |
fun calculate thy class sups base_sort param_map assm_axiom =
|
haftmann@29547
|
34 |
let
|
haftmann@29547
|
35 |
val empty_ctxt = ProofContext.init thy;
|
haftmann@29547
|
36 |
|
haftmann@29547
|
37 |
(* instantiation of canonical interpretation *)
|
haftmann@29575
|
38 |
val aT = TFree (Name.aT, base_sort);
|
haftmann@29627
|
39 |
val param_map_const = (map o apsnd) Const param_map;
|
haftmann@29627
|
40 |
val param_map_inst = (map o apsnd)
|
haftmann@29627
|
41 |
(Const o apsnd (map_atyps (K aT))) param_map;
|
haftmann@29627
|
42 |
val const_morph = Element.inst_morphism thy
|
haftmann@29627
|
43 |
(Symtab.empty, Symtab.make param_map_inst);
|
haftmann@29734
|
44 |
val typ_morph = Element.inst_morphism thy
|
haftmann@29734
|
45 |
(Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
|
haftmann@29734
|
46 |
val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
|
haftmann@29547
|
47 |
|> Expression.cert_goal_expression ([(class, (("", false),
|
haftmann@29627
|
48 |
Expression.Named param_map_const))], []);
|
haftmann@29734
|
49 |
val (props, inst_morph) = if null param_map
|
haftmann@29734
|
50 |
then (raw_props |> map (Morphism.term typ_morph),
|
haftmann@29734
|
51 |
raw_inst_morph $> typ_morph)
|
haftmann@29734
|
52 |
else (raw_props, raw_inst_morph); (*FIXME proper handling in
|
haftmann@29734
|
53 |
locale.ML / expression.ML would be desirable*)
|
haftmann@29547
|
54 |
|
haftmann@29547
|
55 |
(* witness for canonical interpretation *)
|
haftmann@29547
|
56 |
val prop = try the_single props;
|
haftmann@29547
|
57 |
val wit = Option.map (fn prop => let
|
haftmann@29547
|
58 |
val sup_axioms = map_filter (fst o rules thy) sups;
|
haftmann@29547
|
59 |
val loc_intro_tac = case Locale.intros_of thy class
|
haftmann@29547
|
60 |
of (_, NONE) => all_tac
|
haftmann@29547
|
61 |
| (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
|
haftmann@29547
|
62 |
val tac = loc_intro_tac
|
haftmann@29547
|
63 |
THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
|
haftmann@29547
|
64 |
in Element.prove_witness empty_ctxt prop tac end) prop;
|
haftmann@29547
|
65 |
val axiom = Option.map Element.conclude_witness wit;
|
haftmann@29547
|
66 |
|
haftmann@29547
|
67 |
(* canonical interpretation *)
|
haftmann@29547
|
68 |
val base_morph = inst_morph
|
haftmann@29547
|
69 |
$> Morphism.binding_morphism
|
haftmann@29547
|
70 |
(Binding.add_prefix false (class_prefix class))
|
haftmann@29547
|
71 |
$> Element.satisfy_morphism (the_list wit);
|
haftmann@29547
|
72 |
val defs = these_defs thy sups;
|
haftmann@29547
|
73 |
val eq_morph = Element.eq_morphism thy defs;
|
haftmann@29547
|
74 |
val morph = base_morph $> eq_morph;
|
haftmann@29547
|
75 |
|
haftmann@29547
|
76 |
(* assm_intro *)
|
haftmann@29547
|
77 |
fun prove_assm_intro thm =
|
haftmann@29547
|
78 |
let
|
haftmann@29627
|
79 |
val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
|
haftmann@29627
|
80 |
val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
|
haftmann@29627
|
81 |
val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
|
haftmann@29627
|
82 |
in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
|
haftmann@29547
|
83 |
val assm_intro = Option.map prove_assm_intro
|
haftmann@29547
|
84 |
(fst (Locale.intros_of thy class));
|
haftmann@29547
|
85 |
|
haftmann@29547
|
86 |
(* of_class *)
|
haftmann@29547
|
87 |
val of_class_prop_concl = Logic.mk_inclass (aT, class);
|
haftmann@29547
|
88 |
val of_class_prop = case prop of NONE => of_class_prop_concl
|
haftmann@29627
|
89 |
| SOME prop => Logic.mk_implies (Morphism.term const_morph
|
haftmann@29627
|
90 |
((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
|
haftmann@29547
|
91 |
val sup_of_classes = map (snd o rules thy) sups;
|
haftmann@29547
|
92 |
val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
|
haftmann@29547
|
93 |
val axclass_intro = #intro (AxClass.get_info thy class);
|
haftmann@29547
|
94 |
val base_sort_trivs = Drule.sort_triv thy (aT, base_sort);
|
haftmann@29547
|
95 |
val tac = REPEAT (SOMEGOAL
|
haftmann@29547
|
96 |
(Tactic.match_tac (axclass_intro :: sup_of_classes
|
haftmann@29547
|
97 |
@ loc_axiom_intros @ base_sort_trivs)
|
haftmann@29547
|
98 |
ORELSE' Tactic.assume_tac));
|
haftmann@29547
|
99 |
val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
|
haftmann@29547
|
100 |
|
haftmann@29547
|
101 |
in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
|
haftmann@29547
|
102 |
|
haftmann@29632
|
103 |
|
haftmann@29665
|
104 |
(* reading and processing class specifications *)
|
haftmann@29665
|
105 |
|
haftmann@29665
|
106 |
fun prep_class_elems prep_decl thy supexpr sups proto_base_sort raw_elems =
|
haftmann@29632
|
107 |
let
|
haftmann@29632
|
108 |
|
haftmann@29665
|
109 |
(* user space type system: only permits 'a type variable, improves towards 'a *)
|
haftmann@29665
|
110 |
val base_constraints = (map o apsnd)
|
haftmann@29665
|
111 |
(map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
|
haftmann@29665
|
112 |
(these_operations thy sups);
|
haftmann@29665
|
113 |
val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
|
haftmann@29665
|
114 |
if v = Name.aT then T
|
haftmann@29665
|
115 |
else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
|
haftmann@29665
|
116 |
| T => T);
|
haftmann@29665
|
117 |
fun singleton_fixate thy algebra Ts =
|
haftmann@29665
|
118 |
let
|
haftmann@29665
|
119 |
fun extract f = (fold o fold_atyps) f Ts [];
|
haftmann@29665
|
120 |
val tfrees = extract
|
haftmann@29665
|
121 |
(fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
|
haftmann@29665
|
122 |
val inferred_sort = extract
|
haftmann@29665
|
123 |
(fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
|
haftmann@29665
|
124 |
val fixate_sort = if null tfrees then inferred_sort
|
haftmann@29753
|
125 |
else case tfrees
|
haftmann@29753
|
126 |
of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
|
haftmann@29753
|
127 |
then Sorts.inter_sort algebra (a_sort, inferred_sort)
|
haftmann@29753
|
128 |
else error ("Type inference imposes additional sort constraint "
|
haftmann@29753
|
129 |
^ Syntax.string_of_sort_global thy inferred_sort
|
haftmann@29753
|
130 |
^ " of type parameter " ^ Name.aT ^ " of sort "
|
haftmann@29753
|
131 |
^ Syntax.string_of_sort_global thy a_sort ^ ".")
|
haftmann@29753
|
132 |
| _ => error "Multiple type variables in class specification.";
|
haftmann@29665
|
133 |
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
|
haftmann@29665
|
134 |
fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
|
haftmann@29665
|
135 |
let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
|
haftmann@29575
|
136 |
|
haftmann@29753
|
137 |
(* preprocessing elements, retrieving base sort from type-checked elements *)
|
haftmann@29702
|
138 |
val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
|
haftmann@29702
|
139 |
#> redeclare_operations thy sups
|
haftmann@29702
|
140 |
#> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
|
haftmann@29702
|
141 |
#> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
|
haftmann@29665
|
142 |
val ((_, _, inferred_elems), _) = ProofContext.init thy
|
haftmann@29702
|
143 |
|> prep_decl supexpr init_class_body raw_elems;
|
haftmann@29665
|
144 |
fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
|
haftmann@29665
|
145 |
| fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
|
haftmann@29665
|
146 |
| fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
|
haftmann@29665
|
147 |
fold_types f t #> (fold o fold_types) f ts) o snd) assms
|
haftmann@29665
|
148 |
| fold_element_types f (Element.Defines _) =
|
haftmann@29665
|
149 |
error ("\"defines\" element not allowed in class specification.")
|
haftmann@29665
|
150 |
| fold_element_types f (Element.Notes _) =
|
haftmann@29665
|
151 |
error ("\"notes\" element not allowed in class specification.");
|
haftmann@29665
|
152 |
val base_sort = if null inferred_elems then proto_base_sort else
|
haftmann@29665
|
153 |
case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
|
haftmann@29665
|
154 |
of [] => error "No type variable in class specification"
|
haftmann@29665
|
155 |
| [(_, sort)] => sort
|
haftmann@29665
|
156 |
| _ => error "Multiple type variables in class specification"
|
haftmann@29575
|
157 |
|
haftmann@29665
|
158 |
in (base_sort, inferred_elems) end;
|
haftmann@29575
|
159 |
|
haftmann@29665
|
160 |
val cert_class_elems = prep_class_elems Expression.cert_declaration;
|
haftmann@29665
|
161 |
val read_class_elems = prep_class_elems Expression.cert_read_declaration;
|
haftmann@29665
|
162 |
|
haftmann@29665
|
163 |
fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
|
haftmann@29575
|
164 |
let
|
haftmann@29665
|
165 |
|
haftmann@29575
|
166 |
(* prepare import *)
|
haftmann@29575
|
167 |
val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
|
haftmann@29608
|
168 |
val sups = map (prep_class thy) raw_supclasses
|
haftmann@29608
|
169 |
|> Sign.minimize_sort thy;
|
haftmann@29608
|
170 |
val _ = case filter_out (is_class thy) sups
|
haftmann@29608
|
171 |
of [] => ()
|
haftmann@29734
|
172 |
| no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
|
haftmann@29608
|
173 |
val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
|
haftmann@29575
|
174 |
val supparam_names = map fst supparams;
|
haftmann@29575
|
175 |
val _ = if has_duplicates (op =) supparam_names
|
haftmann@29575
|
176 |
then error ("Duplicate parameter(s) in superclasses: "
|
haftmann@29575
|
177 |
^ (commas o map quote o duplicates (op =)) supparam_names)
|
haftmann@29575
|
178 |
else ();
|
haftmann@29575
|
179 |
val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
|
haftmann@29575
|
180 |
sups, []);
|
haftmann@29608
|
181 |
val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
|
haftmann@29575
|
182 |
|
haftmann@29575
|
183 |
(* infer types and base sort *)
|
haftmann@29665
|
184 |
val (base_sort, inferred_elems) = prep_class_elems thy supexpr sups
|
haftmann@29665
|
185 |
given_basesort raw_elems;
|
haftmann@29575
|
186 |
val sup_sort = inter_sort base_sort sups
|
haftmann@29575
|
187 |
|
haftmann@29575
|
188 |
(* process elements as class specification *)
|
haftmann@29665
|
189 |
val class_ctxt = begin sups base_sort (ProofContext.init thy)
|
haftmann@29665
|
190 |
val ((_, _, syntax_elems), _) = class_ctxt
|
haftmann@29702
|
191 |
|> Expression.cert_declaration supexpr I inferred_elems;
|
haftmann@29665
|
192 |
fun check_vars e vs = if null vs
|
haftmann@29665
|
193 |
then error ("No type variable in part of specification element "
|
haftmann@29665
|
194 |
^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
|
haftmann@29665
|
195 |
else ();
|
haftmann@29665
|
196 |
fun check_element (e as Element.Fixes fxs) =
|
haftmann@29665
|
197 |
map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
|
haftmann@29665
|
198 |
| check_element (e as Element.Assumes assms) =
|
haftmann@29665
|
199 |
maps (fn (_, ts_pss) => map
|
haftmann@29665
|
200 |
(fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
|
haftmann@29665
|
201 |
| check_element e = [()];
|
haftmann@29665
|
202 |
val _ = map check_element syntax_elems;
|
haftmann@29665
|
203 |
fun fork_syn (Element.Fixes xs) =
|
haftmann@29665
|
204 |
fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
|
haftmann@29665
|
205 |
#>> Element.Fixes
|
haftmann@29665
|
206 |
| fork_syn x = pair x;
|
haftmann@29575
|
207 |
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
|
haftmann@29575
|
208 |
val constrain = Element.Constrains ((map o apsnd o map_atyps)
|
haftmann@29575
|
209 |
(K (TFree (Name.aT, base_sort))) supparams);
|
haftmann@29753
|
210 |
(*FIXME perhaps better: control type variable by explicit
|
haftmann@29575
|
211 |
parameter instantiation of import expression*)
|
haftmann@29665
|
212 |
|
haftmann@29575
|
213 |
in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
|
haftmann@29575
|
214 |
|
haftmann@29665
|
215 |
val cert_class_spec = prep_class_spec (K I) cert_class_elems;
|
haftmann@29665
|
216 |
val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
|
haftmann@29665
|
217 |
|
haftmann@29665
|
218 |
|
haftmann@29665
|
219 |
(* class establishment *)
|
haftmann@29575
|
220 |
|
haftmann@28715
|
221 |
fun add_consts bname class base_sort sups supparams global_syntax thy =
|
wenzelm@24968
|
222 |
let
|
haftmann@29753
|
223 |
(*FIXME simplify*)
|
haftmann@29509
|
224 |
val supconsts = supparams
|
haftmann@26518
|
225 |
|> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
|
haftmann@25683
|
226 |
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
|
haftmann@29509
|
227 |
val all_params = Locale.params_of thy class;
|
haftmann@28715
|
228 |
val raw_params = (snd o chop (length supparams)) all_params;
|
haftmann@29509
|
229 |
fun add_const (b, SOME raw_ty, _) thy =
|
haftmann@25683
|
230 |
let
|
haftmann@29509
|
231 |
val v = Binding.base_name b;
|
haftmann@28965
|
232 |
val c = Sign.full_bname thy v;
|
haftmann@25683
|
233 |
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
|
haftmann@25683
|
234 |
val ty0 = Type.strip_sorts ty;
|
haftmann@25683
|
235 |
val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
|
haftmann@25683
|
236 |
val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
|
haftmann@25683
|
237 |
in
|
haftmann@25683
|
238 |
thy
|
haftmann@28965
|
239 |
|> Sign.declare_const [] ((Binding.name v, ty0), syn)
|
haftmann@25683
|
240 |
|> snd
|
haftmann@25683
|
241 |
|> pair ((v, ty), (c, ty'))
|
haftmann@25683
|
242 |
end;
|
haftmann@28715
|
243 |
in
|
haftmann@28715
|
244 |
thy
|
haftmann@29547
|
245 |
|> Sign.add_path (class_prefix class)
|
haftmann@28715
|
246 |
|> fold_map add_const raw_params
|
haftmann@28715
|
247 |
||> Sign.restore_naming thy
|
haftmann@28715
|
248 |
|-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
|
haftmann@28715
|
249 |
end;
|
haftmann@28715
|
250 |
|
haftmann@28715
|
251 |
fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
|
haftmann@28715
|
252 |
let
|
haftmann@29753
|
253 |
(*FIXME simplify*)
|
haftmann@25683
|
254 |
fun globalize param_map = map_aterms
|
haftmann@25683
|
255 |
(fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
|
haftmann@25683
|
256 |
| t => t);
|
haftmann@29509
|
257 |
val raw_pred = Locale.intros_of thy class
|
haftmann@25683
|
258 |
|> fst
|
haftmann@29509
|
259 |
|> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
|
haftmann@25683
|
260 |
fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
|
haftmann@25683
|
261 |
of [] => NONE
|
haftmann@25683
|
262 |
| [thm] => SOME thm;
|
wenzelm@24968
|
263 |
in
|
wenzelm@24968
|
264 |
thy
|
haftmann@28715
|
265 |
|> add_consts bname class base_sort sups supparams global_syntax
|
haftmann@25683
|
266 |
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
|
haftmann@26518
|
267 |
(map (fst o snd) params)
|
wenzelm@30215
|
268 |
[(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
|
haftmann@25683
|
269 |
#> snd
|
haftmann@25683
|
270 |
#> `get_axiom
|
haftmann@25683
|
271 |
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
|
haftmann@29526
|
272 |
#> pair (param_map, params, assm_axiom)))
|
wenzelm@24968
|
273 |
end;
|
wenzelm@24968
|
274 |
|
haftmann@26518
|
275 |
fun gen_class prep_spec bname raw_supclasses raw_elems thy =
|
haftmann@24748
|
276 |
let
|
haftmann@28965
|
277 |
val class = Sign.full_bname thy bname;
|
haftmann@29509
|
278 |
val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
|
haftmann@26247
|
279 |
prep_spec thy raw_supclasses raw_elems;
|
haftmann@24218
|
280 |
in
|
haftmann@24218
|
281 |
thy
|
haftmann@29509
|
282 |
|> Expression.add_locale bname "" supexpr elems
|
haftmann@29509
|
283 |
|> snd |> LocalTheory.exit_global
|
haftmann@26518
|
284 |
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
|
haftmann@29526
|
285 |
|-> (fn (param_map, params, assm_axiom) =>
|
haftmann@29547
|
286 |
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
|
haftmann@29547
|
287 |
#-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
|
haftmann@29547
|
288 |
Locale.add_registration (class, (morph, export_morph))
|
haftmann@29547
|
289 |
#> Locale.activate_global_facts (class, morph $> export_morph)
|
haftmann@29547
|
290 |
#> register class sups params base_sort base_morph axiom assm_intro of_class))
|
haftmann@29378
|
291 |
|> TheoryTarget.init (SOME class)
|
haftmann@25038
|
292 |
|> pair class
|
haftmann@24218
|
293 |
end;
|
haftmann@24218
|
294 |
|
haftmann@24218
|
295 |
in
|
haftmann@24218
|
296 |
|
haftmann@29509
|
297 |
val class = gen_class cert_class_spec;
|
haftmann@26518
|
298 |
val class_cmd = gen_class read_class_spec;
|
haftmann@24218
|
299 |
|
haftmann@24218
|
300 |
end; (*local*)
|
haftmann@24218
|
301 |
|
haftmann@24218
|
302 |
|
haftmann@29358
|
303 |
(** subclass relations **)
|
haftmann@25462
|
304 |
|
haftmann@29358
|
305 |
local
|
haftmann@25462
|
306 |
|
haftmann@29358
|
307 |
fun gen_subclass prep_class do_proof raw_sup lthy =
|
haftmann@25462
|
308 |
let
|
haftmann@29358
|
309 |
val thy = ProofContext.theory_of lthy;
|
haftmann@29558
|
310 |
val proto_sup = prep_class thy raw_sup;
|
haftmann@29558
|
311 |
val proto_sub = case TheoryTarget.peek lthy
|
haftmann@29558
|
312 |
of {is_class = false, ...} => error "Not in a class context"
|
haftmann@29358
|
313 |
| {target, ...} => target;
|
haftmann@29558
|
314 |
val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
|
haftmann@29509
|
315 |
|
haftmann@29509
|
316 |
val expr = ([(sup, (("", false), Expression.Positional []))], []);
|
haftmann@29558
|
317 |
val (([props], deps, export), goal_ctxt) =
|
haftmann@29509
|
318 |
Expression.cert_goal_expression expr lthy;
|
haftmann@29526
|
319 |
val some_prop = try the_single props;
|
haftmann@29558
|
320 |
val some_dep_morph = try the_single (map snd deps);
|
haftmann@29558
|
321 |
fun after_qed some_wit =
|
haftmann@29558
|
322 |
ProofContext.theory (register_subclass (sub, sup)
|
haftmann@29558
|
323 |
some_dep_morph some_wit export)
|
haftmann@29558
|
324 |
#> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
|
haftmann@29558
|
325 |
in do_proof after_qed some_prop goal_ctxt end;
|
haftmann@25462
|
326 |
|
haftmann@29575
|
327 |
fun user_proof after_qed some_prop =
|
haftmann@29575
|
328 |
Element.witness_proof (after_qed o try the_single o the_single)
|
haftmann@29575
|
329 |
[the_list some_prop];
|
haftmann@25462
|
330 |
|
haftmann@29575
|
331 |
fun tactic_proof tac after_qed some_prop ctxt =
|
haftmann@29575
|
332 |
after_qed (Option.map
|
haftmann@29575
|
333 |
(fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt;
|
haftmann@25462
|
334 |
|
haftmann@29358
|
335 |
in
|
haftmann@25462
|
336 |
|
haftmann@29358
|
337 |
val subclass = gen_subclass (K I) user_proof;
|
haftmann@29358
|
338 |
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
|
haftmann@29358
|
339 |
val subclass_cmd = gen_subclass Sign.read_class user_proof;
|
haftmann@26259
|
340 |
|
haftmann@29358
|
341 |
end; (*local*)
|
haftmann@26518
|
342 |
|
haftmann@24218
|
343 |
end;
|