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