src/CTT/rew.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 35762 af3ff2ba4c54
child 39159 0dec18004e75
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      CTT/rew.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 
     5 Simplifier for CTT, using Typedsimp.
     6 *)
     7 
     8 (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
     9   for using assumptions as rewrite rules*)
    10 fun peEs 0 = []
    11   | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
    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
    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")
    27   end;
    28 
    29 structure TSimp = TSimpFun (TSimp_data);
    30 
    31 val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
    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));