author  wenzelm 
Mon, 10 Nov 2014 21:49:48 +0100  
changeset 58963  26bf09b95dda 
parent 39159  0dec18004e75 
child 59498  50b60f501b05 
permissions  rwrr 
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 (n1)); 
0  12 

13 
(*Tactic used for proving conditions for the cond_rls*) 

14 
val prove_cond_tac = eresolve_tac (peEs 5); 

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 fallback 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 fallback without context);
wenzelm
parents:
39159
diff
changeset

34 
fun make_rew_tac ctxt ntac = 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
39159
diff
changeset

35 
TRY (eqintr_tac ctxt) THEN TRYALL (resolve_tac [TSimp.split_eqn]) THEN 
0  36 
ntac; 
37 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback 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 fallback 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 fallback without context);
wenzelm
parents:
39159
diff
changeset

41 
fun hyp_rew_tac ctxt thms = make_rew_tac ctxt 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
39159
diff
changeset

42 
(TSimp.cond_norm_tac ctxt (prove_cond_tac, standard_congr_rls, thms)); 