author | wenzelm |
Fri, 15 Sep 2006 22:56:08 +0200 | |
changeset 20547 | 796ae7fa1049 |
parent 19170 | a55a3464a1de |
child 20773 | 468af396cf6f |
permissions | -rw-r--r-- |
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
2 |
Author: Jia Meng, NICTA |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
3 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
4 |
Set of rules used for ATPs |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
5 |
*) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
6 |
|
19170 | 7 |
signature RES_ATPSET = |
8 |
sig |
|
9 |
type atpset |
|
10 |
val local_AtpSet_of: Proof.context -> atpset |
|
11 |
val add_atp_rules: atpset * Thm.thm list -> atpset |
|
12 |
val del_atp_rules: atpset * Thm.thm list -> atpset |
|
13 |
val get_AtpSet: theory -> atpset |
|
14 |
val print_local_AtpSet: Proof.context -> unit |
|
15 |
val AtpSet_of: theory -> atpset |
|
16 |
val add_atp_rule: Thm.thm * atpset -> atpset |
|
17 |
val del_atp_rule: Thm.thm * atpset -> atpset |
|
18 |
val print_atpset: atpset -> unit |
|
19 |
val setup: theory -> theory |
|
20 |
val get_local_AtpSet: Proof.context -> atpset |
|
21 |
val rep_as: atpset -> Thm.thm list |
|
22 |
val merge_atpset: atpset * atpset -> atpset |
|
23 |
val add_atp_rule': Thm.thm -> atpset -> atpset |
|
24 |
val del_atp_rule': Thm.thm -> atpset -> atpset |
|
25 |
val Add_AtpRs: Thm.thm list -> unit |
|
26 |
val Del_AtpRs: Thm.thm list -> unit |
|
27 |
val empty_atpset: atpset |
|
28 |
val put_local_AtpSet: atpset -> Proof.context -> Proof.context |
|
29 |
val print_AtpSet: theory -> unit |
|
30 |
val atp_rules_of_thy: theory -> Thm.thm list |
|
31 |
val atp_rules_of_ctxt: Proof.context -> Thm.thm list |
|
32 |
end; |
|
33 |
||
34 |
||
35 |
||
36 |
structure ResAtpSet : RES_ATPSET = |
|
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
37 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
38 |
struct |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
39 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
40 |
datatype atpset = AtpSet of thm list |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
41 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
42 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
43 |
val mem_thm = member Drule.eq_thm_prop; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
44 |
val rem_thm = remove Drule.eq_thm_prop; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
45 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
46 |
val empty_atpset = AtpSet []; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
47 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
48 |
fun add_atp_rule (thm,AtpSet thms) = |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
49 |
if mem_thm thms thm then (warning ("Ignoring duplicate ATP rules\n" ^ string_of_thm thm); AtpSet thms) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
50 |
else |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
51 |
AtpSet (thm::thms); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
52 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
53 |
fun add_atp_rule' thm ars = add_atp_rule (thm,ars); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
54 |
fun add_atp_rules (ars,thms) = foldl add_atp_rule ars thms; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
55 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
56 |
fun del_atp_rule (thm,AtpSet thms) = |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
57 |
if mem_thm thms thm then AtpSet (rem_thm thm thms) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
58 |
else |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
59 |
(warning "Undeclared rule for ATPs"; AtpSet thms); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
60 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
61 |
fun del_atp_rule' thm ars = del_atp_rule (thm,ars); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
62 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
63 |
fun del_atp_rules (ars,thms) = foldl del_atp_rule ars thms; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
64 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
65 |
fun merge_atpset (ars1, AtpSet thms2) = add_atp_rules (ars1,thms2); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
66 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
67 |
fun print_atpset (AtpSet thms) = |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
68 |
let val pretty_thms = map Display.pretty_thm in |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
69 |
[Pretty.big_list "Rules for ATPs:" (pretty_thms thms)] |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
70 |
|> Pretty.chunks |> Pretty.writeln |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
71 |
end; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
72 |
|
19170 | 73 |
fun rep_as (AtpSet thms) = thms; |
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
74 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
75 |
(* global AtpSet *) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
76 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
77 |
structure GlobalAtpSet = TheoryDataFun |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
78 |
(struct |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
79 |
val name = "AtpSet"; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
80 |
type T = atpset ref; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
81 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
82 |
val empty = ref empty_atpset; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
83 |
fun copy (ref atpst) = ref atpst : T; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
84 |
val extend = copy; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
85 |
fun merge _ (ref atpst1, ref atpst2) = |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
86 |
ref (merge_atpset (atpst1, atpst2)); |
20547 | 87 |
fun print _ (ref atpst) = print_atpset atpst; |
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
88 |
end); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
89 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
90 |
val print_AtpSet = GlobalAtpSet.print; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
91 |
val get_AtpSet = ! o GlobalAtpSet.get; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
92 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
93 |
val change_AtpSet_of = change o GlobalAtpSet.get; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
94 |
fun change_AtpSet f = change_AtpSet_of (Context.the_context ()) f; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
95 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
96 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
97 |
fun AtpSet_of thy = get_AtpSet thy; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
98 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
99 |
fun Add_AtpRs args = change_AtpSet (fn ars => add_atp_rules (ars,args)); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
100 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
101 |
fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args)); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
102 |
|
19170 | 103 |
fun atp_rules_of_thy thy = rep_as (AtpSet_of thy); |
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
104 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
105 |
(* local AtpSet *) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
106 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
107 |
structure LocalAtpSet = ProofDataFun |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
108 |
(struct |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
109 |
val name = "AtpSet"; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
110 |
type T = atpset; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
111 |
val init = get_AtpSet; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
112 |
fun print _ atpst = print_atpset atpst; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
113 |
end); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
114 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
115 |
val print_local_AtpSet = LocalAtpSet.print; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
116 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
117 |
val get_local_AtpSet = LocalAtpSet.get; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
118 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
119 |
val put_local_AtpSet = LocalAtpSet.put; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
120 |
|
19170 | 121 |
fun local_AtpSet_of ctxt = get_local_AtpSet ctxt; |
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
122 |
|
19170 | 123 |
fun atp_rules_of_ctxt ctxt = rep_as (local_AtpSet_of ctxt); |
19159
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
124 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
125 |
(* attributes *) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
126 |
fun attrib f = Thm.declaration_attribute (fn th => |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
127 |
fn Context.Theory thy => (change_AtpSet_of thy (f th); Context.Theory thy) |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
128 |
| Context.Proof ctxt => Context.Proof (LocalAtpSet.map (f th) ctxt)); |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
129 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
130 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
131 |
val add_rule = attrib add_atp_rule'; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
132 |
val del_rule = attrib del_atp_rule'; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
133 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
134 |
val atpN = "atp"; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
135 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
136 |
val setup_attrs = Attrib.add_attributes |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
137 |
[(atpN, Attrib.add_del_args add_rule del_rule, "declaration of ATP rules")]; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
138 |
|
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
139 |
val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs; |
f737ecbad1c4
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
mengj
parents:
diff
changeset
|
140 |
|
20547 | 141 |
end; |