author  wenzelm 
Sat, 01 Jul 2000 19:55:22 +0200  
changeset 9230  17ae63f82ad8 
parent 7645  c67115c0e105 
child 13105  3d1e7a199bdc 
permissions  rwrr 
0  1 
(* Title: Provers/simp 
2 
Author: Tobias Nipkow 

3 
Copyright 1993 University of Cambridge 

4 

5 
Generic simplifier, suitable for most logics. The only known exception is 

6 
Constructive Type Theory. The reflexivity axiom must be unconditional, 

7 
namely a=a not a:A ==> a=a:A. Used typedsimp.ML otherwise. 

8 
*) 

9 

10 
signature SIMP_DATA = 

11 
sig 

12 
val dest_red : term > term * term * term 

13 
val mk_rew_rules : thm > thm list 

14 
val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *) 

15 
val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *) 

16 
val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *) 

17 
val refl_thms : thm list 

18 
val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) 

19 
val trans_thms : thm list 

20 
end; 

21 

22 

23 
infix 4 addrews addcongs addsplits delrews delcongs setauto; 

24 

25 
signature SIMP = 

26 
sig 

27 
type simpset 

28 
val empty_ss : simpset 

29 
val addcongs : simpset * thm list > simpset 

30 
val addrews : simpset * thm list > simpset 

31 
val addsplits : simpset * thm list > simpset 

32 
val delcongs : simpset * thm list > simpset 

33 
val delrews : simpset * thm list > simpset 

34 
val dest_ss : simpset > thm list * thm list 

35 
val print_ss : simpset > unit 

36 
val setauto : simpset * (thm list > int > tactic) > simpset 

37 
val ASM_SIMP_TAC : simpset > int > tactic 

38 
val SPLIT_TAC : simpset > int > tactic 

39 
val SIMP_SPLIT2_TAC : simpset > int > tactic 

40 
val SIMP_THM : simpset > thm > thm 

41 
val SIMP_TAC : simpset > int > tactic 

42 
val mk_congs : theory > string list > thm list 

43 
val mk_typed_congs : theory > (string * string) list > thm list 

44 
(* temporarily disabled: 

45 
val extract_free_congs : unit > thm list 

46 
*) 

47 
val tracing : bool ref 

48 
end; 

49 

50 
functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 

51 
struct 

52 

53 
local open Simp_data Logic in 

54 

55 
(*For taking apart reductions into left, right hand sides*) 

56 
val lhs_of = #2 o dest_red; 

57 
val rhs_of = #3 o dest_red; 

58 

59 
(*** Indexing and filtering of theorems ***) 

60 

61 
fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2); 

62 

63 
(*insert a thm in a discrimination net by its lhs*) 

64 
fun lhs_insert_thm (th,net) = 

65 
Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl) 

66 
handle Net.INSERT => net; 

67 

68 
(*match subgoal i against possible theorems in the net. 

69 
Similar to match_from_nat_tac, but the net does not contain numbers; 

70 
rewrite rules are not ordered.*) 

71 
fun net_tac net = 

72 
SUBGOAL(fn (prem,i) => 

73 
match_tac (Net.match_term net (strip_assums_concl prem)) i); 

74 

75 
(*match subgoal i against possible theorems indexed by lhs in the net*) 

76 
fun lhs_net_tac net = 

77 
SUBGOAL(fn (prem,i) => 

78 
bimatch_tac (Net.match_term net 

79 
(lhs_of (strip_assums_concl prem))) i); 

80 

81 
fun nth_subgoal i thm = nth_elem(i1,prems_of thm); 

82 

83 
fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm); 

84 

85 
fun lhs_of_eq i thm = lhs_of(goal_concl i thm) 

86 
and rhs_of_eq i thm = rhs_of(goal_concl i thm); 

87 

88 
fun var_lhs(thm,i) = 

89 
let fun var(Var _) = true 

90 
 var(Abs(_,_,t)) = var t 

91 
 var(f$_) = var f 

92 
 var _ = false; 

93 
in var(lhs_of_eq i thm) end; 

94 

95 
fun contains_op opns = 

96 
let fun contains(Const(s,_)) = s mem opns  

97 
contains(s$t) = contains s orelse contains t  

98 
contains(Abs(_,_,t)) = contains t  

99 
contains _ = false; 

100 
in contains end; 

101 

102 
fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i; 

103 

104 
val (normI_thms,normE_thms) = split_list norm_thms; 

105 

106 
(*Get the norm constants from norm_thms*) 

107 
val norms = 

108 
let fun norm thm = 

109 
case lhs_of(concl_of thm) of 

110 
Const(n,_)$_ => n 

111 
 _ => (prths normE_thms; error"No constant in lhs of a norm_thm") 

112 
in map norm normE_thms end; 

113 

114 
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of 

115 
Const(s,_)$_ => s mem norms  _ => false; 

116 

117 
val refl_tac = resolve_tac refl_thms; 

118 

119 
fun find_res thms thm = 

120 
let fun find [] = (prths thms; error"Check Simp_Data") 

6966  121 
 find(th::thms) = thm RS th handle THM _ => find thms 
0  122 
in find thms end; 
123 

124 
val mk_trans = find_res trans_thms; 

125 

126 
fun mk_trans2 thm = 

127 
let fun mk[] = error"Check transitivity" 

6966  128 
 mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts 
0  129 
in mk trans_thms end; 
130 

131 
(*Applies tactic and returns the first resulting state, FAILS if none!*) 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

132 
fun one_result(tac,thm) = case Seq.pull(tac thm) of 
0  133 
Some(thm',_) => thm' 
134 
 None => raise THM("Simplifier: could not continue", 0, [thm]); 

135 

136 
fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm); 

137 

138 

139 
(**** Adding "NORM" tags ****) 

140 

141 
(*get name of the constant from conclusion of a congruence rule*) 

142 
fun cong_const cong = 

143 
case head_of (lhs_of (concl_of cong)) of 

144 
Const(c,_) => c 

145 
 _ => "" (*a placeholder distinct from const names*); 

146 

147 
(*true if the term is an atomic proposition (no ==> signs) *) 

148 
val atomic = null o strip_assums_hyp; 

149 

150 
(*ccs contains the names of the constants possessing congruence rules*) 

151 
fun add_hidden_vars ccs = 

152 
let fun add_hvars(tm,hvars) = case tm of 

153 
Abs(_,_,body) => add_term_vars(body,hvars) 

154 
 _$_ => let val (f,args) = strip_comb tm 

155 
in case f of 

156 
Const(c,T) => 

157 
if c mem ccs 

158 
then foldr add_hvars (args,hvars) 

159 
else add_term_vars(tm,hvars) 

160 
 _ => add_term_vars(tm,hvars) 

161 
end 

162 
 _ => hvars; 

163 
in add_hvars end; 

164 

165 
fun add_new_asm_vars new_asms = 

166 
let fun itf((tm,at),vars) = 

167 
if at then vars else add_term_vars(tm,vars) 

168 
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm 

169 
in if length(tml)=length(al) 

170 
then foldr itf (tml~~al,vars) 

171 
else vars 

172 
end 

173 
fun add_vars (tm,vars) = case tm of 

174 
Abs (_,_,body) => add_vars(body,vars) 

175 
 r$s => (case head_of tm of 

176 
Const(c,T) => (case assoc(new_asms,c) of 

177 
None => add_vars(r,add_vars(s,vars)) 

178 
 Some(al) => add_list(tm,al,vars)) 

179 
 _ => add_vars(r,add_vars(s,vars))) 

180 
 _ => vars 

181 
in add_vars end; 

182 

183 

184 
fun add_norms(congs,ccs,new_asms) thm = 

185 
let val thm' = mk_trans2 thm; 

186 
(* thm': [?z > l; Prems; r > ?t] ==> ?z > ?t *) 

187 
val nops = nprems_of thm' 

188 
val lhs = rhs_of_eq 1 thm' 

189 
val rhs = lhs_of_eq nops thm' 

190 
val asms = tl(rev(tl(prems_of thm'))) 

191 
val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[]) 

192 
val hvars = add_new_asm_vars new_asms (rhs,hvars) 

193 
fun it_asms (asm,hvars) = 

194 
if atomic asm then add_new_asm_vars new_asms (asm,hvars) 

195 
else add_term_frees(asm,hvars) 

196 
val hvars = foldr it_asms (asms,hvars) 

197 
val hvs = map (#1 o dest_Var) hvars 

198 
val refl1_tac = refl_tac 1 

3537  199 
fun norm_step_tac st = st > 
200 
(case head_of(rhs_of_eq 1 st) of 

201 
Var(ixn,_) => if ixn mem hvs then refl1_tac 

202 
else resolve_tac normI_thms 1 ORELSE refl1_tac 

203 
 Const _ => resolve_tac normI_thms 1 ORELSE 

204 
resolve_tac congs 1 ORELSE refl1_tac 

205 
 Free _ => resolve_tac congs 1 ORELSE refl1_tac 

206 
 _ => refl1_tac)) 

207 
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

208 
val Some(thm'',_) = Seq.pull(add_norm_tac thm') 
0  209 
in thm'' end; 
210 

211 
fun add_norm_tags congs = 

212 
let val ccs = map cong_const congs 

213 
val new_asms = filter (exists not o #2) 

214 
(ccs ~~ (map (map atomic o prems_of) congs)); 

215 
in add_norms(congs,ccs,new_asms) end; 

216 

217 
fun normed_rews congs = 

218 
let val add_norms = add_norm_tags congs; 

219 
in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm)) 

220 
end; 

221 

222 
fun NORM norm_lhs_tac = EVERY'[resolve_tac [red2], norm_lhs_tac, refl_tac]; 

223 

224 
val trans_norms = map mk_trans normE_thms; 

225 

226 

227 
(* SIMPSET *) 

228 

229 
datatype simpset = 

230 
SS of {auto_tac: thm list > int > tactic, 

231 
congs: thm list, 

232 
cong_net: thm Net.net, 

233 
mk_simps: thm > thm list, 

234 
simps: (thm * thm list) list, 

235 
simp_net: thm Net.net, 

236 
splits: thm list, 

237 
split_consts: string list} 

238 

239 
val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty, 

240 
mk_simps=normed_rews[], simps=[], simp_net=Net.empty, 

241 
splits=[], split_consts=[]}; 

242 

243 
(** Insertion of congruences, rewrites and case splits **) 

244 

245 
(*insert a thm in a thm net*) 

246 
fun insert_thm_warn (th,net) = 

247 
Net.insert_term((concl_of th, th), net, eq_thm) 

248 
handle Net.INSERT => 

249 
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; 

250 
net); 

251 

252 
val insert_thms = foldr insert_thm_warn; 

253 

254 
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, 

255 
splits,split_consts}, thm) = 

256 
let val thms = mk_simps thm 

257 
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, 

258 
simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net), 

259 
splits=splits,split_consts=split_consts} 

260 
end; 

261 

262 
val op addrews = foldl addrew; 

263 

264 
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, 

265 
splits,split_consts}, thms) = 

266 
let val congs' = thms @ congs; 

267 
in SS{auto_tac=auto_tac, congs= congs', 

268 
cong_net= insert_thms (map mk_trans thms,cong_net), 

269 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net, 

270 
splits=splits,split_consts=split_consts} 

271 
end; 

272 

273 
fun split_err() = error("split rule not of the form ?P(c(...)) = ..."); 

274 

275 
fun split_const(_ $ t) = 

276 
(case head_of t of Const(a,_) => a  _ => split_err()) 

277 
 split_const _ = split_err(); 

278 

279 
fun addsplit(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, 

280 
splits,split_consts}, thm) = 

281 
let val a = split_const(lhs_of(concl_of thm)) 

282 
in SS{auto_tac=auto_tac,congs=congs,cong_net=cong_net, 

283 
mk_simps=mk_simps,simps=simps,simp_net=simp_net, 

284 
splits=splits@[mk_trans thm],split_consts=split_consts@[a]} end; 

285 

286 
val op addsplits = foldl addsplit; 

287 

288 
(** Deletion of congruences and rewrites **) 

289 

290 
(*delete a thm from a thm net*) 

291 
fun delete_thm_warn (th,net) = 

292 
Net.delete_term((concl_of th, th), net, eq_thm) 

293 
handle Net.DELETE => 

294 
(writeln"\nNo such rewrite or congruence rule:"; print_thm th; 

295 
net); 

296 

297 
val delete_thms = foldr delete_thm_warn; 

298 

299 
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, 

300 
splits,split_consts}, thms) = 

301 
let val congs' = foldl (gen_rem eq_thm) (congs,thms) 

302 
in SS{auto_tac=auto_tac, congs= congs', 

303 
cong_net= delete_thms(map mk_trans thms,cong_net), 

304 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net, 

305 
splits=splits,split_consts=split_consts} 

306 
end; 

307 

308 
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net, 

309 
splits,split_consts}, thm) = 

310 
let fun find((p as (th,ths))::ps',ps) = 

311 
if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps) 

312 
 find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; 

313 
print_thm thm; 

314 
([],simps')) 

315 
val (thms,simps') = find(simps,[]) 

316 
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, 

317 
simps = simps', simp_net = delete_thms(thms,simp_net), 

318 
splits=splits,split_consts=split_consts} 

319 
end; 

320 

321 
val op delrews = foldl delrew; 

322 

323 

324 
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net, 

325 
splits,split_consts,...}, auto_tac) = 

326 
SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, 

327 
simps=simps, simp_net=simp_net,splits=splits,split_consts=split_consts}; 

328 

329 

330 
(** Inspection of a simpset **) 

331 

332 
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); 

333 

334 
fun print_ss(SS{congs,simps,splits,...}) = 

335 
(writeln"Congruences:"; prths congs; 

336 
writeln"Case Splits"; prths splits; 

337 
writeln"Rewrite Rules:"; prths (map #1 simps); ()); 

338 

339 

340 
(* Rewriting with case splits *) 

341 

342 
fun splittable a i thm = 

343 
let val tm = goal_concl i thm 

344 
fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) 

345 
 nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) 

346 
 nobound(Bound n,j,k) = n < k orelse k+j <= n 

347 
 nobound(_) = true; 

348 
fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al 

349 
fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1) 

350 
 find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in 

351 
case f of Const(c,_) => if c=a then check_args(al,j) 

352 
else find_if(s,j) orelse find_if(t,j) 

353 
 _ => find_if(s,j) orelse find_if(t,j) end 

354 
 find_if(_) = false; 

355 
in find_if(tm,0) end; 

356 

357 
fun split_tac (cong_tac,splits,split_consts) i = 

358 
let fun seq_try (split::splits,a::bs) thm = tapply( 

359 
COND (splittable a i) (DETERM(resolve_tac[split]i)) 

1512  360 
((seq_try(splits,bs))), thm) 
361 
 seq_try([],_) thm = no_tac thm 

362 
and try_rew thm = tapply((seq_try(splits,split_consts)) 

363 
ORELSE one_subt, thm) 

0  364 
and one_subt thm = 
365 
let val test = has_fewer_prems (nprems_of thm + 1) 

366 
fun loop thm = tapply(COND test no_tac 

1512  367 
((try_rew THEN DEPTH_FIRST test (refl_tac i)) 
368 
ORELSE (refl_tac i THEN loop)), thm) 

369 
in (cong_tac THEN loop) thm end 

0  370 
in if null splits then no_tac 
1512  371 
else COND (may_match(split_consts,i)) try_rew no_tac 
0  372 
end; 
373 

374 
fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i = 

375 
let val cong_tac = net_tac cong_net i 

376 
in NORM (split_tac (cong_tac,splits,split_consts)) i end; 

377 

378 
(* Rewriting Automaton *) 

379 

380 
datatype cntrl = STOP  MK_EQ  ASMS of int  SIMP_LHS  REW  REFL  TRUE 

381 
 PROVE  POP_CS  POP_ARTR  SPLIT; 

382 
(* 

5961  383 
fun pr_cntrl c = case c of STOP => std_output("STOP")  MK_EQ => std_output("MK_EQ")  
384 
ASMS i => print_int i  POP_ARTR => std_output("POP_ARTR")  

385 
SIMP_LHS => std_output("SIMP_LHS")  REW => std_output("REW")  REFL => std_output("REFL")  

386 
TRUE => std_output("TRUE")  PROVE => std_output("PROVE")  POP_CS => std_output("POP_CS")  SPLIT 

387 
=> std_output("SPLIT"); 

0  388 
*) 
389 
fun simp_refl([],_,ss) = ss 

390 
 simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) 

391 
else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); 

392 

393 
(** Tracing **) 

394 

395 
val tracing = ref false; 

396 

397 
(*Replace parameters by Free variables in P*) 

398 
fun variants_abs ([],P) = P 

399 
 variants_abs ((a,T)::aTs, P) = 

400 
variants_abs (aTs, #2 (variant_abs(a,T,P))); 

401 

402 
(*Select subgoal i from proof state; substitute parameters, for printing*) 

403 
fun prepare_goal i st = 

404 
let val subgi = nth_subgoal i st 

405 
val params = rev(strip_params subgi) 

406 
in variants_abs (params, strip_assums_concl subgi) end; 

407 

408 
(*print lhs of conclusion of subgoal i*) 

409 
fun pr_goal_lhs i st = 

410 
writeln (Sign.string_of_term (#sign(rep_thm st)) 

411 
(lhs_of (prepare_goal i st))); 

412 

413 
(*print conclusion of subgoal i*) 

414 
fun pr_goal_concl i st = 

415 
writeln (Sign.string_of_term (#sign(rep_thm st)) (prepare_goal i st)) 

416 

417 
(*print subgoals i to j (inclusive)*) 

418 
fun pr_goals (i,j) st = 

419 
if i>j then () 

420 
else (pr_goal_concl i st; pr_goals (i+1,j) st); 

421 

422 
(*Print rewrite for tracing; i=subgoal#, n=number of new subgoals, 

423 
thm=old state, thm'=new state *) 

424 
fun pr_rew (i,n,thm,thm',not_asms) = 

425 
if !tracing 

426 
then (if not_asms then () else writeln"Assumption used in"; 

427 
pr_goal_lhs i thm; writeln">"; pr_goal_lhs (i+n) thm'; 

428 
if n>0 then (writeln"Conditions:"; pr_goals (i, i+n1) thm') 

429 
else (); 

430 
writeln"" ) 

431 
else (); 

432 

433 
(* Skip the first n hyps of a goal, and return the rest in generalized form *) 

434 
fun strip_varify(Const("==>", _) $ H $ B, n, vs) = 

435 
if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) 

436 
else strip_varify(B,n1,vs) 

437 
 strip_varify(Const("all",_)$Abs(_,T,t), n, vs) = 

438 
strip_varify(t,n,Var(("?",length vs),T)::vs) 

439 
 strip_varify _ = []; 

440 

441 
fun execute(ss,if_fl,auto_tac,cong_tac,splits,split_consts,net,i) thm = let 

442 

443 
fun simp_lhs(thm,ss,anet,ats,cs) = 

444 
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else 

445 
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

446 
else case Seq.pull(cong_tac i thm) of 
0  447 
Some(thm',_) => 
448 
let val ps = prems_of thm and ps' = prems_of thm'; 

449 
val n = length(ps')length(ps); 

450 
val a = length(strip_assums_hyp(nth_elem(i1,ps))) 

451 
val l = map (fn p => length(strip_assums_hyp(p))) 

452 
(take(n,drop(i1,ps'))); 

453 
in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end 

454 
 None => (REW::ss,thm,anet,ats,cs); 

455 

456 
(*NB: the "Adding rewrites:" trace will look strange because assumptions 

457 
are represented by rules, generalized over their parameters*) 

458 
fun add_asms(ss,thm,a,anet,ats,cs) = 

459 
let val As = strip_varify(nth_subgoal i thm, a, []); 

231  460 
val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As; 
0  461 
val new_rws = flat(map mk_rew_rules thms); 
462 
val rwrls = map mk_trans (flat(map mk_rew_rules thms)); 

463 
val anet' = foldr lhs_insert_thm (rwrls,anet) 

464 
in if !tracing andalso not(null new_rws) 

465 
then (writeln"Adding rewrites:"; prths new_rws; ()) 

466 
else (); 

467 
(ss,thm,anet',anet::ats,cs) 

468 
end; 

469 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

470 
fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of 
0  471 
Some(thm',seq') => 
472 
let val n = (nprems_of thm')  (nprems_of thm) 

473 
in pr_rew(i,n,thm,thm',more); 

474 
if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) 

475 
else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), 

476 
thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) 

477 
end 

478 
 None => if more 

479 
then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm), 

480 
thm,ss,anet,ats,cs,false) 

481 
else (ss,thm,anet,ats,cs); 

482 

483 
fun try_true(thm,ss,anet,ats,cs) = 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

484 
case Seq.pull(auto_tac i thm) of 
0  485 
Some(thm',_) => (ss,thm',anet,ats,cs) 
486 
 None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs 

487 
in if !tracing 

488 
then (writeln"*** Failed to prove precondition. Normal form:"; 

489 
pr_goal_concl i thm; writeln"") 

490 
else (); 

491 
rew(seq,thm0,ss0,anet0,ats0,cs0,more) 

492 
end; 

493 

494 
fun split(thm,ss,anet,ats,cs) = 

4271
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

495 
case Seq.pull(tapply(split_tac 
0  496 
(cong_tac i,splits,split_consts) i,thm)) of 
497 
Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs) 

498 
 None => (ss,thm,anet,ats,cs); 

499 

500 
fun step(s::ss, thm, anet, ats, cs) = case s of 

501 
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) 

502 
 ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) 

503 
 SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) 

1512  504 
 REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) 
0  505 
 REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) 
506 
 TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) 

507 
 PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss 

508 
else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) 

509 
 POP_ARTR => (ss,thm,hd ats,tl ats,cs) 

510 
 POP_CS => (ss,thm,anet,ats,tl cs) 

511 
 SPLIT => split(thm,ss,anet,ats,cs); 

512 

513 
fun exec(state as (s::ss, thm, _, _, _)) = 

514 
if s=STOP then thm else exec(step(state)); 

515 

516 
in exec(ss, thm, Net.empty, [], []) end; 

517 

518 

519 
(*ss = list of commands (not simpset!); 

520 
fl = even use case splits to solve conditional rewrite rules; 

521 
addhyps = add hyps to simpset*) 

522 
fun EXEC_TAC (ss,fl,addhyps) simpset = METAHYPS 

523 
(fn hyps => 

524 
case (if addhyps then simpset addrews hyps else simpset) of 

525 
(SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) => 

526 
PRIMITIVE(execute(ss,fl,auto_tac hyps, 

527 
net_tac cong_net,splits,split_consts, 

528 
simp_net, 1)) 

529 
THEN TRY(auto_tac hyps 1)); 

530 

531 
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,false); 

532 

533 
val ASM_SIMP_TAC = 

534 
EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],false,true); 

535 

536 
val SIMP_SPLIT2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,SPLIT,REFL,STOP],true,false); 

537 

538 
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,splits,split_consts,...}) = 

539 
let val cong_tac = net_tac cong_net 

540 
in fn thm => 

541 
let val state = thm RSN (2,red1) 

542 
in execute(ss,fl,auto_tac[],cong_tac,splits,split_consts,simp_net,1)state 

543 
end 

544 
end; 

545 

546 
val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,SPLIT,REFL,STOP],false); 

547 

548 

549 
(* Compute Congruence rules for individual constants using the substition 

550 
rules *) 

551 

552 
val subst_thms = map standard subst_thms; 

553 

554 

555 
fun exp_app(0,t) = t 

556 
 exp_app(i,t) = exp_app(i1,t $ Bound (i1)); 

557 

558 
fun exp_abs(Type("fun",[T1,T2]),t,i) = 

559 
Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) 

560 
 exp_abs(T,t,i) = exp_app(i,t); 

561 

562 
fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0); 

563 

564 

565 
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = 

566 
let fun xn_list(x,n) = 

567 
let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); 

2266  568 
in ListPair.map eta_Var (ixs, take(n+1,Ts)) end 
0  569 
val lhs = list_comb(f,xn_list("X",k1)) 
570 
val rhs = list_comb(f,xn_list("X",i1) @ [Bound 0] @ yik) 

571 
in Abs("", T, Const(eq,[fT,fT]>eqT) $ lhs $ rhs) end; 

572 

573 
fun find_subst tsig T = 

574 
let fun find (thm::thms) = 

575 
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); 

576 
val [P] = term_vars(concl_of thm) \\ [va,vb] 

577 
val eqT::_ = binder_types cT 

578 
in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P) 

579 
else find thms 

580 
end 

581 
 find [] = None 

582 
in find subst_thms end; 

583 

584 
fun mk_cong sg (f,aTs,rT) (refl,eq) = 

585 
let val tsig = #tsig(Sign.rep_sg sg); 

586 
val k = length aTs; 

587 
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = 

231  588 
let val ca = cterm_of sg va 
589 
and cx = cterm_of sg (eta_Var(("X"^si,0),T)) 

590 
val cb = cterm_of sg vb 

591 
and cy = cterm_of sg (eta_Var(("Y"^si,0),T)) 

592 
val cP = cterm_of sg P 

593 
and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) 

0  594 
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; 
595 
fun mk(c,T::Ts,i,yik) = 

596 
let val si = radixstring(26,"a",i) 

597 
in case find_subst tsig T of 

598 
None => mk(c,Ts,i1,eta_Var(("X"^si,0),T)::yik) 

599 
 Some s => let val c' = c RSN (2,ri(s,i,si,T,yik)) 

600 
in mk(c',Ts,i1,eta_Var(("Y"^si,0),T)::yik) end 

601 
end 

602 
 mk(c,[],_,_) = c; 

603 
in mk(refl,rev aTs,k1,[]) end; 

604 

605 
fun mk_cong_type sg (f,T) = 

606 
let val (aTs,rT) = strip_type T; 

607 
val tsig = #tsig(Sign.rep_sg sg); 

608 
fun find_refl(r::rs) = 

609 
let val (Const(eq,eqT),_,_) = dest_red(concl_of r) 

610 
in if Type.typ_instance(tsig, rT, hd(binder_types eqT)) 

611 
then Some(r,(eq,body_type eqT)) else find_refl rs 

612 
end 

613 
 find_refl([]) = None; 

614 
in case find_refl refl_thms of 

615 
None => []  Some(refl) => [mk_cong sg (f,aTs,rT) refl] 

616 
end; 

617 

618 
fun mk_cong_thy thy f = 

619 
let val sg = sign_of thy; 

611  620 
val T = case Sign.const_type sg f of 
0  621 
None => error(f^" not declared")  Some(T) => T; 
622 
val T' = incr_tvar 9 T; 

623 
in mk_cong_type sg (Const(f,T'),T') end; 

624 

625 
fun mk_congs thy = filter_out is_fact o flat o map (mk_cong_thy thy); 

626 

627 
fun mk_typed_congs thy = 

628 
let val sg = sign_of thy; 

7645  629 
val S0 = Sign.defaultS sg; 
0  630 
fun readfT(f,s) = 
631 
let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s); 

611  632 
val t = case Sign.const_type sg f of 
0  633 
Some(_) => Const(f,T)  None => Free(f,T) 
634 
in (t,T) end 

635 
in flat o map (mk_cong_type sg o readfT) end; 

636 

637 
(* This code is fishy, esp the "let val T' = ..." 

638 
fun extract_free_congs() = 

639 
let val {prop,sign,...} = rep_thm(topthm()); 

640 
val frees = add_term_frees(prop,[]); 

641 
fun filter(Free(a,T as Type("fun",_))) = 

642 
let val T' = incr_tvar 9 (Type.varifyT T) 

643 
in [(Free(a,T),T)] end 

644 
 filter _ = [] 

645 
in flat(map (mk_cong_type sign) (flat (map filter frees))) end; 

646 
*) 

647 

648 
end (* local *) 

649 
end (* SIMP *); 