author | wenzelm |
Sun, 10 Feb 2008 20:49:48 +0100 | |
changeset 26054 | 345e495d3b92 |
parent 25620 | a6cb8f60cff7 |
child 26276 | 3386bb568550 |
permissions | -rw-r--r-- |
24914 | 1 |
(* Title: Pure/Isar/subclass.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
25196 | 5 |
User interface for proving subclass relationship between type classes. |
24914 | 6 |
*) |
7 |
||
8 |
signature SUBCLASS = |
|
9 |
sig |
|
10 |
val subclass: class -> local_theory -> Proof.state |
|
11 |
val subclass_cmd: xstring -> local_theory -> Proof.state |
|
25002 | 12 |
val prove_subclass: tactic -> class -> local_theory -> local_theory |
24914 | 13 |
end; |
14 |
||
15 |
structure Subclass : SUBCLASS = |
|
16 |
struct |
|
17 |
||
18 |
local |
|
19 |
||
25002 | 20 |
fun gen_subclass prep_class do_proof raw_sup lthy = |
24914 | 21 |
let |
25620 | 22 |
val thy = ProofContext.theory_of lthy; |
24914 | 23 |
val sup = prep_class thy raw_sup; |
25011 | 24 |
val sub = case TheoryTarget.peek lthy |
25 |
of {is_class = false, ...} => error "No class context" |
|
26 |
| {target, ...} => target; |
|
25002 | 27 |
val sub_params = map fst (Class.these_params thy [sub]); |
28 |
val sup_params = map fst (Class.these_params thy [sup]); |
|
29 |
val err_params = subtract (op =) sub_params sup_params; |
|
30 |
val _ = if null err_params then [] else |
|
31 |
error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^ |
|
25620 | 32 |
commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); |
25002 | 33 |
val sublocale_prop = |
25027
44b60657f54f
removed obsolete Class.class_of_locale/locale_of_class;
wenzelm
parents:
25011
diff
changeset
|
34 |
Locale.global_asms_of thy sup |
25002 | 35 |
|> maps snd |
25620 | 36 |
|> the_single |
37 |
|> ObjectLogic.ensure_propT thy; |
|
38 |
fun after_qed thm = |
|
39 |
LocalTheory.theory (Class.prove_subclass (sub, sup) thm) |
|
25289 | 40 |
#> LocalTheory.reinit; |
25002 | 41 |
in |
42 |
do_proof after_qed sublocale_prop lthy |
|
43 |
end; |
|
24934
9f5d60fe9086
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24914
diff
changeset
|
44 |
|
25620 | 45 |
fun user_proof after_qed prop = |
46 |
Proof.theorem_i NONE (after_qed o the_single o the_single) [[(prop, [])]]; |
|
25002 | 47 |
|
25620 | 48 |
fun tactic_proof tac after_qed prop lthy = |
49 |
after_qed (Goal.prove (LocalTheory.target_of lthy) [] [] prop |
|
25002 | 50 |
(K tac)) lthy; |
24914 | 51 |
|
52 |
in |
|
53 |
||
25002 | 54 |
val subclass = gen_subclass (K I) user_proof; |
55 |
val subclass_cmd = gen_subclass Sign.read_class user_proof; |
|
56 |
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); |
|
24914 | 57 |
|
58 |
end; (*local*) |
|
59 |
||
60 |
end; |