author | ballarin |
Tue, 30 Dec 2008 11:10:01 +0100 | |
changeset 29252 | ea97aa6aeba2 |
parent 29227 | 089499f104d3 |
permissions | -rw-r--r-- |
24914 | 1 |
(* Title: Pure/Isar/subclass.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
25196 | 4 |
User interface for proving subclass relationship between type classes. |
24914 | 5 |
*) |
6 |
||
7 |
signature SUBCLASS = |
|
8 |
sig |
|
9 |
val subclass: class -> local_theory -> Proof.state |
|
10 |
val subclass_cmd: xstring -> local_theory -> Proof.state |
|
25002 | 11 |
val prove_subclass: tactic -> class -> local_theory -> local_theory |
24914 | 12 |
end; |
13 |
||
14 |
structure Subclass : SUBCLASS = |
|
15 |
struct |
|
16 |
||
17 |
local |
|
18 |
||
25002 | 19 |
fun gen_subclass prep_class do_proof raw_sup lthy = |
24914 | 20 |
let |
25620 | 21 |
val thy = ProofContext.theory_of lthy; |
24914 | 22 |
val sup = prep_class thy raw_sup; |
25011 | 23 |
val sub = case TheoryTarget.peek lthy |
29227 | 24 |
of {is_class = false, ...} => error "Not a class context" |
25011 | 25 |
| {target, ...} => target; |
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
26 |
val _ = if Sign.subsort thy ([sup], [sub]) |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
27 |
then error ("Class " ^ Syntax.string_of_sort lthy [sup] |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
28 |
^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub]) |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
29 |
else (); |
25002 | 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 |
|
26950 | 34 |
error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ |
35 |
commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); |
|
25002 | 36 |
val sublocale_prop = |
25027
44b60657f54f
removed obsolete Class.class_of_locale/locale_of_class;
wenzelm
parents:
25011
diff
changeset
|
37 |
Locale.global_asms_of thy sup |
25002 | 38 |
|> maps snd |
28716 | 39 |
|> try the_single |
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
40 |
|> Option.map (ObjectLogic.ensure_propT thy); |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
41 |
fun after_qed some_thm = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
42 |
LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm) |
26276 | 43 |
#> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
25002 | 44 |
in |
45 |
do_proof after_qed sublocale_prop lthy |
|
46 |
end; |
|
24934
9f5d60fe9086
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24914
diff
changeset
|
47 |
|
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
48 |
fun user_proof after_qed NONE = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
49 |
Proof.theorem_i NONE (K (after_qed NONE)) [[]] |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
50 |
| user_proof after_qed (SOME prop) = |
28716 | 51 |
Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; |
25002 | 52 |
|
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
53 |
fun tactic_proof tac after_qed NONE lthy = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
54 |
after_qed NONE lthy |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
55 |
| tactic_proof tac after_qed (SOME prop) lthy = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
56 |
after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
57 |
(K tac))) lthy; |
24914 | 58 |
|
59 |
in |
|
60 |
||
25002 | 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); |
|
24914 | 64 |
|
65 |
end; (*local*) |
|
66 |
||
67 |
end; |