author  paulson 
Wed, 19 Mar 1997 10:23:09 +0100  
changeset 2813  cc4c816dafdc 
parent 2689  6d3d893453de 
child 2868  17a23a62f82a 
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 

17 
signature CLASSICAL_DATA = 

18 
sig 

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

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

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

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

22 
val sizef : thm > int (* size function for BEST_FIRST *) 
0  23 
val hyp_subst_tacs: (int > tactic) list 
24 
end; 

25 

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

1800  27 
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 
2630  28 
setSWrapper compSWrapper setWrapper compWrapper 
29 
addSbefore addSaltern addbefore addaltern; 

0  30 

31 

32 
signature CLASSICAL = 

33 
sig 

34 
type claset 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

53 

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

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

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

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

57 
hazIs: thm list, hazEs: thm list, 
2630  58 
uwrapper: (int > tactic) > (int > tactic), 
59 
swrapper: (int > tactic) > (int > tactic), 

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

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

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

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

64 

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

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

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

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

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

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

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

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

72 
val depth_tac : claset > int > int > tactic 
1938  73 
val DEEPEN : (int > int > tactic) > int > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

75 

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

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

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

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

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

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

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

82 
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

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

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

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

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

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

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

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

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

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

93 
val instp_step_tac : claset > int > tactic 
1724  94 

95 
val claset : claset ref 

96 
val AddDs : thm list > unit 

97 
val AddEs : thm list > unit 

98 
val AddIs : thm list > unit 

99 
val AddSDs : thm list > unit 

100 
val AddSEs : thm list > unit 

101 
val AddSIs : thm list > unit 

1807  102 
val Delrules : thm list > unit 
1814  103 
val Safe_step_tac : int > tactic 
1800  104 
val Step_tac : int > tactic 
1724  105 
val Fast_tac : int > tactic 
1800  106 
val Best_tac : int > tactic 
2066  107 
val Slow_tac : int > tactic 
108 
val Slow_best_tac : int > tactic 

1800  109 
val Deepen_tac : int > int > tactic 
1724  110 

0  111 
end; 
112 

113 

114 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 

115 
struct 

116 

117 
local open Data in 

118 

1800  119 
(*** Useful tactics for classical reasoning ***) 
0  120 

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

0  123 

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

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

126 

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

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

128 
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

129 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  130 

131 
(*Like mp_tac but instantiates no variables*) 

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

132 
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

133 

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

0  136 

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

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

139 

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

141 
trying rules in order. *) 

142 
fun swap_res_tac rls = 

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

145 
contr_tac ORELSE' 

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

0  147 
end; 
148 

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

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

150 
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

151 

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

152 
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

153 
rule_by_tactic (TRYALL (etac revcut_rl)); 
0  154 

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

155 

1800  156 
(**** Classical rule sets ****) 
0  157 

158 
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; 

159 

160 
datatype claset = 

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

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

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

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

164 
hazEs : thm list, (*unsafe elimination rules*) 
2630  165 
uwrapper : (int > tactic) > 
166 
(int > tactic), (*for transforming step_tac*) 

167 
swrapper : (int > tactic) > 

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

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

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

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

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

172 
dup_netpair : netpair}; (*nets for duplication*) 
0  173 

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

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

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

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

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

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

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

180 

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

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

182 
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

183 
safep_brls contains all brules that generate 1 or more new subgoals. 
1800  184 
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

185 
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

186 
*) 
0  187 

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

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

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

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

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

192 
hazEs = [], 
2630  193 
uwrapper = I, 
194 
swrapper = I, 

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

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

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

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

198 
dup_netpair = (Net.empty,Net.empty)}; 
0  199 

200 
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = 

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

201 
(writeln"Introduction rules"; prths hazIs; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

202 
writeln"Safe introduction rules"; prths safeIs; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

203 
writeln"Elimination rules"; prths hazEs; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

204 
writeln"Safe elimination rules"; prths safeEs; 
0  205 
()); 
206 

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

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

208 

2630  209 
fun getWrapper (CS{uwrapper,...}) = uwrapper; 
210 

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

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

212 

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

213 

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

215 

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

216 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  217 
***) 
0  218 

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

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

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

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

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

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

224 

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

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

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

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

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

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

231 

1800  232 
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

233 

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

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

235 
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

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

237 
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

238 

1800  239 
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

240 

1800  241 
val delete = delete_tagged_list o joinrules; 
242 

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

243 
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

244 
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

245 

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

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

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

248 
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

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

250 
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

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

252 
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

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

254 
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

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

256 
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

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

258 

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

260 

2630  261 
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

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

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

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

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

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

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

268 
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

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

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

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

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

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

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

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

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

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

278 
hazEs = hazEs, 
2630  279 
uwrapper = uwrapper, 
280 
swrapper = swrapper, 

281 
haz_netpair = haz_netpair, 

282 
dup_netpair = dup_netpair} 

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

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

284 

2630  285 
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

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

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

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

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

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

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

292 
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

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

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

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

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

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

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

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

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

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

302 
hazEs = hazEs, 
2630  303 
uwrapper = uwrapper, 
304 
swrapper = swrapper, 

305 
haz_netpair = haz_netpair, 

306 
dup_netpair = dup_netpair} 

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

307 
end; 
0  308 

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

309 
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

310 

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

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

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

313 

0  314 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
315 

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

316 

1800  317 
(*** Hazardous (unsafe) rules ***) 
0  318 

2630  319 
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

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

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

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

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

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

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

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

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

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

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

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

331 
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

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

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

334 
hazEs = hazEs, 
2630  335 
uwrapper = uwrapper, 
336 
swrapper = swrapper, 

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

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

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

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

340 

2630  341 
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

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

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

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

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

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

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

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

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

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

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

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

353 
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

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

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

356 
hazIs = hazIs, 
2630  357 
uwrapper = uwrapper, 
358 
swrapper = swrapper, 

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

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

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

361 
end; 
0  362 

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

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

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

365 

0  366 
fun cs addDs ths = cs addEs (map make_elim ths); 
367 

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

368 

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

371 
to insert. 

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

372 
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

373 
searches in all the lists and chooses the relevant delXX functions. 
1800  374 
***) 
375 

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

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

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

378 
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

379 
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

380 
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

381 
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

382 
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

383 
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

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

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

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

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

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

389 
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

390 
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

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

392 
else cs; 
1800  393 

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

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

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

396 
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

397 
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

398 
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

399 
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

400 
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

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

402 
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

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

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

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

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

407 
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

408 
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

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

410 
else cs; 
1800  411 

412 

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

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

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

415 
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

416 
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

417 
CS{haz_netpair = delete ([th], []) haz_netpair, 
1800  418 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
419 
safeIs = safeIs, 

420 
safeEs = safeEs, 

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

421 
hazIs = rem_thm (hazIs,th), 
1800  422 
hazEs = hazEs, 
2630  423 
uwrapper = uwrapper, 
424 
swrapper = swrapper, 

1800  425 
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

426 
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

427 
else cs; 
1800  428 

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

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

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

431 
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

432 
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

433 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
1800  434 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
435 
safeIs = safeIs, 

436 
safeEs = safeEs, 

437 
hazIs = hazIs, 

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

438 
hazEs = rem_thm (hazEs,th), 
2630  439 
uwrapper = uwrapper, 
440 
swrapper = swrapper, 

1800  441 
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

442 
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

443 
else cs; 
1800  444 

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

445 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
1800  446 
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

447 
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

448 
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

449 
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

450 
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

451 
cs); 
1800  452 

453 
val op delrules = foldl delrule; 

454 

455 

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

457 

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

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

460 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
2630  461 
setWrapper new_uwrapper = 
462 
CS{safeIs = safeIs, 

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

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

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

465 
hazEs = hazEs, 
2630  466 
uwrapper = new_uwrapper, 
467 
swrapper = swrapper, 

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

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

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

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

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

472 

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

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

476 
setSWrapper new_swrapper = 

477 
CS{safeIs = safeIs, 

478 
safeEs = safeEs, 

479 
hazIs = hazIs, 

480 
hazEs = hazEs, 

481 
uwrapper = uwrapper, 

482 
swrapper = new_swrapper, 

483 
safe0_netpair = safe0_netpair, 

484 
safep_netpair = safep_netpair, 

485 
haz_netpair = haz_netpair, 

486 
dup_netpair = dup_netpair}; 

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

487 

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

490 

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

492 
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

493 

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

496 
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

497 

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

500 
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

501 

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

504 
treatment of priority might get muddled up.*) 

505 
fun merge_cs 

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

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

2630  510 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
511 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

1711  512 
in cs addSIs safeIs' 
513 
addSEs safeEs' 

514 
addIs hazIs' 

515 
addEs hazEs' 

516 
end; 

517 

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

518 

1800  519 
(**** Simple tactics for theorem proving ****) 
0  520 

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

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

524 
eq_assume_tac, 

525 
eq_mp_tac, 

526 
bimatch_from_nets_tac safe0_netpair, 

527 
FIRST' hyp_subst_tacs, 

528 
bimatch_from_nets_tac safep_netpair]); 

0  529 

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

2630  531 
fun safe_tac cs = REPEAT_DETERM_FIRST 
532 
(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

533 

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

534 
(*But these unsafe steps at least solve a subgoal!*) 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

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

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

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

539 

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

540 
(*These are much worse since they could generate more and more subgoals*) 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

542 
biresolve_from_nets_tac safep_netpair; 
0  543 

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

545 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  546 

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

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

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

549 

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

0  553 

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

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

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

0  558 

1800  559 
(**** The following tactics all fail unless they solve one goal ****) 
0  560 

561 
(*Dumb but fast*) 

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

563 

564 
(*Slower but smarter than fast_tac*) 

565 
fun best_tac cs = 

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

567 

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

569 

570 
fun slow_best_tac cs = 

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

572 

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

573 

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

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

576 

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

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

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

579 
, 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

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

581 

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

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

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

584 
, 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

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

586 

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

588 
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

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

591 

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

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

593 
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

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

595 
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

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

597 

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

598 
(*Searching to depth m.*) 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

599 
fun depth_tac cs m i = STATE(fn state => 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

600 
SELECT_GOAL 
2630  601 
(getWrapper cs 
602 
(fn i => REPEAT_DETERM1 (safe_step_tac cs i) THEN_ELSE 

603 
(DEPTH_SOLVE (depth_tac cs m i), 

604 
inst0_step_tac cs i APPEND 

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

605 
COND (K(m=0)) no_tac 
2630  606 
((instp_step_tac cs i APPEND dup_step_tac cs i) 
607 
THEN DEPTH_SOLVE (depth_tac cs (m1) i)))) 1) 

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

608 
i); 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

609 

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

610 
(*Iterative deepening tactical. Allows us to "deepen" any search tactic*) 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

611 
fun DEEPEN tacf m i = STATE(fn state => 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

612 
if has_fewer_prems i state then no_tac 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

613 
else (writeln ("Depth = " ^ string_of_int m); 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

614 
tacf m i ORELSE DEEPEN tacf (m+2) i)); 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

615 

2173  616 
(*Search, with depth bound m. 
617 
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

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

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

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

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

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

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

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

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

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

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

628 
end); 
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 
fun deepen_tac cs = DEEPEN (safe_depth_tac cs); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

631 

1724  632 
val claset = ref empty_cs; 
633 

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

635 

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

637 

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

639 

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

641 

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

643 

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

645 

1807  646 
fun Delrules ts = (claset := !claset delrules ts); 
647 

1800  648 
(*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*) 
649 

1814  650 
fun Safe_step_tac i = safe_step_tac (!claset) i; 
651 

1800  652 
fun Step_tac i = step_tac (!claset) i; 
653 

1724  654 
fun Fast_tac i = fast_tac (!claset) i; 
655 

1800  656 
fun Best_tac i = best_tac (!claset) i; 
657 

2066  658 
fun Slow_tac i = slow_tac (!claset) i; 
659 

660 
fun Slow_best_tac i = slow_best_tac (!claset) i; 

661 

1800  662 
fun Deepen_tac m = deepen_tac (!claset) m; 
663 

0  664 
end; 
665 
end; 

2630  666 

667 