author  wenzelm 
Tue, 25 Jul 2006 21:18:00 +0200  
changeset 20194  c9dbce9a23a1 
parent 19925  3f9341831812 
child 20951  868120282837 
permissions  rwrr 
0  1 
(* Title: FOLP/simp 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1993 University of Cambridge 

5 

6 
FOLP version of... 

7 

8 
Generic simplifier, suitable for most logics. (from Provers) 

9 

10 
This version allows instantiation of Vars in the subgoal, since the proof 

11 
term must change. 

12 
*) 

13 

14 
signature SIMP_DATA = 

15 
sig 

16 
val case_splits : (thm * string) list 

17 
val dest_red : term > term * term * term 

18 
val mk_rew_rules : thm > thm list 

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

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

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

22 
val refl_thms : thm list 

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

24 
val trans_thms : thm list 

25 
end; 

26 

27 

28 
infix 4 addrews addcongs delrews delcongs setauto; 

29 

30 
signature SIMP = 

31 
sig 

32 
type simpset 

33 
val empty_ss : simpset 

34 
val addcongs : simpset * thm list > simpset 

35 
val addrews : simpset * thm list > simpset 

36 
val delcongs : simpset * thm list > simpset 

37 
val delrews : simpset * thm list > simpset 

38 
val dest_ss : simpset > thm list * thm list 

39 
val print_ss : simpset > unit 

40 
val setauto : simpset * (int > tactic) > simpset 

41 
val ASM_SIMP_CASE_TAC : simpset > int > tactic 

42 
val ASM_SIMP_TAC : simpset > int > tactic 

43 
val CASE_TAC : simpset > int > tactic 

44 
val SIMP_CASE2_TAC : simpset > int > tactic 

45 
val SIMP_THM : simpset > thm > thm 

46 
val SIMP_TAC : simpset > int > tactic 

47 
val SIMP_CASE_TAC : simpset > int > tactic 

48 
val mk_congs : theory > string list > thm list 

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

50 
(* temporarily disabled: 

51 
val extract_free_congs : unit > thm list 

52 
*) 

53 
val tracing : bool ref 

54 
end; 

55 

56 
functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 

57 
struct 

58 

19805  59 
local open Simp_data in 
0  60 

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

62 
val lhs_of = #2 o dest_red; 

63 
val rhs_of = #3 o dest_red; 

64 

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

66 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
7645
diff
changeset

67 
fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2); 
0  68 

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

70 
fun lhs_insert_thm (th,net) = 

16800  71 
Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net 
0  72 
handle Net.INSERT => net; 
73 

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

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

76 
rewrite rules are not ordered.*) 

77 
fun net_tac net = 

78 
SUBGOAL(fn (prem,i) => 

19805  79 
resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i); 
0  80 

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

82 
fun lhs_net_tac net = 

83 
SUBGOAL(fn (prem,i) => 

1459  84 
biresolve_tac (Net.unify_term net 
19805  85 
(lhs_of (Logic.strip_assums_concl prem))) i); 
0  86 

15570  87 
fun nth_subgoal i thm = List.nth(prems_of thm,i1); 
0  88 

19805  89 
fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); 
0  90 

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

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

93 

94 
fun var_lhs(thm,i) = 

95 
let fun var(Var _) = true 

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

97 
 var(f$_) = var f 

98 
 var _ = false; 

99 
in var(lhs_of_eq i thm) end; 

100 

101 
fun contains_op opns = 

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

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

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

105 
contains _ = false; 

106 
in contains end; 

107 

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

109 

110 
val (normI_thms,normE_thms) = split_list norm_thms; 

111 

112 
(*Get the norm constants from norm_thms*) 

113 
val norms = 

114 
let fun norm thm = 

115 
case lhs_of(concl_of thm) of 

1459  116 
Const(n,_)$_ => n 
117 
 _ => (prths normE_thms; error"No constant in lhs of a norm_thm") 

0  118 
in map norm normE_thms end; 
119 

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

1459  121 
Const(s,_)$_ => s mem norms  _ => false; 
0  122 

123 
val refl_tac = resolve_tac refl_thms; 

124 

125 
fun find_res thms thm = 

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

6969  127 
 find(th::thms) = thm RS th handle THM _ => find thms 
0  128 
in find thms end; 
129 

130 
val mk_trans = find_res trans_thms; 

131 

132 
fun mk_trans2 thm = 

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

6969  134 
 mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts 
0  135 
in mk trans_thms end; 
136 

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

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

138 
fun one_result(tac,thm) = case Seq.pull(tac thm) of 
15531  139 
SOME(thm',_) => thm' 
140 
 NONE => raise THM("Simplifier: could not continue", 0, [thm]); 

0  141 

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

143 

144 

145 
(**** Adding "NORM" tags ****) 

146 

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

148 
fun cong_const cong = 

149 
case head_of (lhs_of (concl_of cong)) of 

1459  150 
Const(c,_) => c 
151 
 _ => "" (*a placeholder distinct from const names*); 

0  152 

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

19805  154 
val atomic = null o Logic.strip_assums_hyp; 
0  155 

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

157 
fun add_hidden_vars ccs = 

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

1459  159 
Abs(_,_,body) => add_term_vars(body,hvars) 
160 
 _$_ => let val (f,args) = strip_comb tm 

161 
in case f of 

162 
Const(c,T) => 

163 
if c mem ccs 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

164 
then foldr add_hvars hvars args 
1459  165 
else add_term_vars(tm,hvars) 
166 
 _ => add_term_vars(tm,hvars) 

167 
end 

168 
 _ => hvars; 

0  169 
in add_hvars end; 
170 

171 
fun add_new_asm_vars new_asms = 

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

1459  173 
if at then vars else add_term_vars(tm,vars) 
174 
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm 

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

176 
then foldr itf vars (tml~~al) 
1459  177 
else vars 
178 
end 

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

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

181 
 r$s => (case head_of tm of 

17325  182 
Const(c,T) => (case AList.lookup (op =) new_asms c of 
15531  183 
NONE => add_vars(r,add_vars(s,vars)) 
184 
 SOME(al) => add_list(tm,al,vars)) 

1459  185 
 _ => add_vars(r,add_vars(s,vars))) 
186 
 _ => vars 

0  187 
in add_vars end; 
188 

189 

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

191 
let val thm' = mk_trans2 thm; 

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

193 
val nops = nprems_of thm' 

194 
val lhs = rhs_of_eq 1 thm' 

195 
val rhs = lhs_of_eq nops thm' 

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

197 
val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms) 
0  198 
val hvars = add_new_asm_vars new_asms (rhs,hvars) 
199 
fun it_asms (asm,hvars) = 

1459  200 
if atomic asm then add_new_asm_vars new_asms (asm,hvars) 
201 
else add_term_frees(asm,hvars) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

202 
val hvars = foldr it_asms hvars asms 
0  203 
val hvs = map (#1 o dest_Var) hvars 
204 
val refl1_tac = refl_tac 1 

3537  205 
fun norm_step_tac st = st > 
206 
(case head_of(rhs_of_eq 1 st) of 

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

208 
else resolve_tac normI_thms 1 ORELSE refl1_tac 

209 
 Const _ => resolve_tac normI_thms 1 ORELSE 

210 
resolve_tac congs 1 ORELSE refl1_tac 

211 
 Free _ => resolve_tac congs 1 ORELSE refl1_tac 

212 
 _ => refl1_tac) 

213 
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac 

15531  214 
val SOME(thm'',_) = Seq.pull(add_norm_tac thm') 
0  215 
in thm'' end; 
216 

217 
fun add_norm_tags congs = 

218 
let val ccs = map cong_const congs 

15570  219 
val new_asms = List.filter (exists not o #2) 
1459  220 
(ccs ~~ (map (map atomic o prems_of) congs)); 
0  221 
in add_norms(congs,ccs,new_asms) end; 
222 

223 
fun normed_rews congs = 

19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19876
diff
changeset

224 
let val add_norms = add_norm_tags congs in 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19876
diff
changeset

225 
fn thm => Variable.tradeT (Variable.thm_context thm) 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19876
diff
changeset

226 
(map (add_norms o mk_trans) o maps mk_rew_rules) [thm] 
0  227 
end; 
228 

1459  229 
fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; 
0  230 

231 
val trans_norms = map mk_trans normE_thms; 

232 

233 

234 
(* SIMPSET *) 

235 

236 
datatype simpset = 

1459  237 
SS of {auto_tac: int > tactic, 
238 
congs: thm list, 

239 
cong_net: thm Net.net, 

240 
mk_simps: thm > thm list, 

241 
simps: (thm * thm list) list, 

242 
simp_net: thm Net.net} 

0  243 

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

1459  245 
mk_simps=normed_rews[], simps=[], simp_net=Net.empty}; 
0  246 

247 
(** Insertion of congruences and rewrites **) 

248 

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

250 
fun insert_thm_warn (th,net) = 

16800  251 
Net.insert_term Drule.eq_thm_prop (concl_of th, th) net 
0  252 
handle Net.INSERT => 
253 
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; 

254 
net); 

255 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

256 
val insert_thms = foldr insert_thm_warn; 
0  257 

258 
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = 

259 
let val thms = mk_simps thm 

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

261 
simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms} 
0  262 
end; 
263 

15570  264 
val op addrews = Library.foldl addrew; 
0  265 

266 
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = 

267 
let val congs' = thms @ congs; 

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

269 
cong_net= insert_thms cong_net (map mk_trans thms), 
0  270 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} 
271 
end; 

272 

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

274 

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

276 
fun delete_thm_warn (th,net) = 

16800  277 
Net.delete_term Drule.eq_thm_prop (concl_of th, th) net 
0  278 
handle Net.DELETE => 
279 
(writeln"\nNo such rewrite or congruence rule:"; print_thm th; 

280 
net); 

281 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

282 
val delete_thms = foldr delete_thm_warn; 
0  283 

284 
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = 

15570  285 
let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms) 
0  286 
in SS{auto_tac=auto_tac, congs= congs', 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

287 
cong_net= delete_thms cong_net (map mk_trans thms), 
0  288 
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} 
289 
end; 

290 

291 
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = 

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

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
7645
diff
changeset

293 
if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) 
0  294 
 find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; 
1459  295 
print_thm thm; 
296 
([],simps')) 

0  297 
val (thms,simps') = find(simps,[]) 
298 
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

299 
simps = simps', simp_net = delete_thms simp_net thms} 
0  300 
end; 
301 

15570  302 
val op delrews = Library.foldl delrew; 
0  303 

304 

305 
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = 

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

307 
simps=simps, simp_net=simp_net}; 

308 

309 

310 
(** Inspection of a simpset **) 

311 

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

313 

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

1459  315 
(writeln"Congruences:"; prths congs; 
316 
writeln"Rewrite Rules:"; prths (map #1 simps); ()); 

0  317 

318 

319 
(* Rewriting with conditionals *) 

320 

321 
val (case_thms,case_consts) = split_list case_splits; 

322 
val case_rews = map mk_trans case_thms; 

323 

324 
fun if_rewritable ifc i thm = 

325 
let val tm = goal_concl i thm 

1459  326 
fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) 
327 
 nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) 

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

329 
 nobound(_) = true; 

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

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

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

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

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

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

336 
 find_if(_) = false; 

0  337 
in find_if(tm,0) end; 
338 

339 
fun IF1_TAC cong_tac i = 

1512  340 
let fun seq_try (ifth::ifths,ifc::ifcs) thm = 
341 
(COND (if_rewritable ifc i) (DETERM(rtac ifth i)) 

342 
(seq_try(ifths,ifcs))) thm 

343 
 seq_try([],_) thm = no_tac thm 

344 
and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm 

1459  345 
and one_subt thm = 
346 
let val test = has_fewer_prems (nprems_of thm + 1) 

1512  347 
fun loop thm = 
348 
COND test no_tac 

349 
((try_rew THEN DEPTH_FIRST test (refl_tac i)) 

350 
ORELSE (refl_tac i THEN loop)) thm 

351 
in (cong_tac THEN loop) thm end 

352 
in COND (may_match(case_consts,i)) try_rew no_tac end; 

0  353 

354 
fun CASE_TAC (SS{cong_net,...}) i = 

355 
let val cong_tac = net_tac cong_net i 

356 
in NORM (IF1_TAC cong_tac) i end; 

357 

358 
(* Rewriting Automaton *) 

359 

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

1459  361 
 PROVE  POP_CS  POP_ARTR  IF; 
0  362 
(* 
5963  363 
fun pr_cntrl c = case c of STOP => std_output("STOP")  MK_EQ => std_output("MK_EQ")  
364 
ASMS i => print_int i  POP_ARTR => std_output("POP_ARTR")  

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

366 
TRUE => std_output("TRUE")  PROVE => std_output("PROVE")  POP_CS => std_output("POP_CS")  IF 

367 
=> std_output("IF"); 

0  368 
*) 
369 
fun simp_refl([],_,ss) = ss 

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

1459  371 
else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); 
0  372 

373 
(** Tracing **) 

374 

375 
val tracing = ref false; 

376 

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

378 
fun variants_abs ([],P) = P 

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

20194  380 
variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P))); 
0  381 

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

383 
fun prepare_goal i st = 

384 
let val subgi = nth_subgoal i st 

19805  385 
val params = rev (Logic.strip_params subgi) 
386 
in variants_abs (params, Logic.strip_assums_concl subgi) end; 

0  387 

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

389 
fun pr_goal_lhs i st = 

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

1459  391 
(lhs_of (prepare_goal i st))); 
0  392 

393 
(*print conclusion of subgoal i*) 

394 
fun pr_goal_concl i st = 

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

396 

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

398 
fun pr_goals (i,j) st = 

399 
if i>j then () 

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

401 

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

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

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

405 
if !tracing 

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

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

1459  408 
if n>0 then (writeln"Conditions:"; pr_goals (i, i+n1) thm') 
0  409 
else (); 
410 
writeln"" ) 

411 
else (); 

412 

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

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

1459  415 
if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) 
416 
else strip_varify(B,n1,vs) 

0  417 
 strip_varify(Const("all",_)$Abs(_,T,t), n, vs) = 
1459  418 
strip_varify(t,n,Var(("?",length vs),T)::vs) 
0  419 
 strip_varify _ = []; 
420 

421 
fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let 

422 

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

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

425 
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

426 
else case Seq.pull(cong_tac i thm) of 
15531  427 
SOME(thm',_) => 
1459  428 
let val ps = prems_of thm and ps' = prems_of thm'; 
429 
val n = length(ps')length(ps); 

19805  430 
val a = length(Logic.strip_assums_hyp(List.nth(ps,i1))) 
431 
val l = map (fn p => length(Logic.strip_assums_hyp(p))) 

15570  432 
(Library.take(n,Library.drop(i1,ps'))); 
1459  433 
in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end 
15531  434 
 NONE => (REW::ss,thm,anet,ats,cs); 
0  435 

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

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

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

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

1459  440 
val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As; 
15570  441 
val new_rws = List.concat(map mk_rew_rules thms); 
442 
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms)); 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

443 
val anet' = foldr lhs_insert_thm anet rwrls 
0  444 
in if !tracing andalso not(null new_rws) 
1459  445 
then (writeln"Adding rewrites:"; prths new_rws; ()) 
446 
else (); 

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

0  448 
end; 
449 

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

450 
fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of 
15531  451 
SOME(thm',seq') => 
1459  452 
let val n = (nprems_of thm')  (nprems_of thm) 
453 
in pr_rew(i,n,thm,thm',more); 

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

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

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

457 
end 

15531  458 
 NONE => if more 
1512  459 
then rew((lhs_net_tac anet i THEN assume_tac i) thm, 
1459  460 
thm,ss,anet,ats,cs,false) 
461 
else (ss,thm,anet,ats,cs); 

0  462 

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

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

464 
case Seq.pull(auto_tac i thm) of 
15531  465 
SOME(thm',_) => (ss,thm',anet,ats,cs) 
466 
 NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs 

1459  467 
in if !tracing 
468 
then (writeln"*** Failed to prove precondition. Normal form:"; 

469 
pr_goal_concl i thm; writeln"") 

470 
else (); 

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

472 
end; 

0  473 

474 
fun if_exp(thm,ss,anet,ats,cs) = 

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

475 
case Seq.pull (IF1_TAC (cong_tac i) i thm) of 
15531  476 
SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) 
477 
 NONE => (ss,thm,anet,ats,cs); 

0  478 

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

1459  480 
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) 
481 
 ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) 

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

1512  483 
 REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) 
1459  484 
 REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) 
485 
 TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) 

486 
 PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss 

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

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

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

490 
 IF => if_exp(thm,ss,anet,ats,cs); 

0  491 

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

1459  493 
if s=STOP then thm else exec(step(state)); 
0  494 

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

496 

497 

498 
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = 

499 
let val cong_tac = net_tac cong_net 

1512  500 
in fn i => 
501 
(fn thm => 

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

502 
if i <= 0 orelse nprems_of thm < i then Seq.empty 
3a82492e70c5
changed Pure/Sequence interface  isatool fixseq;
wenzelm
parents:
3537
diff
changeset

503 
else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) 
1512  504 
THEN TRY(auto_tac i) 
0  505 
end; 
506 

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

508 
val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); 

509 

510 
val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); 

511 
val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); 

512 

513 
val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); 

514 

515 
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = 

516 
let val cong_tac = net_tac cong_net 

517 
in fn thm => let val state = thm RSN (2,red1) 

1459  518 
in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end 
0  519 
end; 
520 

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

522 

523 

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

525 
rules *) 

526 

527 
val subst_thms = map standard subst_thms; 

528 

529 

530 
fun exp_app(0,t) = t 

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

532 

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

1459  534 
Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) 
0  535 
 exp_abs(T,t,i) = exp_app(i,t); 
536 

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

538 

539 

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

541 
let fun xn_list(x,n) = 

1459  542 
let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); 
15570  543 
in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end 
0  544 
val lhs = list_comb(f,xn_list("X",k1)) 
545 
val rhs = list_comb(f,xn_list("X",i1) @ [Bound 0] @ yik) 

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

547 

16931  548 
fun find_subst sg T = 
0  549 
let fun find (thm::thms) = 
1459  550 
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); 
551 
val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb] 

552 
val eqT::_ = binder_types cT 

16931  553 
in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) 
1459  554 
else find thms 
555 
end 

15531  556 
 find [] = NONE 
0  557 
in find subst_thms end; 
558 

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

16931  560 
let val k = length aTs; 
0  561 
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = 
1459  562 
let val ca = cterm_of sg va 
563 
and cx = cterm_of sg (eta_Var(("X"^si,0),T)) 

564 
val cb = cterm_of sg vb 

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

566 
val cP = cterm_of sg P 

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

568 
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; 

0  569 
fun mk(c,T::Ts,i,yik) = 
1459  570 
let val si = radixstring(26,"a",i) 
16931  571 
in case find_subst sg T of 
15531  572 
NONE => mk(c,Ts,i1,eta_Var(("X"^si,0),T)::yik) 
573 
 SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) 

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

0  576 
 mk(c,[],_,_) = c; 
577 
in mk(refl,rev aTs,k1,[]) end; 

578 

579 
fun mk_cong_type sg (f,T) = 

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

581 
fun find_refl(r::rs) = 

1459  582 
let val (Const(eq,eqT),_,_) = dest_red(concl_of r) 
16931  583 
in if Sign.typ_instance sg (rT, hd(binder_types eqT)) 
15531  584 
then SOME(r,(eq,body_type eqT)) else find_refl rs 
1459  585 
end 
15531  586 
 find_refl([]) = NONE; 
0  587 
in case find_refl refl_thms of 
15531  588 
NONE => []  SOME(refl) => [mk_cong sg (f,aTs,rT) refl] 
0  589 
end; 
590 

591 
fun mk_cong_thy thy f = 

592 
let val sg = sign_of thy; 

611  593 
val T = case Sign.const_type sg f of 
15531  594 
NONE => error(f^" not declared")  SOME(T) => T; 
16876  595 
val T' = Logic.incr_tvar 9 T; 
0  596 
in mk_cong_type sg (Const(f,T'),T') end; 
597 

15570  598 
fun mk_congs thy = List.concat o map (mk_cong_thy thy); 
0  599 

600 
fun mk_typed_congs thy = 

601 
let val sg = sign_of thy; 

7645  602 
val S0 = Sign.defaultS sg; 
0  603 
fun readfT(f,s) = 
16876  604 
let val T = Logic.incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s); 
1459  605 
val t = case Sign.const_type sg f of 
15531  606 
SOME(_) => Const(f,T)  NONE => Free(f,T) 
1459  607 
in (t,T) end 
15570  608 
in List.concat o map (mk_cong_type sg o readfT) end; 
0  609 

610 
end (* local *) 

611 
end (* SIMP *); 