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