author  wenzelm 
Sat, 14 May 2011 17:55:08 +0200  
changeset 42807  e639d91d9073 
parent 42799  4e33894aec6d 
child 42810  2425068fe13a 
permissions  rwrr 
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 ("Illformed 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 ("Illformed 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 ("Illformed 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 ("Illformed 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 ("Illformed 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 
(* oldstyle 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 
(*Twoway 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 
(*Nondeterministic! 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 (depthfirst)" #> 

948 
Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depthfirst)" #> 

949 
Method.setup @{binding best} (cla_method' best_tac) "classical prover (bestfirst)" #> 

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; 