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