author | wenzelm |
Thu, 03 Mar 2022 17:13:24 +0100 | |
changeset 75203 | ee1bd0687c2b |
parent 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
19761 | 1 |
(* Title: CTT/rew.ML |
1459 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1991 University of Cambridge |
4 |
||
19761 | 5 |
Simplifier for CTT, using Typedsimp. |
0 | 6 |
*) |
7 |
||
8 |
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE |
|
9 |
for using assumptions as rewrite rules*) |
|
10 |
fun peEs 0 = [] |
|
39159 | 11 |
| peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1)); |
0 | 12 |
|
13 |
(*Tactic used for proving conditions for the cond_rls*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
14 |
fun prove_cond_tac ctxt = eresolve_tac ctxt (peEs 5); |
0 | 15 |
|
16 |
||
17 |
structure TSimp_data: TSIMP_DATA = |
|
18 |
struct |
|
39159 | 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} |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
39159
diff
changeset
|
26 |
val routine_tac = routine_tac @{thms routine_rls} |
0 | 27 |
end; |
28 |
||
29 |
structure TSimp = TSimpFun (TSimp_data); |
|
30 |
||
39159 | 31 |
val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls}; |
0 | 32 |
|
33 |
(*Make a rewriting tactic from a normalization tactic*) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
39159
diff
changeset
|
34 |
fun make_rew_tac ctxt ntac = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
35 |
TRY (eqintr_tac ctxt) THEN TRYALL (resolve_tac ctxt [TSimp.split_eqn]) THEN |
0 | 36 |
ntac; |
37 |
||
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
39159
diff
changeset
|
38 |
fun rew_tac ctxt thms = make_rew_tac ctxt |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
39159
diff
changeset
|
39 |
(TSimp.norm_tac ctxt (standard_congr_rls, thms)); |
0 | 40 |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
39159
diff
changeset
|
41 |
fun hyp_rew_tac ctxt thms = make_rew_tac ctxt |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
42 |
(TSimp.cond_norm_tac ctxt (prove_cond_tac ctxt, standard_congr_rls, thms)); |