author | ballarin |
Mon, 08 Dec 2008 14:22:42 +0100 | |
changeset 29020 | 3e95d28114a1 |
parent 28716 | ee6f9e50f9c8 |
child 29227 | 089499f104d3 |
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; |
|
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
27 |
val _ = if Sign.subsort thy ([sup], [sub]) |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
28 |
then error ("Class " ^ Syntax.string_of_sort lthy [sup] |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
29 |
^ " 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
|
30 |
else (); |
25002 | 31 |
val sub_params = map fst (Class.these_params thy [sub]); |
32 |
val sup_params = map fst (Class.these_params thy [sup]); |
|
33 |
val err_params = subtract (op =) sub_params sup_params; |
|
34 |
val _ = if null err_params then [] else |
|
26950 | 35 |
error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ |
36 |
commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); |
|
25002 | 37 |
val sublocale_prop = |
25027
44b60657f54f
removed obsolete Class.class_of_locale/locale_of_class;
wenzelm
parents:
25011
diff
changeset
|
38 |
Locale.global_asms_of thy sup |
25002 | 39 |
|> maps snd |
28716 | 40 |
|> try the_single |
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
41 |
|> Option.map (ObjectLogic.ensure_propT thy); |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
42 |
fun after_qed some_thm = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
43 |
LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm) |
26276 | 44 |
#> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
25002 | 45 |
in |
46 |
do_proof after_qed sublocale_prop lthy |
|
47 |
end; |
|
24934
9f5d60fe9086
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24914
diff
changeset
|
48 |
|
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
49 |
fun user_proof after_qed NONE = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
50 |
Proof.theorem_i NONE (K (after_qed NONE)) [[]] |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
51 |
| user_proof after_qed (SOME prop) = |
28716 | 52 |
Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; |
25002 | 53 |
|
27684
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
54 |
fun tactic_proof tac after_qed NONE lthy = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
55 |
after_qed NONE lthy |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
56 |
| tactic_proof tac after_qed (SOME prop) lthy = |
f45fd1159a4b
subclass now also works for subclasses with empty specificaton
haftmann
parents:
26950
diff
changeset
|
57 |
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
|
58 |
(K tac))) lthy; |
24914 | 59 |
|
60 |
in |
|
61 |
||
25002 | 62 |
val subclass = gen_subclass (K I) user_proof; |
63 |
val subclass_cmd = gen_subclass Sign.read_class user_proof; |
|
64 |
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); |
|
24914 | 65 |
|
66 |
end; (*local*) |
|
67 |
||
68 |
end; |