author  wenzelm 
Fri, 13 May 2011 16:03:03 +0200  
changeset 42792  85fb70b0c5e8 
parent 42791  36f787ae5f70 
child 42793  88bee9f6eec7 
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 astar_tac: claset > int > tactic 

82 
val slow_astar_tac: claset > int > tactic 

83 
val best_tac: claset > int > tactic 

84 
val first_best_tac: claset > int > tactic 

85 
val slow_best_tac: claset > int > tactic 

86 
val depth_tac: claset > int > int > tactic 

87 
val deepen_tac: claset > int > int > tactic 

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

88 

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

91 
val dup_intr: thm > thm 

92 
val dup_step_tac: claset > int > tactic 

93 
val eq_mp_tac: int > tactic 

94 
val haz_step_tac: claset > int > tactic 

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

96 
val mp_tac: int > tactic 

97 
val safe_tac: claset > tactic 

98 
val safe_steps_tac: claset > int > tactic 

99 
val safe_step_tac: claset > int > tactic 

100 
val clarify_tac: claset > int > tactic 

101 
val clarify_step_tac: claset > int > tactic 

102 
val step_tac: claset > int > tactic 

103 
val slow_step_tac: claset > int > tactic 

104 
val swapify: thm list > thm list 

105 
val swap_res_tac: thm list > int > tactic 

106 
val inst_step_tac: claset > int > tactic 

107 
val inst0_step_tac: claset > int > tactic 

108 
val instp_step_tac: claset > int > tactic 

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

109 
end; 
1724  110 

5841  111 
signature CLASSICAL = 
112 
sig 

113 
include BASIC_CLASSICAL 

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

114 
val classical_rule: thm > thm 
15036  115 
val add_context_safe_wrapper: string * (Proof.context > wrapper) > theory > theory 
116 
val del_context_safe_wrapper: string > theory > theory 

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

118 
val del_context_unsafe_wrapper: string > theory > theory 

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

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

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

125 
val safe_intro: int option > attribute 

126 
val haz_dest: int option > attribute 

127 
val haz_elim: int option > attribute 

128 
val haz_intro: int option > attribute 

129 
val rule_del: attribute 

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

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

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

0  138 

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

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

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

143 

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

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

145 
Classical reasoning requires stronger elimination rules. For 
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

146 
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

147 

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

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

149 

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

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

152 

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

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

154 
*) 
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 
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

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

158 
let 
42792  159 
val rule' = rule RS Data.classical; 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

173 
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

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

175 

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

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

178 

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

179 

1800  180 
(*** Useful tactics for classical reasoning ***) 
0  181 

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

42792  185 
val contr_tac = 
186 
eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac); 

0  187 

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

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

189 
Could do the same thing for P<>Q and P... *) 
42792  190 
fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i; 
0  191 

192 
(*Like mp_tac but instantiates no variables*) 

42792  193 
fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; 
0  194 

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

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

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

200 
trying rules in order. *) 

10736  201 
fun swap_res_tac rls = 
42792  202 
let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in 
203 
assume_tac ORELSE' 

204 
contr_tac ORELSE' 

205 
biresolve_tac (fold_rev addrl rls []) 

206 
end; 

0  207 

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

208 
(*Duplication of hazardous rules, for complete provers*) 
42792  209 
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

210 

6967  211 
fun dup_elim th = 
36546  212 
let 
213 
val rl = (th RSN (2, revcut_rl)) > Thm.assumption 2 > Seq.hd; 

42361  214 
val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); 
36546  215 
in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; 
216 

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

217 

1800  218 
(**** Classical rule sets ****) 
0  219 

220 
datatype claset = 

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

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

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

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

9938  226 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 
12401  227 
safe0_netpair : netpair, (*nets for trivial cases*) 
228 
safep_netpair : netpair, (*nets for >0 subgoals*) 

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

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

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

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

233 
(*Desired invariants are 
9938  234 
safe0_netpair = build safe0_brls, 
235 
safep_netpair = build safep_brls, 

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

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

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

239 

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

241 
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

242 
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

243 
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

244 
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

245 
*) 
0  246 

6502  247 
val empty_netpair = (Net.empty, Net.empty); 
248 

10736  249 
val empty_cs = 
9938  250 
CS{safeIs = [], 
251 
safeEs = [], 

252 
hazIs = [], 

253 
hazEs = [], 

4651  254 
swrappers = [], 
255 
uwrappers = [], 

6502  256 
safe0_netpair = empty_netpair, 
257 
safep_netpair = empty_netpair, 

258 
haz_netpair = empty_netpair, 

6955  259 
dup_netpair = empty_netpair, 
260 
xtra_netpair = empty_netpair}; 

0  261 

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

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

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

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

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

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

8727  270 
> Pretty.chunks > Pretty.writeln 
3546  271 
end; 
0  272 

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

274 

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

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

277 

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

278 

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

280 

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

281 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  282 
***) 
0  283 

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

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

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

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

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

288 

12401  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 @ map (pair false) intrs; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

291 

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

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

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

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

298 

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

10736  301 

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

303 

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

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

305 
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

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

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

309 

23178  310 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  311 
fun delete x = delete_tagged_list (joinrules x); 
12401  312 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  313 

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

314 
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

315 
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

316 

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

319 

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

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

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

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

324 
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

325 

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

326 

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

328 

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

332 
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

333 
else 
42790  334 
let 
335 
val th' = flat_rule th; 

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

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

339 
val nE = length safeEs; 

340 
val _ = warn_other th cs; 

341 
in 

342 
CS 

343 
{safeIs = th::safeIs, 

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

344 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
9938  345 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
42790  346 
safeEs = safeEs, 
347 
hazIs = hazIs, 

348 
hazEs = hazEs, 

349 
swrappers = swrappers, 

350 
uwrappers = uwrappers, 

351 
haz_netpair = haz_netpair, 

352 
dup_netpair = dup_netpair, 

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

355 

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

359 
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

360 
else if has_fewer_prems 1 th then 
42790  361 
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

362 
else 
42790  363 
let 
364 
val th' = classical_rule (flat_rule th); 

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

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

368 
val nE = length safeEs + 1; 

369 
val _ = warn_other th cs; 

370 
in 

371 
CS 

372 
{safeEs = th::safeEs, 

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

373 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
9938  374 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
42790  375 
safeIs = safeIs, 
376 
hazIs = hazIs, 

377 
hazEs = hazEs, 

378 
swrappers = swrappers, 

379 
uwrappers = uwrappers, 

380 
haz_netpair = haz_netpair, 

381 
dup_netpair = dup_netpair, 

18691  382 
xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} 
42790  383 
end; 
0  384 

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

385 

1800  386 
(*** Hazardous (unsafe) rules ***) 
0  387 

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

391 
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

392 
else 
42790  393 
let 
394 
val th' = flat_rule th; 

395 
val nI = length hazIs + 1; 

396 
val nE = length hazEs; 

397 
val _ = warn_other th cs; 

398 
in 

399 
CS 

400 
{hazIs = th :: hazIs, 

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

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

403 
safeIs = safeIs, 

404 
safeEs = safeEs, 

405 
hazEs = hazEs, 

406 
swrappers = swrappers, 

407 
uwrappers = uwrappers, 

9938  408 
safe0_netpair = safe0_netpair, 
409 
safep_netpair = safep_netpair, 

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

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

413 
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

414 

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

418 
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

419 
else if has_fewer_prems 1 th then 
42790  420 
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

421 
else 
42790  422 
let 
423 
val th' = classical_rule (flat_rule th); 

424 
val nI = length hazIs; 

425 
val nE = length hazEs + 1; 

426 
val _ = warn_other th cs; 

427 
in 

428 
CS 

429 
{hazEs = th :: hazEs, 

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

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

432 
safeIs = safeIs, 

433 
safeEs = safeEs, 

434 
hazIs = hazIs, 

435 
swrappers = swrappers, 

436 
uwrappers = uwrappers, 

9938  437 
safe0_netpair = safe0_netpair, 
438 
safep_netpair = safep_netpair, 

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

0  441 

442 

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

443 

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

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

452 
if mem_thm safeIs th then 

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

453 
let 
42790  454 
val th' = flat_rule th; 
455 
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; 

456 
in 

457 
CS 

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

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

460 
safeIs = rem_thm th safeIs, 

461 
safeEs = safeEs, 

462 
hazIs = hazIs, 

463 
hazEs = hazEs, 

464 
swrappers = swrappers, 

465 
uwrappers = uwrappers, 

466 
haz_netpair = haz_netpair, 

467 
dup_netpair = dup_netpair, 

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

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

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

470 
else cs; 
1800  471 

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

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

475 
if mem_thm safeEs th then 

476 
let 

477 
val th' = classical_rule (flat_rule th); 

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

479 
in 

480 
CS 

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

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

483 
safeIs = safeIs, 

484 
safeEs = rem_thm th safeEs, 

485 
hazIs = hazIs, 

486 
hazEs = hazEs, 

487 
swrappers = swrappers, 

488 
uwrappers = uwrappers, 

489 
haz_netpair = haz_netpair, 

490 
dup_netpair = dup_netpair, 

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

492 
end 

493 
else cs; 

1800  494 

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

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

498 
if mem_thm hazIs th then 

499 
let val th' = flat_rule th in 

500 
CS 

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

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

502 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
42790  503 
safeIs = safeIs, 
504 
safeEs = safeEs, 

505 
hazIs = rem_thm th hazIs, 

506 
hazEs = hazEs, 

507 
swrappers = swrappers, 

508 
uwrappers = uwrappers, 

9938  509 
safe0_netpair = safe0_netpair, 
510 
safep_netpair = safep_netpair, 

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

512 
end 
42790  513 
else cs 
514 
handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) 

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

1800  516 

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

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

520 
if mem_thm hazEs th then 

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

522 
CS 

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

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

524 
dup_netpair = delete ([], [dup_elim th']) dup_netpair, 
42790  525 
safeIs = safeIs, 
526 
safeEs = safeEs, 

527 
hazIs = hazIs, 

528 
hazEs = rem_thm th hazEs, 

529 
swrappers = swrappers, 

530 
uwrappers = uwrappers, 

9938  531 
safe0_netpair = safe0_netpair, 
532 
safep_netpair = safep_netpair, 

12401  533 
xtra_netpair = delete' ([], [th]) xtra_netpair} 
42790  534 
end 
535 
else cs; 

1800  536 

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

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

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

542 
mem_thm safeEs th' orelse mem_thm hazEs th' 

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

543 
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

544 
else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs) 
9938  545 
end; 
1800  546 

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

547 
fun cs delrules ths = fold delrule ths cs; 
1800  548 

549 

42790  550 
fun make_elim th = 
551 
if has_fewer_prems 1 th then 

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

553 
else Tactic.make_elim th; 

554 

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

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

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

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

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

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

561 

562 

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

563 
(*** Modifying the wrapper tacticals ***) 
22674  564 
fun map_swrappers f 
565 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

569 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  570 
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

571 

22674  572 
fun map_uwrappers f 
573 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

577 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  578 
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

579 

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

583 
fun delete_warn msg (key : string) xs = 

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

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

586 

4651  587 
(*Add/replace a safe wrapper*) 
22674  588 
fun cs addSWrapper new_swrapper = map_swrappers 
589 
(update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; 

4651  590 

591 
(*Add/replace an unsafe wrapper*) 

22674  592 
fun cs addWrapper new_uwrapper = map_uwrappers 
593 
(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

594 

4651  595 
(*Remove a safe wrapper*) 
22674  596 
fun cs delSWrapper name = map_swrappers 
597 
(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

598 

4651  599 
(*Remove an unsafe wrapper*) 
22674  600 
fun cs delWrapper name = map_uwrappers 
601 
(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

602 

11168  603 
(* compose a safe tactic alternatively before/after safe_step_tac *) 
42790  604 
fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); 
605 
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

606 

11168  607 
(*compose a tactic alternatively before/after the step tactic *) 
42790  608 
fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); 
609 
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

610 

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

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

614 
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

615 

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

618 
treatment of priority might get muddled up.*) 

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

624 
let 

625 
val safeIs' = fold rem_thm safeIs safeIs2; 

626 
val safeEs' = fold rem_thm safeEs safeEs2; 

627 
val hazIs' = fold rem_thm hazIs hazIs2; 

628 
val hazEs' = fold rem_thm hazEs hazEs2; 

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

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

24358  632 
in cs3 end; 
1711  633 

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

634 

1800  635 
(**** Simple tactics for theorem proving ****) 
0  636 

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

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

642 
bimatch_from_nets_tac safe0_netpair, 

42792  643 
FIRST' Data.hyp_subst_tacs, 
9938  644 
bimatch_from_nets_tac safep_netpair]); 
0  645 

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

5757  649 

0  650 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
5757  651 
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

652 

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

653 

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

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

655 

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

657 

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

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

659 
create precisely n subgoals.*) 
10736  660 
fun n_bimatch_from_nets_tac n = 
42790  661 
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

662 

42792  663 
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

664 
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

665 

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

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

667 
fun bimatch2_tac netpair i = 
42790  668 
n_bimatch_from_nets_tac 2 netpair i THEN 
669 
(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

670 

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

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

42792  676 
FIRST' Data.hyp_subst_tacs, 
9938  677 
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

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

679 

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

680 
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

681 

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

684 

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

32862  687 
fun inst0_step_tac (CS {safe0_netpair, ...}) = 
688 
assume_tac APPEND' 

689 
contr_tac APPEND' 

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

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

691 

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

694 
biresolve_from_nets_tac safep_netpair; 
0  695 

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

697 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  698 

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

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

701 

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

0  705 

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

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

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

0  710 

42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

711 

1800  712 
(**** The following tactics all fail unless they solve one goal ****) 
0  713 

714 
(*Dumb but fast*) 

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

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

718 
(*Slower but smarter than fast_tac*) 

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

719 
fun best_tac cs = 
35625  720 
Object_Logic.atomize_prems_tac THEN' 
42792  721 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1)); 
0  722 

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

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

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

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

730 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 
0  731 

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

732 
fun slow_best_tac cs = 
35625  733 
Object_Logic.atomize_prems_tac THEN' 
42792  734 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1)); 
0  735 

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

736 

10736  737 
(***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

738 

36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

739 
val weight_ASTAR = 5; 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

740 

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

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

743 
SELECT_GOAL 
42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

744 
(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

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

746 

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

749 
SELECT_GOAL 
42791
36f787ae5f70
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
wenzelm
parents:
42790
diff
changeset

750 
(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

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

752 

42790  753 

1800  754 
(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

755 
of much experimentation! Changing APPEND to ORELSE below would prove 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

758 

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

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

760 
That's hard to implement and did not perform better in experiments, due to 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

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

764 

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

769 
fun depth_tac cs m i state = SELECT_GOAL 

770 
(safe_steps_tac cs 1 THEN_ELSE 

771 
(DEPTH_SOLVE (depth_tac cs m 1), 

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

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

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

775 

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

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

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

782 
in 

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

784 
end); 

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

785 

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

787 

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

788 

1724  789 

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

792 
datatype context_cs = ContextCS of 

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

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

795 

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

797 
let 

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

799 
in 

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

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

804 

805 
fun make_context_cs (swrappers, uwrappers) = 

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

807 

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

809 

810 
fun merge_context_cs (ctxt_cs1, ctxt_cs2) = 

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

813 
let 

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

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

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

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

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

15036  819 

820 

821 

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

823 

24021  824 
(* global clasets *) 
1724  825 

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

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

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

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

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

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

17880  837 

42361  838 
val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of; 
15036  839 
fun map_context_cs f = GlobalClaset.map (apsnd 
840 
(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

841 

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

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

843 
let val (cs, ctxt_cs) = GlobalClaset.get thy 
42361  844 
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

845 

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

846 

15036  847 
(* context dependent components *) 
848 

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

849 
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

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

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

852 
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

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

855 

24021  856 
(* local clasets *) 
5841  857 

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

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

866 

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

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

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

5841  870 

24021  871 
(* generic clasets *) 
872 

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

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

876 

5885  877 
(* attributes *) 
878 

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

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

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

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

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

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

890 

5841  891 

5885  892 
(** concrete syntax of attributes **) 
5841  893 

894 
val introN = "intro"; 

895 
val elimN = "elim"; 

896 
val destN = "dest"; 

897 

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

900 
"classical swap of introduction rule" #> 

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

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

5841  909 

910 

911 

7230  912 
(** proof methods **) 
913 

914 
local 

915 

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

916 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  917 
let 
33369  918 
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

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

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

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

924 
Method.trace ctxt rules; 
32952  925 
fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq 
18834  926 
end) 
21687  927 
THEN_ALL_NEW Goal.norm_hhf_tac; 
5841  928 

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

929 
in 
7281  930 

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

931 
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

932 
 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

933 

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

934 
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

935 
HEADGOAL (rule_tac ctxt rules facts) ORELSE 
26470  936 
Class.default_intro_tac ctxt facts; 
10309  937 

7230  938 
end; 
5841  939 

940 

7230  941 
(* contradiction method *) 
6502  942 

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

945 

946 
(* automatic methods *) 

5841  947 

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

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

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

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

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

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

5927  956 

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

7132  959 

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

5841  962 

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

5841  965 

966 

967 

968 
(** setup_methods **) 

969 

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

971 
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

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

974 
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

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

978 
"proof by contradiction" #> 

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

980 
"repeatedly apply safe steps" #> 

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

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

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

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

985 
"classical prover (iterative deepening)" #> 

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

987 
"classical prover (apply safe rules)"; 

5841  988 

989 

990 

991 
(** theory setup **) 

992 

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

993 
val setup = setup_attrs #> setup_methods; 
5841  994 

995 

8667  996 

997 
(** outer syntax **) 

998 

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

1000 
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

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

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

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

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

1005 
in print_cs ctxt (claset_of ctxt) end))); 
8667  1006 

5841  1007 
end; 