author | haftmann |
Thu, 25 Oct 2007 19:27:54 +0200 | |
changeset 25196 | 0db9a16c0d3c |
parent 25189 | a1997f7a394a |
child 25267 | 1f745c599b5c |
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 |
25189 | 22 |
(*FIXME make more use of local context; drop redundancies*) |
24914 | 23 |
val ctxt = LocalTheory.target_of lthy; |
24 |
val thy = ProofContext.theory_of ctxt; |
|
25 |
val sup = prep_class thy raw_sup; |
|
25011 | 26 |
val sub = case TheoryTarget.peek lthy |
27 |
of {is_class = false, ...} => error "No class context" |
|
28 |
| {target, ...} => target; |
|
25002 | 29 |
val sub_params = map fst (Class.these_params thy [sub]); |
30 |
val sup_params = map fst (Class.these_params thy [sup]); |
|
31 |
val err_params = subtract (op =) sub_params sup_params; |
|
32 |
val _ = if null err_params then [] else |
|
33 |
error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^ |
|
34 |
commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); |
|
35 |
val sublocale_prop = |
|
25027
44b60657f54f
removed obsolete Class.class_of_locale/locale_of_class;
wenzelm
parents:
25011
diff
changeset
|
36 |
Locale.global_asms_of thy sup |
25002 | 37 |
|> maps snd |
38 |
|> map (ObjectLogic.ensure_propT thy); |
|
39 |
fun after_qed thms = |
|
25196 | 40 |
LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt) |
25189 | 41 |
(*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*); |
25002 | 42 |
in |
43 |
do_proof after_qed sublocale_prop lthy |
|
44 |
end; |
|
24934
9f5d60fe9086
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24914
diff
changeset
|
45 |
|
25002 | 46 |
fun user_proof after_qed props = |
47 |
Proof.theorem_i NONE (after_qed o the_single) [map (rpair []) props]; |
|
48 |
||
49 |
fun tactic_proof tac after_qed props lthy = |
|
50 |
after_qed (Goal.prove_multi (LocalTheory.target_of lthy) [] [] props |
|
51 |
(K tac)) lthy; |
|
24914 | 52 |
|
53 |
in |
|
54 |
||
25002 | 55 |
val subclass = gen_subclass (K I) user_proof; |
56 |
val subclass_cmd = gen_subclass Sign.read_class user_proof; |
|
57 |
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); |
|
24914 | 58 |
|
59 |
end; (*local*) |
|
60 |
||
61 |
end; |