src/CTT/rew.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59498 50b60f501b05
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
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@39159
    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*)
wenzelm@59498
    14
fun prove_cond_tac ctxt = eresolve_tac ctxt (peEs 5);
clasohm@0
    15
clasohm@0
    16
clasohm@0
    17
structure TSimp_data: TSIMP_DATA =
clasohm@0
    18
  struct
wenzelm@39159
    19
  val refl              = @{thm refl_elem}
wenzelm@39159
    20
  val sym               = @{thm sym_elem}
wenzelm@39159
    21
  val trans             = @{thm trans_elem}
wenzelm@39159
    22
  val refl_red          = @{thm refl_red}
wenzelm@39159
    23
  val trans_red         = @{thm trans_red}
wenzelm@39159
    24
  val red_if_equal      = @{thm red_if_equal}
wenzelm@39159
    25
  val default_rls       = @{thms comp_rls}
wenzelm@58963
    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@39159
    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*)
wenzelm@58963
    34
fun make_rew_tac ctxt ntac =
wenzelm@59498
    35
    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac ctxt [TSimp.split_eqn])  THEN  
clasohm@0
    36
    ntac;
clasohm@0
    37
wenzelm@58963
    38
fun rew_tac ctxt thms = make_rew_tac ctxt
wenzelm@58963
    39
    (TSimp.norm_tac ctxt (standard_congr_rls, thms));
clasohm@0
    40
wenzelm@58963
    41
fun hyp_rew_tac ctxt thms = make_rew_tac ctxt
wenzelm@59498
    42
    (TSimp.cond_norm_tac ctxt (prove_cond_tac ctxt, standard_congr_rls, thms));