author | wenzelm |
Wed, 13 Apr 2005 18:34:22 +0200 | |
changeset 15703 | 727ef1b8b3ee |
parent 15574 | b1d1b5bfc464 |
child 15707 | 80b421d8a8be |
permissions | -rw-r--r-- |
9938 | 1 |
(* Title: Provers/classical.ML |
0 | 2 |
ID: $Id$ |
9938 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
Theorem prover for classical reasoning, including predicate calculus, set |
|
7 |
theory, etc. |
|
8 |
||
9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset
|
9 |
Rules must be classified as intro, elim, safe, hazardous (unsafe). |
0 | 10 |
|
11 |
A rule is unsafe unless it can be applied blindly without harmful results. |
|
12 |
For a rule to be safe, its premises and conclusion should be logically |
|
13 |
equivalent. There should be no variables in the premises that are not in |
|
14 |
the conclusion. |
|
15 |
*) |
|
16 |
||
15452 | 17 |
|
18 |
(*added: get_delta_claset, put_delta_claset. |
|
19 |
changed: safe_{dest,elim,intro}_local and haz_{dest,elim,intro}_local |
|
20 |
06/01/05 |
|
21 |
*) |
|
22 |
||
23 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
24 |
(*higher precedence than := facilitates use of references*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
25 |
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules |
4651 | 26 |
addSWrapper delSWrapper addWrapper delWrapper |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
27 |
addSbefore addSafter addbefore addafter |
5523 | 28 |
addD2 addE2 addSD2 addSE2; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
29 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
30 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
31 |
(*should be a type abbreviation in signature CLASSICAL*) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
32 |
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; |
4651 | 33 |
type wrapper = (int -> tactic) -> (int -> tactic); |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
34 |
|
0 | 35 |
signature CLASSICAL_DATA = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
36 |
sig |
9171 | 37 |
val make_elim : thm -> thm (* Tactic.make_elim or a classical version*) |
9938 | 38 |
val mp : thm (* [| P-->Q; P |] ==> Q *) |
39 |
val not_elim : thm (* [| ~P; P |] ==> R *) |
|
40 |
val classical : thm (* (~P ==> P) ==> P *) |
|
41 |
val sizef : thm -> int (* size function for BEST_FIRST *) |
|
0 | 42 |
val hyp_subst_tacs: (int -> tactic) list |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
43 |
end; |
0 | 44 |
|
5841 | 45 |
signature BASIC_CLASSICAL = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
46 |
sig |
0 | 47 |
type claset |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
48 |
val empty_cs: claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
49 |
val print_cs: claset -> unit |
4380 | 50 |
val print_claset: theory -> unit |
4653 | 51 |
val rep_cs: (* BLAST_DATA in blast.ML dependent on this *) |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
52 |
claset -> {safeIs: thm list, safeEs: thm list, |
9938 | 53 |
hazIs: thm list, hazEs: thm list, |
10736 | 54 |
swrappers: (string * wrapper) list, |
9938 | 55 |
uwrappers: (string * wrapper) list, |
56 |
safe0_netpair: netpair, safep_netpair: netpair, |
|
12401 | 57 |
haz_netpair: netpair, dup_netpair: netpair, |
58 |
xtra_netpair: ContextRules.netpair} |
|
9938 | 59 |
val merge_cs : claset * claset -> claset |
60 |
val addDs : claset * thm list -> claset |
|
61 |
val addEs : claset * thm list -> claset |
|
62 |
val addIs : claset * thm list -> claset |
|
63 |
val addSDs : claset * thm list -> claset |
|
64 |
val addSEs : claset * thm list -> claset |
|
65 |
val addSIs : claset * thm list -> claset |
|
66 |
val delrules : claset * thm list -> claset |
|
67 |
val addSWrapper : claset * (string * wrapper) -> claset |
|
68 |
val delSWrapper : claset * string -> claset |
|
69 |
val addWrapper : claset * (string * wrapper) -> claset |
|
70 |
val delWrapper : claset * string -> claset |
|
71 |
val addSbefore : claset * (string * (int -> tactic)) -> claset |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
72 |
val addSafter : claset * (string * (int -> tactic)) -> claset |
9938 | 73 |
val addbefore : claset * (string * (int -> tactic)) -> claset |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
74 |
val addafter : claset * (string * (int -> tactic)) -> claset |
5523 | 75 |
val addD2 : claset * (string * thm) -> claset |
76 |
val addE2 : claset * (string * thm) -> claset |
|
77 |
val addSD2 : claset * (string * thm) -> claset |
|
78 |
val addSE2 : claset * (string * thm) -> claset |
|
9938 | 79 |
val appSWrappers : claset -> wrapper |
80 |
val appWrappers : claset -> wrapper |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
81 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
82 |
val claset_ref_of_sg: Sign.sg -> claset ref |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
83 |
val claset_ref_of: theory -> claset ref |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
84 |
val claset_of_sg: Sign.sg -> claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
85 |
val claset_of: theory -> claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
86 |
val CLASET: (claset -> tactic) -> tactic |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
87 |
val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
88 |
val claset: unit -> claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
89 |
val claset_ref: unit -> claset ref |
15036 | 90 |
val local_claset_of : Proof.context -> claset |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
91 |
|
9938 | 92 |
val fast_tac : claset -> int -> tactic |
93 |
val slow_tac : claset -> int -> tactic |
|
94 |
val weight_ASTAR : int ref |
|
95 |
val astar_tac : claset -> int -> tactic |
|
96 |
val slow_astar_tac : claset -> int -> tactic |
|
97 |
val best_tac : claset -> int -> tactic |
|
98 |
val first_best_tac : claset -> int -> tactic |
|
99 |
val slow_best_tac : claset -> int -> tactic |
|
100 |
val depth_tac : claset -> int -> int -> tactic |
|
101 |
val deepen_tac : claset -> int -> int -> tactic |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
102 |
|
9938 | 103 |
val contr_tac : int -> tactic |
104 |
val dup_elim : thm -> thm |
|
105 |
val dup_intr : thm -> thm |
|
106 |
val dup_step_tac : claset -> int -> tactic |
|
107 |
val eq_mp_tac : int -> tactic |
|
108 |
val haz_step_tac : claset -> int -> tactic |
|
109 |
val joinrules : thm list * thm list -> (bool * thm) list |
|
110 |
val mp_tac : int -> tactic |
|
111 |
val safe_tac : claset -> tactic |
|
112 |
val safe_steps_tac : claset -> int -> tactic |
|
113 |
val safe_step_tac : claset -> int -> tactic |
|
114 |
val clarify_tac : claset -> int -> tactic |
|
115 |
val clarify_step_tac : claset -> int -> tactic |
|
116 |
val step_tac : claset -> int -> tactic |
|
117 |
val slow_step_tac : claset -> int -> tactic |
|
118 |
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
|
119 |
val swapify : thm list -> thm list |
|
120 |
val swap_res_tac : thm list -> int -> tactic |
|
121 |
val inst_step_tac : claset -> int -> tactic |
|
122 |
val inst0_step_tac : claset -> int -> tactic |
|
123 |
val instp_step_tac : claset -> int -> tactic |
|
1724 | 124 |
|
9938 | 125 |
val AddDs : thm list -> unit |
126 |
val AddEs : thm list -> unit |
|
127 |
val AddIs : thm list -> unit |
|
128 |
val AddSDs : thm list -> unit |
|
129 |
val AddSEs : thm list -> unit |
|
130 |
val AddSIs : thm list -> unit |
|
131 |
val Delrules : thm list -> unit |
|
132 |
val Safe_tac : tactic |
|
133 |
val Safe_step_tac : int -> tactic |
|
134 |
val Clarify_tac : int -> tactic |
|
135 |
val Clarify_step_tac : int -> tactic |
|
136 |
val Step_tac : int -> tactic |
|
137 |
val Fast_tac : int -> tactic |
|
138 |
val Best_tac : int -> tactic |
|
139 |
val Slow_tac : int -> tactic |
|
2066 | 140 |
val Slow_best_tac : int -> tactic |
9938 | 141 |
val Deepen_tac : int -> int -> tactic |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
142 |
end; |
1724 | 143 |
|
5841 | 144 |
signature CLASSICAL = |
145 |
sig |
|
146 |
include BASIC_CLASSICAL |
|
15036 | 147 |
val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory |
148 |
val del_context_safe_wrapper: string -> theory -> theory |
|
149 |
val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory |
|
150 |
val del_context_unsafe_wrapper: string -> theory -> theory |
|
5841 | 151 |
val print_local_claset: Proof.context -> unit |
152 |
val get_local_claset: Proof.context -> claset |
|
153 |
val put_local_claset: claset -> Proof.context -> Proof.context |
|
154 |
val safe_dest_global: theory attribute |
|
155 |
val safe_elim_global: theory attribute |
|
156 |
val safe_intro_global: theory attribute |
|
6955 | 157 |
val haz_dest_global: theory attribute |
158 |
val haz_elim_global: theory attribute |
|
159 |
val haz_intro_global: theory attribute |
|
9938 | 160 |
val rule_del_global: theory attribute |
6955 | 161 |
val safe_dest_local: Proof.context attribute |
162 |
val safe_elim_local: Proof.context attribute |
|
163 |
val safe_intro_local: Proof.context attribute |
|
5885 | 164 |
val haz_dest_local: Proof.context attribute |
165 |
val haz_elim_local: Proof.context attribute |
|
166 |
val haz_intro_local: Proof.context attribute |
|
9938 | 167 |
val rule_del_local: Proof.context attribute |
7272 | 168 |
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list |
7559 | 169 |
val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method |
170 |
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method |
|
15703 | 171 |
val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method |
172 |
val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method |
|
5841 | 173 |
val setup: (theory -> theory) list |
15452 | 174 |
|
175 |
val get_delta_claset: ProofContext.context -> claset |
|
176 |
val put_delta_claset: claset -> ProofContext.context -> ProofContext.context |
|
177 |
||
5841 | 178 |
end; |
179 |
||
0 | 180 |
|
5927 | 181 |
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
0 | 182 |
struct |
183 |
||
7354 | 184 |
local open Data in |
0 | 185 |
|
1800 | 186 |
(*** Useful tactics for classical reasoning ***) |
0 | 187 |
|
1524 | 188 |
val imp_elim = (*cannot use bind_thm within a structure!*) |
9938 | 189 |
store_thm ("imp_elim", Data.make_elim mp); |
0 | 190 |
|
10736 | 191 |
(*Prove goal that assumes both P and ~P. |
4392 | 192 |
No backtracking if it finds an equal assumption. Perhaps should call |
193 |
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) |
|
10736 | 194 |
val contr_tac = eresolve_tac [not_elim] THEN' |
4392 | 195 |
(eq_assume_tac ORELSE' assume_tac); |
0 | 196 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
197 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q. |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
198 |
Could do the same thing for P<->Q and P... *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
199 |
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; |
0 | 200 |
|
201 |
(*Like mp_tac but instantiates no variables*) |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
202 |
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
203 |
|
1524 | 204 |
val swap = |
205 |
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); |
|
0 | 206 |
|
207 |
(*Creates rules to eliminate ~A, from rules to introduce A*) |
|
208 |
fun swapify intrs = intrs RLN (2, [swap]); |
|
12401 | 209 |
fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x; |
0 | 210 |
|
211 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
212 |
trying rules in order. *) |
|
10736 | 213 |
fun swap_res_tac rls = |
54 | 214 |
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls |
10736 | 215 |
in assume_tac ORELSE' |
216 |
contr_tac ORELSE' |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
217 |
biresolve_tac (foldr addrl [] rls) |
0 | 218 |
end; |
219 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
220 |
(*Duplication of hazardous rules, for complete provers*) |
2689
6d3d893453de
dup_intr & dup_elim no longer call standard -- this
paulson
parents:
2630
diff
changeset
|
221 |
fun dup_intr th = zero_var_indexes (th RS classical); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
222 |
|
6967 | 223 |
fun dup_elim th = |
13525 | 224 |
(case try (fn () => |
225 |
rule_by_tactic (TRYALL (etac revcut_rl)) |
|
226 |
(th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of |
|
15531 | 227 |
SOME th' => th' |
6967 | 228 |
| _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); |
0 | 229 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
230 |
|
1800 | 231 |
(**** Classical rule sets ****) |
0 | 232 |
|
233 |
datatype claset = |
|
12401 | 234 |
CS of {safeIs : thm list, (*safe introduction rules*) |
235 |
safeEs : thm list, (*safe elimination rules*) |
|
236 |
hazIs : thm list, (*unsafe introduction rules*) |
|
237 |
hazEs : thm list, (*unsafe elimination rules*) |
|
238 |
swrappers : (string * wrapper) list, (*for transforming safe_step_tac*) |
|
9938 | 239 |
uwrappers : (string * wrapper) list, (*for transforming step_tac*) |
12401 | 240 |
safe0_netpair : netpair, (*nets for trivial cases*) |
241 |
safep_netpair : netpair, (*nets for >0 subgoals*) |
|
242 |
haz_netpair : netpair, (*nets for unsafe rules*) |
|
243 |
dup_netpair : netpair, (*nets for duplication*) |
|
244 |
xtra_netpair : ContextRules.netpair}; (*nets for extra rules*) |
|
0 | 245 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
246 |
(*Desired invariants are |
9938 | 247 |
safe0_netpair = build safe0_brls, |
248 |
safep_netpair = build safep_brls, |
|
249 |
haz_netpair = build (joinrules(hazIs, hazEs)), |
|
10736 | 250 |
dup_netpair = build (joinrules(map dup_intr hazIs, |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
251 |
map dup_elim hazEs)) |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
252 |
|
10736 | 253 |
where build = build_netpair(Net.empty,Net.empty), |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
254 |
safe0_brls contains all brules that solve the subgoal, and |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
255 |
safep_brls contains all brules that generate 1 or more new subgoals. |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
256 |
The theorem lists are largely comments, though they are used in merge_cs and print_cs. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
257 |
Nets must be built incrementally, to save space and time. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
258 |
*) |
0 | 259 |
|
6502 | 260 |
val empty_netpair = (Net.empty, Net.empty); |
261 |
||
10736 | 262 |
val empty_cs = |
9938 | 263 |
CS{safeIs = [], |
264 |
safeEs = [], |
|
265 |
hazIs = [], |
|
266 |
hazEs = [], |
|
4651 | 267 |
swrappers = [], |
268 |
uwrappers = [], |
|
6502 | 269 |
safe0_netpair = empty_netpair, |
270 |
safep_netpair = empty_netpair, |
|
271 |
haz_netpair = empty_netpair, |
|
6955 | 272 |
dup_netpair = empty_netpair, |
273 |
xtra_netpair = empty_netpair}; |
|
0 | 274 |
|
15036 | 275 |
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) = |
3546 | 276 |
let val pretty_thms = map Display.pretty_thm in |
9760 | 277 |
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), |
278 |
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), |
|
279 |
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), |
|
15036 | 280 |
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), |
281 |
Pretty.strs ("safe wrappers:" :: map #1 swrappers), |
|
282 |
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] |
|
8727 | 283 |
|> Pretty.chunks |> Pretty.writeln |
3546 | 284 |
end; |
0 | 285 |
|
4653 | 286 |
fun rep_cs (CS args) = args; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
287 |
|
10736 | 288 |
local |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
289 |
fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l; |
10736 | 290 |
in |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
291 |
fun appSWrappers (CS{swrappers,...}) = wrap swrappers; |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
292 |
fun appWrappers (CS{uwrappers,...}) = wrap uwrappers; |
4651 | 293 |
end; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
294 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
295 |
|
1800 | 296 |
(*** Adding (un)safe introduction or elimination rules. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
297 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
298 |
In case of overlap, new rules are tried BEFORE old ones!! |
1800 | 299 |
***) |
0 | 300 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
301 |
(*For use with biresolve_tac. Combines intro rules with swap to handle negated |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
302 |
assumptions. Pairs elim rules with true. *) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
303 |
fun joinrules (intrs, elims) = |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
304 |
(map (pair true) (elims @ swapify intrs) @ map (pair false) intrs); |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
305 |
|
12401 | 306 |
fun joinrules' (intrs, elims) = |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
307 |
(map (pair true) elims @ map (pair false) intrs); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
308 |
|
10736 | 309 |
(*Priority: prefer rules with fewest subgoals, |
1231 | 310 |
then rules added most recently (preferring the head of the list).*) |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
311 |
fun tag_brls k [] = [] |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
312 |
| tag_brls k (brl::brls) = |
10736 | 313 |
(1000000*subgoals_of_brl brl + k, brl) :: |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
314 |
tag_brls (k+1) brls; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
315 |
|
12401 | 316 |
fun tag_brls' _ _ [] = [] |
317 |
| tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; |
|
10736 | 318 |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
319 |
fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
320 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
321 |
(*Insert into netpair that already has nI intr rules and nE elim rules. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
322 |
Count the intr rules double (to account for swapify). Negate to give the |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
323 |
new insertions the lowest priority.*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
324 |
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; |
12401 | 325 |
fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules'; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
326 |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
327 |
fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls; |
12362 | 328 |
fun delete x = delete_tagged_list (joinrules x); |
12401 | 329 |
fun delete' x = delete_tagged_list (joinrules' x); |
1800 | 330 |
|
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset
|
331 |
val mem_thm = gen_mem Drule.eq_thm_prop |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset
|
332 |
and rem_thm = gen_rem Drule.eq_thm_prop; |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
333 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
334 |
(*Warn if the rule is already present ELSEWHERE in the claset. The addition |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
335 |
is still allowed.*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
336 |
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = |
10736 | 337 |
if mem_thm (th, safeIs) then |
9938 | 338 |
warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
339 |
else if mem_thm (th, safeEs) then |
9408 | 340 |
warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) |
10736 | 341 |
else if mem_thm (th, hazIs) then |
9760 | 342 |
warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th) |
10736 | 343 |
else if mem_thm (th, hazEs) then |
9760 | 344 |
warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
345 |
else (); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
346 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
347 |
|
1800 | 348 |
(*** Safe rules ***) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
349 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
350 |
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 351 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
352 |
th) = |
|
10736 | 353 |
if mem_thm (th, safeIs) then |
9938 | 354 |
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); |
355 |
cs) |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
356 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
357 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
15570 | 358 |
List.partition Thm.no_prems [th] |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
359 |
val nI = length safeIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
360 |
and nE = length safeEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
361 |
in warn_dup th cs; |
9938 | 362 |
CS{safeIs = th::safeIs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
363 |
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
9938 | 364 |
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
365 |
safeEs = safeEs, |
|
366 |
hazIs = hazIs, |
|
367 |
hazEs = hazEs, |
|
368 |
swrappers = swrappers, |
|
369 |
uwrappers = uwrappers, |
|
370 |
haz_netpair = haz_netpair, |
|
371 |
dup_netpair = dup_netpair, |
|
12401 | 372 |
xtra_netpair = insert' 0 (nI,nE) ([th], []) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
373 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
374 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
375 |
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 376 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
377 |
th) = |
|
10736 | 378 |
if mem_thm (th, safeEs) then |
9938 | 379 |
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); |
380 |
cs) |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
381 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
382 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
15570 | 383 |
List.partition (fn rl => nprems_of rl=1) [th] |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
384 |
val nI = length safeIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
385 |
and nE = length safeEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
386 |
in warn_dup th cs; |
9938 | 387 |
CS{safeEs = th::safeEs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
388 |
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
9938 | 389 |
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
390 |
safeIs = safeIs, |
|
391 |
hazIs = hazIs, |
|
392 |
hazEs = hazEs, |
|
393 |
swrappers = swrappers, |
|
394 |
uwrappers = uwrappers, |
|
395 |
haz_netpair = haz_netpair, |
|
396 |
dup_netpair = dup_netpair, |
|
12401 | 397 |
xtra_netpair = insert' 0 (nI,nE) ([], [th]) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
398 |
end; |
0 | 399 |
|
15570 | 400 |
fun rev_foldl f (e, l) = Library.foldl f (e, rev l); |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
401 |
|
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
402 |
val op addSIs = rev_foldl addSI; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
403 |
val op addSEs = rev_foldl addSE; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
404 |
|
9938 | 405 |
fun cs addSDs ths = cs addSEs (map Data.make_elim ths); |
0 | 406 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
407 |
|
1800 | 408 |
(*** Hazardous (unsafe) rules ***) |
0 | 409 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
410 |
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 411 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
412 |
th)= |
|
10736 | 413 |
if mem_thm (th, hazIs) then |
9938 | 414 |
(warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); |
415 |
cs) |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
416 |
else |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
417 |
let val nI = length hazIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
418 |
and nE = length hazEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
419 |
in warn_dup th cs; |
9938 | 420 |
CS{hazIs = th::hazIs, |
421 |
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, |
|
422 |
dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, |
|
10736 | 423 |
safeIs = safeIs, |
9938 | 424 |
safeEs = safeEs, |
425 |
hazEs = hazEs, |
|
426 |
swrappers = swrappers, |
|
427 |
uwrappers = uwrappers, |
|
428 |
safe0_netpair = safe0_netpair, |
|
429 |
safep_netpair = safep_netpair, |
|
12401 | 430 |
xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
431 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
432 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
433 |
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 434 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
435 |
th) = |
|
10736 | 436 |
if mem_thm (th, hazEs) then |
9938 | 437 |
(warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); |
438 |
cs) |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
439 |
else |
10736 | 440 |
let val nI = length hazIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
441 |
and nE = length hazEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
442 |
in warn_dup th cs; |
9938 | 443 |
CS{hazEs = th::hazEs, |
444 |
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, |
|
445 |
dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, |
|
10736 | 446 |
safeIs = safeIs, |
9938 | 447 |
safeEs = safeEs, |
448 |
hazIs = hazIs, |
|
449 |
swrappers = swrappers, |
|
450 |
uwrappers = uwrappers, |
|
451 |
safe0_netpair = safe0_netpair, |
|
452 |
safep_netpair = safep_netpair, |
|
12401 | 453 |
xtra_netpair = insert' 1 (nI,nE) ([], [th]) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
454 |
end; |
0 | 455 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
456 |
val op addIs = rev_foldl addI; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
457 |
val op addEs = rev_foldl addE; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
458 |
|
9938 | 459 |
fun cs addDs ths = cs addEs (map Data.make_elim ths); |
0 | 460 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
461 |
|
10736 | 462 |
(*** Deletion of rules |
1800 | 463 |
Working out what to delete, requires repeating much of the code used |
9938 | 464 |
to insert. |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
465 |
Separate functions delSI, etc., are not exported; instead delrules |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
466 |
searches in all the lists and chooses the relevant delXX functions. |
1800 | 467 |
***) |
468 |
||
10736 | 469 |
fun delSI th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
470 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 471 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
472 |
if mem_thm (th, safeIs) then |
15570 | 473 |
let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th] |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
474 |
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
9938 | 475 |
safep_netpair = delete (safep_rls, []) safep_netpair, |
476 |
safeIs = rem_thm (safeIs,th), |
|
477 |
safeEs = safeEs, |
|
478 |
hazIs = hazIs, |
|
479 |
hazEs = hazEs, |
|
480 |
swrappers = swrappers, |
|
481 |
uwrappers = uwrappers, |
|
482 |
haz_netpair = haz_netpair, |
|
483 |
dup_netpair = dup_netpair, |
|
12401 | 484 |
xtra_netpair = delete' ([th], []) xtra_netpair} |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
485 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
486 |
else cs; |
1800 | 487 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
488 |
fun delSE th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
489 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 490 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
491 |
if mem_thm (th, safeEs) then |
15570 | 492 |
let val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th] |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
493 |
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
9938 | 494 |
safep_netpair = delete ([], safep_rls) safep_netpair, |
495 |
safeIs = safeIs, |
|
496 |
safeEs = rem_thm (safeEs,th), |
|
497 |
hazIs = hazIs, |
|
498 |
hazEs = hazEs, |
|
499 |
swrappers = swrappers, |
|
500 |
uwrappers = uwrappers, |
|
501 |
haz_netpair = haz_netpair, |
|
502 |
dup_netpair = dup_netpair, |
|
12401 | 503 |
xtra_netpair = delete' ([], [th]) xtra_netpair} |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
504 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
505 |
else cs; |
1800 | 506 |
|
507 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
508 |
fun delI th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
509 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 510 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
511 |
if mem_thm (th, hazIs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
512 |
CS{haz_netpair = delete ([th], []) haz_netpair, |
9938 | 513 |
dup_netpair = delete ([dup_intr th], []) dup_netpair, |
10736 | 514 |
safeIs = safeIs, |
9938 | 515 |
safeEs = safeEs, |
516 |
hazIs = rem_thm (hazIs,th), |
|
517 |
hazEs = hazEs, |
|
518 |
swrappers = swrappers, |
|
519 |
uwrappers = uwrappers, |
|
520 |
safe0_netpair = safe0_netpair, |
|
521 |
safep_netpair = safep_netpair, |
|
12401 | 522 |
xtra_netpair = delete' ([th], []) xtra_netpair} |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
523 |
else cs; |
1800 | 524 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
525 |
fun delE th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
526 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 527 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
528 |
if mem_thm (th, hazEs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
529 |
CS{haz_netpair = delete ([], [th]) haz_netpair, |
9938 | 530 |
dup_netpair = delete ([], [dup_elim th]) dup_netpair, |
10736 | 531 |
safeIs = safeIs, |
9938 | 532 |
safeEs = safeEs, |
533 |
hazIs = hazIs, |
|
534 |
hazEs = rem_thm (hazEs,th), |
|
535 |
swrappers = swrappers, |
|
536 |
uwrappers = uwrappers, |
|
537 |
safe0_netpair = safe0_netpair, |
|
538 |
safep_netpair = safep_netpair, |
|
12401 | 539 |
xtra_netpair = delete' ([], [th]) xtra_netpair} |
6955 | 540 |
else cs; |
541 |
||
1800 | 542 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
543 |
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
544 |
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = |
9938 | 545 |
let val th' = Data.make_elim th in |
546 |
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse |
|
547 |
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
548 |
mem_thm (th', safeEs) orelse mem_thm (th', hazEs) |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
549 |
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) |
9938 | 550 |
else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs) |
551 |
end; |
|
1800 | 552 |
|
15570 | 553 |
val op delrules = Library.foldl delrule; |
1800 | 554 |
|
555 |
||
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
556 |
(*** Modifying the wrapper tacticals ***) |
10736 | 557 |
fun update_swrappers |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
558 |
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
6955 | 559 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
560 |
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
561 |
swrappers = f swrappers, uwrappers = uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
562 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
6955 | 563 |
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
564 |
|
10736 | 565 |
fun update_uwrappers |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
566 |
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
6955 | 567 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
568 |
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
569 |
swrappers = swrappers, uwrappers = f uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
570 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
6955 | 571 |
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
572 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
573 |
|
4651 | 574 |
(*Add/replace a safe wrapper*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
575 |
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => |
9721 | 576 |
overwrite_warn (swrappers, new_swrapper) |
577 |
("Overwriting safe wrapper " ^ fst new_swrapper)); |
|
4651 | 578 |
|
579 |
(*Add/replace an unsafe wrapper*) |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
580 |
fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers => |
9721 | 581 |
overwrite_warn (uwrappers, new_uwrapper) |
9938 | 582 |
("Overwriting unsafe wrapper "^fst new_uwrapper)); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
583 |
|
4651 | 584 |
(*Remove a safe wrapper*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
585 |
fun cs delSWrapper name = update_swrappers cs (fn swrappers => |
15036 | 586 |
let val swrappers' = filter_out (equal name o #1) swrappers in |
587 |
if length swrappers <> length swrappers' then swrappers' |
|
588 |
else (warning ("No such safe wrapper in claset: "^ name); swrappers) |
|
589 |
end); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
590 |
|
4651 | 591 |
(*Remove an unsafe wrapper*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
592 |
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => |
15036 | 593 |
let val uwrappers' = filter_out (equal name o #1) uwrappers in |
594 |
if length uwrappers <> length uwrappers' then uwrappers' |
|
595 |
else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers) |
|
596 |
end); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
597 |
|
11168 | 598 |
(* compose a safe tactic alternatively before/after safe_step_tac *) |
10736 | 599 |
fun cs addSbefore (name, tac1) = |
5523 | 600 |
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
601 |
fun cs addSafter (name, tac2) = |
5523 | 602 |
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
603 |
|
11168 | 604 |
(*compose a tactic alternatively before/after the step tactic *) |
10736 | 605 |
fun cs addbefore (name, tac1) = |
5523 | 606 |
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
607 |
fun cs addafter (name, tac2) = |
5523 | 608 |
cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
609 |
|
10736 | 610 |
fun cs addD2 (name, thm) = |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
611 |
cs addafter (name, datac thm 1); |
10736 | 612 |
fun cs addE2 (name, thm) = |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
613 |
cs addafter (name, eatac thm 1); |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
614 |
fun cs addSD2 (name, thm) = |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
615 |
cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
616 |
fun cs addSE2 (name, thm) = |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
617 |
cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
618 |
|
1711 | 619 |
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. |
620 |
Merging the term nets may look more efficient, but the rather delicate |
|
621 |
treatment of priority might get muddled up.*) |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
622 |
fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
623 |
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) = |
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset
|
624 |
let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs) |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset
|
625 |
val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs) |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset
|
626 |
val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs) |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12401
diff
changeset
|
627 |
val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
628 |
val cs1 = cs addSIs safeIs' |
9938 | 629 |
addSEs safeEs' |
630 |
addIs hazIs' |
|
631 |
addEs hazEs' |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
632 |
val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
633 |
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); |
10736 | 634 |
in cs3 |
1711 | 635 |
end; |
636 |
||
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
637 |
|
1800 | 638 |
(**** Simple tactics for theorem proving ****) |
0 | 639 |
|
640 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
10736 | 641 |
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
4651 | 642 |
appSWrappers cs (FIRST' [ |
9938 | 643 |
eq_assume_tac, |
644 |
eq_mp_tac, |
|
645 |
bimatch_from_nets_tac safe0_netpair, |
|
646 |
FIRST' hyp_subst_tacs, |
|
647 |
bimatch_from_nets_tac safep_netpair]); |
|
0 | 648 |
|
5757 | 649 |
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) |
10736 | 650 |
fun safe_steps_tac cs = REPEAT_DETERM1 o |
9938 | 651 |
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); |
5757 | 652 |
|
0 | 653 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
5757 | 654 |
fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
655 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
656 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
657 |
(*** Clarify_tac: do safe steps without causing branching ***) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
658 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
659 |
fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
660 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
661 |
(*version of bimatch_from_nets_tac that only applies rules that |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
662 |
create precisely n subgoals.*) |
10736 | 663 |
fun n_bimatch_from_nets_tac n = |
15570 | 664 |
biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true; |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
665 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
666 |
fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
667 |
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
668 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
669 |
(*Two-way branching is allowed only if one of the branches immediately closes*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
670 |
fun bimatch2_tac netpair i = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
671 |
n_bimatch_from_nets_tac 2 netpair i THEN |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
672 |
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
673 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
674 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
10736 | 675 |
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
4651 | 676 |
appSWrappers cs (FIRST' [ |
9938 | 677 |
eq_assume_contr_tac, |
678 |
bimatch_from_nets_tac safe0_netpair, |
|
679 |
FIRST' hyp_subst_tacs, |
|
680 |
n_bimatch_from_nets_tac 1 safep_netpair, |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
681 |
bimatch2_tac safep_netpair]); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
682 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
683 |
fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
684 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
685 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
686 |
(*** Unsafe steps instantiate variables or lose information ***) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
687 |
|
4066 | 688 |
(*Backtracking is allowed among the various these unsafe ways of |
689 |
proving a subgoal. *) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
690 |
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
10736 | 691 |
assume_tac APPEND' |
692 |
contr_tac APPEND' |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
693 |
biresolve_from_nets_tac safe0_netpair; |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
694 |
|
4066 | 695 |
(*These unsafe steps could generate more subgoals.*) |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
696 |
fun instp_step_tac (CS{safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
697 |
biresolve_from_nets_tac safep_netpair; |
0 | 698 |
|
699 |
(*These steps could instantiate variables and are therefore unsafe.*) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
700 |
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; |
0 | 701 |
|
10736 | 702 |
fun haz_step_tac (CS{haz_netpair,...}) = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
703 |
biresolve_from_nets_tac haz_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
704 |
|
0 | 705 |
(*Single step for the prover. FAILS unless it makes progress. *) |
10736 | 706 |
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs |
9938 | 707 |
(inst_step_tac cs ORELSE' haz_step_tac cs) i; |
0 | 708 |
|
709 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
710 |
allows backtracking from "safe" rules to "unsafe" rules here.*) |
|
10736 | 711 |
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs |
9938 | 712 |
(inst_step_tac cs APPEND' haz_step_tac cs) i; |
0 | 713 |
|
1800 | 714 |
(**** The following tactics all fail unless they solve one goal ****) |
0 | 715 |
|
716 |
(*Dumb but fast*) |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
717 |
fun fast_tac cs = |
11754 | 718 |
ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
0 | 719 |
|
720 |
(*Slower but smarter than fast_tac*) |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
721 |
fun best_tac cs = |
11754 | 722 |
ObjectLogic.atomize_tac THEN' |
0 | 723 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); |
724 |
||
9402 | 725 |
(*even a bit smarter than best_tac*) |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
726 |
fun first_best_tac cs = |
11754 | 727 |
ObjectLogic.atomize_tac THEN' |
9402 | 728 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); |
729 |
||
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
730 |
fun slow_tac cs = |
11754 | 731 |
ObjectLogic.atomize_tac THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
732 |
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
0 | 733 |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
734 |
fun slow_best_tac cs = |
11754 | 735 |
ObjectLogic.atomize_tac THEN' |
0 | 736 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
737 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
738 |
|
10736 | 739 |
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) |
740 |
val weight_ASTAR = ref 5; |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
741 |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
742 |
fun astar_tac cs = |
11754 | 743 |
ObjectLogic.atomize_tac THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
744 |
SELECT_GOAL |
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
745 |
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev) |
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
746 |
(step_tac cs 1)); |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
747 |
|
10736 | 748 |
fun slow_astar_tac cs = |
11754 | 749 |
ObjectLogic.atomize_tac THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
750 |
SELECT_GOAL |
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
751 |
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev) |
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
752 |
(slow_step_tac cs 1)); |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
753 |
|
1800 | 754 |
(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
755 |
of much experimentation! Changing APPEND to ORELSE below would prove |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
756 |
easy theorems faster, but loses completeness -- and many of the harder |
1800 | 757 |
theorems such as 43. ****) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
758 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
759 |
(*Non-deterministic! Could always expand the first unsafe connective. |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
760 |
That's hard to implement and did not perform better in experiments, due to |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
761 |
greater search depth required.*) |
10736 | 762 |
fun dup_step_tac (cs as (CS{dup_netpair,...})) = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
763 |
biresolve_from_nets_tac dup_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
764 |
|
5523 | 765 |
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) |
5757 | 766 |
local |
10736 | 767 |
fun slow_step_tac' cs = appWrappers cs |
9938 | 768 |
(instp_step_tac cs APPEND' dup_step_tac cs); |
10736 | 769 |
in fun depth_tac cs m i state = SELECT_GOAL |
770 |
(safe_steps_tac cs 1 THEN_ELSE |
|
9938 | 771 |
(DEPTH_SOLVE (depth_tac cs m 1), |
772 |
inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac |
|
773 |
(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)) |
|
5757 | 774 |
)) i state; |
775 |
end; |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
776 |
|
10736 | 777 |
(*Search, with depth bound m. |
2173 | 778 |
This is the "entry point", which does safe inferences first.*) |
10736 | 779 |
fun safe_depth_tac cs m = |
780 |
SUBGOAL |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
781 |
(fn (prem,i) => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
782 |
let val deti = |
9938 | 783 |
(*No Vars in the goal? No need to backtrack between goals.*) |
784 |
case term_vars prem of |
|
10736 | 785 |
[] => DETERM |
9938 | 786 |
| _::_ => I |
10736 | 787 |
in SELECT_GOAL (TRY (safe_tac cs) THEN |
9938 | 788 |
DEPTH_SOLVE (deti (depth_tac cs m 1))) i |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
789 |
end); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
790 |
|
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
791 |
fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
792 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
793 |
|
1724 | 794 |
|
15036 | 795 |
(** context dependent claset components **) |
796 |
||
797 |
datatype context_cs = ContextCS of |
|
798 |
{swrappers: (string * (Proof.context -> wrapper)) list, |
|
799 |
uwrappers: (string * (Proof.context -> wrapper)) list}; |
|
800 |
||
801 |
fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) = |
|
802 |
let |
|
803 |
fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt)); |
|
804 |
in |
|
805 |
cs |> fold_rev (add_wrapper (op addSWrapper)) swrappers |
|
806 |
|> fold_rev (add_wrapper (op addWrapper)) uwrappers |
|
807 |
end; |
|
808 |
||
809 |
fun make_context_cs (swrappers, uwrappers) = |
|
810 |
ContextCS {swrappers = swrappers, uwrappers = uwrappers}; |
|
811 |
||
812 |
val empty_context_cs = make_context_cs ([], []); |
|
813 |
||
814 |
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = |
|
815 |
let |
|
816 |
val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1; |
|
817 |
val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2; |
|
818 |
||
819 |
val swrappers' = merge_alists swrappers1 swrappers2; |
|
820 |
val uwrappers' = merge_alists uwrappers1 uwrappers2; |
|
821 |
in make_context_cs (swrappers', uwrappers') end; |
|
822 |
||
823 |
||
824 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
825 |
(** claset theory data **) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
826 |
|
7354 | 827 |
(* theory data kind 'Provers/claset' *) |
1724 | 828 |
|
7354 | 829 |
structure GlobalClasetArgs = |
830 |
struct |
|
831 |
val name = "Provers/claset"; |
|
15036 | 832 |
type T = claset ref * context_cs; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
833 |
|
15036 | 834 |
val empty = (ref empty_cs, empty_context_cs); |
835 |
fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; (*create new reference!*) |
|
6556 | 836 |
val prep_ext = copy; |
15036 | 837 |
fun merge ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) = |
838 |
(ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2)); |
|
839 |
fun print _ (ref cs, _) = print_cs cs; |
|
7354 | 840 |
end; |
1724 | 841 |
|
7354 | 842 |
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); |
843 |
val print_claset = GlobalClaset.print; |
|
15036 | 844 |
val claset_ref_of_sg = #1 o GlobalClaset.get_sg; |
845 |
val claset_ref_of = #1 o GlobalClaset.get; |
|
846 |
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; |
|
847 |
||
848 |
fun map_context_cs f = GlobalClaset.map (apsnd |
|
849 |
(fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers)))); |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
850 |
|
1724 | 851 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
852 |
(* access claset *) |
1724 | 853 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
854 |
val claset_of_sg = ! o claset_ref_of_sg; |
6391 | 855 |
val claset_of = claset_of_sg o Theory.sign_of; |
1800 | 856 |
|
6391 | 857 |
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; |
858 |
fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state; |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
859 |
|
5028 | 860 |
val claset = claset_of o Context.the_context; |
6391 | 861 |
val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
862 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
863 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
864 |
(* change claset *) |
1800 | 865 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
866 |
fun change_claset f x = claset_ref () := (f (claset (), x)); |
1724 | 867 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
868 |
val AddDs = change_claset (op addDs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
869 |
val AddEs = change_claset (op addEs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
870 |
val AddIs = change_claset (op addIs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
871 |
val AddSDs = change_claset (op addSDs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
872 |
val AddSEs = change_claset (op addSEs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
873 |
val AddSIs = change_claset (op addSIs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
874 |
val Delrules = change_claset (op delrules); |
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
875 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
876 |
|
15036 | 877 |
(* context dependent components *) |
878 |
||
879 |
fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper])); |
|
880 |
fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1))); |
|
881 |
||
882 |
fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper])); |
|
883 |
fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1))); |
|
884 |
||
885 |
||
5841 | 886 |
(* proof data kind 'Provers/claset' *) |
887 |
||
888 |
structure LocalClasetArgs = |
|
889 |
struct |
|
890 |
val name = "Provers/claset"; |
|
891 |
type T = claset; |
|
892 |
val init = claset_of; |
|
15036 | 893 |
fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt)); |
5841 | 894 |
end; |
895 |
||
896 |
structure LocalClaset = ProofDataFun(LocalClasetArgs); |
|
897 |
val print_local_claset = LocalClaset.print; |
|
898 |
val get_local_claset = LocalClaset.get; |
|
899 |
val put_local_claset = LocalClaset.put; |
|
900 |
||
15036 | 901 |
fun local_claset_of ctxt = |
902 |
context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); |
|
903 |
||
15452 | 904 |
(* added for delta_claset: 06/01/05 *) |
905 |
||
906 |
structure DeltaClasetArgs = |
|
907 |
struct |
|
908 |
val name = "delta_claset"; |
|
909 |
type T = claset; |
|
910 |
val empty = empty_cs; |
|
911 |
end; |
|
912 |
||
913 |
structure DeltaClaset = DeltaDataFun(DeltaClasetArgs); |
|
914 |
val get_delta_claset = DeltaClaset.get; |
|
915 |
val put_delta_claset = DeltaClaset.put; |
|
916 |
||
917 |
val get_new_thm_id = ProofContext.get_delta_count_incr; |
|
918 |
||
919 |
||
920 |
local |
|
921 |
fun rename_thm' (ctxt,thm) = |
|
922 |
let val new_id = get_new_thm_id ctxt |
|
923 |
val new_name = "anon_" ^ (string_of_int new_id) |
|
924 |
in |
|
925 |
Thm.name_thm(new_name,thm) |
|
926 |
end; |
|
927 |
||
928 |
in |
|
929 |
||
930 |
(* rename thm if call_atp is true *) |
|
931 |
fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm; |
|
932 |
||
933 |
end |
|
934 |
||
5841 | 935 |
|
5885 | 936 |
(* attributes *) |
937 |
||
938 |
fun change_global_cs f (thy, th) = |
|
939 |
let val r = claset_ref_of thy |
|
6096 | 940 |
in r := f (! r, [th]); (thy, th) end; |
5885 | 941 |
|
942 |
fun change_local_cs f (ctxt, th) = |
|
6096 | 943 |
let val cs = f (get_local_claset ctxt, [th]) |
5885 | 944 |
in (put_local_claset cs ctxt, th) end; |
945 |
||
946 |
val safe_dest_global = change_global_cs (op addSDs); |
|
947 |
val safe_elim_global = change_global_cs (op addSEs); |
|
948 |
val safe_intro_global = change_global_cs (op addSIs); |
|
6955 | 949 |
val haz_dest_global = change_global_cs (op addDs); |
950 |
val haz_elim_global = change_global_cs (op addEs); |
|
951 |
val haz_intro_global = change_global_cs (op addIs); |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
952 |
val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; |
5885 | 953 |
|
15452 | 954 |
|
955 |
(* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *) |
|
956 |
fun safe_dest_local (ctxt,th) = |
|
957 |
let val thm_name = Thm.name_of_thm th |
|
958 |
val th' = if (thm_name = "") then rename_thm (ctxt,th) else th |
|
959 |
val delta_cs = get_delta_claset ctxt |
|
960 |
val new_dcs = delta_cs addSDs [th'] |
|
961 |
val ctxt' = put_delta_claset new_dcs ctxt |
|
962 |
in |
|
963 |
change_local_cs (op addSDs) (ctxt',th) |
|
964 |
end; |
|
965 |
||
966 |
fun safe_elim_local (ctxt, th)= |
|
967 |
let val thm_name = Thm.name_of_thm th |
|
968 |
val th' = if (thm_name = "") then rename_thm (ctxt,th) else th |
|
969 |
val delta_cs = get_delta_claset ctxt |
|
970 |
val new_dcs = delta_cs addSEs [th'] |
|
971 |
val ctxt' = put_delta_claset new_dcs ctxt |
|
972 |
in |
|
973 |
change_local_cs (op addSEs) (ctxt',th) |
|
974 |
end; |
|
975 |
||
976 |
fun safe_intro_local (ctxt, th) = |
|
977 |
let val thm_name = Thm.name_of_thm th |
|
978 |
val th' = if (thm_name = "") then rename_thm (ctxt,th) else th |
|
979 |
val delta_cs = get_delta_claset ctxt |
|
980 |
val new_dcs = delta_cs addSIs [th'] |
|
981 |
val ctxt' = put_delta_claset new_dcs ctxt |
|
982 |
in |
|
983 |
change_local_cs (op addSIs) (ctxt',th) |
|
984 |
end; |
|
985 |
||
986 |
fun haz_dest_local (ctxt, th)= |
|
987 |
let val thm_name = Thm.name_of_thm th |
|
988 |
val th' = if (thm_name = "") then rename_thm (ctxt,th)else th |
|
989 |
val delta_cs = get_delta_claset ctxt |
|
990 |
val new_dcs = delta_cs addDs [th'] |
|
991 |
val ctxt' = put_delta_claset new_dcs ctxt |
|
992 |
in |
|
993 |
change_local_cs (op addDs) (ctxt',th) |
|
994 |
end; |
|
995 |
||
996 |
fun haz_elim_local (ctxt,th) = |
|
997 |
let val thm_name = Thm.name_of_thm th |
|
998 |
val th' = if (thm_name = "") then rename_thm (ctxt,th) else th |
|
999 |
val delta_cs = get_delta_claset ctxt |
|
1000 |
val new_dcs = delta_cs addEs [th'] |
|
1001 |
val ctxt' = put_delta_claset new_dcs ctxt |
|
1002 |
in |
|
1003 |
change_local_cs (op addEs) (ctxt',th) |
|
1004 |
end; |
|
1005 |
||
1006 |
fun haz_intro_local (ctxt,th) = |
|
1007 |
let val thm_name = Thm.name_of_thm th |
|
1008 |
val th' = if (thm_name = "") then rename_thm (ctxt,th) else th |
|
1009 |
val delta_cs = get_delta_claset ctxt |
|
1010 |
val new_dcs = delta_cs addIs [th'] |
|
1011 |
val ctxt' = put_delta_claset new_dcs ctxt |
|
1012 |
in |
|
1013 |
change_local_cs (op addIs) (ctxt',th) |
|
1014 |
end; |
|
1015 |
||
1016 |
||
1017 |
(* when a rule is removed from local_claset, it is not removed from delta_claset in ProofContext.context. But this is unlikely to happen. *) |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1018 |
val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; |
5885 | 1019 |
|
1020 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1021 |
(* tactics referring to the implicit claset *) |
1800 | 1022 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1023 |
(*the abstraction over the proof state delays the dereferencing*) |
9938 | 1024 |
fun Safe_tac st = safe_tac (claset()) st; |
1025 |
fun Safe_step_tac i st = safe_step_tac (claset()) i st; |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1026 |
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; |
9938 | 1027 |
fun Clarify_tac i st = clarify_tac (claset()) i st; |
1028 |
fun Step_tac i st = step_tac (claset()) i st; |
|
1029 |
fun Fast_tac i st = fast_tac (claset()) i st; |
|
1030 |
fun Best_tac i st = best_tac (claset()) i st; |
|
1031 |
fun Slow_tac i st = slow_tac (claset()) i st; |
|
1032 |
fun Slow_best_tac i st = slow_best_tac (claset()) i st; |
|
1033 |
fun Deepen_tac m = deepen_tac (claset()) m; |
|
2066 | 1034 |
|
1800 | 1035 |
|
10736 | 1036 |
end; |
5841 | 1037 |
|
1038 |
||
1039 |
||
5885 | 1040 |
(** concrete syntax of attributes **) |
5841 | 1041 |
|
1042 |
(* add / del rules *) |
|
1043 |
||
1044 |
val introN = "intro"; |
|
1045 |
val elimN = "elim"; |
|
1046 |
val destN = "dest"; |
|
9938 | 1047 |
val ruleN = "rule"; |
5841 | 1048 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1049 |
fun add_rule xtra haz safe = Attrib.syntax |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1050 |
(Scan.lift (Args.query |-- Scan.option Args.nat >> xtra || Args.bang >> K safe || |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1051 |
Scan.succeed haz)); |
5841 | 1052 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1053 |
fun del_rule att = Attrib.syntax (Scan.lift Args.del >> K att); |
5841 | 1054 |
|
1055 |
||
1056 |
(* setup_attrs *) |
|
1057 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9938
diff
changeset
|
1058 |
fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x; |
9184 | 1059 |
|
5841 | 1060 |
val setup_attrs = Attrib.add_attributes |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9938
diff
changeset
|
1061 |
[("elim_format", (elim_format, elim_format), |
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9938
diff
changeset
|
1062 |
"destruct rule turned into elimination rule format (classical)"), |
12401 | 1063 |
("swapped", (swapped, swapped), "classical swap of introduction rule"), |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1064 |
(destN, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1065 |
(add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1066 |
add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1067 |
"declaration of destruction rule"), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1068 |
(elimN, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1069 |
(add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1070 |
add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1071 |
"declaration of elimination rule"), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1072 |
(introN, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1073 |
(add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global, |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1074 |
add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1075 |
"declaration of introduction rule"), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1076 |
(ruleN, (del_rule rule_del_global, del_rule rule_del_local), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1077 |
"remove declaration of intro/elim/dest rule")]; |
5841 | 1078 |
|
1079 |
||
1080 |
||
7230 | 1081 |
(** proof methods **) |
1082 |
||
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset
|
1083 |
fun METHOD_CLASET tac ctxt = |
15036 | 1084 |
Method.METHOD (tac ctxt (local_claset_of ctxt)); |
5841 | 1085 |
|
8098 | 1086 |
fun METHOD_CLASET' tac ctxt = |
15036 | 1087 |
Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); |
7230 | 1088 |
|
1089 |
||
1090 |
local |
|
1091 |
||
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1092 |
fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => |
5841 | 1093 |
let |
12401 | 1094 |
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; |
1095 |
val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair; |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1096 |
val rules = rules1 @ rules2 @ rules3 @ rules4; |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1097 |
val ruleq = Method.multi_resolves facts rules; |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1098 |
in |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1099 |
Method.trace ctxt rules; |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1100 |
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1101 |
end); |
5841 | 1102 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1103 |
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts |
10394 | 1104 |
| rule_tac rules _ _ facts = Method.rule_tac rules facts; |
7281 | 1105 |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
1106 |
fun default_tac rules ctxt cs facts = |
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset
|
1107 |
HEADGOAL (rule_tac rules ctxt cs facts) ORELSE |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
1108 |
AxClass.default_intro_classes_tac facts; |
10309 | 1109 |
|
7230 | 1110 |
in |
7281 | 1111 |
val rule = METHOD_CLASET' o rule_tac; |
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset
|
1112 |
val default = METHOD_CLASET o default_tac; |
7230 | 1113 |
end; |
5841 | 1114 |
|
1115 |
||
7230 | 1116 |
(* contradiction method *) |
6502 | 1117 |
|
7425 | 1118 |
val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl]; |
6502 | 1119 |
|
1120 |
||
1121 |
(* automatic methods *) |
|
5841 | 1122 |
|
5927 | 1123 |
val cla_modifiers = |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1124 |
[Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest_local): Method.modifier), |
10034 | 1125 |
Args.$$$ destN -- Args.colon >> K (I, haz_dest_local), |
1126 |
Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local), |
|
1127 |
Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local), |
|
1128 |
Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local), |
|
1129 |
Args.$$$ introN -- Args.colon >> K (I, haz_intro_local), |
|
1130 |
Args.del -- Args.colon >> K (I, rule_del_local)]; |
|
5927 | 1131 |
|
7559 | 1132 |
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => |
15036 | 1133 |
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); |
7132 | 1134 |
|
7559 | 1135 |
fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => |
15036 | 1136 |
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt))); |
5841 | 1137 |
|
7559 | 1138 |
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; |
1139 |
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; |
|
5841 | 1140 |
|
1141 |
||
1142 |
||
1143 |
(** setup_methods **) |
|
1144 |
||
1145 |
val setup_methods = Method.add_methods |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1146 |
[("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"), |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
1147 |
("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"), |
6502 | 1148 |
("contradiction", Method.no_args contradiction, "proof by contradiction"), |
10821 | 1149 |
("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"), |
7004 | 1150 |
("fast", cla_method' fast_tac, "classical prover (depth-first)"), |
9806 | 1151 |
("slow", cla_method' slow_tac, "classical prover (slow depth-first)"), |
9773 | 1152 |
("best", cla_method' best_tac, "classical prover (best-first)"), |
10821 | 1153 |
("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")]; |
5841 | 1154 |
|
1155 |
||
1156 |
||
1157 |
(** theory setup **) |
|
1158 |
||
7354 | 1159 |
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; |
5841 | 1160 |
|
1161 |
||
8667 | 1162 |
|
1163 |
(** outer syntax **) |
|
1164 |
||
1165 |
val print_clasetP = |
|
1166 |
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" |
|
1167 |
OuterSyntax.Keyword.diag |
|
9513 | 1168 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep |
9010 | 1169 |
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); |
8667 | 1170 |
|
1171 |
val _ = OuterSyntax.add_parsers [print_clasetP]; |
|
1172 |
||
1173 |
||
5841 | 1174 |
end; |