1 (* Title: Pure/Isar/subclass.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 User interface for proving subclass relationship between type classes. |
|
5 *) |
|
6 |
|
7 signature SUBCLASS = |
|
8 sig |
|
9 val subclass: class -> local_theory -> Proof.state |
|
10 val subclass_cmd: xstring -> local_theory -> Proof.state |
|
11 val prove_subclass: tactic -> class -> local_theory -> local_theory |
|
12 end; |
|
13 |
|
14 structure Subclass : SUBCLASS = |
|
15 struct |
|
16 |
|
17 local |
|
18 |
|
19 fun gen_subclass prep_class do_proof raw_sup lthy = |
|
20 let |
|
21 val thy = ProofContext.theory_of lthy; |
|
22 val sup = prep_class thy raw_sup; |
|
23 val sub = case TheoryTarget.peek lthy |
|
24 of {is_class = false, ...} => error "Not a class context" |
|
25 | {target, ...} => target; |
|
26 val _ = if Sign.subsort thy ([sup], [sub]) |
|
27 then error ("Class " ^ Syntax.string_of_sort lthy [sup] |
|
28 ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub]) |
|
29 else (); |
|
30 val sub_params = map fst (Class.these_params thy [sub]); |
|
31 val sup_params = map fst (Class.these_params thy [sup]); |
|
32 val err_params = subtract (op =) sub_params sup_params; |
|
33 val _ = if null err_params then [] else |
|
34 error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ |
|
35 commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); |
|
36 val sublocale_prop = |
|
37 Locale.global_asms_of thy sup |
|
38 |> maps snd |
|
39 |> try the_single |
|
40 |> Option.map (ObjectLogic.ensure_propT thy); |
|
41 fun after_qed some_thm = |
|
42 LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm) |
|
43 #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
|
44 in |
|
45 do_proof after_qed sublocale_prop lthy |
|
46 end; |
|
47 |
|
48 fun user_proof after_qed NONE = |
|
49 Proof.theorem_i NONE (K (after_qed NONE)) [[]] |
|
50 | user_proof after_qed (SOME prop) = |
|
51 Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; |
|
52 |
|
53 fun tactic_proof tac after_qed NONE lthy = |
|
54 after_qed NONE lthy |
|
55 | tactic_proof tac after_qed (SOME prop) lthy = |
|
56 after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop |
|
57 (K tac))) lthy; |
|
58 |
|
59 in |
|
60 |
|
61 val subclass = gen_subclass (K I) user_proof; |
|
62 val subclass_cmd = gen_subclass Sign.read_class user_proof; |
|
63 fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); |
|
64 |
|
65 end; (*local*) |
|
66 |
|
67 end; |
|