src/CTT/rew.ML
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 1459 d12da312eff4
child 17496 26535df536ae
permissions -rw-r--r--
use more symbols in HTML output
clasohm@1459
     1
(*  Title:      CTT/rew
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Simplifier for CTT, using Typedsimp
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
clasohm@0
    10
  for using assumptions as rewrite rules*)
clasohm@0
    11
fun peEs 0 = []
clasohm@0
    12
  | peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n-1));
clasohm@0
    13
clasohm@0
    14
(*Tactic used for proving conditions for the cond_rls*)
clasohm@0
    15
val prove_cond_tac = eresolve_tac (peEs 5);
clasohm@0
    16
clasohm@0
    17
clasohm@0
    18
structure TSimp_data: TSIMP_DATA =
clasohm@0
    19
  struct
clasohm@1459
    20
  val refl              = refl_elem
clasohm@1459
    21
  val sym               = sym_elem
clasohm@1459
    22
  val trans             = trans_elem
clasohm@1459
    23
  val refl_red          = refl_red
clasohm@1459
    24
  val trans_red         = trans_red
clasohm@1459
    25
  val red_if_equal      = red_if_equal
clasohm@1459
    26
  val default_rls       = comp_rls
clasohm@1459
    27
  val routine_tac       = routine_tac routine_rls
clasohm@0
    28
  end;
clasohm@0
    29
clasohm@0
    30
structure TSimp = TSimpFun (TSimp_data);
clasohm@0
    31
clasohm@0
    32
val standard_congr_rls = intrL2_rls @ elimL_rls;
clasohm@0
    33
clasohm@0
    34
(*Make a rewriting tactic from a normalization tactic*)
clasohm@0
    35
fun make_rew_tac ntac =
clasohm@0
    36
    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
clasohm@0
    37
    ntac;
clasohm@0
    38
clasohm@0
    39
fun rew_tac thms = make_rew_tac
clasohm@0
    40
    (TSimp.norm_tac(standard_congr_rls, thms));
clasohm@0
    41
clasohm@0
    42
fun hyp_rew_tac thms = make_rew_tac
clasohm@0
    43
    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));