author  wenzelm 
Fri, 13 May 2011 15:47:54 +0200  
changeset 42790  e07e56300faa 
parent 42439  9efdd0af15ac 
child 42791  36f787ae5f70 
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 
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

40 
val print_cs: Proof.context > claset > unit 
42790  41 
val rep_cs: claset > 
42 
{safeIs: thm list, 

43 
safeEs: thm list, 

44 
hazIs: thm list, 

45 
hazEs: thm list, 

46 
swrappers: (string * wrapper) list, 

47 
uwrappers: (string * wrapper) list, 

48 
safe0_netpair: netpair, 

49 
safep_netpair: netpair, 

50 
haz_netpair: netpair, 

51 
dup_netpair: netpair, 

52 
xtra_netpair: Context_Rules.netpair} 

53 
val merge_cs: claset * claset > claset 

54 
val addDs: claset * thm list > claset 

55 
val addEs: claset * thm list > claset 

56 
val addIs: claset * thm list > claset 

57 
val addSDs: claset * thm list > claset 

58 
val addSEs: claset * thm list > claset 

59 
val addSIs: claset * thm list > claset 

60 
val delrules: claset * thm list > claset 

61 
val addSWrapper: claset * (string * wrapper) > claset 

62 
val delSWrapper: claset * string > claset 

63 
val addWrapper: claset * (string * wrapper) > claset 

64 
val delWrapper: claset * string > claset 

65 
val addSbefore: claset * (string * (int > tactic)) > claset 

66 
val addSafter: claset * (string * (int > tactic)) > claset 

67 
val addbefore: claset * (string * (int > tactic)) > claset 

68 
val addafter: claset * (string * (int > tactic)) > claset 

69 
val addD2: claset * (string * thm) > claset 

70 
val addE2: claset * (string * thm) > claset 

71 
val addSD2: claset * (string * thm) > claset 

72 
val addSE2: claset * (string * thm) > claset 

73 
val appSWrappers: claset > wrapper 

74 
val appWrappers: claset > wrapper 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

75 

42790  76 
val global_claset_of: theory > claset 
77 
val claset_of: Proof.context > claset 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

78 

42790  79 
val fast_tac: claset > int > tactic 
80 
val slow_tac: claset > int > tactic 

81 
val weight_ASTAR: int Unsynchronized.ref 

82 
val astar_tac: claset > int > tactic 

83 
val slow_astar_tac: claset > int > tactic 

84 
val best_tac: claset > int > tactic 

85 
val first_best_tac: claset > int > tactic 

86 
val slow_best_tac: claset > int > tactic 

87 
val depth_tac: claset > int > int > tactic 

88 
val deepen_tac: claset > int > int > tactic 

1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

89 

42790  90 
val contr_tac: int > tactic 
91 
val dup_elim: thm > thm 

92 
val dup_intr: thm > thm 

93 
val dup_step_tac: claset > int > tactic 

94 
val eq_mp_tac: int > tactic 

95 
val haz_step_tac: claset > int > tactic 

96 
val joinrules: thm list * thm list > (bool * thm) list 

97 
val mp_tac: int > tactic 

98 
val safe_tac: claset > tactic 

99 
val safe_steps_tac: claset > int > tactic 

100 
val safe_step_tac: claset > int > tactic 

101 
val clarify_tac: claset > int > tactic 

102 
val clarify_step_tac: claset > int > tactic 

103 
val step_tac: claset > int > tactic 

104 
val slow_step_tac: claset > int > tactic 

105 
val swapify: thm list > thm list 

106 
val swap_res_tac: thm list > int > tactic 

107 
val inst_step_tac: claset > int > tactic 

108 
val inst0_step_tac: claset > int > tactic 

109 
val instp_step_tac: claset > int > tactic 

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 
15036  116 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
117 
val del_context_safe_wrapper: string > theory > theory 

118 
val add_context_unsafe_wrapper: string * (Proof.context > wrapper) > theory > theory 

119 
val del_context_unsafe_wrapper: string > theory > theory 

32261  120 
val get_claset: Proof.context > claset 
121 
val put_claset: claset > Proof.context > Proof.context 

24021  122 
val get_cs: Context.generic > claset 
123 
val map_cs: (claset > claset) > Context.generic > Context.generic 

18728  124 
val safe_dest: int option > attribute 
125 
val safe_elim: int option > attribute 

126 
val safe_intro: int option > attribute 

127 
val haz_dest: int option > attribute 

128 
val haz_elim: int option > attribute 

129 
val haz_intro: int option > attribute 

130 
val rule_del: attribute 

30513  131 
val cla_modifiers: Method.modifier parser list 
35613  132 
val cla_meth: (claset > tactic) > Proof.context > Proof.method 
133 
val cla_meth': (claset > int > tactic) > Proof.context > Proof.method 

30541  134 
val cla_method: (claset > tactic) > (Proof.context > Proof.method) context_parser 
135 
val cla_method': (claset > int > tactic) > (Proof.context > Proof.method) context_parser 

18708  136 
val setup: theory > theory 
5841  137 
end; 
138 

0  139 

5927  140 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  141 
struct 
142 

7354  143 
local open Data in 
0  144 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

145 
(** classical elimination rules **) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

146 

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 
Classical reasoning requires stronger elimination rules. For 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

149 
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

150 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

151 
[ 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

152 

26938  153 
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

154 
FAILED"; classical_rule will strenthen this to 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

155 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

156 
[ 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

157 
*) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

158 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

159 
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

160 
if is_some (Object_Logic.elim_concl rule) then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

161 
let 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

162 
val rule' = rule RS classical; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

163 
val concl' = Thm.concl_of rule'; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

164 
fun redundant_hyp goal = 
19257  165 
concl' aconv Logic.strip_assums_concl goal orelse 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

166 
(case Logic.strip_assums_hyp goal of 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

167 
hyp :: hyps => exists (fn t => t aconv hyp) hyps 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

168 
 _ => false); 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

169 
val rule'' = 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

170 
rule' > ALLGOALS (SUBGOAL (fn (goal, i) => 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

171 
if i = 1 orelse redundant_hyp goal 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

172 
then Tactic.etac thin_rl i 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

173 
else all_tac)) 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

174 
> Seq.hd 
21963  175 
> Drule.zero_var_indexes; 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset

176 
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

177 
else rule; 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

178 

23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

179 
(*flatten nested meta connectives in prems*) 
35625  180 
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

181 

6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

182 

1800  183 
(*** Useful tactics for classical reasoning ***) 
0  184 

10736  185 
(*Prove goal that assumes both P and ~P. 
4392  186 
No backtracking if it finds an equal assumption. Perhaps should call 
187 
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) 

10736  188 
val contr_tac = eresolve_tac [not_elim] THEN' 
4392  189 
(eq_assume_tac ORELSE' assume_tac); 
0  190 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

191 
(*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

192 
Could do the same thing for P<>Q and P... *) 
26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

193 
fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i THEN assume_tac i; 
0  194 

195 
(*Like mp_tac but instantiates no variables*) 

26412
0918f5c0bbca
pass imp_elim (instead of mp) and swap explicitly  avoids store_thm;
wenzelm
parents:
24867
diff
changeset

196 
fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i THEN eq_assume_tac i; 
0  197 

198 
(*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

199 
fun swapify intrs = intrs RLN (2, [Data.swap]); 
30528  200 
val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap)); 
0  201 

202 
(*Uses introduction rules in the normal way, or on negated assumptions, 

203 
trying rules in order. *) 

10736  204 
fun swap_res_tac rls = 
33339  205 
let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls 
10736  206 
in assume_tac ORELSE' 
207 
contr_tac ORELSE' 

33339  208 
biresolve_tac (fold_rev addrl rls []) 
0  209 
end; 
210 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

211 
(*Duplication of hazardous rules, for complete provers*) 
2689
6d3d893453de
dup_intr & dup_elim no longer call standard  this
paulson
parents:
2630
diff
changeset

212 
fun dup_intr th = zero_var_indexes (th RS classical); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

213 

6967  214 
fun dup_elim th = 
36546  215 
let 
216 
val rl = (th RSN (2, revcut_rl)) > Thm.assumption 2 > Seq.hd; 

42361  217 
val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); 
36546  218 
in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; 
219 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

220 

1800  221 
(**** Classical rule sets ****) 
0  222 

223 
datatype claset = 

12401  224 
CS of {safeIs : thm list, (*safe introduction rules*) 
225 
safeEs : thm list, (*safe elimination rules*) 

226 
hazIs : thm list, (*unsafe introduction rules*) 

227 
hazEs : thm list, (*unsafe elimination rules*) 

228 
swrappers : (string * wrapper) list, (*for transforming safe_step_tac*) 

9938  229 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  230 
safe0_netpair : netpair, (*nets for trivial cases*) 
231 
safep_netpair : netpair, (*nets for >0 subgoals*) 

232 
haz_netpair : netpair, (*nets for unsafe rules*) 

233 
dup_netpair : netpair, (*nets for duplication*) 

33369  234 
xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*) 
0  235 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

236 
(*Desired invariants are 
9938  237 
safe0_netpair = build safe0_brls, 
238 
safep_netpair = build safep_brls, 

239 
haz_netpair = build (joinrules(hazIs, hazEs)), 

10736  240 
dup_netpair = build (joinrules(map dup_intr hazIs, 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

241 
map dup_elim hazEs)) 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

242 

10736  243 
where build = build_netpair(Net.empty,Net.empty), 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

244 
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

245 
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

246 
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

247 
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

248 
*) 
0  249 

6502  250 
val empty_netpair = (Net.empty, Net.empty); 
251 

10736  252 
val empty_cs = 
9938  253 
CS{safeIs = [], 
254 
safeEs = [], 

255 
hazIs = [], 

256 
hazEs = [], 

4651  257 
swrappers = [], 
258 
uwrappers = [], 

6502  259 
safe0_netpair = empty_netpair, 
260 
safep_netpair = empty_netpair, 

261 
haz_netpair = empty_netpair, 

6955  262 
dup_netpair = empty_netpair, 
263 
xtra_netpair = empty_netpair}; 

0  264 

42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

265 
fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) = 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

266 
let val pretty_thms = map (Display.pretty_thm ctxt) in 
9760  267 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 
268 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

269 
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), 

15036  270 
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), 
271 
Pretty.strs ("safe wrappers:" :: map #1 swrappers), 

272 
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] 

8727  273 
> Pretty.chunks > Pretty.writeln 
3546  274 
end; 
0  275 

4653  276 
fun rep_cs (CS args) = args; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

277 

22674  278 
fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers; 
279 
fun appWrappers (CS {uwrappers, ...}) = fold snd uwrappers; 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

280 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

281 

1800  282 
(*** Adding (un)safe introduction or elimination rules. 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

283 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

284 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  285 
***) 
0  286 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

287 
(*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

288 
assumptions. Pairs elim rules with true. *) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

289 
fun joinrules (intrs, elims) = 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

290 
(map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

291 

12401  292 
fun joinrules' (intrs, elims) = 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

293 
map (pair true) elims @ map (pair false) intrs; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

294 

10736  295 
(*Priority: prefer rules with fewest subgoals, 
1231  296 
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

297 
fun tag_brls k [] = [] 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

298 
 tag_brls k (brl::brls) = 
10736  299 
(1000000*subgoals_of_brl brl + k, brl) :: 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

300 
tag_brls (k+1) brls; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

301 

12401  302 
fun tag_brls' _ _ [] = [] 
303 
 tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls; 

10736  304 

23178  305 
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

306 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

307 
(*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

308 
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

309 
new insertions the lowest priority.*) 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

310 
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
12401  311 
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

312 

23178  313 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  314 
fun delete x = delete_tagged_list (joinrules x); 
12401  315 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  316 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22095
diff
changeset

317 
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

318 
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

319 

42790  320 
fun warn msg rules th = 
321 
mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true); 

322 

323 
fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 

324 
warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse 

325 
warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse 

326 
warn "Rule already declared as introduction (intro)\n" hazIs th orelse 

327 
warn "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

328 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

329 

1800  330 
(*** Safe rules ***) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

331 

18691  332 
fun addSI w th 
42790  333 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
334 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

335 
if warn "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

336 
else 
42790  337 
let 
338 
val th' = flat_rule th; 

23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

339 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
42790  340 
List.partition Thm.no_prems [th']; 
341 
val nI = length safeIs + 1; 

342 
val nE = length safeEs; 

343 
val _ = warn_other th cs; 

344 
in 

345 
CS 

346 
{safeIs = th::safeIs, 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

347 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  348 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
42790  349 
safeEs = safeEs, 
350 
hazIs = hazIs, 

351 
hazEs = hazEs, 

352 
swrappers = swrappers, 

353 
uwrappers = uwrappers, 

354 
haz_netpair = haz_netpair, 

355 
dup_netpair = dup_netpair, 

18691  356 
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} 
42790  357 
end; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

358 

18691  359 
fun addSE w th 
42790  360 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
361 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

362 
if warn "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

363 
else if has_fewer_prems 1 th then 
42790  364 
error ("Illformed elimination rule\n" ^ Display.string_of_thm_without_context th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

365 
else 
42790  366 
let 
367 
val th' = classical_rule (flat_rule th); 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

368 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
42790  369 
List.partition (fn rl => nprems_of rl=1) [th']; 
370 
val nI = length safeIs; 

371 
val nE = length safeEs + 1; 

372 
val _ = warn_other th cs; 

373 
in 

374 
CS 

375 
{safeEs = th::safeEs, 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

376 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  377 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
42790  378 
safeIs = safeIs, 
379 
hazIs = hazIs, 

380 
hazEs = hazEs, 

381 
swrappers = swrappers, 

382 
uwrappers = uwrappers, 

383 
haz_netpair = haz_netpair, 

384 
dup_netpair = dup_netpair, 

18691  385 
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} 
42790  386 
end; 
0  387 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

388 

1800  389 
(*** Hazardous (unsafe) rules ***) 
0  390 

18691  391 
fun addI w th 
42790  392 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
393 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

394 
if warn "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

395 
else 
42790  396 
let 
397 
val th' = flat_rule th; 

398 
val nI = length hazIs + 1; 

399 
val nE = length hazEs; 

400 
val _ = warn_other th cs; 

401 
in 

402 
CS 

403 
{hazIs = th :: hazIs, 

404 
haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, 

405 
dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, 

406 
safeIs = safeIs, 

407 
safeEs = safeEs, 

408 
hazEs = hazEs, 

409 
swrappers = swrappers, 

410 
uwrappers = uwrappers, 

9938  411 
safe0_netpair = safe0_netpair, 
412 
safep_netpair = safep_netpair, 

42790  413 
xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} 
414 
end 

415 
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) 

416 
error ("Illformed introduction rule\n" ^ Display.string_of_thm_without_context th); 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

417 

18691  418 
fun addE w th 
42790  419 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
420 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

421 
if warn "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

422 
else if has_fewer_prems 1 th then 
42790  423 
error ("Illformed elimination rule\n" ^ Display.string_of_thm_without_context th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

424 
else 
42790  425 
let 
426 
val th' = classical_rule (flat_rule th); 

427 
val nI = length hazIs; 

428 
val nE = length hazEs + 1; 

429 
val _ = warn_other th cs; 

430 
in 

431 
CS 

432 
{hazEs = th :: hazEs, 

433 
haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, 

434 
dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair, 

435 
safeIs = safeIs, 

436 
safeEs = safeEs, 

437 
hazIs = hazIs, 

438 
swrappers = swrappers, 

439 
uwrappers = uwrappers, 

9938  440 
safe0_netpair = safe0_netpair, 
441 
safep_netpair = safep_netpair, 

42790  442 
xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} 
443 
end; 

0  444 

445 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

446 

10736  447 
(*** Deletion of rules 
1800  448 
Working out what to delete, requires repeating much of the code used 
9938  449 
to insert. 
1800  450 
***) 
451 

10736  452 
fun delSI th 
42790  453 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
454 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

455 
if mem_thm safeIs th then 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

456 
let 
42790  457 
val th' = flat_rule th; 
458 
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; 

459 
in 

460 
CS 

461 
{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 

462 
safep_netpair = delete (safep_rls, []) safep_netpair, 

463 
safeIs = rem_thm th safeIs, 

464 
safeEs = safeEs, 

465 
hazIs = hazIs, 

466 
hazEs = hazEs, 

467 
swrappers = swrappers, 

468 
uwrappers = uwrappers, 

469 
haz_netpair = haz_netpair, 

470 
dup_netpair = dup_netpair, 

471 
xtra_netpair = delete' ([th], []) xtra_netpair} 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

472 
end 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

473 
else cs; 
1800  474 

42790  475 
fun delSE th 
476 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

477 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

478 
if mem_thm safeEs th then 

479 
let 

480 
val th' = classical_rule (flat_rule th); 

481 
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th']; 

482 
in 

483 
CS 

484 
{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 

485 
safep_netpair = delete ([], safep_rls) safep_netpair, 

486 
safeIs = safeIs, 

487 
safeEs = rem_thm th safeEs, 

488 
hazIs = hazIs, 

489 
hazEs = hazEs, 

490 
swrappers = swrappers, 

491 
uwrappers = uwrappers, 

492 
haz_netpair = haz_netpair, 

493 
dup_netpair = dup_netpair, 

494 
xtra_netpair = delete' ([], [th]) xtra_netpair} 

495 
end 

496 
else cs; 

1800  497 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

498 
fun delI th 
42790  499 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
500 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

501 
if mem_thm hazIs th then 

502 
let val th' = flat_rule th in 

503 
CS 

504 
{haz_netpair = delete ([th'], []) haz_netpair, 

23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

505 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
42790  506 
safeIs = safeIs, 
507 
safeEs = safeEs, 

508 
hazIs = rem_thm th hazIs, 

509 
hazEs = hazEs, 

510 
swrappers = swrappers, 

511 
uwrappers = uwrappers, 

9938  512 
safe0_netpair = safe0_netpair, 
513 
safep_netpair = safep_netpair, 

12401  514 
xtra_netpair = delete' ([th], []) xtra_netpair} 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

515 
end 
42790  516 
else cs 
517 
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) 

518 
error ("Illformed introduction rule\n" ^ Display.string_of_thm_without_context th); 

1800  519 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

520 
fun delE th 
42790  521 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
522 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

523 
if mem_thm hazEs th then 

524 
let val th' = classical_rule (flat_rule th) in 

525 
CS 

526 
{haz_netpair = delete ([], [th']) haz_netpair, 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

527 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
42790  528 
safeIs = safeIs, 
529 
safeEs = safeEs, 

530 
hazIs = hazIs, 

531 
hazEs = rem_thm th hazEs, 

532 
swrappers = swrappers, 

533 
uwrappers = uwrappers, 

9938  534 
safe0_netpair = safe0_netpair, 
535 
safep_netpair = safep_netpair, 

12401  536 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
42790  537 
end 
538 
else cs; 

1800  539 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

540 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

541 
fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
42790  542 
let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in 
18691  543 
if mem_thm safeIs th orelse mem_thm safeEs th orelse 
544 
mem_thm hazIs th orelse mem_thm hazEs th orelse 

545 
mem_thm safeEs th' orelse mem_thm hazEs th' 

12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

546 
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs))))) 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset

547 
else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs) 
9938  548 
end; 
1800  549 

18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

550 
fun cs delrules ths = fold delrule ths cs; 
1800  551 

552 

42790  553 
fun make_elim th = 
554 
if has_fewer_prems 1 th then 

555 
error ("Illformed destruction rule\n" ^ Display.string_of_thm_without_context th) 

556 
else Tactic.make_elim th; 

557 

558 
fun cs addSIs ths = fold_rev (addSI NONE) ths cs; 

559 
fun cs addSEs ths = fold_rev (addSE NONE) ths cs; 

560 
fun cs addSDs ths = cs addSEs (map make_elim ths); 

561 
fun cs addIs ths = fold_rev (addI NONE) ths cs; 

562 
fun cs addEs ths = fold_rev (addE NONE) ths cs; 

563 
fun cs addDs ths = cs addEs (map make_elim ths); 

564 

565 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

566 
(*** Modifying the wrapper tacticals ***) 
22674  567 
fun map_swrappers f 
568 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

569 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

570 
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

571 
swrappers = f swrappers, uwrappers = uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

572 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  573 
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

574 

22674  575 
fun map_uwrappers f 
576 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

577 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

578 
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

579 
swrappers = swrappers, uwrappers = f uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

580 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  581 
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

582 

22674  583 
fun update_warn msg (p as (key : string, _)) xs = 
42790  584 
(if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); 
22674  585 

586 
fun delete_warn msg (key : string) xs = 

587 
if AList.defined (op =) xs key then AList.delete (op =) key xs 

42790  588 
else (warning msg; xs); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

589 

4651  590 
(*Add/replace a safe wrapper*) 
22674  591 
fun cs addSWrapper new_swrapper = map_swrappers 
592 
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

4651  593 

594 
(*Add/replace an unsafe wrapper*) 

22674  595 
fun cs addWrapper new_uwrapper = map_uwrappers 
596 
(update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

597 

4651  598 
(*Remove a safe wrapper*) 
22674  599 
fun cs delSWrapper name = map_swrappers 
600 
(delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

601 

4651  602 
(*Remove an unsafe wrapper*) 
22674  603 
fun cs delWrapper name = map_uwrappers 
604 
(delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

605 

11168  606 
(* compose a safe tactic alternatively before/after safe_step_tac *) 
42790  607 
fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); 
608 
fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

609 

11168  610 
(*compose a tactic alternatively before/after the step tactic *) 
42790  611 
fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); 
612 
fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

613 

42790  614 
fun cs addD2 (name, thm) = cs addafter (name, datac thm 1); 
615 
fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1); 

616 
fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); 

617 
fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

618 

1711  619 
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. 
620 
Merging the term nets may look more efficient, but the rather delicate 

621 
treatment of priority might get muddled up.*) 

22674  622 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  623 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  624 
swrappers, uwrappers, ...}) = 
24358  625 
if pointer_eq (cs, cs') then cs 
626 
else 

627 
let 

628 
val safeIs' = fold rem_thm safeIs safeIs2; 

629 
val safeEs' = fold rem_thm safeEs safeEs2; 

630 
val hazIs' = fold rem_thm hazIs hazIs2; 

631 
val hazEs' = fold rem_thm hazEs hazEs2; 

42790  632 
val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs'; 
633 
val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; 

634 
val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; 

24358  635 
in cs3 end; 
1711  636 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

637 

1800  638 
(**** Simple tactics for theorem proving ****) 
0  639 

640 
(*Attack subgoals using safe inferences  matching, not resolution*) 

42790  641 
fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) = 
4651  642 
appSWrappers cs (FIRST' [ 
9938  643 
eq_assume_tac, 
644 
eq_mp_tac, 

645 
bimatch_from_nets_tac safe0_netpair, 

646 
FIRST' hyp_subst_tacs, 

647 
bimatch_from_nets_tac safep_netpair]); 

0  648 

5757  649 
(*Repeatedly attack a subgoal using safe inferences  it's deterministic!*) 
42790  650 
fun safe_steps_tac cs = 
651 
REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 

5757  652 

0  653 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
5757  654 
fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

655 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

656 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

657 
(*** Clarify_tac: do safe steps without causing branching ***) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

658 

42790  659 
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

660 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

661 
(*version of bimatch_from_nets_tac that only applies rules that 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

662 
create precisely n subgoals.*) 
10736  663 
fun n_bimatch_from_nets_tac n = 
42790  664 
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

665 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

666 
fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

667 
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

668 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

669 
(*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

670 
fun bimatch2_tac netpair i = 
42790  671 
n_bimatch_from_nets_tac 2 netpair i THEN 
672 
(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

673 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

674 
(*Attack subgoals using safe inferences  matching, not resolution*) 
10736  675 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  676 
appSWrappers cs (FIRST' [ 
9938  677 
eq_assume_contr_tac, 
678 
bimatch_from_nets_tac safe0_netpair, 

679 
FIRST' hyp_subst_tacs, 

680 
n_bimatch_from_nets_tac 1 safep_netpair, 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

681 
bimatch2_tac safep_netpair]); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

682 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

683 
fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

684 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

685 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

686 
(*** Unsafe steps instantiate variables or lose information ***) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

687 

4066  688 
(*Backtracking is allowed among the various these unsafe ways of 
689 
proving a subgoal. *) 

32862  690 
fun inst0_step_tac (CS {safe0_netpair, ...}) = 
691 
assume_tac APPEND' 

692 
contr_tac APPEND' 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

693 
biresolve_from_nets_tac safe0_netpair; 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

694 

4066  695 
(*These unsafe steps could generate more subgoals.*) 
32862  696 
fun instp_step_tac (CS {safep_netpair, ...}) = 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

697 
biresolve_from_nets_tac safep_netpair; 
0  698 

699 
(*These steps could instantiate variables and are therefore unsafe.*) 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

700 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  701 

10736  702 
fun haz_step_tac (CS{haz_netpair,...}) = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

703 
biresolve_from_nets_tac haz_netpair; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

704 

0  705 
(*Single step for the prover. FAILS unless it makes progress. *) 
42790  706 
fun step_tac cs i = 
707 
safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i; 

0  708 

709 
(*Using a "safe" rule to instantiate variables is unsafe. This tactic 

710 
allows backtracking from "safe" rules to "unsafe" rules here.*) 

42790  711 
fun slow_step_tac cs i = 
712 
safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i; 

0  713 

1800  714 
(**** The following tactics all fail unless they solve one goal ****) 
0  715 

716 
(*Dumb but fast*) 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

717 
fun fast_tac cs = 
35625  718 
Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 
0  719 

720 
(*Slower but smarter than fast_tac*) 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

721 
fun best_tac cs = 
35625  722 
Object_Logic.atomize_prems_tac THEN' 
0  723 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 
724 

9402  725 
(*even a bit smarter than best_tac*) 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

726 
fun first_best_tac cs = 
35625  727 
Object_Logic.atomize_prems_tac THEN' 
9402  728 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs))); 
729 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

730 
fun slow_tac cs = 
35625  731 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

732 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  733 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

734 
fun slow_best_tac cs = 
35625  735 
Object_Logic.atomize_prems_tac THEN' 
0  736 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 
737 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

738 

10736  739 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
42790  740 
val weight_ASTAR = Unsynchronized.ref 5; (* FIXME argument / config option !? *) 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

741 

10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

742 
fun astar_tac cs = 
35625  743 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

744 
SELECT_GOAL 
42790  745 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev) 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

746 
(step_tac cs 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

747 

10736  748 
fun slow_astar_tac cs = 
35625  749 
Object_Logic.atomize_prems_tac THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

750 
SELECT_GOAL 
42790  751 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev) 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

752 
(slow_step_tac cs 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

753 

42790  754 

1800  755 
(**** 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

756 
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

757 
easy theorems faster, but loses completeness  and many of the harder 
1800  758 
theorems such as 43. ****) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

759 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

760 
(*Nondeterministic! Could always expand the first unsafe connective. 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

761 
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

762 
greater search depth required.*) 
32863  763 
fun dup_step_tac (CS {dup_netpair, ...}) = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

764 
biresolve_from_nets_tac dup_netpair; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

765 

5523  766 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  767 
local 
42790  768 
fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs); 
769 
in 

770 
fun depth_tac cs m i state = SELECT_GOAL 

771 
(safe_steps_tac cs 1 THEN_ELSE 

772 
(DEPTH_SOLVE (depth_tac cs m 1), 

773 
inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac 

774 
(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m  1) 1)))) i state; 

5757  775 
end; 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

776 

10736  777 
(*Search, with depth bound m. 
2173  778 
This is the "entry point", which does safe inferences first.*) 
42790  779 
fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) => 
780 
let val deti = 

781 
(*No Vars in the goal? No need to backtrack between goals.*) 

782 
if exists_subterm (fn Var _ => true  _ => false) prem then DETERM else I 

783 
in 

784 
SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i 

785 
end); 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

786 

42790  787 
fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

788 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

789 

1724  790 

15036  791 
(** context dependent claset components **) 
792 

793 
datatype context_cs = ContextCS of 

794 
{swrappers: (string * (Proof.context > wrapper)) list, 

795 
uwrappers: (string * (Proof.context > wrapper)) list}; 

796 

797 
fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) = 

798 
let 

799 
fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt)); 

800 
in 

22674  801 
cs 
802 
> fold_rev (add_wrapper (op addSWrapper)) swrappers 

15036  803 
> fold_rev (add_wrapper (op addWrapper)) uwrappers 
804 
end; 

805 

806 
fun make_context_cs (swrappers, uwrappers) = 

807 
ContextCS {swrappers = swrappers, uwrappers = uwrappers}; 

808 

809 
val empty_context_cs = make_context_cs ([], []); 

810 

811 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

24358  812 
if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1 
813 
else 

814 
let 

815 
val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1; 

816 
val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2; 

817 
val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2); 

818 
val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2); 

819 
in make_context_cs (swrappers', uwrappers') end; 

15036  820 

821 

822 

17880  823 
(** claset data **) 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

824 

24021  825 
(* global clasets *) 
1724  826 

33522  827 
structure GlobalClaset = Theory_Data 
22846  828 
( 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

829 
type T = claset * context_cs; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

830 
val empty = (empty_cs, empty_context_cs); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

831 
val extend = I; 
33522  832 
fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) = 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

833 
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); 
22846  834 
); 
1724  835 

32261  836 
val get_global_claset = #1 o GlobalClaset.get; 
837 
val map_global_claset = GlobalClaset.map o apfst; 

17880  838 

42361  839 
val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of; 
15036  840 
fun map_context_cs f = GlobalClaset.map (apsnd 
841 
(fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers)))); 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

842 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

843 
fun global_claset_of thy = 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

844 
let val (cs, ctxt_cs) = GlobalClaset.get thy 
42361  845 
in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end; 
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

846 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

847 

15036  848 
(* context dependent components *) 
849 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

850 
fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper))); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

851 
fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name))); 
15036  852 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

853 
fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper))); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

854 
fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name))); 
15036  855 

856 

24021  857 
(* local clasets *) 
5841  858 

33519  859 
structure LocalClaset = Proof_Data 
22846  860 
( 
5841  861 
type T = claset; 
32261  862 
val init = get_global_claset; 
22846  863 
); 
5841  864 

32261  865 
val get_claset = LocalClaset.get; 
866 
val put_claset = LocalClaset.put; 

867 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

868 
fun claset_of ctxt = 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

869 
context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); 
22846  870 

5841  871 

24021  872 
(* generic clasets *) 
873 

32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

874 
val get_cs = Context.cases global_claset_of claset_of; 
32261  875 
fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f); 
24021  876 

877 

5885  878 
(* attributes *) 
879 

18728  880 
fun attrib f = Thm.declaration_attribute (fn th => 
32261  881 
Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th))); 
5885  882 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

883 
fun safe_dest w = attrib (addSE w o make_elim); 
18691  884 
val safe_elim = attrib o addSE; 
885 
val safe_intro = attrib o addSI; 

21689
58abd6d8abd1
Removal of theorem tagging, which the ATP linkup no longer requires,
paulson
parents:
21687
diff
changeset

886 
fun haz_dest w = attrib (addE w o make_elim); 
18691  887 
val haz_elim = attrib o addE; 
888 
val haz_intro = attrib o addI; 

33369  889 
val rule_del = attrib delrule o Context_Rules.rule_del; 
5885  890 

891 

10736  892 
end; 
5841  893 

894 

895 

5885  896 
(** concrete syntax of attributes **) 
5841  897 

898 
val introN = "intro"; 

899 
val elimN = "elim"; 

900 
val destN = "dest"; 

901 

30528  902 
val setup_attrs = 
903 
Attrib.setup @{binding swapped} (Scan.succeed swapped) 

904 
"classical swap of introduction rule" #> 

33369  905 
Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query) 
30528  906 
"declaration of Classical destruction rule" #> 
33369  907 
Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query) 
30528  908 
"declaration of Classical elimination rule" #> 
33369  909 
Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query) 
30528  910 
"declaration of Classical introduction rule" #> 
911 
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) 

912 
"remove declaration of intro/elim/dest rule"; 

5841  913 

914 

915 

7230  916 
(** proof methods **) 
917 

918 
local 

919 

30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

920 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  921 
let 
33369  922 
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; 
32148
253f6808dabe
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

923 
val CS {xtra_netpair, ...} = claset_of ctxt; 
33369  924 
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

925 
val rules = rules1 @ rules2 @ rules3 @ rules4; 
18223  926 
val ruleq = Drule.multi_resolves facts rules; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

927 
in 
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

928 
Method.trace ctxt rules; 
32952  929 
fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq 
18834  930 
end) 
21687  931 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  932 

30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

933 
in 
7281  934 

30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

935 
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

936 
 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

937 

983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

938 
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

939 
HEADGOAL (rule_tac ctxt rules facts) ORELSE 
26470  940 
Class.default_intro_tac ctxt facts; 
10309  941 

7230  942 
end; 
5841  943 

944 

7230  945 
(* contradiction method *) 
6502  946 

7425  947 
val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl]; 
6502  948 

949 

950 
(* automatic methods *) 

5841  951 

5927  952 
val cla_modifiers = 
18728  953 
[Args.$$$ destN  Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier), 
954 
Args.$$$ destN  Args.colon >> K (I, haz_dest NONE), 

955 
Args.$$$ elimN  Args.bang_colon >> K (I, safe_elim NONE), 

956 
Args.$$$ elimN  Args.colon >> K (I, haz_elim NONE), 

957 
Args.$$$ introN  Args.bang_colon >> K (I, safe_intro NONE), 

958 
Args.$$$ introN  Args.colon >> K (I, haz_intro NONE), 

959 
Args.del  Args.colon >> K (I, rule_del)]; 

5927  960 

35613  961 
fun cla_meth tac ctxt = METHOD (fn facts => 
962 
ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt)); 

7132  963 

35613  964 
fun cla_meth' tac ctxt = METHOD (fn facts => 
965 
HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt))); 

5841  966 

35613  967 
fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac); 
968 
fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac); 

5841  969 

970 

971 

972 
(** setup_methods **) 

973 

30541  974 
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

975 
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

976 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules))) 
30541  977 
"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

978 
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

979 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) 
30541  980 
"apply some intro/elim rule (potentially classical)" #> 
981 
Method.setup @{binding contradiction} (Scan.succeed (K contradiction)) 

982 
"proof by contradiction" #> 

983 
Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac)) 

984 
"repeatedly apply safe steps" #> 

985 
Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depthfirst)" #> 

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

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

988 
Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4)) 

989 
"classical prover (iterative deepening)" #> 

990 
Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) 

991 
"classical prover (apply safe rules)"; 

5841  992 

993 

994 

995 
(** theory setup **) 

996 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

997 
val setup = setup_attrs #> setup_methods; 
5841  998 

999 

8667  1000 

1001 
(** outer syntax **) 

1002 

24867  1003 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

1004 
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

1005 
Keyword.diag 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26470
diff
changeset

1006 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o 
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

1007 
Toplevel.keep (fn state => 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

1008 
let val ctxt = Toplevel.context_of state 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42361
diff
changeset

1009 
in print_cs ctxt (claset_of ctxt) end))); 
8667  1010 

5841  1011 
end; 