1459

1 
(* Title: CTT/rew

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1991 University of Cambridge


5 


6 
Simplifier for CTT, using Typedsimp


7 
*)


8 


9 
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE


10 
for using assumptions as rewrite rules*)


11 
fun peEs 0 = []


12 
 peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n1));


13 


14 
(*Tactic used for proving conditions for the cond_rls*)


15 
val prove_cond_tac = eresolve_tac (peEs 5);


16 


17 


18 
structure TSimp_data: TSIMP_DATA =


19 
struct

1459

20 
val refl = refl_elem


21 
val sym = sym_elem


22 
val trans = trans_elem


23 
val refl_red = refl_red


24 
val trans_red = trans_red


25 
val red_if_equal = red_if_equal


26 
val default_rls = comp_rls


27 
val routine_tac = routine_tac routine_rls

0

28 
end;


29 


30 
structure TSimp = TSimpFun (TSimp_data);


31 


32 
val standard_congr_rls = intrL2_rls @ elimL_rls;


33 


34 
(*Make a rewriting tactic from a normalization tactic*)


35 
fun make_rew_tac ntac =


36 
TRY eqintr_tac THEN TRYALL (resolve_tac [TSimp.split_eqn]) THEN


37 
ntac;


38 


39 
fun rew_tac thms = make_rew_tac


40 
(TSimp.norm_tac(standard_congr_rls, thms));


41 


42 
fun hyp_rew_tac thms = make_rew_tac


43 
(TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));
