equal
deleted
inserted
replaced
9 for using assumptions as rewrite rules*) |
9 for using assumptions as rewrite rules*) |
10 fun peEs 0 = [] |
10 fun peEs 0 = [] |
11 | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1)); |
11 | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1)); |
12 |
12 |
13 (*Tactic used for proving conditions for the cond_rls*) |
13 (*Tactic used for proving conditions for the cond_rls*) |
14 val prove_cond_tac = eresolve_tac (peEs 5); |
14 fun prove_cond_tac ctxt = eresolve_tac ctxt (peEs 5); |
15 |
15 |
16 |
16 |
17 structure TSimp_data: TSIMP_DATA = |
17 structure TSimp_data: TSIMP_DATA = |
18 struct |
18 struct |
19 val refl = @{thm refl_elem} |
19 val refl = @{thm refl_elem} |
30 |
30 |
31 val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls}; |
31 val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls}; |
32 |
32 |
33 (*Make a rewriting tactic from a normalization tactic*) |
33 (*Make a rewriting tactic from a normalization tactic*) |
34 fun make_rew_tac ctxt ntac = |
34 fun make_rew_tac ctxt ntac = |
35 TRY (eqintr_tac ctxt) THEN TRYALL (resolve_tac [TSimp.split_eqn]) THEN |
35 TRY (eqintr_tac ctxt) THEN TRYALL (resolve_tac ctxt [TSimp.split_eqn]) THEN |
36 ntac; |
36 ntac; |
37 |
37 |
38 fun rew_tac ctxt thms = make_rew_tac ctxt |
38 fun rew_tac ctxt thms = make_rew_tac ctxt |
39 (TSimp.norm_tac ctxt (standard_congr_rls, thms)); |
39 (TSimp.norm_tac ctxt (standard_congr_rls, thms)); |
40 |
40 |
41 fun hyp_rew_tac ctxt thms = make_rew_tac ctxt |
41 fun hyp_rew_tac ctxt thms = make_rew_tac ctxt |
42 (TSimp.cond_norm_tac ctxt (prove_cond_tac, standard_congr_rls, thms)); |
42 (TSimp.cond_norm_tac ctxt (prove_cond_tac ctxt, standard_congr_rls, thms)); |