1(*  Title:      CTT/rew.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1991  University of Cambridge
4
5Simplifier for CTT, using Typedsimp.
6*)
7
8(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
9  for using assumptions as rewrite rules*)
10fun 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*)
14fun prove_cond_tac ctxt = eresolve_tac ctxt (peEs 5);
15
16
17structure 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
29structure TSimp = TSimpFun (TSimp_data);
30
31val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};
32
33(*Make a rewriting tactic from a normalization tactic*)
34fun make_rew_tac ctxt ntac =
35    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac ctxt [TSimp.split_eqn])  THEN  
36    ntac;
37
38fun rew_tac ctxt thms = make_rew_tac ctxt
39    (TSimp.norm_tac ctxt (standard_congr_rls, thms));
40
41fun hyp_rew_tac ctxt thms = make_rew_tac ctxt
42    (TSimp.cond_norm_tac ctxt (prove_cond_tac ctxt, standard_congr_rls, thms));
43