66 |
66 |
67 (* canonical interpretation *) |
67 (* canonical interpretation *) |
68 val base_morph = inst_morph |
68 val base_morph = inst_morph |
69 $> Morphism.binding_morphism (Binding.prefix false (class_prefix class)) |
69 $> Morphism.binding_morphism (Binding.prefix false (class_prefix class)) |
70 $> Element.satisfy_morphism (the_list wit); |
70 $> Element.satisfy_morphism (the_list wit); |
71 val eqs = these_defs thy sups; |
71 val eq_morph = Element.eq_morphism thy (these_defs thy sups); |
72 val eq_morph = Element.eq_morphism thy eqs; |
|
73 |
72 |
74 (* assm_intro *) |
73 (* assm_intro *) |
75 fun prove_assm_intro thm = |
74 fun prove_assm_intro thm = |
76 let |
75 let |
77 val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; |
76 val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; |
94 (Tactic.match_tac (axclass_intro :: sup_of_classes |
93 (Tactic.match_tac (axclass_intro :: sup_of_classes |
95 @ loc_axiom_intros @ base_sort_trivs) |
94 @ loc_axiom_intros @ base_sort_trivs) |
96 ORELSE' Tactic.assume_tac)); |
95 ORELSE' Tactic.assume_tac)); |
97 val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac); |
96 val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac); |
98 |
97 |
99 in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end; |
98 in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end; |
100 |
99 |
101 |
100 |
102 (* reading and processing class specifications *) |
101 (* reading and processing class specifications *) |
103 |
102 |
104 fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems = |
103 fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems = |
285 |> snd |> LocalTheory.exit_global |
284 |> snd |> LocalTheory.exit_global |
286 |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax |
285 |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax |
287 ||> Theory.checkpoint |
286 ||> Theory.checkpoint |
288 |-> (fn (param_map, params, assm_axiom) => |
287 |-> (fn (param_map, params, assm_axiom) => |
289 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
288 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
290 #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) => |
289 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
291 Locale.add_registration_eqs (class, base_morph) eqs export_morph |
290 Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph |
|
291 (*FIXME should not modify base_morph, although admissible*) |
292 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
292 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
293 |> TheoryTarget.init (SOME class) |
293 |> TheoryTarget.init (SOME class) |
294 |> pair class |
294 |> pair class |
295 end; |
295 end; |
296 |
296 |