author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 1459 d12da312eff4
permissions -rw-r--r--
Initial revision

(*  Title: 	CTT/rew
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Simplifier for CTT, using Typedsimp

(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
  for using assumptions as rewrite rules*)
fun peEs 0 = []
  | peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n-1));

(*Tactic used for proving conditions for the cond_rls*)
val prove_cond_tac = eresolve_tac (peEs 5);

structure TSimp_data: TSIMP_DATA =
  val refl		= refl_elem
  val sym		= sym_elem
  val trans		= trans_elem
  val refl_red		= refl_red
  val trans_red		= trans_red
  val red_if_equal	= red_if_equal
  val default_rls 	= comp_rls
  val routine_tac 	= routine_tac routine_rls

structure TSimp = TSimpFun (TSimp_data);

val standard_congr_rls = intrL2_rls @ elimL_rls;

(*Make a rewriting tactic from a normalization tactic*)
fun make_rew_tac ntac =
    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  

fun rew_tac thms = make_rew_tac
    (TSimp.norm_tac(standard_congr_rls, thms));

fun hyp_rew_tac thms = make_rew_tac
    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));