src/CTT/rew.ML
author haftmann
Tue Sep 20 08:21:49 2005 +0200 (2005-09-20)
changeset 17496 26535df536ae
parent 1459 d12da312eff4
child 19761 5cd82054c2c6
permissions -rw-r--r--
slight adaptions to library changes
     1 (*  Title:      CTT/rew
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     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 (curry (op RS) ProdE) (peEs (n-1));
    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
    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
    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));