author | wenzelm |
Tue, 17 Mar 2009 14:09:20 +0100 | |
changeset 30558 | 2ef9892114fd |
parent 30541 | 9f168bdc468a |
child 30609 | 983e8b6e4e69 |
permissions | -rw-r--r-- |
9938 | 1 |
(* Title: Provers/classical.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
0 | 3 |
|
4 |
Theorem prover for classical reasoning, including predicate calculus, set |
|
5 |
theory, etc. |
|
6 |
||
9563
216d053992a5
fixed classification of rules in atts and modifiers (final!?);
wenzelm
parents:
9513
diff
changeset
|
7 |
Rules must be classified as intro, elim, safe, hazardous (unsafe). |
0 | 8 |
|
9 |
A rule is unsafe unless it can be applied blindly without harmful results. |
|
10 |
For a rule to be safe, its premises and conclusion should be logically |
|
11 |
equivalent. There should be no variables in the premises that are not in |
|
12 |
the conclusion. |
|
13 |
*) |
|
14 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
15 |
(*higher precedence than := facilitates use of references*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
16 |
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules |
4651 | 17 |
addSWrapper delSWrapper addWrapper delWrapper |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
18 |
addSbefore addSafter addbefore addafter |
5523 | 19 |
addD2 addE2 addSD2 addSE2; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
20 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
21 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
22 |
(*should be a type abbreviation in signature CLASSICAL*) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
23 |
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; |
4651 | 24 |
type wrapper = (int -> tactic) -> (int -> tactic); |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
25 |
|
0 | 26 |
signature CLASSICAL_DATA = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
27 |
sig |
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
28 |
val imp_elim : thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) |
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
29 |
val not_elim : thm (* ~P ==> P ==> R *) |
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
30 |
val swap : thm (* ~ P ==> (~ R ==> P) ==> R *) |
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
31 |
val classical : thm (* (~ P ==> P) ==> P *) |
9938 | 32 |
val sizef : thm -> int (* size function for BEST_FIRST *) |
0 | 33 |
val hyp_subst_tacs: (int -> tactic) list |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
34 |
end; |
0 | 35 |
|
5841 | 36 |
signature BASIC_CLASSICAL = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
37 |
sig |
0 | 38 |
type claset |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
39 |
val empty_cs: claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
40 |
val print_cs: claset -> unit |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
41 |
val rep_cs: |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
42 |
claset -> {safeIs: thm list, safeEs: thm list, |
9938 | 43 |
hazIs: thm list, hazEs: thm list, |
10736 | 44 |
swrappers: (string * wrapper) list, |
9938 | 45 |
uwrappers: (string * wrapper) list, |
46 |
safe0_netpair: netpair, safep_netpair: netpair, |
|
12401 | 47 |
haz_netpair: netpair, dup_netpair: netpair, |
48 |
xtra_netpair: ContextRules.netpair} |
|
9938 | 49 |
val merge_cs : claset * claset -> claset |
50 |
val addDs : claset * thm list -> claset |
|
51 |
val addEs : claset * thm list -> claset |
|
52 |
val addIs : claset * thm list -> claset |
|
53 |
val addSDs : claset * thm list -> claset |
|
54 |
val addSEs : claset * thm list -> claset |
|
55 |
val addSIs : claset * thm list -> claset |
|
56 |
val delrules : claset * thm list -> claset |
|
57 |
val addSWrapper : claset * (string * wrapper) -> claset |
|
58 |
val delSWrapper : claset * string -> claset |
|
59 |
val addWrapper : claset * (string * wrapper) -> claset |
|
60 |
val delWrapper : claset * string -> claset |
|
61 |
val addSbefore : claset * (string * (int -> tactic)) -> claset |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
62 |
val addSafter : claset * (string * (int -> tactic)) -> claset |
9938 | 63 |
val addbefore : claset * (string * (int -> tactic)) -> claset |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
64 |
val addafter : claset * (string * (int -> tactic)) -> claset |
5523 | 65 |
val addD2 : claset * (string * thm) -> claset |
66 |
val addE2 : claset * (string * thm) -> claset |
|
67 |
val addSD2 : claset * (string * thm) -> claset |
|
68 |
val addSE2 : claset * (string * thm) -> claset |
|
9938 | 69 |
val appSWrappers : claset -> wrapper |
70 |
val appWrappers : claset -> wrapper |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
71 |
|
17880 | 72 |
val change_claset: (claset -> claset) -> unit |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
73 |
val claset_of: theory -> claset |
17880 | 74 |
val claset: unit -> claset |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
75 |
val CLASET: (claset -> tactic) -> tactic |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
76 |
val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic |
15036 | 77 |
val local_claset_of : Proof.context -> claset |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
78 |
|
9938 | 79 |
val fast_tac : claset -> int -> tactic |
80 |
val slow_tac : claset -> int -> tactic |
|
81 |
val weight_ASTAR : int ref |
|
82 |
val astar_tac : claset -> int -> tactic |
|
83 |
val slow_astar_tac : claset -> int -> tactic |
|
84 |
val best_tac : claset -> int -> tactic |
|
85 |
val first_best_tac : claset -> int -> tactic |
|
86 |
val slow_best_tac : claset -> int -> tactic |
|
87 |
val depth_tac : claset -> int -> int -> tactic |
|
88 |
val deepen_tac : claset -> int -> int -> tactic |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
89 |
|
9938 | 90 |
val contr_tac : int -> tactic |
91 |
val dup_elim : thm -> thm |
|
92 |
val dup_intr : thm -> thm |
|
93 |
val dup_step_tac : claset -> int -> tactic |
|
94 |
val eq_mp_tac : int -> tactic |
|
95 |
val haz_step_tac : claset -> int -> tactic |
|
96 |
val joinrules : thm list * thm list -> (bool * thm) list |
|
97 |
val mp_tac : int -> tactic |
|
98 |
val safe_tac : claset -> tactic |
|
99 |
val safe_steps_tac : claset -> int -> tactic |
|
100 |
val safe_step_tac : claset -> int -> tactic |
|
101 |
val clarify_tac : claset -> int -> tactic |
|
102 |
val clarify_step_tac : claset -> int -> tactic |
|
103 |
val step_tac : claset -> int -> tactic |
|
104 |
val slow_step_tac : claset -> int -> tactic |
|
105 |
val swapify : thm list -> thm list |
|
106 |
val swap_res_tac : thm list -> int -> tactic |
|
107 |
val inst_step_tac : claset -> int -> tactic |
|
108 |
val inst0_step_tac : claset -> int -> tactic |
|
109 |
val instp_step_tac : claset -> int -> tactic |
|
1724 | 110 |
|
9938 | 111 |
val AddDs : thm list -> unit |
112 |
val AddEs : thm list -> unit |
|
113 |
val AddIs : thm list -> unit |
|
114 |
val AddSDs : thm list -> unit |
|
115 |
val AddSEs : thm list -> unit |
|
116 |
val AddSIs : thm list -> unit |
|
117 |
val Delrules : thm list -> unit |
|
118 |
val Safe_tac : tactic |
|
119 |
val Safe_step_tac : int -> tactic |
|
120 |
val Clarify_tac : int -> tactic |
|
121 |
val Clarify_step_tac : int -> tactic |
|
122 |
val Step_tac : int -> tactic |
|
123 |
val Fast_tac : int -> tactic |
|
124 |
val Best_tac : int -> tactic |
|
125 |
val Slow_tac : int -> tactic |
|
2066 | 126 |
val Slow_best_tac : int -> tactic |
9938 | 127 |
val Deepen_tac : int -> int -> tactic |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
128 |
end; |
1724 | 129 |
|
5841 | 130 |
signature CLASSICAL = |
131 |
sig |
|
132 |
include BASIC_CLASSICAL |
|
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
133 |
val classical_rule: thm -> thm |
15036 | 134 |
val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory |
135 |
val del_context_safe_wrapper: string -> theory -> theory |
|
136 |
val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory |
|
137 |
val del_context_unsafe_wrapper: string -> theory -> theory |
|
17880 | 138 |
val get_claset: theory -> claset |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
139 |
val map_claset: (claset -> claset) -> theory -> theory |
24021 | 140 |
val get_cs: Context.generic -> claset |
141 |
val map_cs: (claset -> claset) -> Context.generic -> Context.generic |
|
18728 | 142 |
val safe_dest: int option -> attribute |
143 |
val safe_elim: int option -> attribute |
|
144 |
val safe_intro: int option -> attribute |
|
145 |
val haz_dest: int option -> attribute |
|
146 |
val haz_elim: int option -> attribute |
|
147 |
val haz_intro: int option -> attribute |
|
148 |
val rule_del: attribute |
|
30513 | 149 |
val cla_modifiers: Method.modifier parser list |
7559 | 150 |
val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method |
151 |
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method |
|
30541 | 152 |
val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser |
153 |
val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser |
|
18708 | 154 |
val setup: theory -> theory |
5841 | 155 |
end; |
156 |
||
0 | 157 |
|
5927 | 158 |
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
0 | 159 |
struct |
160 |
||
7354 | 161 |
local open Data in |
0 | 162 |
|
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
163 |
(** classical elimination rules **) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
164 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
165 |
(* |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
166 |
Classical reasoning requires stronger elimination rules. For |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
167 |
instance, make_elim of Pure transforms the HOL rule injD into |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
168 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
169 |
[| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
170 |
|
26938 | 171 |
Such rules can cause fast_tac to fail and blast_tac to report "PROOF |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
172 |
FAILED"; classical_rule will strenthen this to |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
173 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
174 |
[| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
175 |
*) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
176 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
177 |
fun classical_rule rule = |
19257 | 178 |
if ObjectLogic.is_elim rule then |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
179 |
let |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
180 |
val rule' = rule RS classical; |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
181 |
val concl' = Thm.concl_of rule'; |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
182 |
fun redundant_hyp goal = |
19257 | 183 |
concl' aconv Logic.strip_assums_concl goal orelse |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
184 |
(case Logic.strip_assums_hyp goal of |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
185 |
hyp :: hyps => exists (fn t => t aconv hyp) hyps |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
186 |
| _ => false); |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
187 |
val rule'' = |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
188 |
rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
189 |
if i = 1 orelse redundant_hyp goal |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
190 |
then Tactic.etac thin_rl i |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
191 |
else all_tac)) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
192 |
|> Seq.hd |
21963 | 193 |
|> Drule.zero_var_indexes; |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset
|
194 |
in if Thm.equiv_thm (rule, rule'') then rule else rule'' end |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
195 |
else rule; |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
196 |
|
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
197 |
(*flatten nested meta connectives in prems*) |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
198 |
val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems); |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
199 |
|
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
200 |
|
1800 | 201 |
(*** Useful tactics for classical reasoning ***) |
0 | 202 |
|
10736 | 203 |
(*Prove goal that assumes both P and ~P. |
4392 | 204 |
No backtracking if it finds an equal assumption. Perhaps should call |
205 |
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) |
|
10736 | 206 |
val contr_tac = eresolve_tac [not_elim] THEN' |
4392 | 207 |
(eq_assume_tac ORELSE' assume_tac); |
0 | 208 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
209 |
(*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
|
210 |
Could do the same thing for P<->Q and P... *) |
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
211 |
fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i THEN assume_tac i; |
0 | 212 |
|
213 |
(*Like mp_tac but instantiates no variables*) |
|
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
214 |
fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i THEN eq_assume_tac i; |
0 | 215 |
|
216 |
(*Creates rules to eliminate ~A, from rules to introduce A*) |
|
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
217 |
fun swapify intrs = intrs RLN (2, [Data.swap]); |
30528 | 218 |
val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap)); |
0 | 219 |
|
220 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
221 |
trying rules in order. *) |
|
10736 | 222 |
fun swap_res_tac rls = |
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
wenzelm
parents:
24867
diff
changeset
|
223 |
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls |
10736 | 224 |
in assume_tac ORELSE' |
225 |
contr_tac ORELSE' |
|
30190 | 226 |
biresolve_tac (List.foldr addrl [] rls) |
0 | 227 |
end; |
228 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
229 |
(*Duplication of hazardous rules, for complete provers*) |
2689
6d3d893453de
dup_intr & dup_elim no longer call standard -- this
paulson
parents:
2630
diff
changeset
|
230 |
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
|
231 |
|
6967 | 232 |
fun dup_elim th = |
13525 | 233 |
rule_by_tactic (TRYALL (etac revcut_rl)) |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
234 |
((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
235 |
|
1800 | 236 |
(**** Classical rule sets ****) |
0 | 237 |
|
238 |
datatype claset = |
|
12401 | 239 |
CS of {safeIs : thm list, (*safe introduction rules*) |
240 |
safeEs : thm list, (*safe elimination rules*) |
|
241 |
hazIs : thm list, (*unsafe introduction rules*) |
|
242 |
hazEs : thm list, (*unsafe elimination rules*) |
|
243 |
swrappers : (string * wrapper) list, (*for transforming safe_step_tac*) |
|
9938 | 244 |
uwrappers : (string * wrapper) list, (*for transforming step_tac*) |
12401 | 245 |
safe0_netpair : netpair, (*nets for trivial cases*) |
246 |
safep_netpair : netpair, (*nets for >0 subgoals*) |
|
247 |
haz_netpair : netpair, (*nets for unsafe rules*) |
|
248 |
dup_netpair : netpair, (*nets for duplication*) |
|
249 |
xtra_netpair : ContextRules.netpair}; (*nets for extra rules*) |
|
0 | 250 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
251 |
(*Desired invariants are |
9938 | 252 |
safe0_netpair = build safe0_brls, |
253 |
safep_netpair = build safep_brls, |
|
254 |
haz_netpair = build (joinrules(hazIs, hazEs)), |
|
10736 | 255 |
dup_netpair = build (joinrules(map dup_intr hazIs, |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
256 |
map dup_elim hazEs)) |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
257 |
|
10736 | 258 |
where build = build_netpair(Net.empty,Net.empty), |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
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
|
263 |
*) |
0 | 264 |
|
6502 | 265 |
val empty_netpair = (Net.empty, Net.empty); |
266 |
||
10736 | 267 |
val empty_cs = |
9938 | 268 |
CS{safeIs = [], |
269 |
safeEs = [], |
|
270 |
hazIs = [], |
|
271 |
hazEs = [], |
|
4651 | 272 |
swrappers = [], |
273 |
uwrappers = [], |
|
6502 | 274 |
safe0_netpair = empty_netpair, |
275 |
safep_netpair = empty_netpair, |
|
276 |
haz_netpair = empty_netpair, |
|
6955 | 277 |
dup_netpair = empty_netpair, |
278 |
xtra_netpair = empty_netpair}; |
|
0 | 279 |
|
15036 | 280 |
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) = |
3546 | 281 |
let val pretty_thms = map Display.pretty_thm in |
9760 | 282 |
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), |
283 |
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), |
|
284 |
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), |
|
15036 | 285 |
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), |
286 |
Pretty.strs ("safe wrappers:" :: map #1 swrappers), |
|
287 |
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] |
|
8727 | 288 |
|> Pretty.chunks |> Pretty.writeln |
3546 | 289 |
end; |
0 | 290 |
|
4653 | 291 |
fun rep_cs (CS args) = args; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
292 |
|
22674 | 293 |
fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers; |
294 |
fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers; |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
295 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
296 |
|
1800 | 297 |
(*** Adding (un)safe introduction or elimination rules. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
298 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
299 |
In case of overlap, new rules are tried BEFORE old ones!! |
1800 | 300 |
***) |
0 | 301 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
302 |
(*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
|
303 |
assumptions. Pairs elim rules with true. *) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
304 |
fun joinrules (intrs, elims) = |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
305 |
(map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs; |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
306 |
|
12401 | 307 |
fun joinrules' (intrs, elims) = |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
308 |
map (pair true) elims @ map (pair false) intrs; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
309 |
|
10736 | 310 |
(*Priority: prefer rules with fewest subgoals, |
1231 | 311 |
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
|
312 |
fun tag_brls k [] = [] |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
313 |
| tag_brls k (brl::brls) = |
10736 | 314 |
(1000000*subgoals_of_brl brl + k, brl) :: |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
315 |
tag_brls (k+1) brls; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
316 |
|
12401 | 317 |
fun tag_brls' _ _ [] = [] |
318 |
| tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; |
|
10736 | 319 |
|
23178 | 320 |
fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
321 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
322 |
(*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
|
323 |
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
|
324 |
new insertions the lowest priority.*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
325 |
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; |
12401 | 326 |
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
|
327 |
|
23178 | 328 |
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; |
12362 | 329 |
fun delete x = delete_tagged_list (joinrules x); |
12401 | 330 |
fun delete' x = delete_tagged_list (joinrules' x); |
1800 | 331 |
|
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset
|
332 |
val mem_thm = member Thm.eq_thm_prop |
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset
|
333 |
and rem_thm = remove Thm.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
|
334 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
335 |
(*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
|
336 |
is still allowed.*) |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
337 |
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = |
18691 | 338 |
if mem_thm safeIs th then |
26928 | 339 |
warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th) |
18691 | 340 |
else if mem_thm safeEs th then |
26928 | 341 |
warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th) |
18691 | 342 |
else if mem_thm hazIs th then |
26928 | 343 |
warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th) |
18691 | 344 |
else if mem_thm hazEs th then |
26928 | 345 |
warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
346 |
else (); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
347 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
348 |
|
1800 | 349 |
(*** Safe rules ***) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
350 |
|
18691 | 351 |
fun addSI w th |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
352 |
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
353 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
18691 | 354 |
if mem_thm safeIs th then |
26928 | 355 |
(warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th); |
9938 | 356 |
cs) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
357 |
else |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
358 |
let val th' = flat_rule th |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
359 |
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
360 |
List.partition Thm.no_prems [th'] |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
361 |
val nI = length safeIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
362 |
and nE = length safeEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
363 |
in warn_dup th cs; |
9938 | 364 |
CS{safeIs = th::safeIs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
365 |
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
9938 | 366 |
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
367 |
safeEs = safeEs, |
|
368 |
hazIs = hazIs, |
|
369 |
hazEs = hazEs, |
|
370 |
swrappers = swrappers, |
|
371 |
uwrappers = uwrappers, |
|
372 |
haz_netpair = haz_netpair, |
|
373 |
dup_netpair = dup_netpair, |
|
18691 | 374 |
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
375 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
376 |
|
18691 | 377 |
fun addSE w th |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
378 |
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
379 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
18691 | 380 |
if mem_thm safeEs th then |
26928 | 381 |
(warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th); |
9938 | 382 |
cs) |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
383 |
else if has_fewer_prems 1 th then |
26928 | 384 |
error("Ill-formed elimination rule\n" ^ Display.string_of_thm th) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
385 |
else |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
386 |
let |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
387 |
val th' = classical_rule (flat_rule th) |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
388 |
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
389 |
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
|
390 |
val nI = length safeIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
391 |
and nE = length safeEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
392 |
in warn_dup th cs; |
9938 | 393 |
CS{safeEs = th::safeEs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
394 |
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
9938 | 395 |
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
396 |
safeIs = safeIs, |
|
397 |
hazIs = hazIs, |
|
398 |
hazEs = hazEs, |
|
399 |
swrappers = swrappers, |
|
400 |
uwrappers = uwrappers, |
|
401 |
haz_netpair = haz_netpair, |
|
402 |
dup_netpair = dup_netpair, |
|
18691 | 403 |
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
404 |
end; |
0 | 405 |
|
18691 | 406 |
fun cs addSIs ths = fold_rev (addSI NONE) ths cs; |
407 |
fun cs addSEs ths = fold_rev (addSE NONE) ths cs; |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
408 |
|
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset
|
409 |
fun make_elim th = |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
410 |
if has_fewer_prems 1 th then |
26928 | 411 |
error("Ill-formed destruction rule\n" ^ Display.string_of_thm th) |
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset
|
412 |
else Tactic.make_elim th; |
17084
fb0a80aef0be
classical rules must have names for ATP integration
paulson
parents:
17057
diff
changeset
|
413 |
|
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset
|
414 |
fun cs addSDs ths = cs addSEs (map make_elim ths); |
0 | 415 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
416 |
|
1800 | 417 |
(*** Hazardous (unsafe) rules ***) |
0 | 418 |
|
18691 | 419 |
fun addI w th |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
420 |
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
421 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
18691 | 422 |
if mem_thm hazIs th then |
26928 | 423 |
(warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th); |
9938 | 424 |
cs) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
425 |
else |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
426 |
let val th' = flat_rule th |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
427 |
val nI = length hazIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
428 |
and nE = length hazEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
429 |
in warn_dup th cs; |
9938 | 430 |
CS{hazIs = th::hazIs, |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
431 |
haz_netpair = insert (nI,nE) ([th'], []) haz_netpair, |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
432 |
dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair, |
10736 | 433 |
safeIs = safeIs, |
9938 | 434 |
safeEs = safeEs, |
435 |
hazEs = hazEs, |
|
436 |
swrappers = swrappers, |
|
437 |
uwrappers = uwrappers, |
|
438 |
safe0_netpair = safe0_netpair, |
|
439 |
safep_netpair = safep_netpair, |
|
18691 | 440 |
xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair} |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
441 |
end |
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
442 |
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) |
26928 | 443 |
error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
444 |
|
18691 | 445 |
fun addE w th |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
446 |
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
447 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
18691 | 448 |
if mem_thm hazEs th then |
26928 | 449 |
(warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th); |
9938 | 450 |
cs) |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
451 |
else if has_fewer_prems 1 th then |
26928 | 452 |
error("Ill-formed elimination rule\n" ^ Display.string_of_thm th) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
453 |
else |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
454 |
let |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
455 |
val th' = classical_rule (flat_rule th) |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
456 |
val nI = length hazIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
457 |
and nE = length hazEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
458 |
in warn_dup th cs; |
9938 | 459 |
CS{hazEs = th::hazEs, |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
460 |
haz_netpair = insert (nI,nE) ([], [th']) haz_netpair, |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
461 |
dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair, |
10736 | 462 |
safeIs = safeIs, |
9938 | 463 |
safeEs = safeEs, |
464 |
hazIs = hazIs, |
|
465 |
swrappers = swrappers, |
|
466 |
uwrappers = uwrappers, |
|
467 |
safe0_netpair = safe0_netpair, |
|
468 |
safep_netpair = safep_netpair, |
|
18691 | 469 |
xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair} |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
470 |
end; |
0 | 471 |
|
18691 | 472 |
fun cs addIs ths = fold_rev (addI NONE) ths cs; |
473 |
fun cs addEs ths = fold_rev (addE NONE) ths cs; |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
474 |
|
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset
|
475 |
fun cs addDs ths = cs addEs (map make_elim ths); |
0 | 476 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
477 |
|
10736 | 478 |
(*** Deletion of rules |
1800 | 479 |
Working out what to delete, requires repeating much of the code used |
9938 | 480 |
to insert. |
1800 | 481 |
***) |
482 |
||
10736 | 483 |
fun delSI th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
484 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 485 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
18691 | 486 |
if mem_thm safeIs th then |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
487 |
let val th' = flat_rule th |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
488 |
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
|
489 |
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
9938 | 490 |
safep_netpair = delete (safep_rls, []) safep_netpair, |
18691 | 491 |
safeIs = rem_thm th safeIs, |
9938 | 492 |
safeEs = safeEs, |
493 |
hazIs = hazIs, |
|
494 |
hazEs = hazEs, |
|
495 |
swrappers = swrappers, |
|
496 |
uwrappers = uwrappers, |
|
497 |
haz_netpair = haz_netpair, |
|
498 |
dup_netpair = dup_netpair, |
|
12401 | 499 |
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
|
500 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
501 |
else cs; |
1800 | 502 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
503 |
fun delSE th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
504 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 505 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
18691 | 506 |
if mem_thm safeEs th then |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
507 |
let |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
508 |
val th' = classical_rule (flat_rule th) |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
509 |
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th'] |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
510 |
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
9938 | 511 |
safep_netpair = delete ([], safep_rls) safep_netpair, |
512 |
safeIs = safeIs, |
|
18691 | 513 |
safeEs = rem_thm th safeEs, |
9938 | 514 |
hazIs = hazIs, |
515 |
hazEs = hazEs, |
|
516 |
swrappers = swrappers, |
|
517 |
uwrappers = uwrappers, |
|
518 |
haz_netpair = haz_netpair, |
|
519 |
dup_netpair = dup_netpair, |
|
12401 | 520 |
xtra_netpair = delete' ([], [th]) xtra_netpair} |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
521 |
end |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
522 |
else cs; |
1800 | 523 |
|
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 delI 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}) = |
18691 | 528 |
if mem_thm hazIs th then |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
529 |
let val th' = flat_rule th |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
530 |
in CS{haz_netpair = delete ([th'], []) haz_netpair, |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
531 |
dup_netpair = delete ([dup_intr th'], []) dup_netpair, |
10736 | 532 |
safeIs = safeIs, |
9938 | 533 |
safeEs = safeEs, |
18691 | 534 |
hazIs = rem_thm th hazIs, |
9938 | 535 |
hazEs = hazEs, |
536 |
swrappers = swrappers, |
|
537 |
uwrappers = uwrappers, |
|
538 |
safe0_netpair = safe0_netpair, |
|
539 |
safep_netpair = safep_netpair, |
|
12401 | 540 |
xtra_netpair = delete' ([th], []) xtra_netpair} |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
541 |
end |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
542 |
else cs |
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
543 |
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) |
26928 | 544 |
error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th); |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset
|
545 |
|
1800 | 546 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
547 |
fun delE th |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
548 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
9938 | 549 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
550 |
if mem_thm hazEs th then |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
551 |
let val th' = classical_rule (flat_rule th) |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
552 |
in CS{haz_netpair = delete ([], [th']) haz_netpair, |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
553 |
dup_netpair = delete ([], [dup_elim th']) dup_netpair, |
10736 | 554 |
safeIs = safeIs, |
9938 | 555 |
safeEs = safeEs, |
556 |
hazIs = hazIs, |
|
18691 | 557 |
hazEs = rem_thm th hazEs, |
9938 | 558 |
swrappers = swrappers, |
559 |
uwrappers = uwrappers, |
|
560 |
safe0_netpair = safe0_netpair, |
|
561 |
safep_netpair = safep_netpair, |
|
12401 | 562 |
xtra_netpair = delete' ([], [th]) xtra_netpair} |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
563 |
end |
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
564 |
else cs; |
1800 | 565 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
566 |
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) |
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
567 |
fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = |
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
568 |
let val th' = Tactic.make_elim th in |
18691 | 569 |
if mem_thm safeIs th orelse mem_thm safeEs th orelse |
570 |
mem_thm hazIs th orelse mem_thm hazEs th orelse |
|
571 |
mem_thm safeEs th' orelse mem_thm hazEs th' |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
572 |
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) |
26928 | 573 |
else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs) |
9938 | 574 |
end; |
1800 | 575 |
|
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
576 |
fun cs delrules ths = fold delrule ths cs; |
1800 | 577 |
|
578 |
||
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
579 |
(*** Modifying the wrapper tacticals ***) |
22674 | 580 |
fun map_swrappers f |
581 |
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
|
582 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
583 |
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
584 |
swrappers = f swrappers, uwrappers = uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
585 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
6955 | 586 |
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
|
587 |
|
22674 | 588 |
fun map_uwrappers f |
589 |
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
|
590 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
591 |
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
592 |
swrappers = swrappers, uwrappers = f uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
593 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
6955 | 594 |
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
|
595 |
|
22674 | 596 |
fun update_warn msg (p as (key : string, _)) xs = |
597 |
(if AList.defined (op =) xs key then warning msg else (); |
|
598 |
AList.update (op =) p xs); |
|
599 |
||
600 |
fun delete_warn msg (key : string) xs = |
|
601 |
if AList.defined (op =) xs key then AList.delete (op =) key xs |
|
602 |
else (warning msg; xs); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
603 |
|
4651 | 604 |
(*Add/replace a safe wrapper*) |
22674 | 605 |
fun cs addSWrapper new_swrapper = map_swrappers |
606 |
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; |
|
4651 | 607 |
|
608 |
(*Add/replace an unsafe wrapper*) |
|
22674 | 609 |
fun cs addWrapper new_uwrapper = map_uwrappers |
610 |
(update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
611 |
|
4651 | 612 |
(*Remove a safe wrapper*) |
22674 | 613 |
fun cs delSWrapper name = map_swrappers |
614 |
(delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
615 |
|
4651 | 616 |
(*Remove an unsafe wrapper*) |
22674 | 617 |
fun cs delWrapper name = map_uwrappers |
618 |
(delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
619 |
|
11168 | 620 |
(* compose a safe tactic alternatively before/after safe_step_tac *) |
10736 | 621 |
fun cs addSbefore (name, tac1) = |
5523 | 622 |
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
623 |
fun cs addSafter (name, tac2) = |
5523 | 624 |
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
625 |
|
11168 | 626 |
(*compose a tactic alternatively before/after the step tactic *) |
10736 | 627 |
fun cs addbefore (name, tac1) = |
5523 | 628 |
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
629 |
fun cs addafter (name, tac2) = |
5523 | 630 |
cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
631 |
|
10736 | 632 |
fun cs addD2 (name, thm) = |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
633 |
cs addafter (name, datac thm 1); |
10736 | 634 |
fun cs addE2 (name, thm) = |
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
635 |
cs addafter (name, eatac thm 1); |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
636 |
fun cs addSD2 (name, thm) = |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
637 |
cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
638 |
fun cs addSE2 (name, thm) = |
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11168
diff
changeset
|
639 |
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
|
640 |
|
1711 | 641 |
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. |
642 |
Merging the term nets may look more efficient, but the rather delicate |
|
643 |
treatment of priority might get muddled up.*) |
|
22674 | 644 |
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, |
24358 | 645 |
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, |
22674 | 646 |
swrappers, uwrappers, ...}) = |
24358 | 647 |
if pointer_eq (cs, cs') then cs |
648 |
else |
|
649 |
let |
|
650 |
val safeIs' = fold rem_thm safeIs safeIs2; |
|
651 |
val safeEs' = fold rem_thm safeEs safeEs2; |
|
652 |
val hazIs' = fold rem_thm hazIs hazIs2; |
|
653 |
val hazEs' = fold rem_thm hazEs hazEs2; |
|
654 |
val cs1 = cs addSIs safeIs' |
|
655 |
addSEs safeEs' |
|
656 |
addIs hazIs' |
|
657 |
addEs hazEs'; |
|
658 |
val cs2 = map_swrappers |
|
659 |
(fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; |
|
660 |
val cs3 = map_uwrappers |
|
661 |
(fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; |
|
662 |
in cs3 end; |
|
1711 | 663 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
664 |
|
1800 | 665 |
(**** Simple tactics for theorem proving ****) |
0 | 666 |
|
667 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
10736 | 668 |
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
4651 | 669 |
appSWrappers cs (FIRST' [ |
9938 | 670 |
eq_assume_tac, |
671 |
eq_mp_tac, |
|
672 |
bimatch_from_nets_tac safe0_netpair, |
|
673 |
FIRST' hyp_subst_tacs, |
|
674 |
bimatch_from_nets_tac safep_netpair]); |
|
0 | 675 |
|
5757 | 676 |
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) |
10736 | 677 |
fun safe_steps_tac cs = REPEAT_DETERM1 o |
9938 | 678 |
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); |
5757 | 679 |
|
0 | 680 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
5757 | 681 |
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
|
682 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
683 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
684 |
(*** 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
|
685 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
686 |
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
|
687 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
688 |
(*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
|
689 |
create precisely n subgoals.*) |
10736 | 690 |
fun n_bimatch_from_nets_tac n = |
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30541
diff
changeset
|
691 |
biresolution_from_nets_tac (order_list 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
|
692 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
693 |
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
|
694 |
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
|
695 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
696 |
(*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
|
697 |
fun bimatch2_tac netpair i = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
698 |
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
|
699 |
(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
|
700 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
701 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
10736 | 702 |
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
4651 | 703 |
appSWrappers cs (FIRST' [ |
9938 | 704 |
eq_assume_contr_tac, |
705 |
bimatch_from_nets_tac safe0_netpair, |
|
706 |
FIRST' hyp_subst_tacs, |
|
707 |
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
|
708 |
bimatch2_tac safep_netpair]); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
709 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
710 |
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
|
711 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
712 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
713 |
(*** 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
|
714 |
|
4066 | 715 |
(*Backtracking is allowed among the various these unsafe ways of |
716 |
proving a subgoal. *) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
717 |
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
10736 | 718 |
assume_tac APPEND' |
719 |
contr_tac APPEND' |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
720 |
biresolve_from_nets_tac safe0_netpair; |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
721 |
|
4066 | 722 |
(*These unsafe steps could generate more subgoals.*) |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
723 |
fun instp_step_tac (CS{safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
724 |
biresolve_from_nets_tac safep_netpair; |
0 | 725 |
|
726 |
(*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
|
727 |
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; |
0 | 728 |
|
10736 | 729 |
fun haz_step_tac (CS{haz_netpair,...}) = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
730 |
biresolve_from_nets_tac haz_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
731 |
|
0 | 732 |
(*Single step for the prover. FAILS unless it makes progress. *) |
10736 | 733 |
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs |
9938 | 734 |
(inst_step_tac cs ORELSE' haz_step_tac cs) i; |
0 | 735 |
|
736 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
737 |
allows backtracking from "safe" rules to "unsafe" rules here.*) |
|
10736 | 738 |
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs |
9938 | 739 |
(inst_step_tac cs APPEND' haz_step_tac cs) i; |
0 | 740 |
|
1800 | 741 |
(**** The following tactics all fail unless they solve one goal ****) |
0 | 742 |
|
743 |
(*Dumb but fast*) |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
744 |
fun fast_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
745 |
ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
0 | 746 |
|
747 |
(*Slower but smarter than fast_tac*) |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
748 |
fun best_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
749 |
ObjectLogic.atomize_prems_tac THEN' |
0 | 750 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); |
751 |
||
9402 | 752 |
(*even a bit smarter than best_tac*) |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
753 |
fun first_best_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
754 |
ObjectLogic.atomize_prems_tac THEN' |
9402 | 755 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); |
756 |
||
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
757 |
fun slow_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
758 |
ObjectLogic.atomize_prems_tac THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
759 |
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
0 | 760 |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
761 |
fun slow_best_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
762 |
ObjectLogic.atomize_prems_tac THEN' |
0 | 763 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
764 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
765 |
|
10736 | 766 |
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) |
767 |
val weight_ASTAR = ref 5; |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
768 |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
769 |
fun astar_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
770 |
ObjectLogic.atomize_prems_tac THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
771 |
SELECT_GOAL |
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
772 |
(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
|
773 |
(step_tac cs 1)); |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
774 |
|
10736 | 775 |
fun slow_astar_tac cs = |
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset
|
776 |
ObjectLogic.atomize_prems_tac THEN' |
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
777 |
SELECT_GOAL |
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
778 |
(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
|
779 |
(slow_step_tac cs 1)); |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
780 |
|
1800 | 781 |
(**** 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
|
782 |
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
|
783 |
easy theorems faster, but loses completeness -- and many of the harder |
1800 | 784 |
theorems such as 43. ****) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
785 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
786 |
(*Non-deterministic! Could always expand the first unsafe connective. |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
787 |
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
|
788 |
greater search depth required.*) |
10736 | 789 |
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
|
790 |
biresolve_from_nets_tac dup_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
791 |
|
5523 | 792 |
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) |
5757 | 793 |
local |
10736 | 794 |
fun slow_step_tac' cs = appWrappers cs |
9938 | 795 |
(instp_step_tac cs APPEND' dup_step_tac cs); |
10736 | 796 |
in fun depth_tac cs m i state = SELECT_GOAL |
797 |
(safe_steps_tac cs 1 THEN_ELSE |
|
9938 | 798 |
(DEPTH_SOLVE (depth_tac cs m 1), |
799 |
inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac |
|
800 |
(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)) |
|
5757 | 801 |
)) i state; |
802 |
end; |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
803 |
|
10736 | 804 |
(*Search, with depth bound m. |
2173 | 805 |
This is the "entry point", which does safe inferences first.*) |
10736 | 806 |
fun safe_depth_tac cs m = |
807 |
SUBGOAL |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
808 |
(fn (prem,i) => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
809 |
let val deti = |
9938 | 810 |
(*No Vars in the goal? No need to backtrack between goals.*) |
29267 | 811 |
if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I |
10736 | 812 |
in SELECT_GOAL (TRY (safe_tac cs) THEN |
9938 | 813 |
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
|
814 |
end); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
815 |
|
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
816 |
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
|
817 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
818 |
|
1724 | 819 |
|
15036 | 820 |
(** context dependent claset components **) |
821 |
||
822 |
datatype context_cs = ContextCS of |
|
823 |
{swrappers: (string * (Proof.context -> wrapper)) list, |
|
824 |
uwrappers: (string * (Proof.context -> wrapper)) list}; |
|
825 |
||
826 |
fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) = |
|
827 |
let |
|
828 |
fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt)); |
|
829 |
in |
|
22674 | 830 |
cs |
831 |
|> fold_rev (add_wrapper (op addSWrapper)) swrappers |
|
15036 | 832 |
|> fold_rev (add_wrapper (op addWrapper)) uwrappers |
833 |
end; |
|
834 |
||
835 |
fun make_context_cs (swrappers, uwrappers) = |
|
836 |
ContextCS {swrappers = swrappers, uwrappers = uwrappers}; |
|
837 |
||
838 |
val empty_context_cs = make_context_cs ([], []); |
|
839 |
||
840 |
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = |
|
24358 | 841 |
if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 |
842 |
else |
|
843 |
let |
|
844 |
val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1; |
|
845 |
val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2; |
|
846 |
val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2); |
|
847 |
val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2); |
|
848 |
in make_context_cs (swrappers', uwrappers') end; |
|
15036 | 849 |
|
850 |
||
851 |
||
17880 | 852 |
(** claset data **) |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
853 |
|
24021 | 854 |
(* global clasets *) |
1724 | 855 |
|
16424 | 856 |
structure GlobalClaset = TheoryDataFun |
22846 | 857 |
( |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
858 |
type T = claset * context_cs; |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
859 |
val empty = (empty_cs, empty_context_cs); |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
860 |
val copy = I; |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
861 |
val extend = I; |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
862 |
fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) = |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
863 |
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); |
22846 | 864 |
); |
1724 | 865 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
866 |
val get_claset = #1 o GlobalClaset.get; |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
867 |
val map_claset = GlobalClaset.map o apfst; |
17880 | 868 |
|
15036 | 869 |
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; |
870 |
fun map_context_cs f = GlobalClaset.map (apsnd |
|
871 |
(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
|
872 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
873 |
fun change_claset f = Context.>> (Context.map_theory (map_claset f)); |
1800 | 874 |
|
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset
|
875 |
fun claset_of thy = |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
876 |
let val (cs, ctxt_cs) = GlobalClaset.get thy |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
877 |
in context_cs (ProofContext.init thy) cs (ctxt_cs) end; |
26425
6561665c5cb1
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26412
diff
changeset
|
878 |
val claset = claset_of o ML_Context.the_global_context; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
879 |
|
17880 | 880 |
fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st; |
881 |
fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st; |
|
1724 | 882 |
|
17880 | 883 |
fun AddDs args = change_claset (fn cs => cs addDs args); |
884 |
fun AddEs args = change_claset (fn cs => cs addEs args); |
|
885 |
fun AddIs args = change_claset (fn cs => cs addIs args); |
|
886 |
fun AddSDs args = change_claset (fn cs => cs addSDs args); |
|
887 |
fun AddSEs args = change_claset (fn cs => cs addSEs args); |
|
888 |
fun AddSIs args = change_claset (fn cs => cs addSIs args); |
|
889 |
fun Delrules args = change_claset (fn cs => cs delrules args); |
|
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
890 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
891 |
|
15036 | 892 |
(* context dependent components *) |
893 |
||
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
894 |
fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper))); |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
895 |
fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name))); |
15036 | 896 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
897 |
fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper))); |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
898 |
fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name))); |
15036 | 899 |
|
900 |
||
24021 | 901 |
(* local clasets *) |
5841 | 902 |
|
16424 | 903 |
structure LocalClaset = ProofDataFun |
22846 | 904 |
( |
5841 | 905 |
type T = claset; |
17880 | 906 |
val init = get_claset; |
22846 | 907 |
); |
5841 | 908 |
|
15036 | 909 |
fun local_claset_of ctxt = |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
910 |
context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); |
22846 | 911 |
|
5841 | 912 |
|
24021 | 913 |
(* generic clasets *) |
914 |
||
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
915 |
val get_cs = Context.cases claset_of local_claset_of; |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
916 |
fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f); |
24021 | 917 |
|
918 |
||
5885 | 919 |
(* attributes *) |
920 |
||
18728 | 921 |
fun attrib f = Thm.declaration_attribute (fn th => |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
922 |
Context.mapping (map_claset (f th)) (LocalClaset.map (f th))); |
5885 | 923 |
|
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset
|
924 |
fun safe_dest w = attrib (addSE w o make_elim); |
18691 | 925 |
val safe_elim = attrib o addSE; |
926 |
val safe_intro = attrib o addSI; |
|
21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset
|
927 |
fun haz_dest w = attrib (addE w o make_elim); |
18691 | 928 |
val haz_elim = attrib o addE; |
929 |
val haz_intro = attrib o addI; |
|
930 |
val rule_del = attrib delrule o ContextRules.rule_del; |
|
5885 | 931 |
|
932 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
933 |
(* tactics referring to the implicit claset *) |
1800 | 934 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
935 |
(*the abstraction over the proof state delays the dereferencing*) |
9938 | 936 |
fun Safe_tac st = safe_tac (claset()) st; |
937 |
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
|
938 |
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; |
9938 | 939 |
fun Clarify_tac i st = clarify_tac (claset()) i st; |
940 |
fun Step_tac i st = step_tac (claset()) i st; |
|
941 |
fun Fast_tac i st = fast_tac (claset()) i st; |
|
942 |
fun Best_tac i st = best_tac (claset()) i st; |
|
943 |
fun Slow_tac i st = slow_tac (claset()) i st; |
|
944 |
fun Slow_best_tac i st = slow_best_tac (claset()) i st; |
|
945 |
fun Deepen_tac m = deepen_tac (claset()) m; |
|
2066 | 946 |
|
1800 | 947 |
|
10736 | 948 |
end; |
5841 | 949 |
|
950 |
||
951 |
||
5885 | 952 |
(** concrete syntax of attributes **) |
5841 | 953 |
|
954 |
val introN = "intro"; |
|
955 |
val elimN = "elim"; |
|
956 |
val destN = "dest"; |
|
9938 | 957 |
val ruleN = "rule"; |
5841 | 958 |
|
30528 | 959 |
val setup_attrs = |
960 |
Attrib.setup @{binding swapped} (Scan.succeed swapped) |
|
961 |
"classical swap of introduction rule" #> |
|
962 |
Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query) |
|
963 |
"declaration of Classical destruction rule" #> |
|
964 |
Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query) |
|
965 |
"declaration of Classical elimination rule" #> |
|
966 |
Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query) |
|
967 |
"declaration of Classical introduction rule" #> |
|
968 |
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) |
|
969 |
"remove declaration of intro/elim/dest rule"; |
|
5841 | 970 |
|
971 |
||
972 |
||
7230 | 973 |
(** proof methods **) |
974 |
||
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset
|
975 |
fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt)); |
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset
|
976 |
fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt)); |
7230 | 977 |
|
978 |
||
979 |
local |
|
980 |
||
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
981 |
fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) => |
5841 | 982 |
let |
12401 | 983 |
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt; |
984 |
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
|
985 |
val rules = rules1 @ rules2 @ rules3 @ rules4; |
18223 | 986 |
val ruleq = Drule.multi_resolves facts rules; |
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
987 |
in |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
988 |
Method.trace ctxt rules; |
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
989 |
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) |
18834 | 990 |
end) |
21687 | 991 |
THEN_ALL_NEW Goal.norm_hhf_tac; |
5841 | 992 |
|
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset
|
993 |
fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts |
10394 | 994 |
| rule_tac rules _ _ facts = Method.rule_tac rules facts; |
7281 | 995 |
|
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset
|
996 |
fun default_tac rules ctxt cs facts = |
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset
|
997 |
HEADGOAL (rule_tac rules ctxt cs facts) ORELSE |
26470 | 998 |
Class.default_intro_tac ctxt facts; |
10309 | 999 |
|
7230 | 1000 |
in |
7281 | 1001 |
val rule = METHOD_CLASET' o rule_tac; |
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
13525
diff
changeset
|
1002 |
val default = METHOD_CLASET o default_tac; |
7230 | 1003 |
end; |
5841 | 1004 |
|
1005 |
||
7230 | 1006 |
(* contradiction method *) |
6502 | 1007 |
|
7425 | 1008 |
val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl]; |
6502 | 1009 |
|
1010 |
||
1011 |
(* automatic methods *) |
|
5841 | 1012 |
|
5927 | 1013 |
val cla_modifiers = |
18728 | 1014 |
[Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier), |
1015 |
Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE), |
|
1016 |
Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE), |
|
1017 |
Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE), |
|
1018 |
Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE), |
|
1019 |
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE), |
|
1020 |
Args.del -- Args.colon >> K (I, rule_del)]; |
|
5927 | 1021 |
|
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset
|
1022 |
fun cla_meth tac prems ctxt = METHOD (fn facts => |
15036 | 1023 |
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt)); |
7132 | 1024 |
|
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30190
diff
changeset
|
1025 |
fun cla_meth' tac prems ctxt = METHOD (fn facts => |
15036 | 1026 |
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt))); |
5841 | 1027 |
|
30541 | 1028 |
fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac); |
1029 |
fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac); |
|
5841 | 1030 |
|
1031 |
||
1032 |
||
1033 |
(** setup_methods **) |
|
1034 |
||
30541 | 1035 |
val setup_methods = |
1036 |
Method.setup @{binding default} (Attrib.thms >> default) |
|
1037 |
"apply some intro/elim rule (potentially classical)" #> |
|
1038 |
Method.setup @{binding rule} (Attrib.thms >> rule) |
|
1039 |
"apply some intro/elim rule (potentially classical)" #> |
|
1040 |
Method.setup @{binding contradiction} (Scan.succeed (K contradiction)) |
|
1041 |
"proof by contradiction" #> |
|
1042 |
Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac)) |
|
1043 |
"repeatedly apply safe steps" #> |
|
1044 |
Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #> |
|
1045 |
Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #> |
|
1046 |
Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #> |
|
1047 |
Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4)) |
|
1048 |
"classical prover (iterative deepening)" #> |
|
1049 |
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) |
|
1050 |
"classical prover (apply safe rules)"; |
|
5841 | 1051 |
|
1052 |
||
1053 |
||
1054 |
(** theory setup **) |
|
1055 |
||
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
1056 |
val setup = setup_attrs #> setup_methods; |
5841 | 1057 |
|
1058 |
||
8667 | 1059 |
|
1060 |
(** outer syntax **) |
|
1061 |
||
24867 | 1062 |
val _ = |
8667 | 1063 |
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" |
17057 | 1064 |
OuterKeyword.diag |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
1065 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset
|
1066 |
Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of))); |
8667 | 1067 |
|
5841 | 1068 |
end; |