2 Author: Stefan Berghofer (original code) |
2 Author: Stefan Berghofer (original code) |
3 Author: Christian Urban |
3 Author: Christian Urban |
4 |
4 |
5 Automatic proofs for equivariance of inductive predicates. |
5 Automatic proofs for equivariance of inductive predicates. |
6 *) |
6 *) |
|
7 |
7 |
8 |
8 signature NOMINAL_EQVT = |
9 signature NOMINAL_EQVT = |
9 sig |
10 sig |
10 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
11 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
11 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
12 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
30 |
31 |
31 |
32 |
32 (** equivariance tactics **) |
33 (** equivariance tactics **) |
33 |
34 |
34 val perm_boolE = @{thm permute_boolE} |
35 val perm_boolE = @{thm permute_boolE} |
35 val perm_cancel = @{thms permute_minus_cancel(2)} |
|
36 |
36 |
37 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
37 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
38 let |
38 let |
39 val thy = ProofContext.theory_of ctxt |
39 val thy = ProofContext.theory_of ctxt |
40 val cpi = Thm.cterm_of thy (mk_minus pi) |
40 val cpi = Thm.cterm_of thy (mk_minus pi) |
41 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
41 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
42 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
42 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
43 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
43 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
|
44 val eqvt_sconfig = |
|
45 eqvt_strict_config addpres @{thms permute_minus_cancel(2)} addexcls pred_names |
44 in |
46 in |
45 eqvt_strict_tac ctxt [] pred_names THEN' |
47 eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN' |
46 SUBPROOF (fn {prems, context as ctxt, ...} => |
48 SUBPROOF (fn {prems, context as ctxt, ...} => |
47 let |
49 let |
48 val prems' = map (transform_prem2 ctxt pred_names) prems |
50 val prems' = map (transform_prem2 ctxt pred_names) prems |
49 val tac1 = resolve_tac prems' |
51 val tac1 = resolve_tac prems' |
50 val tac2 = EVERY' [ rtac pi_intro_rule, |
52 val tac2 = EVERY' [ rtac pi_intro_rule, |
51 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
53 eqvt_tac ctxt eqvt_sconfig, resolve_tac prems' ] |
52 val tac3 = EVERY' [ rtac pi_intro_rule, |
54 val tac3 = EVERY' [ rtac pi_intro_rule, |
53 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, |
55 eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, |
54 simp_tac simps2, resolve_tac prems'] |
56 simp_tac simps2, resolve_tac prems'] |
55 in |
57 in |
56 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
58 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
57 end) ctxt |
59 end) ctxt |
58 end |
60 end |