17 |
17 |
18 local |
18 local |
19 |
19 |
20 fun gen_subclass prep_class do_proof raw_sup lthy = |
20 fun gen_subclass prep_class do_proof raw_sup lthy = |
21 let |
21 let |
22 (*FIXME make more use of local context; drop redundancies*) |
22 val thy = ProofContext.theory_of lthy; |
23 val ctxt = LocalTheory.target_of lthy; |
|
24 val thy = ProofContext.theory_of ctxt; |
|
25 val sup = prep_class thy raw_sup; |
23 val sup = prep_class thy raw_sup; |
26 val sub = case TheoryTarget.peek lthy |
24 val sub = case TheoryTarget.peek lthy |
27 of {is_class = false, ...} => error "No class context" |
25 of {is_class = false, ...} => error "No class context" |
28 | {target, ...} => target; |
26 | {target, ...} => target; |
29 val sub_params = map fst (Class.these_params thy [sub]); |
27 val sub_params = map fst (Class.these_params thy [sub]); |
30 val sup_params = map fst (Class.these_params thy [sup]); |
28 val sup_params = map fst (Class.these_params thy [sup]); |
31 val err_params = subtract (op =) sub_params sup_params; |
29 val err_params = subtract (op =) sub_params sup_params; |
32 val _ = if null err_params then [] else |
30 val _ = if null err_params then [] else |
33 error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^ |
31 error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^ |
34 commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); |
32 commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); |
35 val sublocale_prop = |
33 val sublocale_prop = |
36 Locale.global_asms_of thy sup |
34 Locale.global_asms_of thy sup |
37 |> maps snd |
35 |> maps snd |
38 |> map (ObjectLogic.ensure_propT thy); |
36 |> the_single |
39 fun after_qed thms = |
37 |> ObjectLogic.ensure_propT thy; |
40 LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt) |
38 fun after_qed thm = |
|
39 LocalTheory.theory (Class.prove_subclass (sub, sup) thm) |
41 #> LocalTheory.reinit; |
40 #> LocalTheory.reinit; |
42 in |
41 in |
43 do_proof after_qed sublocale_prop lthy |
42 do_proof after_qed sublocale_prop lthy |
44 end; |
43 end; |
45 |
44 |
46 fun user_proof after_qed props = |
45 fun user_proof after_qed prop = |
47 Proof.theorem_i NONE (after_qed o the_single) [map (rpair []) props]; |
46 Proof.theorem_i NONE (after_qed o the_single o the_single) [[(prop, [])]]; |
48 |
47 |
49 fun tactic_proof tac after_qed props lthy = |
48 fun tactic_proof tac after_qed prop lthy = |
50 after_qed (Goal.prove_multi (LocalTheory.target_of lthy) [] [] props |
49 after_qed (Goal.prove (LocalTheory.target_of lthy) [] [] prop |
51 (K tac)) lthy; |
50 (K tac)) lthy; |
52 |
51 |
53 in |
52 in |
54 |
53 |
55 val subclass = gen_subclass (K I) user_proof; |
54 val subclass = gen_subclass (K I) user_proof; |