author  paulson 
Sat, 01 Nov 1997 13:03:00 +0100  
changeset 4066  7b508ac609f7 
parent 3727  ed63c05d7992 
child 4079  9df5e4f22d96 
permissions  rwrr 
0  1 
(* Title: Provers/classical 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Theorem prover for classical reasoning, including predicate calculus, set 

7 
theory, etc. 

8 

9 
Rules must be classified as intr, elim, safe, hazardous. 

10 

11 
A rule is unsafe unless it can be applied blindly without harmful results. 

12 
For a rule to be safe, its premises and conclusion should be logically 

13 
equivalent. There should be no variables in the premises that are not in 

14 
the conclusion. 

15 
*) 

16 

2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

17 
(*Should be a type abbreviation in signature CLASSICAL*) 
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

18 
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; 
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

19 

0  20 
signature CLASSICAL_DATA = 
21 
sig 

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

22 
val mp : thm (* [ P>Q; P ] ==> Q *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

23 
val not_elim : thm (* [ ~P; P ] ==> R *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

24 
val classical : thm (* (~P ==> P) ==> P *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

25 
val sizef : thm > int (* size function for BEST_FIRST *) 
0  26 
val hyp_subst_tacs: (int > tactic) list 
27 
end; 

28 

29 
(*Higher precedence than := facilitates use of references*) 

1800  30 
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 
2630  31 
setSWrapper compSWrapper setWrapper compWrapper 
32 
addSbefore addSaltern addbefore addaltern; 

0  33 

34 

35 
signature CLASSICAL = 

36 
sig 

37 
type claset 

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

38 
val empty_cs : claset 
1711  39 
val merge_cs : claset * claset > claset 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

40 
val addDs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

41 
val addEs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

42 
val addIs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

43 
val addSDs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

44 
val addSEs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

45 
val addSIs : claset * thm list > claset 
1800  46 
val delrules : claset * thm list > claset 
2630  47 
val setSWrapper : claset * ((int > tactic) > (int > tactic)) >claset 
48 
val compSWrapper : claset * ((int > tactic) > (int > tactic)) >claset 

49 
val setWrapper : claset * ((int > tactic) > (int > tactic)) >claset 

50 
val compWrapper : claset * ((int > tactic) > (int > tactic)) >claset 

51 
val addSbefore : claset * (int > tactic) > claset 

52 
val addSaltern : claset * (int > tactic) > claset 

53 
val addbefore : claset * (int > tactic) > claset 

54 
val addaltern : claset * (int > tactic) > claset 

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

55 

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

56 
val print_cs : claset > unit 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

58 
claset > {safeIs: thm list, safeEs: thm list, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

59 
hazIs: thm list, hazEs: thm list, 
2630  60 
uwrapper: (int > tactic) > (int > tactic), 
61 
swrapper: (int > tactic) > (int > tactic), 

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

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

63 
haz_netpair: netpair, dup_netpair: netpair} 
2630  64 
val getWrapper : claset > (int > tactic) > (int > tactic) 
65 
val getSWrapper : claset > (int > tactic) > (int > tactic) 

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

66 

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

67 
val fast_tac : claset > int > tactic 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

68 
val slow_tac : claset > int > tactic 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

69 
val weight_ASTAR : int ref 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

70 
val astar_tac : claset > int > tactic 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

71 
val slow_astar_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

72 
val best_tac : claset > int > tactic 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

73 
val slow_best_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

74 
val depth_tac : claset > int > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

75 
val deepen_tac : claset > int > int > tactic 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

76 

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

77 
val contr_tac : int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

78 
val dup_elim : thm > thm 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

79 
val dup_intr : thm > thm 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

80 
val dup_step_tac : claset > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

81 
val eq_mp_tac : int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

82 
val haz_step_tac : claset > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

83 
val joinrules : thm list * thm list > (bool * thm) list 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

84 
val mp_tac : int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

85 
val safe_tac : claset > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

86 
val safe_step_tac : claset > int > tactic 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

87 
val clarify_tac : claset > int > tactic 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

88 
val clarify_step_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

89 
val step_tac : claset > int > tactic 
2630  90 
val slow_step_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

91 
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

92 
val swapify : thm list > thm list 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

93 
val swap_res_tac : thm list > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

94 
val inst_step_tac : claset > int > tactic 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

95 
val inst0_step_tac : claset > int > tactic 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

96 
val instp_step_tac : claset > int > tactic 
1724  97 

98 
val claset : claset ref 

99 
val AddDs : thm list > unit 

100 
val AddEs : thm list > unit 

101 
val AddIs : thm list > unit 

102 
val AddSDs : thm list > unit 

103 
val AddSEs : thm list > unit 

104 
val AddSIs : thm list > unit 

1807  105 
val Delrules : thm list > unit 
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

106 
val Safe_tac : tactic 
1814  107 
val Safe_step_tac : int > tactic 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

108 
val Clarify_tac : int > tactic 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

109 
val Clarify_step_tac : int > tactic 
1800  110 
val Step_tac : int > tactic 
1724  111 
val Fast_tac : int > tactic 
1800  112 
val Best_tac : int > tactic 
2066  113 
val Slow_tac : int > tactic 
114 
val Slow_best_tac : int > tactic 

1800  115 
val Deepen_tac : int > int > tactic 
1724  116 

0  117 
end; 
118 

119 

120 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 

121 
struct 

122 

123 
local open Data in 

124 

1800  125 
(*** Useful tactics for classical reasoning ***) 
0  126 

1524  127 
val imp_elim = (*cannot use bind_thm within a structure!*) 
128 
store_thm ("imp_elim", make_elim mp); 

0  129 

130 
(*Solve goal that assumes both P and ~P. *) 

131 
val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; 

132 

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

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

134 
Could do the same thing for P<>Q and P... *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

135 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  136 

137 
(*Like mp_tac but instantiates no variables*) 

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

138 
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

139 

1524  140 
val swap = 
141 
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); 

0  142 

143 
(*Creates rules to eliminate ~A, from rules to introduce A*) 

144 
fun swapify intrs = intrs RLN (2, [swap]); 

145 

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

147 
trying rules in order. *) 

148 
fun swap_res_tac rls = 

54  149 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
150 
in assume_tac ORELSE' 

151 
contr_tac ORELSE' 

152 
biresolve_tac (foldr addrl (rls,[])) 

0  153 
end; 
154 

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

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

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

157 

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

158 
fun dup_elim th = th RSN (2, revcut_rl) > assumption 2 > Sequence.hd > 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

159 
rule_by_tactic (TRYALL (etac revcut_rl)); 
0  160 

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

161 

1800  162 
(**** Classical rule sets ****) 
0  163 

164 
datatype claset = 

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

165 
CS of {safeIs : thm list, (*safe introduction rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

166 
safeEs : thm list, (*safe elimination rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

167 
hazIs : thm list, (*unsafe introduction rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

168 
hazEs : thm list, (*unsafe elimination rules*) 
2630  169 
uwrapper : (int > tactic) > 
170 
(int > tactic), (*for transforming step_tac*) 

171 
swrapper : (int > tactic) > 

172 
(int > tactic), (*for transform. safe_step_tac*) 

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

173 
safe0_netpair : netpair, (*nets for trivial cases*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

174 
safep_netpair : netpair, (*nets for >0 subgoals*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

175 
haz_netpair : netpair, (*nets for unsafe rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

176 
dup_netpair : netpair}; (*nets for duplication*) 
0  177 

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

178 
(*Desired invariants are 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

179 
safe0_netpair = build safe0_brls, 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

180 
safep_netpair = build safep_brls, 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

181 
haz_netpair = build (joinrules(hazIs, hazEs)), 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

182 
dup_netpair = build (joinrules(map dup_intr hazIs, 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

184 

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

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

186 
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

187 
safep_brls contains all brules that generate 1 or more new subgoals. 
1800  188 
The theorem lists are largely comments, though they are used in merge_cs. 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

189 
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

190 
*) 
0  191 

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

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

193 
CS{safeIs = [], 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

194 
safeEs = [], 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

195 
hazIs = [], 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

196 
hazEs = [], 
2630  197 
uwrapper = I, 
198 
swrapper = I, 

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

199 
safe0_netpair = (Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

200 
safep_netpair = (Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

201 
haz_netpair = (Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

202 
dup_netpair = (Net.empty,Net.empty)}; 
0  203 

3546  204 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
205 
let val pretty_thms = map Display.pretty_thm in 

206 
Pretty.writeln (Pretty.big_list "introduction rules:" (pretty_thms hazIs)); 

207 
Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); 

208 
Pretty.writeln (Pretty.big_list "elimination rules:" (pretty_thms hazEs)); 

209 
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)) 

210 
end; 

0  211 

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

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

213 

2630  214 
fun getWrapper (CS{uwrapper,...}) = uwrapper; 
215 

216 
fun getSWrapper (CS{swrapper,...}) = swrapper; 

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

217 

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

218 

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

220 

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

221 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  222 
***) 
0  223 

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

224 
(*For use with biresolve_tac. Combines intr rules with swap to handle negated 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

225 
assumptions. Pairs elim rules with true. *) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

226 
fun joinrules (intrs,elims) = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

229 

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

230 
(*Priority: prefer rules with fewest subgoals, 
1231  231 
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

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

233 
 tag_brls k (brl::brls) = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

234 
(1000000*subgoals_of_brl brl + k, brl) :: 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

236 

1800  237 
fun insert_tagged_list kbrls netpr = foldr insert_tagged_brl (kbrls, netpr); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

238 

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

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

240 
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

241 
new insertions the lowest priority.*) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

242 
fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

243 

1800  244 
fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

245 

1800  246 
val delete = delete_tagged_list o joinrules; 
247 

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

248 
val mem_thm = gen_mem eq_thm 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

249 
and rem_thm = gen_rem eq_thm; 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

250 

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

251 
(*Warn if the rule is already present ELSEWHERE in the claset. The addition 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

252 
is still allowed.*) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

253 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

254 
if mem_thm (th, safeIs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

255 
warning ("rule already in claset as Safe Intr\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

256 
else if mem_thm (th, safeEs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

257 
warning ("rule already in claset as Safe Elim\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

258 
else if mem_thm (th, hazIs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

259 
warning ("rule already in claset as unsafe Intr\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

260 
else if mem_thm (th, hazEs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

261 
warning ("rule already in claset as unsafe Elim\n" ^ string_of_thm th) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

262 
else (); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

263 

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

265 

2630  266 
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

267 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

269 
if mem_thm (th, safeIs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

270 
(warning ("ignoring duplicate Safe Intr\n" ^ string_of_thm th); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

273 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

274 
partition (fn rl => nprems_of rl=0) [th] 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

275 
val nI = length safeIs + 1 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

277 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

279 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

280 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

283 
hazEs = hazEs, 
2630  284 
uwrapper = uwrapper, 
285 
swrapper = swrapper, 

286 
haz_netpair = haz_netpair, 

287 
dup_netpair = dup_netpair} 

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

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

289 

2630  290 
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

291 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

293 
if mem_thm (th, safeEs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

294 
(warning ("ignoring duplicate Safe Elim\n" ^ string_of_thm th); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

297 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

298 
partition (fn rl => nprems_of rl=1) [th] 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

299 
val nI = length safeIs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

300 
and nE = length safeEs + 1 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

301 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

303 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

304 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

307 
hazEs = hazEs, 
2630  308 
uwrapper = uwrapper, 
309 
swrapper = swrapper, 

310 
haz_netpair = haz_netpair, 

311 
dup_netpair = dup_netpair} 

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

312 
end; 
0  313 

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

314 
fun rev_foldl f (e, l) = foldl f (e, rev l); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

315 

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

316 
val op addSIs = rev_foldl addSI; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

317 
val op addSEs = rev_foldl addSE; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

318 

0  319 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
320 

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

321 

1800  322 
(*** Hazardous (unsafe) rules ***) 
0  323 

2630  324 
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

325 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

327 
if mem_thm (th, hazIs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

328 
(warning ("ignoring duplicate unsafe Intr\n" ^ string_of_thm th); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

331 
let val nI = length hazIs + 1 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

333 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

334 
CS{hazIs = th::hazIs, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

335 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

336 
dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

339 
hazEs = hazEs, 
2630  340 
uwrapper = uwrapper, 
341 
swrapper = swrapper, 

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

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

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

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

345 

2630  346 
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

347 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

349 
if mem_thm (th, hazEs) then 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

350 
(warning ("ignoring duplicate unsafe Elim\n" ^ string_of_thm th); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

353 
let val nI = length hazIs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

354 
and nE = length hazEs + 1 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

355 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

356 
CS{hazEs = th::hazEs, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

357 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

358 
dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

361 
hazIs = hazIs, 
2630  362 
uwrapper = uwrapper, 
363 
swrapper = swrapper, 

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

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

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

366 
end; 
0  367 

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

368 
val op addIs = rev_foldl addI; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

369 
val op addEs = rev_foldl addE; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

370 

0  371 
fun cs addDs ths = cs addEs (map make_elim ths); 
372 

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

373 

1800  374 
(*** Deletion of rules 
375 
Working out what to delete, requires repeating much of the code used 

376 
to insert. 

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

377 
Separate functions delSI, etc., are not exported; instead delrules 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

378 
searches in all the lists and chooses the relevant delXX functions. 
1800  379 
***) 
380 

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

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

382 
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

383 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

384 
if mem_thm (th, safeIs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

385 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

386 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

387 
safep_netpair = delete (safep_rls, []) safep_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

388 
safeIs = rem_thm (safeIs,th), 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

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

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

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

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

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

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

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

397 
else cs; 
1800  398 

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

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

400 
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

401 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

402 
if mem_thm (th, safeEs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

403 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

404 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

405 
safep_netpair = delete ([], safep_rls) safep_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

407 
safeEs = rem_thm (safeEs,th), 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

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

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

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

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

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

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

415 
else cs; 
1800  416 

417 

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

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

419 
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

420 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

421 
if mem_thm (th, hazIs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

422 
CS{haz_netpair = delete ([th], []) haz_netpair, 
1800  423 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
424 
safeIs = safeIs, 

425 
safeEs = safeEs, 

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

426 
hazIs = rem_thm (hazIs,th), 
1800  427 
hazEs = hazEs, 
2630  428 
uwrapper = uwrapper, 
429 
swrapper = swrapper, 

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

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

432 
else cs; 
1800  433 

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

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

435 
(cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

436 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

437 
if mem_thm (th, hazEs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

438 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
1800  439 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
440 
safeIs = safeIs, 

441 
safeEs = safeEs, 

442 
hazIs = hazIs, 

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

443 
hazEs = rem_thm (hazEs,th), 
2630  444 
uwrapper = uwrapper, 
445 
swrapper = swrapper, 

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

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

448 
else cs; 
1800  449 

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

450 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
1800  451 
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

452 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

453 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

454 
then delSI th (delSE th (delI th (delE th cs))) 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

455 
else (warning ("rule not in claset\n" ^ (string_of_thm th)); 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

456 
cs); 
1800  457 

458 
val op delrules = foldl delrule; 

459 

460 

2630  461 
(*** Setting or modifying the wrapper tacticals ***) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

462 

2630  463 
(*Set a new uwrapper*) 
464 
fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 

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

465 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
2630  466 
setWrapper new_uwrapper = 
467 
CS{safeIs = safeIs, 

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

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

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

470 
hazEs = hazEs, 
2630  471 
uwrapper = new_uwrapper, 
472 
swrapper = swrapper, 

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

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

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

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

476 
dup_netpair = dup_netpair}; 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

477 

2630  478 
(*Set a new swrapper*) 
479 
fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 

480 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 

481 
setSWrapper new_swrapper = 

482 
CS{safeIs = safeIs, 

483 
safeEs = safeEs, 

484 
hazIs = hazIs, 

485 
hazEs = hazEs, 

486 
uwrapper = uwrapper, 

487 
swrapper = new_swrapper, 

488 
safe0_netpair = safe0_netpair, 

489 
safep_netpair = safep_netpair, 

490 
haz_netpair = haz_netpair, 

491 
dup_netpair = dup_netpair}; 

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

492 

2630  493 
(*Compose a tactical with the existing uwrapper*) 
494 
fun cs compWrapper uwrapper' = cs setWrapper (uwrapper' o getWrapper cs); 

495 

496 
(*Compose a tactical with the existing swrapper*) 

497 
fun cs compSWrapper swrapper' = cs setSWrapper (swrapper' o getSWrapper cs); 

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

498 

2630  499 
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) 
500 
fun cs addSbefore tac1 = cs compSWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); 

501 
fun cs addSaltern tac2 = cs compSWrapper (fn tac1 => tac1 ORELSE' tac2); 

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

502 

2630  503 
(*compose a tactic sequentially before/alternatively after the step tactic*) 
504 
fun cs addbefore tac1 = cs compWrapper (fn tac2 => tac1 THEN_MAYBE' tac2); 

505 
fun cs addaltern tac2 = cs compWrapper (fn tac1 => tac1 APPEND' tac2); 

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

506 

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

509 
treatment of priority might get muddled up.*) 

510 
fun merge_cs 

2630  511 
(cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, 
1711  512 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) = 
513 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 

514 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  515 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
516 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

1711  517 
in cs addSIs safeIs' 
518 
addSEs safeEs' 

519 
addIs hazIs' 

520 
addEs hazEs' 

521 
end; 

522 

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

523 

1800  524 
(**** Simple tactics for theorem proving ****) 
0  525 

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

2630  527 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
528 
getSWrapper cs (FIRST' [ 

529 
eq_assume_tac, 

530 
eq_mp_tac, 

531 
bimatch_from_nets_tac safe0_netpair, 

532 
FIRST' hyp_subst_tacs, 

533 
bimatch_from_nets_tac safep_netpair]); 

0  534 

535 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 

2630  536 
fun safe_tac cs = REPEAT_DETERM_FIRST 
537 
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 

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

538 

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

539 

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

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

541 

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

542 
fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

543 

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

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

545 
create precisely n subgoals.*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

546 
fun n_bimatch_from_nets_tac n = 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

547 
biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

548 

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

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

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

551 

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

552 
(*Twoway branching is allowed only if one of the branches immediately closes*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

553 
fun bimatch2_tac netpair i = 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

554 
n_bimatch_from_nets_tac 2 netpair i THEN 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

555 
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

556 

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

557 
(*Attack subgoals using safe inferences  matching, not resolution*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

558 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

559 
getSWrapper cs (FIRST' [ 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

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

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

562 
FIRST' hyp_subst_tacs, 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

563 
n_bimatch_from_nets_tac 1 safep_netpair, 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

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

565 

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

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

567 

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

568 

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

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

570 

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

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

573 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

574 
assume_tac APPEND' 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

575 
contr_tac APPEND' 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

577 

4066  578 
(*These unsafe steps could generate more subgoals.*) 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

579 
fun instp_step_tac (CS{safep_netpair,...}) = 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

580 
biresolve_from_nets_tac safep_netpair; 
0  581 

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

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

583 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  584 

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

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

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

587 

0  588 
(*Single step for the prover. FAILS unless it makes progress. *) 
2630  589 
fun step_tac cs i = getWrapper cs 
590 
(K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) i; 

0  591 

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

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

2630  594 
fun slow_step_tac cs i = getWrapper cs 
595 
(K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i; 

0  596 

1800  597 
(**** The following tactics all fail unless they solve one goal ****) 
0  598 

599 
(*Dumb but fast*) 

600 
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 

601 

602 
(*Slower but smarter than fast_tac*) 

603 
fun best_tac cs = 

604 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 

605 

606 
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 

607 

608 
fun slow_best_tac cs = 

609 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 

610 

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

611 

1800  612 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

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

614 

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

615 
fun astar_tac cs = 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

616 
SELECT_GOAL ( ASTAR (has_fewer_prems 1 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

617 
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

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

619 

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

620 
fun slow_astar_tac cs = 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

621 
SELECT_GOAL ( ASTAR (has_fewer_prems 1 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

622 
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

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

624 

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

626 
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

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

629 

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

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

631 
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

632 
greater search depth required.*) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

633 
fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

635 

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

636 
(*Searching to depth m.*) 
3537  637 
fun depth_tac cs m i state = 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

638 
SELECT_GOAL 
2630  639 
(getWrapper cs 
3204
c1653e2e146d
corrected depth_tac: no call for safe_step_tac if subgoal not present
oheimb
parents:
2868
diff
changeset

640 
(fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac 
c1653e2e146d
corrected depth_tac: no call for safe_step_tac if subgoal not present
oheimb
parents:
2868
diff
changeset

641 
(safe_step_tac cs i)) THEN_ELSE 
2630  642 
(DEPTH_SOLVE (depth_tac cs m i), 
643 
inst0_step_tac cs i APPEND 

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

644 
COND (K(m=0)) no_tac 
2630  645 
((instp_step_tac cs i APPEND dup_step_tac cs i) 
646 
THEN DEPTH_SOLVE (depth_tac cs (m1) i)))) 1) 

3537  647 
i state; 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

648 

2173  649 
(*Search, with depth bound m. 
650 
This is the "entry point", which does safe inferences first.*) 

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

651 
fun safe_depth_tac cs m = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

653 
(fn (prem,i) => 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

654 
let val deti = 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

655 
(*No Vars in the goal? No need to backtrack between goals.*) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

656 
case term_vars prem of 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

657 
[] => DETERM 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

658 
 _::_ => I 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

659 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

660 
DEPTH_SOLVE (deti (depth_tac cs m 1))) i 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

662 

2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

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

664 

1724  665 
val claset = ref empty_cs; 
666 

667 
fun AddDs ts = (claset := !claset addDs ts); 

668 

669 
fun AddEs ts = (claset := !claset addEs ts); 

670 

671 
fun AddIs ts = (claset := !claset addIs ts); 

672 

673 
fun AddSDs ts = (claset := !claset addSDs ts); 

674 

675 
fun AddSEs ts = (claset := !claset addSEs ts); 

676 

677 
fun AddSIs ts = (claset := !claset addSIs ts); 

678 

1807  679 
fun Delrules ts = (claset := !claset delrules ts); 
680 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

681 
(** The abstraction over the proof state delays the dereferencing **) 
1800  682 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

683 
fun Safe_tac st = safe_tac (!claset) st; 
1814  684 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

685 
fun Safe_step_tac i st = safe_step_tac (!claset) i st; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

686 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

687 
fun Clarify_step_tac i st = clarify_step_tac (!claset) i st; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

688 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

689 
fun Clarify_tac i st = clarify_tac (!claset) i st; 
1800  690 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

691 
fun Step_tac i st = step_tac (!claset) i st; 
1724  692 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

693 
fun Fast_tac i st = fast_tac (!claset) i st; 
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

694 

ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

695 
fun Best_tac i st = best_tac (!claset) i st; 
1800  696 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

697 
fun Slow_tac i st = slow_tac (!claset) i st; 
2066  698 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

699 
fun Slow_best_tac i st = slow_best_tac (!claset) i st; 
2066  700 

3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

701 
fun Deepen_tac m = deepen_tac (!claset) m; 
1800  702 

0  703 
end; 
704 
end; 

2630  705 

706 