author  wenzelm 
Tue, 09 Dec 2014 19:39:40 +0100  
changeset 59119  c90c02940964 
parent 58963  26bf09b95dda 
child 59164  ff40c53d1af9 
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 

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 
58958  75 
val dup_elim: Context.generic option > 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 
42793  79 
val haz_step_tac: Proof.context > int > tactic 
42790  80 
val joinrules: thm list * thm list > (bool * thm) list 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

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

84 
val safe_step_tac: Proof.context > int > tactic 

85 
val clarify_tac: Proof.context > int > tactic 

86 
val clarify_step_tac: Proof.context > int > tactic 

87 
val step_tac: Proof.context > int > tactic 

88 
val slow_step_tac: Proof.context > int > tactic 

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

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

93 
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

94 
end; 
1724  95 

5841  96 
signature CLASSICAL = 
97 
sig 

98 
include BASIC_CLASSICAL 

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

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

102 
{safeIs: thm Item_Net.T, 

103 
safeEs: thm Item_Net.T, 

104 
hazIs: thm Item_Net.T, 

105 
hazEs: thm Item_Net.T, 

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

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

108 
safe0_netpair: netpair, 

109 
safep_netpair: netpair, 

110 
haz_netpair: netpair, 

111 
dup_netpair: netpair, 

112 
xtra_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 

118 
val haz_dest: int option > attribute 

119 
val haz_elim: int option > attribute 

120 
val haz_intro: int option > attribute 

121 
val rule_del: attribute 

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

125 
val cla_method': 

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

5841  127 
end; 
128 

0  129 

42799  130 
functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 
0  131 
struct 
132 

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

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

134 

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

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

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

137 
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

138 

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

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

140 

26938  141 
Such rules can cause fast_tac to fail and blast_tac to report "PROOF 
59119  142 
FAILED"; classical_rule will strengthen this to 
18534
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 
[ 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

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

146 

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

147 
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

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

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

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

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

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

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

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

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

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

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

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

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

164 
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

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

166 

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

167 
(*flatten nested meta connectives in prems*) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

168 
fun flat_rule opt_context th = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

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

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

171 
(case opt_context of 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

172 
NONE => Proof_Context.init_global (Thm.theory_of_thm th) 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

173 
 SOME context => Context.proof_of context); 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

174 
in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end; 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

175 

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

176 

1800  177 
(*** Useful tactics for classical reasoning ***) 
0  178 

10736  179 
(*Prove goal that assumes both P and ~P. 
4392  180 
No backtracking if it finds an equal assumption. Perhaps should call 
181 
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

182 
fun contr_tac ctxt = 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

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

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

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

186 
Could do the same thing for P<>Q and P... *) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

187 
fun mp_tac ctxt i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; 
0  188 

189 
(*Like mp_tac but instantiates no variables*) 

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

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

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

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

197 
trying rules in order. *) 

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

198 
fun swap_res_tac ctxt rls = 
42792  199 
let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

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

201 
contr_tac ctxt ORELSE' 
42792  202 
biresolve_tac (fold_rev addrl rls []) 
203 
end; 

0  204 

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

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

207 

58958  208 
fun dup_elim context th = 
36546  209 
let 
58958  210 
val ctxt = 
211 
(case context of 

212 
SOME c => Context.proof_of c 

213 
 NONE => Proof_Context.init_global (Thm.theory_of_thm th)); 

214 
val rl = (th RSN (2, revcut_rl)) > Thm.assumption (SOME ctxt) 2 > Seq.hd; 

58838  215 
in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end; 
36546  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 

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 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

225 
{safeIs : thm Item_Net.T, (*safe introduction rules*) 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

226 
safeEs : thm Item_Net.T, (*safe elimination rules*) 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

227 
hazIs : thm Item_Net.T, (*unsafe introduction rules*) 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

228 
hazEs : thm Item_Net.T, (*unsafe elimination rules*) 
42793  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 
haz_netpair : netpair, (*nets for unsafe rules*) 

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

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

0  236 

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

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

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

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

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

243 

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

245 
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

246 
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

247 
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

248 
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

249 
*) 
0  250 

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

10736  253 
val empty_cs = 
42793  254 
CS 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

255 
{safeIs = Thm.full_rules, 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

256 
safeEs = Thm.full_rules, 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

257 
hazIs = Thm.full_rules, 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

258 
hazEs = Thm.full_rules, 
42793  259 
swrappers = [], 
260 
uwrappers = [], 

261 
safe0_netpair = empty_netpair, 

262 
safep_netpair = empty_netpair, 

263 
haz_netpair = empty_netpair, 

264 
dup_netpair = empty_netpair, 

265 
xtra_netpair = empty_netpair}; 

0  266 

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

268 

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

269 

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

271 

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

272 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  273 
***) 
0  274 

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

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

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

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

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

279 

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

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

282 

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

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

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

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

289 

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

10736  292 

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

294 

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

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

296 
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

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

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

300 

23178  301 
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; 
12362  302 
fun delete x = delete_tagged_list (joinrules x); 
12401  303 
fun delete' x = delete_tagged_list (joinrules' x); 
1800  304 

42793  305 
fun string_of_thm NONE = Display.string_of_thm_without_context 
42817  306 
 string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context); 
42793  307 

308 
fun make_elim context th = 

309 
if has_fewer_prems 1 th then 

310 
error ("Illformed destruction rule\n" ^ string_of_thm context th) 

311 
else Tactic.make_elim th; 

42790  312 

52699  313 
fun warn_thm (SOME (Context.Proof ctxt)) msg th = 
57859
29e728588163
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073)  avoid duplicate warnings;
wenzelm
parents:
56334
diff
changeset

314 
if Context_Position.is_really_visible ctxt 
52699  315 
then warning (msg ^ Display.string_of_thm ctxt th) else () 
316 
 warn_thm _ _ _ = (); 

42793  317 

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

318 
fun warn_rules context msg rules th = 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

319 
Item_Net.member rules th andalso (warn_thm context msg th; true); 
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

320 

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

321 
fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

322 
warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse 
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

323 
warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse 
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

324 
warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse 
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

325 
warn_rules context "Rule already declared as elimination (elim)\n" hazEs th; 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

326 

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

327 

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

329 

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

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

333 
if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

336 
val th' = flat_rule context th; 
23594
e65e466dda01
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23178
diff
changeset

337 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
42790  338 
List.partition Thm.no_prems [th']; 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

339 
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

340 
val nE = Item_Net.length safeEs; 
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

341 
val _ = warn_claset context th cs; 
42790  342 
in 
343 
CS 

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

344 
{safeIs = Item_Net.update th safeIs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

349 
hazEs = hazEs, 

350 
swrappers = swrappers, 

351 
uwrappers = uwrappers, 

352 
haz_netpair = haz_netpair, 

353 
dup_netpair = dup_netpair, 

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

356 

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

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

360 
if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

361 
else if has_fewer_prems 1 th then 
42793  362 
error ("Illformed elimination rule\n" ^ string_of_thm context th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

365 
val th' = classical_rule (flat_rule context th); 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

366 
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
42790  367 
List.partition (fn rl => nprems_of rl=1) [th']; 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

368 
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

369 
val nE = Item_Net.length safeEs + 1; 
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

370 
val _ = warn_claset context th cs; 
42790  371 
in 
372 
CS 

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

373 
{safeEs = Item_Net.update th safeEs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

378 
hazEs = hazEs, 

379 
swrappers = swrappers, 

380 
uwrappers = uwrappers, 

381 
haz_netpair = haz_netpair, 

382 
dup_netpair = dup_netpair, 

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

42793  386 
fun addSD w context th = addSE w context (make_elim context th); 
387 

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

388 

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

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

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

394 
if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

397 
val th' = flat_rule context th; 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

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

399 
val nE = Item_Net.length hazEs; 
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

400 
val _ = warn_claset context th cs; 
42790  401 
in 
402 
CS 

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

403 
{hazIs = Item_Net.update th hazIs, 
42790  404 
haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, 
405 
dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, 

406 
safeIs = safeIs, 

407 
safeEs = safeEs, 

408 
hazEs = hazEs, 

409 
swrappers = swrappers, 

410 
uwrappers = uwrappers, 

9938  411 
safe0_netpair = safe0_netpair, 
412 
safep_netpair = safep_netpair, 

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

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

42793  416 
error ("Illformed introduction rule\n" ^ string_of_thm context th); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

417 

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

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

421 
if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18534
diff
changeset

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

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

426 
val th' = classical_rule (flat_rule context th); 
42810
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

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

428 
val nE = Item_Net.length hazEs + 1; 
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

429 
val _ = warn_claset context th cs; 
42790  430 
in 
431 
CS 

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

432 
{hazEs = Item_Net.update th hazEs, 
42790  433 
haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, 
58958  434 
dup_netpair = insert (nI, nE) ([], [dup_elim context th']) dup_netpair, 
42790  435 
safeIs = safeIs, 
436 
safeEs = safeEs, 

437 
hazIs = hazIs, 

438 
swrappers = swrappers, 

439 
uwrappers = uwrappers, 

9938  440 
safe0_netpair = safe0_netpair, 
441 
safep_netpair = safep_netpair, 

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

0  444 

42793  445 
fun addD w context th = addE w context (make_elim context th); 
446 

0  447 

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

448 

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

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

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

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

457 
if Item_Net.member safeIs th then 
18534
6799b38ed872
added classical_rule, which replaces Data.make_elim;
wenzelm
parents:
18374
diff
changeset

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

459 
val th' = flat_rule context th; 
42790  460 
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; 
461 
in 

462 
CS 

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

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

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

465 
safeIs = Item_Net.remove th safeIs, 
42790  466 
safeEs = safeEs, 
467 
hazIs = hazIs, 

468 
hazEs = hazEs, 

469 
swrappers = swrappers, 

470 
uwrappers = uwrappers, 

471 
haz_netpair = haz_netpair, 

472 
dup_netpair = dup_netpair, 

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

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

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

475 
else cs; 
1800  476 

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

477 
fun delSE context th 
42790  478 
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
479 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

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

480 
if Item_Net.member safeEs th then 
42790  481 
let 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

482 
val th' = classical_rule (flat_rule context th); 
42790  483 
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th']; 
484 
in 

485 
CS 

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

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

488 
safeIs = safeIs, 

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

489 
safeEs = Item_Net.remove th safeEs, 
42790  490 
hazIs = hazIs, 
491 
hazEs = hazEs, 

492 
swrappers = swrappers, 

493 
uwrappers = uwrappers, 

494 
haz_netpair = haz_netpair, 

495 
dup_netpair = dup_netpair, 

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

497 
end 

498 
else cs; 

1800  499 

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

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

503 
if Item_Net.member hazIs th then 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

504 
let val th' = flat_rule context th in 
42790  505 
CS 
506 
{haz_netpair = delete ([th'], []) haz_netpair, 

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

507 
dup_netpair = delete ([dup_intr th'], []) dup_netpair, 
42790  508 
safeIs = safeIs, 
509 
safeEs = safeEs, 

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

510 
hazIs = Item_Net.remove th hazIs, 
42790  511 
hazEs = hazEs, 
512 
swrappers = swrappers, 

513 
uwrappers = uwrappers, 

9938  514 
safe0_netpair = safe0_netpair, 
515 
safep_netpair = safep_netpair, 

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

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

42793  520 
error ("Illformed introduction rule\n" ^ string_of_thm context th); 
1800  521 

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

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

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

525 
if Item_Net.member hazEs th then 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

526 
let val th' = classical_rule (flat_rule context th) in 
42790  527 
CS 
528 
{haz_netpair = delete ([], [th']) haz_netpair, 

58958  529 
dup_netpair = delete ([], [dup_elim context th']) dup_netpair, 
42790  530 
safeIs = safeIs, 
531 
safeEs = safeEs, 

532 
hazIs = hazIs, 

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

533 
hazEs = Item_Net.remove th hazEs, 
42790  534 
swrappers = swrappers, 
535 
uwrappers = uwrappers, 

9938  536 
safe0_netpair = safe0_netpair, 
537 
safep_netpair = safep_netpair, 

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

1800  541 

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

542 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
42793  543 
fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
544 
let val th' = Tactic.make_elim th in 

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

545 
if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

546 
Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

547 
Item_Net.member safeEs th' orelse Item_Net.member hazEs th' 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset

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

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

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

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

552 
(delE context th (delSE context th' (delE context th' cs))))) 
42807
e639d91d9073
more precise warnings: observe context visibility;
wenzelm
parents:
42799
diff
changeset

553 
else (warn_thm context "Undeclared classical rule\n" th; cs) 
9938  554 
end; 
1800  555 

556 

42793  557 

558 
(** claset data **) 

42790  559 

42793  560 
(* wrappers *) 
42790  561 

22674  562 
fun map_swrappers f 
563 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

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

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

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

567 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  568 
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

569 

22674  570 
fun map_uwrappers f 
42793  571 
(CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
22674  572 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 
573 
CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 

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

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

575 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  576 
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

577 

22674  578 

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

580 

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

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

582 
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

583 

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

584 
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

585 
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

586 

22674  587 
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, 
24358  588 
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, 
22674  589 
swrappers, uwrappers, ...}) = 
24358  590 
if pointer_eq (cs, cs') then cs 
591 
else 

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

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

593 
> merge_thms (addSI NONE NONE) safeIs safeIs2 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

594 
> merge_thms (addSE NONE NONE) safeEs safeEs2 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

595 
> merge_thms (addI NONE NONE) hazIs hazIs2 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

596 
> merge_thms (addE NONE NONE) hazEs hazEs2 
2425068fe13a
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents:
42807
diff
changeset

597 
> 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

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

600 

601 
(* data *) 

602 

603 
structure Claset = Generic_Data 

604 
( 

605 
type T = claset; 

606 
val empty = empty_cs; 

607 
val extend = I; 

608 
val merge = merge_cs; 

609 
); 

610 

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

612 
val rep_claset_of = rep_cs o claset_of; 

613 

614 
val get_cs = Claset.get; 

615 
val map_cs = Claset.map; 

616 

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

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

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

619 
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

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

621 
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

622 

42793  623 
fun map_claset f = Context.proof_map (map_cs f); 
624 
fun put_claset cs = map_claset (K cs); 

625 

626 
fun print_claset ctxt = 

627 
let 

628 
val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; 

51584  629 
val pretty_thms = map (Display.pretty_thm_item ctxt) o Item_Net.content; 
42793  630 
in 
631 
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), 

632 
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), 

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

634 
Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), 

635 
Pretty.strs ("safe wrappers:" :: map #1 swrappers), 

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

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

637 
> Pretty.writeln_chunks 
42793  638 
end; 
639 

640 

641 
(* oldstyle declarations *) 

642 

643 
fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt; 

644 

645 
val op addSIs = decl (addSI NONE); 

646 
val op addSEs = decl (addSE NONE); 

647 
val op addSDs = decl (addSD NONE); 

648 
val op addIs = decl (addI NONE); 

649 
val op addEs = decl (addE NONE); 

650 
val op addDs = decl (addD NONE); 

651 
val op delrules = decl delrule; 

652 

653 

654 

655 
(*** Modifying the wrapper tacticals ***) 

656 

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

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

659 

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

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

662 

663 
fun delete_warn msg (key : string) xs = 

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

665 
else (warning msg; xs); 

666 

667 
(*Add/replace a safe wrapper*) 

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

668 
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

669 
(map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper)); 
42793  670 

671 
(*Add/replace an unsafe wrapper*) 

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

672 
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

673 
(map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper)); 
42793  674 

675 
(*Remove a safe wrapper*) 

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

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

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

679 
(*Remove an unsafe wrapper*) 

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

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

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

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

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

685 
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

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

687 
ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); 
42793  688 

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

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

691 
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

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

693 
ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt); 
42793  694 

58957  695 
fun ctxt addD2 (name, thm) = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

696 
ctxt addafter (name, fn ctxt' => dresolve_tac [thm] THEN' assume_tac ctxt'); 
58957  697 
fun ctxt addE2 (name, thm) = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58958
diff
changeset

698 
ctxt addafter (name, fn ctxt' => eresolve_tac [thm] THEN' assume_tac ctxt'); 
58957  699 
fun ctxt addSD2 (name, thm) = 
700 
ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac); 

701 
fun ctxt addSE2 (name, thm) = 

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

42793  703 

1711  704 

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

705 

1800  706 
(**** Simple tactics for theorem proving ****) 
0  707 

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

42793  709 
fun safe_step_tac ctxt = 
710 
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in 

711 
appSWrappers ctxt 

712 
(FIRST' 

713 
[eq_assume_tac, 

58957  714 
eq_mp_tac ctxt, 
9938  715 
bimatch_from_nets_tac safe0_netpair, 
51798  716 
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), 
42793  717 
bimatch_from_nets_tac safep_netpair]) 
718 
end; 

0  719 

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

5757  723 

0  724 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
42793  725 
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

726 

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

727 

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

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

729 

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

731 

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

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

733 
create precisely n subgoals.*) 
10736  734 
fun n_bimatch_from_nets_tac n = 
42790  735 
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

736 

58957  737 
fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i; 
738 
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

739 

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

740 
(*Twoway branching is allowed only if one of the branches immediately closes*) 
58957  741 
fun bimatch2_tac ctxt netpair i = 
42790  742 
n_bimatch_from_nets_tac 2 netpair i THEN 
58957  743 
(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

744 

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

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

748 
appSWrappers ctxt 

749 
(FIRST' 

58957  750 
[eq_assume_contr_tac ctxt, 
9938  751 
bimatch_from_nets_tac safe0_netpair, 
51798  752 
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), 
9938  753 
n_bimatch_from_nets_tac 1 safep_netpair, 
58957  754 
bimatch2_tac ctxt safep_netpair]) 
42793  755 
end; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

756 

42793  757 
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

758 

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

759 

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

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

761 

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

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

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

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

768 

4066  769 
(*These unsafe steps could generate more subgoals.*) 
42793  770 
fun instp_step_tac ctxt = 
771 
biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt)); 

0  772 

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

42793  774 
fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; 
0  775 

42793  776 
fun haz_step_tac ctxt = 
777 
biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt)); 

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

778 

0  779 
(*Single step for the prover. FAILS unless it makes progress. *) 
42793  780 
fun step_tac ctxt i = 
781 
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i; 

0  782 

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

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

42793  785 
fun slow_step_tac ctxt i = 
786 
safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i; 

0  787 

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

788 

1800  789 
(**** The following tactics all fail unless they solve one goal ****) 
0  790 

791 
(*Dumb but fast*) 

42793  792 
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

793 
Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 
0  794 

795 
(*Slower but smarter than fast_tac*) 

42793  796 
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

797 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  798 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); 
0  799 

9402  800 
(*even a bit smarter than best_tac*) 
42793  801 
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

802 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  803 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); 
9402  804 

42793  805 
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

806 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  807 
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1)); 
0  808 

42793  809 
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

810 
Object_Logic.atomize_prems_tac ctxt THEN' 
42793  811 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); 
0  812 

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

813 

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

815 

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

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

817 

42793  818 
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

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

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

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

823 

42793  824 
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

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

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

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

829 

42790  830 

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

832 
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

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

835 

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

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

837 
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

838 
greater search depth required.*) 
42793  839 
fun dup_step_tac ctxt = 
840 
biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt)); 

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

841 

5523  842 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  843 
local 
42793  844 
fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt); 
42790  845 
in 
42793  846 
fun depth_tac ctxt m i state = SELECT_GOAL 
847 
(safe_steps_tac ctxt 1 THEN_ELSE 

848 
(DEPTH_SOLVE (depth_tac ctxt m 1), 

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

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

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

852 

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

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

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

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

862 

42793  863 
fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); 
24021  864 

865 

5885  866 
(* attributes *) 
867 

42793  868 
fun attrib f = 
869 
Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context); 

5885  870 

18691  871 
val safe_elim = attrib o addSE; 
872 
val safe_intro = attrib o addSI; 

42793  873 
val safe_dest = attrib o addSD; 
18691  874 
val haz_elim = attrib o addE; 
875 
val haz_intro = attrib o addI; 

42793  876 
val haz_dest = attrib o addD; 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset

877 

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

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

879 
Thm.declaration_attribute (fn th => fn context => 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset

880 
context > map_cs (delrule (SOME context) th) > 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
42817
diff
changeset

881 
Thm.attribute_declaration Context_Rules.rule_del th); 
5885  882 

883 

5841  884 

5885  885 
(** concrete syntax of attributes **) 
5841  886 

887 
val introN = "intro"; 

888 
val elimN = "elim"; 

889 
val destN = "dest"; 

890 

58826  891 
val _ = 
892 
Theory.setup 

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

894 
"classical swap of introduction rule" #> 

895 
Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query) 

896 
"declaration of Classical destruction rule" #> 

897 
Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query) 

898 
"declaration of Classical elimination rule" #> 

899 
Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query) 

900 
"declaration of Classical introduction rule" #> 

901 
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) 

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

5841  903 

904 

905 

7230  906 
(** proof methods **) 
907 

908 
local 

909 

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

910 
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => 
5841  911 
let 
33369  912 
val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; 
42793  913 
val {xtra_netpair, ...} = rep_claset_of ctxt; 
33369  914 
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

915 
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

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

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

921 
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; 
5841  922 

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

923 
in 
7281  924 

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

925 
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

926 
 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

927 

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

928 
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

929 
HEADGOAL (rule_tac ctxt rules facts) ORELSE 
26470  930 
Class.default_intro_tac ctxt facts; 
10309  931 

7230  932 
end; 
5841  933 

934 

6502  935 
(* automatic methods *) 
5841  936 

5927  937 
val cla_modifiers = 
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

938 
[Args.$$$ destN  Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

939 
Args.$$$ destN  Args.colon >> K (Method.modifier (haz_dest NONE) @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

940 
Args.$$$ elimN  Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

941 
Args.$$$ elimN  Args.colon >> K (Method.modifier (haz_elim NONE) @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

942 
Args.$$$ introN  Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

943 
Args.$$$ introN  Args.colon >> K (Method.modifier (haz_intro NONE) @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57859
diff
changeset

944 
Args.del  Args.colon >> K (Method.modifier rule_del @{here})]; 
5927  945 

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

5841  948 

949 

950 

58826  951 
(** method setup **) 
5841  952 

58826  953 
val _ = 
954 
Theory.setup 

955 
(Method.setup @{binding default} 

956 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules))) 

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

958 
Method.setup @{binding rule} 

959 
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) 

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

961 
Method.setup @{binding contradiction} 

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

963 
"proof by contradiction" #> 

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

965 
"repeatedly apply safe steps" #> 

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

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

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

969 
Method.setup @{binding deepen} 

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

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

972 
"classical prover (iterative deepening)" #> 

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

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

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

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

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

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

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

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

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

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

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

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

5841  985 

8667  986 

987 
(** outer syntax **) 

988 

24867  989 
val _ = 
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58838
diff
changeset

990 
Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner" 
51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51584
diff
changeset

991 
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of))); 
8667  992 

5841  993 
end; 