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;
wenzelm@19761
     1
(*  Title:      CTT/rew.ML
clasohm@1459
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1991  University of Cambridge
clasohm@0
     4
wenzelm@19761
     5
Simplifier for CTT, using Typedsimp.
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
clasohm@0
     9
  for using assumptions as rewrite rules*)
clasohm@0
    10
fun peEs 0 = []
wenzelm@19761
    11
  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
clasohm@0
    12
clasohm@0
    13
(*Tactic used for proving conditions for the cond_rls*)
clasohm@0
    14
val prove_cond_tac = eresolve_tac (peEs 5);
clasohm@0
    15
clasohm@0
    16
clasohm@0
    17
structure TSimp_data: TSIMP_DATA =
clasohm@0
    18
  struct
wenzelm@19761
    19
  val refl              = thm "refl_elem"
wenzelm@19761
    20
  val sym               = thm "sym_elem"
wenzelm@19761
    21
  val trans             = thm "trans_elem"
wenzelm@19761
    22
  val refl_red          = thm "refl_red"
wenzelm@19761
    23
  val trans_red         = thm "trans_red"
wenzelm@19761
    24
  val red_if_equal      = thm "red_if_equal"
wenzelm@19761
    25
  val default_rls       = thms "comp_rls"
wenzelm@19761
    26
  val routine_tac       = routine_tac (thms "routine_rls")
clasohm@0
    27
  end;
clasohm@0
    28
clasohm@0
    29
structure TSimp = TSimpFun (TSimp_data);
clasohm@0
    30
wenzelm@19761
    31
val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
clasohm@0
    32
clasohm@0
    33
(*Make a rewriting tactic from a normalization tactic*)
clasohm@0
    34
fun make_rew_tac ntac =
clasohm@0
    35
    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
clasohm@0
    36
    ntac;
clasohm@0
    37
clasohm@0
    38
fun rew_tac thms = make_rew_tac
clasohm@0
    39
    (TSimp.norm_tac(standard_congr_rls, thms));
clasohm@0
    40
clasohm@0
    41
fun hyp_rew_tac thms = make_rew_tac
clasohm@0
    42
    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));