72 |
72 |
73 (* assm_intro *) |
73 (* assm_intro *) |
74 fun prove_assm_intro thm = |
74 fun prove_assm_intro thm = |
75 let |
75 let |
76 val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; |
76 val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; |
77 val thm'' = Morphism.thm (const_morph $> eq_morph) thm'; |
77 val const_eq_morph = case eq_morph |
|
78 of SOME eq_morph => const_morph $> eq_morph |
|
79 | NONE => const_morph |
|
80 val thm'' = Morphism.thm const_eq_morph thm'; |
78 val tac = ALLGOALS (ProofContext.fact_tac [thm'']); |
81 val tac = ALLGOALS (ProofContext.fact_tac [thm'']); |
79 in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; |
82 in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; |
80 val assm_intro = Option.map prove_assm_intro |
83 val assm_intro = Option.map prove_assm_intro |
81 (fst (Locale.intros_of thy class)); |
84 (fst (Locale.intros_of thy class)); |
82 |
85 |
288 |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |
291 |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax |
289 ||> Theory.checkpoint |
292 ||> Theory.checkpoint |
290 |-> (fn (param_map, params, assm_axiom) => |
293 |-> (fn (param_map, params, assm_axiom) => |
291 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
294 `(fn thy => calculate thy class sups base_sort param_map assm_axiom) |
292 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
295 #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => |
293 Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph |
296 Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph) |
|
297 (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*) |
|
298 (Option.map (rpair true) eq_morph) export_morph |
294 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
299 #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) |
295 |> Theory_Target.init (SOME class) |
300 |> Theory_Target.init (SOME class) |
296 |> pair class |
301 |> pair class |
297 end; |
302 end; |
298 |
303 |