19761

1 
(* Title: CTT/rew.ML

1459

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

3 
Copyright 1991 University of Cambridge


4 

19761

5 
Simplifier for CTT, using Typedsimp.

0

6 
*)


7 


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


9 
for using assumptions as rewrite rules*)


10 
fun peEs 0 = []

39159

11 
 peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n1));

0

12 


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


14 
val prove_cond_tac = eresolve_tac (peEs 5);


15 


16 


17 
structure TSimp_data: TSIMP_DATA =


18 
struct

39159

19 
val refl = @{thm refl_elem}


20 
val sym = @{thm sym_elem}


21 
val trans = @{thm trans_elem}


22 
val refl_red = @{thm refl_red}


23 
val trans_red = @{thm trans_red}


24 
val red_if_equal = @{thm red_if_equal}


25 
val default_rls = @{thms comp_rls}


26 
val routine_tac = routine_tac (@{thms routine_rls})

0

27 
end;


28 


29 
structure TSimp = TSimpFun (TSimp_data);


30 

39159

31 
val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};

0

32 


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


34 
fun make_rew_tac ntac =


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


36 
ntac;


37 


38 
fun rew_tac thms = make_rew_tac


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


40 


41 
fun hyp_rew_tac thms = make_rew_tac


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