author  wenzelm 
Fri, 23 Nov 2018 16:43:11 +0100  
changeset 69334  6b49700da068 
parent 67649  1e1782c1aedf 
child 69593  3dda49e08b9d 
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 

60943  7 
Rules must be classified as intro, elim, safe, 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 

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

22 
sig 
42790  23 
val imp_elim: thm (* P > Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) 
24 
val not_elim: thm (* ~P ==> P ==> R *) 

25 
val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) 

26 
val classical: thm (* (~ P ==> P) ==> P *) 

50062  27 
val sizef: thm > int (* size function for BEST_FIRST, typically size_of_thm *) 
51798  28 
val hyp_subst_tacs: (Proof.context > int > tactic) list (* optional tactics for 
29 
substitution in the hypotheses; assumed to be safe! *) 

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

30 
end; 
0  31 

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

33 
sig 
42812  34 
type wrapper = (int > tactic) > int > tactic 
0  35 
type claset 
42793  36 
val print_claset: Proof.context > unit 
37 
val addDs: Proof.context * thm list > Proof.context 

38 
val addEs: Proof.context * thm list > Proof.context 

39 
val addIs: Proof.context * thm list > Proof.context 

40 
val addSDs: Proof.context * thm list > Proof.context 

41 
val addSEs: Proof.context * thm list > Proof.context 

42 
val addSIs: Proof.context * thm list > Proof.context 

43 
val delrules: Proof.context * thm list > Proof.context 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

44 
val addSWrapper: Proof.context * (string * (Proof.context > wrapper)) > Proof.context 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

45 
val delSWrapper: Proof.context * string > Proof.context 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

46 
val addWrapper: Proof.context * (string * (Proof.context > wrapper)) > Proof.context 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

47 
val delWrapper: Proof.context * string > Proof.context 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

48 
val addSbefore: Proof.context * (string * (Proof.context > int > tactic)) > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

49 
val addSafter: Proof.context * (string * (Proof.context > int > tactic)) > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

50 
val addbefore: Proof.context * (string * (Proof.context > int > tactic)) > Proof.context 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

51 
val addafter: Proof.context * (string * (Proof.context > int > tactic)) > Proof.context 
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

52 
val addD2: Proof.context * (string * thm) > Proof.context 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

53 
val addE2: Proof.context * (string * thm) > Proof.context 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

54 
val addSD2: Proof.context * (string * thm) > Proof.context 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

55 
val addSE2: Proof.context * (string * thm) > Proof.context 
42793  56 
val appSWrappers: Proof.context > wrapper 
57 
val appWrappers: Proof.context > wrapper 

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

58 

42790  59 
val claset_of: Proof.context > claset 
42793  60 
val put_claset: claset > Proof.context > Proof.context 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

61 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

62 
val map_theory_claset: (Proof.context > Proof.context) > theory > theory 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

63 

42793  64 
val fast_tac: Proof.context > int > tactic 
65 
val slow_tac: Proof.context > int > tactic 

66 
val astar_tac: Proof.context > int > tactic 

67 
val slow_astar_tac: Proof.context > int > tactic 

68 
val best_tac: Proof.context > int > tactic 

69 
val first_best_tac: Proof.context > int > tactic 

70 
val slow_best_tac: Proof.context > int > tactic 

71 
val depth_tac: Proof.context > int > int > tactic 

72 
val deepen_tac: Proof.context > int > int > tactic 

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

73 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

74 
val contr_tac: Proof.context > int > tactic 
59970  75 
val dup_elim: Proof.context > thm > thm 
42790  76 
val dup_intr: thm > thm 
42793  77 
val dup_step_tac: Proof.context > int > tactic 
58957  78 
val eq_mp_tac: Proof.context > int > tactic 
60943  79 
val unsafe_step_tac: Proof.context > int > tactic 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

80 
val mp_tac: Proof.context > int > tactic 
42793  81 
val safe_tac: Proof.context > tactic 
82 
val safe_steps_tac: Proof.context > int > tactic 

83 
val safe_step_tac: Proof.context > int > tactic 

84 
val clarify_tac: Proof.context > int > tactic 

85 
val clarify_step_tac: Proof.context > int > tactic 

86 
val step_tac: Proof.context > int > tactic 

87 
val slow_step_tac: Proof.context > int > tactic 

42790  88 
val swapify: thm list > thm list 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

89 
val swap_res_tac: Proof.context > thm list > int > tactic 
42793  90 
val inst_step_tac: Proof.context > int > tactic 
91 
val inst0_step_tac: Proof.context > int > tactic 

92 
val instp_step_tac: Proof.context > int > tactic 

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

93 
end; 
1724  94 

5841  95 
signature CLASSICAL = 
96 
sig 

97 
include BASIC_CLASSICAL 

59970  98 
val classical_rule: Proof.context > thm > thm 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

99 
type rule = thm * (thm * thm list) * (thm * thm list) 
42812  100 
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net 
101 
val rep_cs: claset > 

60945  102 
{safeIs: rule Item_Net.T, 
103 
safeEs: rule Item_Net.T, 

104 
unsafeIs: rule Item_Net.T, 

105 
unsafeEs: rule Item_Net.T, 

42812  106 
swrappers: (string * (Proof.context > wrapper)) list, 
107 
uwrappers: (string * (Proof.context > wrapper)) list, 

108 
safe0_netpair: netpair, 

109 
safep_netpair: netpair, 

60943  110 
unsafe_netpair: netpair, 
42812  111 
dup_netpair: netpair, 
60942  112 
extra_netpair: Context_Rules.netpair} 
24021  113 
val get_cs: Context.generic > claset 
114 
val map_cs: (claset > claset) > Context.generic > Context.generic 

18728  115 
val safe_dest: int option > attribute 
116 
val safe_elim: int option > attribute 

117 
val safe_intro: int option > attribute 

60943  118 
val unsafe_dest: int option > attribute 
119 
val unsafe_elim: int option > attribute 

120 
val unsafe_intro: int option > attribute 

18728  121 
val rule_del: attribute 
61327  122 
val rule_tac: Proof.context > thm list > thm list > int > tactic 
123 
val standard_tac: Proof.context > thm list > tactic 

30513  124 
val cla_modifiers: Method.modifier parser list 
42793  125 
val cla_method: 
126 
(Proof.context > tactic) > (Proof.context > Proof.method) context_parser 

127 
val cla_method': 

128 
(Proof.context > int > tactic) > (Proof.context > Proof.method) context_parser 

5841  129 
end; 
130 

0  131 

42799  132 
functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 
0  133 
struct 
134 

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

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

136 

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

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

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

139 
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

140 

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

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

142 

26938  143 
Such rules can cause fast_tac to fail and blast_tac to report "PROOF 
59119  144 
FAILED"; classical_rule will strengthen this to 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

145 

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

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

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

148 

59970  149 
fun classical_rule ctxt rule = 
150 
if is_some (Object_Logic.elim_concl ctxt rule) then 

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

151 
let 
60817  152 
val thy = Proof_Context.theory_of ctxt; 
42792  153 
val rule' = rule RS Data.classical; 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

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

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

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

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

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

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

162 
if i = 1 orelse redundant_hyp goal 
60757  163 
then eresolve_tac ctxt [thin_rl] i 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

165 
> Seq.hd 
21963  166 
> Drule.zero_var_indexes; 
60817  167 
in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

169 

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

170 
(*flatten nested meta connectives in prems*) 
59970  171 
fun flat_rule ctxt = 
172 
Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)); 

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

173 

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

174 

1800  175 
(*** Useful tactics for classical reasoning ***) 
0  176 

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

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

180 
fun contr_tac ctxt = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

181 
eresolve_tac ctxt [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); 
0  182 

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

183 
(*Finds P>Q and P in the assumptions, replaces implication by Q. 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

184 
Could do the same thing for P<>Q and P... *) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

185 
fun mp_tac ctxt i = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

186 
eresolve_tac ctxt [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; 
0  187 

188 
(*Like mp_tac but instantiates no variables*) 

58957  189 
fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; 
0  190 

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

192 
fun swapify intrs = intrs RLN (2, [Data.swap]); 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61327
diff
changeset

193 
val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap)); 
0  194 

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

196 
trying rules in order. *) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

197 
fun swap_res_tac ctxt rls = 
61056  198 
let 
67649  199 
val transfer = Thm.transfer' ctxt; 
61056  200 
fun addrl rl brls = (false, transfer rl) :: (true, transfer rl RSN (2, Data.swap)) :: brls; 
201 
in 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

202 
assume_tac ctxt ORELSE' 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

203 
contr_tac ctxt ORELSE' 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

204 
biresolve_tac ctxt (fold_rev addrl rls []) 
42792  205 
end; 
0  206 

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

209 

59970  210 
fun dup_elim ctxt th = 
211 
let val rl = (th RSN (2, revcut_rl)) > Thm.assumption (SOME ctxt) 2 > Seq.hd; 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

212 
in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end; 
36546  213 

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

214 

1800  215 
(**** Classical rule sets ****) 
0  216 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

217 
type rule = thm * (thm * thm list) * (thm * thm list); 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

218 
(*external form, internal form (possibly swapped), dup form (possibly swapped)*) 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

219 

42812  220 
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; 
221 
type wrapper = (int > tactic) > int > tactic; 

222 

0  223 
datatype claset = 
42793  224 
CS of 
60945  225 
{safeIs: rule Item_Net.T, (*safe introduction rules*) 
226 
safeEs: rule Item_Net.T, (*safe elimination rules*) 

227 
unsafeIs: rule Item_Net.T, (*unsafe introduction rules*) 

228 
unsafeEs: rule Item_Net.T, (*unsafe elimination rules*) 

229 
swrappers: (string * (Proof.context > wrapper)) list, (*for transforming safe_step_tac*) 

230 
uwrappers: (string * (Proof.context > wrapper)) list, (*for transforming step_tac*) 

231 
safe0_netpair: netpair, (*nets for trivial cases*) 

232 
safep_netpair: netpair, (*nets for >0 subgoals*) 

233 
unsafe_netpair: netpair, (*nets for unsafe rules*) 

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

235 
extra_netpair: Context_Rules.netpair}; (*nets for extra rules*) 

236 

237 
val empty_rules: rule Item_Net.T = 

238 
Item_Net.init (Thm.eq_thm_prop o apply2 #1) (single o Thm.full_prop_of o #1); 

0  239 

6502  240 
val empty_netpair = (Net.empty, Net.empty); 
241 

10736  242 
val empty_cs = 
42793  243 
CS 
60945  244 
{safeIs = empty_rules, 
245 
safeEs = empty_rules, 

246 
unsafeIs = empty_rules, 

247 
unsafeEs = empty_rules, 

42793  248 
swrappers = [], 
249 
uwrappers = [], 

250 
safe0_netpair = empty_netpair, 

251 
safep_netpair = empty_netpair, 

60943  252 
unsafe_netpair = empty_netpair, 
42793  253 
dup_netpair = empty_netpair, 
60942  254 
extra_netpair = empty_netpair}; 
0  255 

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

257 

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

258 

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

260 

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

261 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  262 
***) 
0  263 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

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

265 

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

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

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

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

272 

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

10736  275 

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

277 

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

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

279 
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

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

281 
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

282 
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

283 

23178  284 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  285 
fun delete x = delete_tagged_list (joinrules x); 
1800  286 

61268  287 
fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); 
42793  288 

60945  289 
fun make_elim ctxt th = 
290 
if has_fewer_prems 1 th then bad_thm ctxt "Illformed destruction rule" th 

42793  291 
else Tactic.make_elim th; 
42790  292 

60945  293 
fun warn_thm ctxt msg th = 
294 
if Context_Position.is_really_visible ctxt 

61268  295 
then warning (msg ^ Thm.string_of_thm ctxt th) else (); 
42793  296 

60945  297 
fun warn_rules ctxt msg rules (r: rule) = 
298 
Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true); 

42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

299 

60945  300 
fun warn_claset ctxt r (CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = 
301 
warn_rules ctxt "Rule already declared as safe introduction (intro!)\n" safeIs r orelse 

302 
warn_rules ctxt "Rule already declared as safe elimination (elim!)\n" safeEs r orelse 

303 
warn_rules ctxt "Rule already declared as introduction (intro)\n" unsafeIs r orelse 

304 
warn_rules ctxt "Rule already declared as elimination (elim)\n" unsafeEs r; 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

305 

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

306 

60946  307 
(*** add rules ***) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

308 

60945  309 
fun add_safe_intro w r 
60943  310 
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
311 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

60945  312 
if Item_Net.member safeIs r then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

313 
else 
42790  314 
let 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

315 
val (th, rl, _) = r; 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

316 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

317 
List.partition (Thm.no_prems o fst) [rl]; 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

318 
val nI = Item_Net.length safeIs + 1; 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

319 
val nE = Item_Net.length safeEs; 
42790  320 
in 
321 
CS 

60945  322 
{safeIs = Item_Net.update r safeIs, 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

323 
safe0_netpair = insert (nI, nE) (map fst safe0_rls, maps snd safe0_rls) safe0_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

324 
safep_netpair = insert (nI, nE) (map fst safep_rls, maps snd safep_rls) safep_netpair, 
42790  325 
safeEs = safeEs, 
60943  326 
unsafeIs = unsafeIs, 
327 
unsafeEs = unsafeEs, 

42790  328 
swrappers = swrappers, 
329 
uwrappers = uwrappers, 

60943  330 
unsafe_netpair = unsafe_netpair, 
42790  331 
dup_netpair = dup_netpair, 
60944  332 
extra_netpair = insert' (the_default 0 w) (nI, nE) ([th], []) extra_netpair} 
42790  333 
end; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

334 

60945  335 
fun add_safe_elim w r 
60943  336 
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
337 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

60945  338 
if Item_Net.member safeEs r then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

339 
else 
42790  340 
let 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

341 
val (th, rl, _) = r; 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

342 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

343 
List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl]; 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

344 
val nI = Item_Net.length safeIs; 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

345 
val nE = Item_Net.length safeEs + 1; 
42790  346 
in 
347 
CS 

60945  348 
{safeEs = Item_Net.update r safeEs, 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

349 
safe0_netpair = insert (nI, nE) ([], map fst safe0_rls) safe0_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

350 
safep_netpair = insert (nI, nE) ([], map fst safep_rls) safep_netpair, 
42790  351 
safeIs = safeIs, 
60943  352 
unsafeIs = unsafeIs, 
353 
unsafeEs = unsafeEs, 

42790  354 
swrappers = swrappers, 
355 
uwrappers = uwrappers, 

60943  356 
unsafe_netpair = unsafe_netpair, 
42790  357 
dup_netpair = dup_netpair, 
60944  358 
extra_netpair = insert' (the_default 0 w) (nI, nE) ([], [th]) extra_netpair} 
42790  359 
end; 
0  360 

60945  361 
fun add_unsafe_intro w r 
60943  362 
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
363 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

60945  364 
if Item_Net.member unsafeIs r then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

365 
else 
42790  366 
let 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

367 
val (th, rl, dup_rl) = r; 
60943  368 
val nI = Item_Net.length unsafeIs + 1; 
369 
val nE = Item_Net.length unsafeEs; 

42790  370 
in 
371 
CS 

60945  372 
{unsafeIs = Item_Net.update r unsafeIs, 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

373 
unsafe_netpair = insert (nI, nE) ([fst rl], snd rl) unsafe_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

374 
dup_netpair = insert (nI, nE) ([fst dup_rl], snd dup_rl) dup_netpair, 
42790  375 
safeIs = safeIs, 
376 
safeEs = safeEs, 

60943  377 
unsafeEs = unsafeEs, 
42790  378 
swrappers = swrappers, 
379 
uwrappers = uwrappers, 

9938  380 
safe0_netpair = safe0_netpair, 
381 
safep_netpair = safep_netpair, 

60942  382 
extra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) extra_netpair} 
60945  383 
end; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

384 

60945  385 
fun add_unsafe_elim w r 
60943  386 
(cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
387 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

60945  388 
if Item_Net.member unsafeEs r then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

389 
else 
42790  390 
let 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

391 
val (th, rl, dup_rl) = r; 
60943  392 
val nI = Item_Net.length unsafeIs; 
393 
val nE = Item_Net.length unsafeEs + 1; 

42790  394 
in 
395 
CS 

60945  396 
{unsafeEs = Item_Net.update r unsafeEs, 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

397 
unsafe_netpair = insert (nI, nE) ([], [fst rl]) unsafe_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

398 
dup_netpair = insert (nI, nE) ([], [fst dup_rl]) dup_netpair, 
42790  399 
safeIs = safeIs, 
400 
safeEs = safeEs, 

60943  401 
unsafeIs = unsafeIs, 
42790  402 
swrappers = swrappers, 
403 
uwrappers = uwrappers, 

9938  404 
safe0_netpair = safe0_netpair, 
405 
safep_netpair = safep_netpair, 

60942  406 
extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair} 
42790  407 
end; 
0  408 

61056  409 
fun trim_context (th, (th1, ths1), (th2, ths2)) = 
410 
(Thm.trim_context th, 

411 
(Thm.trim_context th1, map Thm.trim_context ths1), 

412 
(Thm.trim_context th2, map Thm.trim_context ths2)); 

413 

60946  414 
fun addSI w ctxt th (cs as CS {safeIs, ...}) = 
415 
let 

416 
val th' = flat_rule ctxt th; 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

417 
val rl = (th', swapify [th']); 
61056  418 
val r = trim_context (th, rl, rl); 
60946  419 
val _ = 
420 
warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse 

421 
warn_claset ctxt r cs; 

422 
in add_safe_intro w r cs end; 

423 

424 
fun addSE w ctxt th (cs as CS {safeEs, ...}) = 

425 
let 

426 
val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Illformed elimination rule" th; 

427 
val th' = classical_rule ctxt (flat_rule ctxt th); 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

428 
val rl = (th', []); 
61056  429 
val r = trim_context (th, rl, rl); 
60946  430 
val _ = 
431 
warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse 

432 
warn_claset ctxt r cs; 

433 
in add_safe_elim w r cs end; 

434 

435 
fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th); 

436 

60945  437 
fun addI w ctxt th (cs as CS {unsafeIs, ...}) = 
438 
let 

439 
val th' = flat_rule ctxt th; 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

440 
val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Illformed introduction rule" th; 
61056  441 
val r = trim_context (th, (th', swapify [th']), (dup_th', swapify [dup_th'])); 
60945  442 
val _ = 
443 
warn_rules ctxt "Ignoring duplicate introduction (intro)\n" unsafeIs r orelse 

444 
warn_claset ctxt r cs; 

445 
in add_unsafe_intro w r cs end; 

42793  446 

60945  447 
fun addE w ctxt th (cs as CS {unsafeEs, ...}) = 
448 
let 

449 
val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Illformed elimination rule" th; 

450 
val th' = classical_rule ctxt (flat_rule ctxt th); 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

451 
val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Illformed elimination rule" th; 
61056  452 
val r = trim_context (th, (th', []), (dup_th', [])); 
60945  453 
val _ = 
454 
warn_rules ctxt "Ignoring duplicate elimination (elim)\n" unsafeEs r orelse 

455 
warn_claset ctxt r cs; 

456 
in add_unsafe_elim w r cs end; 

457 

458 
fun addD w ctxt th = addE w ctxt (make_elim ctxt th); 

0  459 

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

460 

60946  461 
(*** delete rules ***) 
462 

463 
local 

1800  464 

60946  465 
fun del_safe_intro (r: rule) 
466 
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 

467 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

468 
let 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

469 
val (th, rl, _) = r; 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

470 
val (safe0_rls, safep_rls) = List.partition (Thm.no_prems o fst) [rl]; 
60946  471 
in 
472 
CS 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

473 
{safe0_netpair = delete (map fst safe0_rls, maps snd safe0_rls) safe0_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

474 
safep_netpair = delete (map fst safep_rls, maps snd safep_rls) safep_netpair, 
60946  475 
safeIs = Item_Net.remove r safeIs, 
476 
safeEs = safeEs, 

477 
unsafeIs = unsafeIs, 

478 
unsafeEs = unsafeEs, 

479 
swrappers = swrappers, 

480 
uwrappers = uwrappers, 

481 
unsafe_netpair = unsafe_netpair, 

482 
dup_netpair = dup_netpair, 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

483 
extra_netpair = delete ([th], []) extra_netpair} 
60946  484 
end; 
1800  485 

60946  486 
fun del_safe_elim (r: rule) 
487 
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 

488 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

489 
let 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

490 
val (th, rl, _) = r; 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

491 
val (safe0_rls, safep_rls) = List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl]; 
60946  492 
in 
493 
CS 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

494 
{safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

495 
safep_netpair = delete ([], map fst safep_rls) safep_netpair, 
60946  496 
safeIs = safeIs, 
497 
safeEs = Item_Net.remove r safeEs, 

498 
unsafeIs = unsafeIs, 

499 
unsafeEs = unsafeEs, 

500 
swrappers = swrappers, 

501 
uwrappers = uwrappers, 

502 
unsafe_netpair = unsafe_netpair, 

503 
dup_netpair = dup_netpair, 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

504 
extra_netpair = delete ([], [th]) extra_netpair} 
60946  505 
end; 
1800  506 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

507 
fun del_unsafe_intro (r as (th, (th', swapped_th'), (dup_th', swapped_dup_th'))) 
60946  508 
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
509 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

510 
CS 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

511 
{unsafe_netpair = delete ([th'], swapped_th') unsafe_netpair, 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

512 
dup_netpair = delete ([dup_th'], swapped_dup_th') dup_netpair, 
60946  513 
safeIs = safeIs, 
514 
safeEs = safeEs, 

515 
unsafeIs = Item_Net.remove r unsafeIs, 

516 
unsafeEs = unsafeEs, 

517 
swrappers = swrappers, 

518 
uwrappers = uwrappers, 

519 
safe0_netpair = safe0_netpair, 

520 
safep_netpair = safep_netpair, 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

521 
extra_netpair = delete ([th], []) extra_netpair}; 
1800  522 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

523 
fun del_unsafe_elim (r as (th, (th', _), (dup_th', _))) 
60946  524 
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
525 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

526 
CS 

527 
{unsafe_netpair = delete ([], [th']) unsafe_netpair, 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

528 
dup_netpair = delete ([], [dup_th']) dup_netpair, 
60946  529 
safeIs = safeIs, 
530 
safeEs = safeEs, 

531 
unsafeIs = unsafeIs, 

532 
unsafeEs = Item_Net.remove r unsafeEs, 

533 
swrappers = swrappers, 

534 
uwrappers = uwrappers, 

535 
safe0_netpair = safe0_netpair, 

536 
safep_netpair = safep_netpair, 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

537 
extra_netpair = delete ([], [th]) extra_netpair}; 
1800  538 

60946  539 
fun del f rules th cs = 
61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

540 
fold f (Item_Net.lookup rules (th, (th, []), (th, []))) cs; 
60946  541 

542 
in 

543 

60945  544 
fun delrule ctxt th (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = 
545 
let 

546 
val th' = Tactic.make_elim th; 

61055
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

547 
val r = (th, (th, []), (th, [])); 
6fc78876f9be
store result of swapify, to avoid later access to implicit context;
wenzelm
parents:
61049
diff
changeset

548 
val r' = (th', (th', []), (th', [])); 
60945  549 
in 
550 
if Item_Net.member safeIs r orelse Item_Net.member safeEs r orelse 

551 
Item_Net.member unsafeIs r orelse Item_Net.member unsafeEs r orelse 

552 
Item_Net.member safeEs r' orelse Item_Net.member unsafeEs r' 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

553 
then 
60942  554 
cs 
60946  555 
> del del_safe_intro safeIs th 
556 
> del del_safe_elim safeEs th 

557 
> del del_safe_elim safeEs th' 

558 
> del del_unsafe_intro unsafeIs th 

559 
> del del_unsafe_elim unsafeEs th 

560 
> del del_unsafe_elim unsafeEs th' 

60945  561 
else (warn_thm ctxt "Undeclared classical rule\n" th; cs) 
9938  562 
end; 
1800  563 

60946  564 
end; 
565 

1800  566 

42793  567 

568 
(** claset data **) 

42790  569 

42793  570 
(* wrappers *) 
42790  571 

22674  572 
fun map_swrappers f 
60943  573 
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
574 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

575 
CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, 

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

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

577 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
60943  578 
unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

579 

22674  580 
fun map_uwrappers f 
60943  581 
(CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, 
582 
safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = 

583 
CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, 

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

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

585 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
60943  586 
unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

587 

22674  588 

42793  589 
(* merge_cs *) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

590 

42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

591 
(*Merge works by adding all new rules of the 2nd claset into the 1st claset, 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

592 
in order to preserve priorities reliably.*) 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

593 

2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

594 
fun merge_thms add thms1 thms2 = 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

595 
fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2); 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

596 

60943  597 
fun merge_cs (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}, 
598 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, unsafeIs = unsafeIs2, unsafeEs = unsafeEs2, 

22674  599 
swrappers, uwrappers, ...}) = 
24358  600 
if pointer_eq (cs, cs') then cs 
601 
else 

42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

602 
cs 
60945  603 
> merge_thms (add_safe_intro NONE) safeIs safeIs2 
604 
> merge_thms (add_safe_elim NONE) safeEs safeEs2 

605 
> merge_thms (add_unsafe_intro NONE) unsafeIs unsafeIs2 

606 
> merge_thms (add_unsafe_elim NONE) unsafeEs unsafeEs2 

42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

607 
> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

608 
> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)); 
42793  609 

610 

611 
(* data *) 

612 

613 
structure Claset = Generic_Data 

614 
( 

615 
type T = claset; 

616 
val empty = empty_cs; 

617 
val extend = I; 

618 
val merge = merge_cs; 

619 
); 

620 

621 
val claset_of = Claset.get o Context.Proof; 

622 
val rep_claset_of = rep_cs o claset_of; 

623 

624 
val get_cs = Claset.get; 

625 
val map_cs = Claset.map; 

626 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

627 
fun map_theory_claset f thy = 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

628 
let 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

629 
val ctxt' = f (Proof_Context.init_global thy); 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

630 
val thy' = Proof_Context.theory_of ctxt'; 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

631 
in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end; 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

632 

42793  633 
fun map_claset f = Context.proof_map (map_cs f); 
634 
fun put_claset cs = map_claset (K cs); 

635 

636 
fun print_claset ctxt = 

637 
let 

60943  638 
val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; 
61268  639 
val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content; 
42793  640 
in 
641 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 

60943  642 
Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), 
42793  643 
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), 
60943  644 
Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs), 
42793  645 
Pretty.strs ("safe wrappers:" :: map #1 swrappers), 
646 
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] 

56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
54742
diff
changeset

647 
> Pretty.writeln_chunks 
42793  648 
end; 
649 

650 

651 
(* oldstyle declarations *) 

652 

60945  653 
fun decl f (ctxt, ths) = map_claset (fold_rev (f ctxt) ths) ctxt; 
42793  654 

655 
val op addSIs = decl (addSI NONE); 

656 
val op addSEs = decl (addSE NONE); 

657 
val op addSDs = decl (addSD NONE); 

658 
val op addIs = decl (addI NONE); 

659 
val op addEs = decl (addE NONE); 

660 
val op addDs = decl (addD NONE); 

661 
val op delrules = decl delrule; 

662 

663 

664 

665 
(*** Modifying the wrapper tacticals ***) 

666 

667 
fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); 

668 
fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); 

669 

670 
fun update_warn msg (p as (key : string, _)) xs = 

671 
(if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); 

672 

673 
fun delete_warn msg (key : string) xs = 

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

675 
else (warning msg; xs); 

676 

677 
(*Add/replace a safe wrapper*) 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

678 
fun ctxt addSWrapper new_swrapper = ctxt > map_claset 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

679 
(map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper)); 
42793  680 

681 
(*Add/replace an unsafe wrapper*) 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

682 
fun ctxt addWrapper new_uwrapper = ctxt > map_claset 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

683 
(map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper)); 
42793  684 

685 
(*Remove a safe wrapper*) 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

686 
fun ctxt delSWrapper name = ctxt > map_claset 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

687 
(map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name)); 
42793  688 

689 
(*Remove an unsafe wrapper*) 

51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

690 
fun ctxt delWrapper name = ctxt > map_claset 
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51688
diff
changeset

691 
(map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); 
42793  692 

693 
(* compose a safe tactic alternatively before/after safe_step_tac *) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

694 
fun ctxt addSbefore (name, tac1) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

695 
ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

696 
fun ctxt addSafter (name, tac2) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

697 
ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); 
42793  698 

699 
(*compose a tactic alternatively before/after the step tactic *) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

700 
fun ctxt addbefore (name, tac1) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

701 
ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2); 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

702 
fun ctxt addafter (name, tac2) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

703 
ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt); 
42793  704 

58957  705 
fun ctxt addD2 (name, thm) = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

706 
ctxt addafter (name, fn ctxt' => dresolve_tac ctxt' [thm] THEN' assume_tac ctxt'); 
58957  707 
fun ctxt addE2 (name, thm) = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

708 
ctxt addafter (name, fn ctxt' => eresolve_tac ctxt' [thm] THEN' assume_tac ctxt'); 
58957  709 
fun ctxt addSD2 (name, thm) = 
710 
ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac); 

711 
fun ctxt addSE2 (name, thm) = 

712 
ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac); 

42793  713 

1711  714 

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

715 

1800  716 
(**** Simple tactics for theorem proving ****) 
0  717 

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

42793  719 
fun safe_step_tac ctxt = 
720 
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 

721 
appSWrappers ctxt 

722 
(FIRST' 

723 
[eq_assume_tac, 

58957  724 
eq_mp_tac ctxt, 
59164  725 
bimatch_from_nets_tac ctxt safe0_netpair, 
51798  726 
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), 
59164  727 
bimatch_from_nets_tac ctxt safep_netpair]) 
42793  728 
end; 
0  729 

5757  730 
(*Repeatedly attack a subgoal using safe inferences  it's deterministic!*) 
42793  731 
fun safe_steps_tac ctxt = 
732 
REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i)); 

5757  733 

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

736 

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

737 

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

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

739 

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

741 

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

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

743 
create precisely n subgoals.*) 
59164  744 
fun n_bimatch_from_nets_tac ctxt n = 
745 
biresolution_from_nets_tac ctxt (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

746 

58957  747 
fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i; 
748 
fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt; 

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

749 

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

750 
(*Twoway branching is allowed only if one of the branches immediately closes*) 
58957  751 
fun bimatch2_tac ctxt netpair i = 
59164  752 
n_bimatch_from_nets_tac ctxt 2 netpair i THEN 
58957  753 
(eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1)); 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

754 

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

755 
(*Attack subgoals using safe inferences  matching, not resolution*) 
42793  756 
fun clarify_step_tac ctxt = 
757 
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 

758 
appSWrappers ctxt 

759 
(FIRST' 

58957  760 
[eq_assume_contr_tac ctxt, 
59164  761 
bimatch_from_nets_tac ctxt safe0_netpair, 
51798  762 
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), 
59164  763 
n_bimatch_from_nets_tac ctxt 1 safep_netpair, 
58957  764 
bimatch2_tac ctxt safep_netpair]) 
42793  765 
end; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

766 

42793  767 
fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

768 

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

769 

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

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

771 

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

42793  774 
fun inst0_step_tac ctxt = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

775 
assume_tac ctxt APPEND' 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

776 
contr_tac ctxt APPEND' 
59164  777 
biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt)); 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

778 

4066  779 
(*These unsafe steps could generate more subgoals.*) 
42793  780 
fun instp_step_tac ctxt = 
59164  781 
biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt)); 
0  782 

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

42793  784 
fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; 
0  785 

60943  786 
fun unsafe_step_tac ctxt = 
787 
biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt)); 

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

788 

0  789 
(*Single step for the prover. FAILS unless it makes progress. *) 
42793  790 
fun step_tac ctxt i = 
60943  791 
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' unsafe_step_tac ctxt) i; 
0  792 

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

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

42793  795 
fun slow_step_tac ctxt i = 
60943  796 
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' unsafe_step_tac ctxt) i; 
0  797 

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

798 

1800  799 
(**** The following tactics all fail unless they solve one goal ****) 
0  800 

801 
(*Dumb but fast*) 

42793  802 
fun fast_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

803 
Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 
0  804 

805 
(*Slower but smarter than fast_tac*) 

42793  806 
fun best_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

807 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  808 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); 
0  809 

9402  810 
(*even a bit smarter than best_tac*) 
42793  811 
fun first_best_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

812 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  813 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); 
9402  814 

42793  815 
fun slow_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

816 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  817 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); 
0  818 

42793  819 
fun slow_best_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

820 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  821 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); 
0  822 

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

823 

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

825 

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

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

827 

42793  828 
fun astar_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

829 
Object_Logic.atomize_prems_tac ctxt THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

830 
SELECT_GOAL 
52462
a241826ed003
actually use Data.sizef, not hardwired size_of_thm;
wenzelm
parents:
51798
diff
changeset

831 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) 
42793  832 
(step_tac ctxt 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

833 

42793  834 
fun slow_astar_tac ctxt = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

835 
Object_Logic.atomize_prems_tac ctxt THEN' 
10382
1fb807260ff1
atomize: all automated tactics that "solve" goals;
wenzelm
parents:
10309
diff
changeset

836 
SELECT_GOAL 
52462
a241826ed003
actually use Data.sizef, not hardwired size_of_thm;
wenzelm
parents:
51798
diff
changeset

837 
(ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) 
42793  838 
(slow_step_tac ctxt 1)); 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

839 

42790  840 

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

842 
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

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

845 

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

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

847 
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

848 
greater search depth required.*) 
42793  849 
fun dup_step_tac ctxt = 
59164  850 
biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt)); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

851 

5523  852 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  853 
local 
42793  854 
fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt); 
42790  855 
in 
42793  856 
fun depth_tac ctxt m i state = SELECT_GOAL 
857 
(safe_steps_tac ctxt 1 THEN_ELSE 

858 
(DEPTH_SOLVE (depth_tac ctxt m 1), 

859 
inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac 

860 
(slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m  1) 1)))) i state; 

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

862 

10736  863 
(*Search, with depth bound m. 
2173  864 
This is the "entry point", which does safe inferences first.*) 
42793  865 
fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) => 
866 
let 

867 
val deti = (*No Vars in the goal? No need to backtrack between goals.*) 

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

42790  869 
in 
42793  870 
SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i 
42790  871 
end); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

872 

42793  873 
fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); 
24021  874 

875 

5885  876 
(* attributes *) 
877 

42793  878 
fun attrib f = 
60945  879 
Thm.declaration_attribute (fn th => fn context => 
880 
map_cs (f (Context.proof_of context) th) context); 

5885  881 

18691  882 
val safe_elim = attrib o addSE; 
883 
val safe_intro = attrib o addSI; 

42793  884 
val safe_dest = attrib o addSD; 
60943  885 
val unsafe_elim = attrib o addE; 
886 
val unsafe_intro = attrib o addI; 

887 
val unsafe_dest = attrib o addD; 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset

888 

7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset

889 
val rule_del = 
60945  890 
Thm.declaration_attribute (fn th => fn context => 
891 
context 

892 
> map_cs (delrule (Context.proof_of context) th) 

893 
> Thm.attribute_declaration Context_Rules.rule_del th); 

5885  894 

895 

5841  896 

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

899 
val introN = "intro"; 

900 
val elimN = "elim"; 

901 
val destN = "dest"; 

902 

58826  903 
val _ = 
904 
Theory.setup 

905 
(Attrib.setup @{binding swapped} (Scan.succeed swapped) 

906 
"classical swap of introduction rule" #> 

60943  907 
Attrib.setup @{binding dest} (Context_Rules.add safe_dest unsafe_dest Context_Rules.dest_query) 
58826  908 
"declaration of Classical destruction rule" #> 
60943  909 
Attrib.setup @{binding elim} (Context_Rules.add safe_elim unsafe_elim Context_Rules.elim_query) 
58826  910 
"declaration of Classical elimination rule" #> 
60943  911 
Attrib.setup @{binding intro} (Context_Rules.add safe_intro unsafe_intro Context_Rules.intro_query) 
58826  912 
"declaration of Classical introduction rule" #> 
913 
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) 

914 
"remove declaration of intro/elim/dest rule"); 

5841  915 

916 

917 

7230  918 
(** proof methods **) 
919 

920 
local 

921 

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

922 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  923 
let 
61049  924 
val [rules1, rules2, rules4] = Context_Rules.find_rules ctxt false facts goal; 
60942  925 
val {extra_netpair, ...} = rep_claset_of ctxt; 
61049  926 
val rules3 = Context_Rules.find_rules_netpair ctxt true facts goal extra_netpair; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

927 
val rules = rules1 @ rules2 @ rules3 @ rules4; 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58893
diff
changeset

928 
val ruleq = Drule.multi_resolves (SOME ctxt) facts rules; 
52732  929 
val _ = Method.trace ctxt rules; 
12376
480303e3fa08
simplified (and clarified) integration with Pure/ContextRules;
wenzelm
parents:
12362
diff
changeset

930 
in 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59164
diff
changeset

931 
fn st => Seq.maps (fn rule => resolve_tac ctxt [rule] i st) ruleq 
18834  932 
end) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

933 
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; 
5841  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 
in 
7281  936 

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

937 
fun rule_tac ctxt [] facts = some_rule_tac ctxt facts 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

938 
 rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts; 
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30558
diff
changeset

939 

60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset

940 
fun standard_tac ctxt facts = 
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset

941 
HEADGOAL (some_rule_tac ctxt facts) ORELSE 
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset

942 
Class.standard_intro_classes_tac ctxt facts; 
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset

943 

7230  944 
end; 
5841  945 

946 

6502  947 
(* automatic methods *) 
5841  948 

5927  949 
val cla_modifiers = 
64556  950 
[Args.$$$ destN  Args.bang_colon >> K (Method.modifier (safe_dest NONE) \<^here>), 
951 
Args.$$$ destN  Args.colon >> K (Method.modifier (unsafe_dest NONE) \<^here>), 

952 
Args.$$$ elimN  Args.bang_colon >> K (Method.modifier (safe_elim NONE) \<^here>), 

953 
Args.$$$ elimN  Args.colon >> K (Method.modifier (unsafe_elim NONE) \<^here>), 

954 
Args.$$$ introN  Args.bang_colon >> K (Method.modifier (safe_intro NONE) \<^here>), 

955 
Args.$$$ introN  Args.colon >> K (Method.modifier (unsafe_intro NONE) \<^here>), 

956 
Args.del  Args.colon >> K (Method.modifier rule_del \<^here>)]; 

5927  957 

42793  958 
fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac); 
959 
fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); 

5841  960 

961 

962 

58826  963 
(** method setup **) 
5841  964 

58826  965 
val _ = 
966 
Theory.setup 

60619
7512716f03db
no arguments for "standard" (or old "default") methods;
wenzelm
parents:
60618
diff
changeset

967 
(Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac)) 
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60097
diff
changeset

968 
"standard proof step: classical intro/elim rule or class introduction" #> 
58826  969 
Method.setup @{binding rule} 
970 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) 

971 
"apply some intro/elim rule (potentially classical)" #> 

972 
Method.setup @{binding contradiction} 

973 
(Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])) 

974 
"proof by contradiction" #> 

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

976 
"repeatedly apply safe steps" #> 

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

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

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

980 
Method.setup @{binding deepen} 

981 
(Scan.lift (Scan.optional Parse.nat 4)  Method.sections cla_modifiers 

982 
>> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n))) 

983 
"classical prover (iterative deepening)" #> 

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

985 
"classical prover (apply safe rules)" #> 

986 
Method.setup @{binding safe_step} (cla_method' safe_step_tac) 

987 
"single classical step (safe rules)" #> 

988 
Method.setup @{binding inst_step} (cla_method' inst_step_tac) 

989 
"single classical step (safe rules, allow instantiations)" #> 

990 
Method.setup @{binding step} (cla_method' step_tac) 

991 
"single classical step (safe and unsafe rules)" #> 

992 
Method.setup @{binding slow_step} (cla_method' slow_step_tac) 

993 
"single classical step (safe and unsafe rules, allow backtracking)" #> 

994 
Method.setup @{binding clarify_step} (cla_method' clarify_step_tac) 

995 
"single classical step (safe rules, without splitting)"); 

5841  996 

8667  997 

998 
(** outer syntax **) 

999 

24867  1000 
val _ = 
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59582
diff
changeset

1001 
Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner" 
60097
d20ca79d50e4
discontinued pointless warnings: commands are only defined inside a theory context;
wenzelm
parents:
59970
diff
changeset

1002 
(Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of))); 
8667  1003 

5841  1004 
end; 