author  paulson 
Fri, 14 Jun 1996 12:26:06 +0200  
changeset 1800  3d9d2ef0cd3b 
parent 1724  bb02e6976258 
child 1807  3ff66483a8d4 
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 

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

17 
infix 1 THEN_MAYBE; 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

18 

0  19 
signature CLASSICAL_DATA = 
20 
sig 

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

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

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

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

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

27 

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

1800  29 
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

30 
setwrapper compwrapper addbefore addafter; 
0  31 

32 

33 
signature CLASSICAL = 

34 
sig 

35 
type claset 

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

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

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

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

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

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

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

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

44 
val addSIs : claset * thm list > claset 
1800  45 
val delrules : claset * thm list > claset 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

46 
val setwrapper : claset * (tactic>tactic) > claset 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

47 
val compwrapper : claset * (tactic>tactic) > claset 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

48 
val addbefore : claset * tactic > claset 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

49 
val addafter : claset * tactic > claset 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

50 

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

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

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

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

54 
hazIs: thm list, hazEs: thm list, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

57 
haz_netpair: netpair, dup_netpair: netpair} 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

58 
val getwrapper : claset > tactic > tactic 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

59 
val THEN_MAYBE : tactic * tactic > tactic 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

60 

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

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

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

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

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

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

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

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

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

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

70 

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

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

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

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

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

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

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

77 
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

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

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

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

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

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

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

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

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

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

87 
val instp_step_tac : claset > int > tactic 
1724  88 

89 
val claset : claset ref 

90 
val AddDs : thm list > unit 

91 
val AddEs : thm list > unit 

92 
val AddIs : thm list > unit 

93 
val AddSDs : thm list > unit 

94 
val AddSEs : thm list > unit 

95 
val AddSIs : thm list > unit 

1800  96 
val Step_tac : int > tactic 
1724  97 
val Fast_tac : int > tactic 
1800  98 
val Best_tac : int > tactic 
99 
val Deepen_tac : int > int > tactic 

1724  100 

0  101 
end; 
102 

103 

104 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 

105 
struct 

106 

107 
local open Data in 

108 

1800  109 
(*** Useful tactics for classical reasoning ***) 
0  110 

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

0  113 

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

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

116 

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

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

118 
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

119 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  120 

121 
(*Like mp_tac but instantiates no variables*) 

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

122 
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

123 

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

0  126 

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

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

129 

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

131 
trying rules in order. *) 

132 
fun swap_res_tac rls = 

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

135 
contr_tac ORELSE' 

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

0  137 
end; 
138 

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

139 
(*Duplication of hazardous rules, for complete provers*) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

141 

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

142 
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

143 
rule_by_tactic (TRYALL (etac revcut_rl)); 
0  144 

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

145 

1800  146 
(**** Classical rule sets ****) 
0  147 

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

149 

150 
datatype claset = 

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

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

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

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

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

155 
wrapper : tactic>tactic, (*for transforming step_tac*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

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

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

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

159 
dup_netpair : netpair}; (*nets for duplication*) 
0  160 

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

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

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

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

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

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

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

167 

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

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

169 
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

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

172 
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

173 
*) 
0  174 

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

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

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

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

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

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

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

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

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

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

184 
dup_netpair = (Net.empty,Net.empty)}; 
0  185 

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

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

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

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

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

190 
writeln"Safe elimination rules"; prths safeEs; 
0  191 
()); 
192 

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

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

194 

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

195 
fun getwrapper (CS{wrapper,...}) = wrapper; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

196 

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

197 

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

199 

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

200 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  201 
***) 
0  202 

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

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

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

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

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

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

208 

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

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

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

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

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

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

215 

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

217 

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

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

219 
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

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

221 
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

222 

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

224 

1800  225 
val delete = delete_tagged_list o joinrules; 
226 

227 
(*** Safe rules ***) 

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

228 

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

229 
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

230 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

232 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1800  233 
partition (fn rl => nprems_of rl=0) ths 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

236 
in CS{safeIs = ths@safeIs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

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

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

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

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

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

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

246 

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

247 
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

248 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

250 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1800  251 
partition (fn rl => nprems_of rl=1) ths 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

253 
and nE = length safeEs + length ths 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

255 
CS{safeEs = ths@safeEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

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

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

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

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

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

264 
end; 
0  265 

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

267 

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

268 

1800  269 
(*** Hazardous (unsafe) rules ***) 
0  270 

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

271 
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

272 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

275 
and nE = length hazEs 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

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

280 
safeIs = safeIs, 
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 
hazEs = hazEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

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

287 

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

288 
fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

289 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

292 
and nE = length hazEs + length ths 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

294 
CS{hazEs = ths@hazEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

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

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

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

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

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

303 
end; 
0  304 

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

306 

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

307 

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

310 
to insert. 

311 
Separate functions delSIs, etc., are not exported; instead delrules 

312 
searches in all the lists and chooses the relevant delXX function. 

313 
***) 

314 

315 
fun delSIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 

316 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 

317 
th) = 

318 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] 

319 
in CS{safeIs = gen_rem eq_thm (safeIs,th), 

320 
safe0_netpair = delete (safe0_rls, []) safe0_netpair, 

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

322 
safeEs = safeEs, 

323 
hazIs = hazIs, 

324 
hazEs = hazEs, 

325 
wrapper = wrapper, 

326 
haz_netpair = haz_netpair, 

327 
dup_netpair = dup_netpair} 

328 
end; 

329 

330 
fun delSEs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 

331 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 

332 
th) = 

333 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] 

334 
in CS{safeEs = gen_rem eq_thm (safeEs,th), 

335 
safe0_netpair = delete ([], safe0_rls) safe0_netpair, 

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

337 
safeIs = safeIs, 

338 
hazIs = hazIs, 

339 
hazEs = hazEs, 

340 
wrapper = wrapper, 

341 
haz_netpair = haz_netpair, 

342 
dup_netpair = dup_netpair} 

343 
end; 

344 

345 

346 
fun delIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 

347 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 

348 
th) = 

349 
CS{hazIs = gen_rem eq_thm (hazIs,th), 

350 
haz_netpair = delete ([th], []) haz_netpair, 

351 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 

352 
safeIs = safeIs, 

353 
safeEs = safeEs, 

354 
hazEs = hazEs, 

355 
wrapper = wrapper, 

356 
safe0_netpair = safe0_netpair, 

357 
safep_netpair = safep_netpair}; 

358 

359 
fun delEs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 

360 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 

361 
th) = 

362 
CS{hazEs = gen_rem eq_thm (hazEs,th), 

363 
haz_netpair = delete ([], [th]) haz_netpair, 

364 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 

365 
safeIs = safeIs, 

366 
safeEs = safeEs, 

367 
hazIs = hazIs, 

368 
wrapper = wrapper, 

369 
safe0_netpair = safe0_netpair, 

370 
safep_netpair = safep_netpair}; 

371 

372 
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = 

373 
if gen_mem eq_thm (th, safeIs) then delSIs(cs,th) 

374 
else if gen_mem eq_thm (th, safeEs) then delSEs(cs,th) 

375 
else if gen_mem eq_thm (th, hazIs) then delIs(cs,th) 

376 
else if gen_mem eq_thm (th, hazEs) then delEs(cs,th) 

377 
else (warning ("rule not in claset\n" ^ (string_of_thm th)); 

378 
cs); 

379 

380 
val op delrules = foldl delrule; 

381 

382 

383 
(*** Setting or modifying the wrapper tactical ***) 

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

384 

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

385 
(*Set a new wrapper*) 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

386 
fun (CS{safeIs, safeEs, hazIs, hazEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

387 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

389 
CS{wrapper = new_wrapper, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

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

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

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

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

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

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

398 

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

399 
(*Compose a tactical with the existing wrapper*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

400 
fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs); 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

401 

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

402 
(*Execute tac1, but only execute tac2 if there are at least as many subgoals 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

403 
as before. This ensures that tac2 is only applied to an outcome of tac1.*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

404 
fun tac1 THEN_MAYBE tac2 = 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

405 
STATE (fn state => 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

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

407 
COND (has_fewer_prems (nprems_of state)) all_tac tac2); 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

408 

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

409 
(*Cause a tactic to be executed before/after the step tactic*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

410 
fun cs addbefore tac2 = cs compwrapper (fn tac1 => tac2 THEN_MAYBE tac1); 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

411 
fun cs addafter tac2 = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2); 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

412 

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

413 

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

416 
treatment of priority might get muddled up.*) 

417 
fun merge_cs 

418 
(cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, ...}, 

419 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) = 

420 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 

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

422 
val hazIs' = gen_rems eq_thm (hazIs2,hazIs) 

423 
val hazEs' = gen_rems eq_thm (hazEs2,hazEs) 

424 
in cs addSIs safeIs' 

425 
addSEs safeEs' 

426 
addIs hazIs' 

427 
addEs hazEs' 

428 
end; 

429 

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

430 

1800  431 
(**** Simple tactics for theorem proving ****) 
0  432 

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

434 
fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = 

435 
FIRST' [eq_assume_tac, 

436 
eq_mp_tac, 

437 
bimatch_from_nets_tac safe0_netpair, 

438 
FIRST' hyp_subst_tacs, 

439 
bimatch_from_nets_tac safep_netpair] ; 

440 

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

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

442 
fun safe_tac cs = REPEAT_DETERM_FIRST (safe_step_tac cs); 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

443 

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

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

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

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

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

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

449 

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

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

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

452 
biresolve_from_nets_tac safep_netpair; 
0  453 

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

455 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  456 

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

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

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

459 

0  460 
(*Single step for the prover. FAILS unless it makes progress. *) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

461 
fun step_tac cs i = 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

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

463 
(FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]); 
0  464 

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

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

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

467 
fun slow_step_tac cs i = 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

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

469 
(safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i)); 
0  470 

1800  471 
(**** The following tactics all fail unless they solve one goal ****) 
0  472 

473 
(*Dumb but fast*) 

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

475 

476 
(*Slower but smarter than fast_tac*) 

477 
fun best_tac cs = 

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

479 

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

481 

482 
fun slow_best_tac cs = 

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

484 

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

485 

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

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

488 

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

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

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

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

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

493 

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

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

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

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

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

498 

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

500 
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

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

503 

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

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

505 
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

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

507 
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

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

509 

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

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

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

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

513 
(REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

515 
inst0_step_tac cs 1 APPEND 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

516 
COND (K(m=0)) no_tac 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

517 
((instp_step_tac cs 1 APPEND dup_step_tac cs 1) 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

518 
THEN DEPTH_SOLVE (depth_tac cs (m1) 1)))) 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

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

520 

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

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

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

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

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

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

526 

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

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

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

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

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

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

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

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

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

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

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

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

538 

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

539 
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

540 

1724  541 
val claset = ref empty_cs; 
542 

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

544 

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

546 

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

548 

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

550 

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

552 

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

554 

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

557 
fun Step_tac i = step_tac (!claset) i; 

558 

1724  559 
fun Fast_tac i = fast_tac (!claset) i; 
560 

1800  561 
fun Best_tac i = best_tac (!claset) i; 
562 

563 
fun Deepen_tac m = deepen_tac (!claset) m; 

564 

0  565 
end; 
566 
end; 