equal
deleted
inserted
replaced
14 |
14 |
15 structure Subclass : SUBCLASS = |
15 structure Subclass : SUBCLASS = |
16 struct |
16 struct |
17 |
17 |
18 local |
18 local |
19 |
|
20 fun the_option [x] = SOME x |
|
21 | the_option [] = NONE |
|
22 | the_option _ = raise Empty; |
|
23 |
19 |
24 fun gen_subclass prep_class do_proof raw_sup lthy = |
20 fun gen_subclass prep_class do_proof raw_sup lthy = |
25 let |
21 let |
26 val thy = ProofContext.theory_of lthy; |
22 val thy = ProofContext.theory_of lthy; |
27 val sup = prep_class thy raw_sup; |
23 val sup = prep_class thy raw_sup; |
39 error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ |
35 error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ |
40 commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); |
36 commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); |
41 val sublocale_prop = |
37 val sublocale_prop = |
42 Locale.global_asms_of thy sup |
38 Locale.global_asms_of thy sup |
43 |> maps snd |
39 |> maps snd |
44 |> the_option |
40 |> try the_single |
45 |> Option.map (ObjectLogic.ensure_propT thy); |
41 |> Option.map (ObjectLogic.ensure_propT thy); |
46 fun after_qed some_thm = |
42 fun after_qed some_thm = |
47 LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm) |
43 LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm) |
48 #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
44 #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
49 in |
45 in |
51 end; |
47 end; |
52 |
48 |
53 fun user_proof after_qed NONE = |
49 fun user_proof after_qed NONE = |
54 Proof.theorem_i NONE (K (after_qed NONE)) [[]] |
50 Proof.theorem_i NONE (K (after_qed NONE)) [[]] |
55 | user_proof after_qed (SOME prop) = |
51 | user_proof after_qed (SOME prop) = |
56 Proof.theorem_i NONE (after_qed o the_option o the_single) [[(prop, [])]]; |
52 Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; |
57 |
53 |
58 fun tactic_proof tac after_qed NONE lthy = |
54 fun tactic_proof tac after_qed NONE lthy = |
59 after_qed NONE lthy |
55 after_qed NONE lthy |
60 | tactic_proof tac after_qed (SOME prop) lthy = |
56 | tactic_proof tac after_qed (SOME prop) lthy = |
61 after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop |
57 after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop |