author  oheimb 
Sat, 15 Feb 1997 17:43:27 +0100  
changeset 2633  37c0b5a7ee5d 
parent 2601  b301958c465d 
child 2727  230f2643107e 
permissions  rwrr 
1459  1 
(* Title: FOL/simpdata 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
282  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Simplification data for FOL 

7 
*) 

8 

9 
(*** Rewrite rules ***) 

10 

11 
fun int_prove_fun s = 

282  12 
(writeln s; 
13 
prove_goal IFOL.thy s 

14 
(fn prems => [ (cut_facts_tac prems 1), 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset

15 
(IntPr.fast_tac 1) ])); 
0  16 

1953  17 
val conj_simps = map int_prove_fun 
1459  18 
["P & True <> P", "True & P <> P", 
0  19 
"P & False <> False", "False & P <> False", 
20 
"P & P <> P", 

1459  21 
"P & ~P <> False", "~P & P <> False", 
0  22 
"(P & Q) & R <> P & (Q & R)"]; 
23 

1953  24 
val disj_simps = map int_prove_fun 
1459  25 
["P  True <> True", "True  P <> True", 
26 
"P  False <> P", "False  P <> P", 

0  27 
"P  P <> P", 
28 
"(P  Q)  R <> P  (Q  R)"]; 

29 

1953  30 
val not_simps = map int_prove_fun 
282  31 
["~(PQ) <> ~P & ~Q", 
1459  32 
"~ False <> True", "~ True <> False"]; 
0  33 

1953  34 
val imp_simps = map int_prove_fun 
1459  35 
["(P > False) <> ~P", "(P > True) <> True", 
36 
"(False > P) <> True", "(True > P) <> P", 

37 
"(P > P) <> True", "(P > ~P) <> ~P"]; 

0  38 

1953  39 
val iff_simps = map int_prove_fun 
1459  40 
["(True <> P) <> P", "(P <> True) <> P", 
0  41 
"(P <> P) <> True", 
1459  42 
"(False <> P) <> ~P", "(P <> False) <> ~P"]; 
0  43 

1953  44 
val quant_simps = map int_prove_fun 
1459  45 
["(ALL x.P) <> P", "(EX x.P) <> P"]; 
0  46 

47 
(*These are NOT supplied by default!*) 

1953  48 
val distrib_simps = map int_prove_fun 
282  49 
["P & (Q  R) <> P&Q  P&R", 
50 
"(Q  R) & P <> Q&P  R&P", 

0  51 
"(P  Q > R) <> (P > R) & (Q > R)"]; 
52 

282  53 
(** Conversion into rewrite rules **) 
0  54 

53  55 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; 
56 

282  57 
(*Make atomic rewrite rules*) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

58 
fun atomize r = 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

59 
case concl_of r of 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

60 
Const("Trueprop",_) $ p => 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

61 
(case p of 
1459  62 
Const("op >",_)$_$_ => atomize(r RS mp) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

63 
 Const("op &",_)$_$_ => atomize(r RS conjunct1) @ 
1459  64 
atomize(r RS conjunct2) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

65 
 Const("All",_)$_ => atomize(r RS spec) 
1459  66 
 Const("True",_) => [] (*True is DELETED*) 
67 
 Const("False",_) => [] (*should False do something?*) 

429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

68 
 _ => [r]) 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

69 
 _ => [r]; 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

70 

282  71 

72 
val P_iff_F = int_prove_fun "~P ==> (P <> False)"; 

73 
val iff_reflection_F = P_iff_F RS iff_reflection; 

74 

75 
val P_iff_T = int_prove_fun "P ==> (P <> True)"; 

76 
val iff_reflection_T = P_iff_T RS iff_reflection; 

77 

78 
(*Make metaequalities. The operator below is Trueprop*) 

79 
fun mk_meta_eq th = case concl_of th of 

394
432bb9995893
Modified mk_meta_eq to leave metaequlities on unchanged.
nipkow
parents:
371
diff
changeset

80 
Const("==",_)$_$_ => th 
432bb9995893
Modified mk_meta_eq to leave metaequlities on unchanged.
nipkow
parents:
371
diff
changeset

81 
 _ $ (Const("op =",_)$_$_) => th RS eq_reflection 
282  82 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 
83 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F 

84 
 _ => th RS iff_reflection_T; 

0  85 

981  86 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

87 
(*** Classical laws ***) 
282  88 

0  89 
fun prove_fun s = 
282  90 
(writeln s; 
91 
prove_goal FOL.thy s 

92 
(fn prems => [ (cut_facts_tac prems 1), 

1459  93 
(Cla.fast_tac FOL_cs 1) ])); 
745  94 

1953  95 
(*Avoids duplication of subgoals after expand_if, when the true and false 
96 
cases boil down to the same thing.*) 

97 
val cases_simp = prove_fun "(P > Q) & (~P > Q) <> Q"; 

98 

99 
(*At present, miniscoping is for classical logic only. We do NOT include 

100 
distribution of ALL over &, or dually that of EX over .*) 

0  101 

1953  102 
(*Miniscoping: pushing in existential quantifiers*) 
103 
val ex_simps = map prove_fun 

2065  104 
["(EX x. x=t & P(x)) <> P(t)", 
105 
"(EX x. t=x & P(x)) <> P(t)", 

106 
"(EX x. P(x) & Q) <> (EX x.P(x)) & Q", 

1953  107 
"(EX x. P & Q(x)) <> P & (EX x.Q(x))", 
108 
"(EX x. P(x)  Q) <> (EX x.P(x))  Q", 

109 
"(EX x. P  Q(x)) <> P  (EX x.Q(x))", 

110 
"(EX x. P(x) > Q) <> (ALL x.P(x)) > Q", 

111 
"(EX x. P > Q(x)) <> P > (EX x.Q(x))"]; 

112 

113 
(*Miniscoping: pushing in universal quantifiers*) 

114 
val all_simps = map prove_fun 

2065  115 
["(ALL x. x=t > P(x)) <> P(t)", 
116 
"(ALL x. t=x > P(x)) <> P(t)", 

117 
"(ALL x. P(x) & Q) <> (ALL x.P(x)) & Q", 

1953  118 
"(ALL x. P & Q(x)) <> P & (ALL x.Q(x))", 
119 
"(ALL x. P(x)  Q) <> (ALL x.P(x))  Q", 

120 
"(ALL x. P  Q(x)) <> P  (ALL x.Q(x))", 

121 
"(ALL x. P(x) > Q) <> (EX x.P(x)) > Q", 

122 
"(ALL x. P > Q(x)) <> P > (ALL x.Q(x))"]; 

123 

1914  124 
fun int_prove nm thm = qed_goal nm IFOL.thy thm 
125 
(fn prems => [ (cut_facts_tac prems 1), 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2469
diff
changeset

126 
(IntPr.fast_tac 1) ]); 
1914  127 

128 
fun prove nm thm = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]); 

129 

130 
int_prove "conj_commute" "P&Q <> Q&P"; 

131 
int_prove "conj_left_commute" "P&(Q&R) <> Q&(P&R)"; 

132 
val conj_comms = [conj_commute, conj_left_commute]; 

133 

134 
int_prove "disj_commute" "PQ <> QP"; 

135 
int_prove "disj_left_commute" "P(QR) <> Q(PR)"; 

136 
val disj_comms = [disj_commute, disj_left_commute]; 

137 

138 
int_prove "conj_disj_distribL" "P&(QR) <> (P&Q  P&R)"; 

139 
int_prove "conj_disj_distribR" "(PQ)&R <> (P&R  Q&R)"; 

140 

141 
int_prove "disj_conj_distribL" "P(Q&R) <> (PQ) & (PR)"; 

142 
int_prove "disj_conj_distribR" "(P&Q)R <> (PR) & (QR)"; 

143 

144 
int_prove "imp_conj_distrib" "(P > (Q&R)) <> (P>Q) & (P>R)"; 

145 
int_prove "imp_conj" "((P&Q)>R) <> (P > (Q > R))"; 

146 
int_prove "imp_disj" "(PQ > R) <> (P>R) & (Q>R)"; 

147 

148 
int_prove "de_Morgan_disj" "(~(P  Q)) <> (~P & ~Q)"; 

149 
prove "de_Morgan_conj" "(~(P & Q)) <> (~P  ~Q)"; 

150 

151 
prove "not_iff" "~(P <> Q) <> (P <> ~Q)"; 

152 

153 
prove "not_all" "(~ (ALL x.P(x))) <> (EX x.~P(x))"; 

154 
prove "imp_all" "((ALL x.P(x)) > Q) <> (EX x.P(x) > Q)"; 

155 
int_prove "not_ex" "(~ (EX x.P(x))) <> (ALL x.~P(x))"; 

156 
int_prove "imp_ex" "((EX x. P(x)) > Q) <> (ALL x. P(x) > Q)"; 

157 

158 
int_prove "ex_disj_distrib" 

159 
"(EX x. P(x)  Q(x)) <> ((EX x. P(x))  (EX x. Q(x)))"; 

160 
int_prove "all_conj_distrib" 

161 
"(ALL x. P(x) & Q(x)) <> ((ALL x. P(x)) & (ALL x. Q(x)))"; 

162 

163 

1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

164 
(*Used in ZF, perhaps elsewhere?*) 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

165 
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y" 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

166 
(fn [prem] => [rewtac prem, rtac refl 1]); 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

167 

0  168 
(*** case splitting ***) 
169 

1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

170 
qed_goal "meta_iffD" IFOL.thy "[ P==Q; Q ] ==> P" 
756  171 
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); 
282  172 

942  173 
local val mktac = mk_case_split_tac meta_iffD 
174 
in 

175 
fun split_tac splits = mktac (map mk_meta_eq splits) 

176 
end; 

1722  177 

178 
local val mktac = mk_case_split_inside_tac meta_iffD 

179 
in 

180 
fun split_inside_tac splits = mktac (map mk_meta_eq splits) 

181 
end; 

182 

183 

2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

184 
(*** Standard simpsets ***) 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

185 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

186 
structure Induction = InductionFun(struct val spec=IFOL.spec end); 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

187 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

188 
open Simplifier Induction; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

189 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

190 
(*Add congruence rules for = or <> (instead of ==) *) 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

191 
infix 4 addcongs delcongs; 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

192 
fun ss addcongs congs = 
2469  193 
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); 
2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

194 
fun ss delcongs congs = 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

195 
ss deleqcongs (congs RL [eq_reflection,iff_reflection]); 
2469  196 

197 
fun Addcongs congs = (simpset := !simpset addcongs congs); 

2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

198 
fun Delcongs congs = (simpset := !simpset delcongs congs); 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

199 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

200 
val IFOL_simps = 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

201 
[refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

202 
imp_simps @ iff_simps @ quant_simps; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

203 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

204 
val notFalseI = int_prove_fun "~False"; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

205 
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

206 

2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

207 
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems), 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

208 
atac, etac FalseE]; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

209 
(*No premature instantiation of variables during simplification*) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

210 
fun safe_solver prems = FIRST'[match_tac (triv_rls@prems), 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

211 
eq_assume_tac, ematch_tac [FalseE]]; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

212 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

213 
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

214 
setSSolver safe_solver 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

215 
setSolver unsafe_solver 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

216 
setmksimps (map mk_meta_eq o atomize o gen_all); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

217 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

218 
val IFOL_ss = FOL_basic_ss addsimps IFOL_simps 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

219 
addcongs [imp_cong]; 
2074
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

220 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

221 
val cla_simps = 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

222 
[de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] @ 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

223 
map prove_fun 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

224 
["~(P&Q) <> ~P  ~Q", 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

225 
"P  ~P", "~P  P", 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

226 
"~ ~ P <> P", "(~P > P) <> P", 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

227 
"(~P <> ~Q) <> (P<>Q)"]; 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

228 

30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

229 
val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps); 
30a65172e003
Added the de Morgan laws (incl quantifier versions) to basic simpset
paulson
parents:
2065
diff
changeset

230 

2469  231 

232 

233 
(*** Install simpsets and datatypes in theory structure ***) 

234 

235 
simpset := FOL_ss; 

236 

237 
exception SS_DATA of simpset; 

238 

239 
let fun merge [] = SS_DATA empty_ss 

240 
 merge ss = let val ss = map (fn SS_DATA x => x) ss; 

241 
in SS_DATA (foldl merge_ss (hd ss, tl ss)) end; 

242 

243 
fun put (SS_DATA ss) = simpset := ss; 

244 

245 
fun get () = SS_DATA (!simpset); 

246 
in add_thydata "FOL" 

247 
("simpset", ThyMethods {merge = merge, put = put, get = get}) 

248 
end; 

249 

250 

251 
add_thy_reader_file "thy_data.ML"; 

2633
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

252 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

253 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

254 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

255 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

256 
(*** Integration of simplifier with classical reasoner ***) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

257 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

258 
(* rot_eq_tac rotates the first equality premise of subgoal i to the front, 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

259 
fails if there is no equaliy or if an equality is already at the front *) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

260 
fun rot_eq_tac i = let 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

261 
fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

262 
 is_eq (Const ("Trueprop", _) $ (Const("op <>",_) $ _ $ _)) = true 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

263 
 is_eq _ = false; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

264 
fun find_eq n [] = None 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

265 
 find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

266 
fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

267 
(case find_eq 0 (Logic.strip_assums_hyp Bi) of 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

268 
None => no_tac 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

269 
 Some 0 => no_tac 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

270 
 Some n => rotate_tac n i) end; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

271 
in STATE rot_eq end; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

272 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

273 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

274 
fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

275 
safe_asm_full_simp_tac ss; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

276 
(*an unsatisfactory fix for the incomplete asm_full_simp_tac! 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

277 
better: asm_really_full_simp_tac, a yet to be implemented version of 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

278 
asm_full_simp_tac that applies all equalities in the 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

279 
premises to all the premises *) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

280 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

281 
(*Add a simpset to a classical set!*) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

282 
infix 4 addss; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

283 
fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

284 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

285 
(*old version, for compatibility with unstable old proofs*) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

286 
infix 4 unsafe_addss; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

287 
fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

288 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

289 
fun Addss ss = (claset := !claset addss ss); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

290 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

291 
(*Designed to be idempotent, except if best_tac instantiates variables 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

292 
in some of the subgoals*) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

293 
(*old version, for compatibility with unstable old proofs*) 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

294 
fun unsafe_auto_tac (cs,ss) = 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

295 
ALLGOALS (asm_full_simp_tac ss) THEN 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

296 
REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

297 
REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

298 
prune_params_tac; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

299 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

300 
type clasimpset = (claset * simpset); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

301 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

302 
val FOL_css = (FOL_cs, FOL_ss); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

303 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

304 
fun pair_upd1 f ((a,b),x) = (f(a,x), b); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

305 
fun pair_upd2 f ((a,b),x) = (a, f(b,x)); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

306 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

307 
infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

308 
addsimps2 delsimps2 addcongs2 delcongs2; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

309 
val op addSIs2 = pair_upd1 (op addSIs); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

310 
val op addSEs2 = pair_upd1 (op addSEs); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

311 
val op addSDs2 = pair_upd1 (op addSDs); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

312 
val op addIs2 = pair_upd1 (op addIs ); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

313 
val op addEs2 = pair_upd1 (op addEs ); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

314 
val op addDs2 = pair_upd1 (op addDs ); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

315 
val op addsimps2 = pair_upd2 (op addsimps); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

316 
val op delsimps2 = pair_upd2 (op delsimps); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

317 
val op addcongs2 = pair_upd2 (op addcongs); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

318 
val op delcongs2 = pair_upd2 (op delcongs); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

319 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

320 
fun auto_tac (cs,ss) = let val cs' = cs addss ss in 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

321 
EVERY [ TRY (safe_tac cs'), 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

322 
REPEAT (FIRSTGOAL (fast_tac cs')), 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

323 
prune_params_tac] end; 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

324 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

325 
fun Auto_tac () = auto_tac (!claset, !simpset); 
37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

326 

37c0b5a7ee5d
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
oheimb
parents:
2601
diff
changeset

327 
fun auto () = by (Auto_tac ()); 