84 end |
84 end |
85 |
85 |
86 |
86 |
87 (** equivariance tactics **) |
87 (** equivariance tactics **) |
88 |
88 |
|
89 val perm_boolE = @{thm permute_boolE} |
|
90 val perm_cancel = @{thms permute_minus_cancel(2)} |
|
91 val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def} |
|
92 |
89 fun eqvt_rel_case_tac ctxt pred_names pi intro = |
93 fun eqvt_rel_case_tac ctxt pred_names pi intro = |
90 let |
94 let |
91 val thy = ProofContext.theory_of ctxt |
95 val thy = ProofContext.theory_of ctxt |
92 val cpi = Thm.cterm_of thy (mk_minus pi) |
96 val cpi = Thm.cterm_of thy (mk_minus pi) |
93 val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE} |
97 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
94 val permute_cancel = @{thms permute_minus_cancel(2)} |
98 val simps = HOL_basic_ss addsimps perm_expand_bool |
95 in |
99 in |
96 eqvt_strict_tac ctxt [] [] THEN' |
100 eqvt_strict_tac ctxt [] pred_names THEN' |
97 SUBPROOF (fn {prems, context, ...} => |
101 SUBPROOF (fn {prems, context as ctxt, ...} => |
98 let |
102 let |
99 val prems' = map (transform_prem ctxt pred_names) prems |
103 val prems' = map (transform_prem ctxt pred_names) prems |
100 val side_cond_tac = EVERY' |
104 val tac1 = resolve_tac prems' |
101 [ rtac rule, eqvt_strict_tac context permute_cancel [], |
105 val tac2 = EVERY' [ rtac pi_intro_rule, |
102 resolve_tac prems' ] |
106 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
|
107 val tac3 = EVERY' [ rtac pi_intro_rule, |
|
108 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems'] |
103 in |
109 in |
104 (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1 |
110 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
105 end) ctxt |
111 end) ctxt |
106 end |
112 end |
107 |
113 |
108 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
114 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
109 let |
115 let |