50 | map_term' _ _ = NONE; |
50 | map_term' _ _ = NONE; |
51 |
51 |
52 fun map_thm_tac ctxt tac thm = |
52 fun map_thm_tac ctxt tac thm = |
53 let |
53 let |
54 val monos = Inductive.get_monos ctxt |
54 val monos = Inductive.get_monos ctxt |
|
55 val simps = HOL_basic_ss addsimps @{thms split_def} |
55 in |
56 in |
56 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
57 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
57 REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), |
58 REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), |
58 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
59 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] |
59 end |
60 end |
60 |
61 |
61 fun map_thm ctxt f tac thm = |
62 fun map_thm ctxt f tac thm = |
62 let |
63 let |
87 |
88 |
88 (** equivariance tactics **) |
89 (** equivariance tactics **) |
89 |
90 |
90 val perm_boolE = @{thm permute_boolE} |
91 val perm_boolE = @{thm permute_boolE} |
91 val perm_cancel = @{thms permute_minus_cancel(2)} |
92 val perm_cancel = @{thms permute_minus_cancel(2)} |
92 val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def} |
|
93 |
93 |
94 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
94 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
95 let |
95 let |
96 val thy = ProofContext.theory_of ctxt |
96 val thy = ProofContext.theory_of ctxt |
97 val cpi = Thm.cterm_of thy (mk_minus pi) |
97 val cpi = Thm.cterm_of thy (mk_minus pi) |
98 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
98 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
99 val simps = HOL_basic_ss addsimps perm_expand_bool |
99 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
|
100 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
100 in |
101 in |
101 eqvt_strict_tac ctxt [] pred_names THEN' |
102 eqvt_strict_tac ctxt [] pred_names THEN' |
102 SUBPROOF (fn {prems, context as ctxt, ...} => |
103 SUBPROOF (fn {prems, context as ctxt, ...} => |
103 let |
104 let |
104 val prems' = map (transform_prem ctxt pred_names) prems |
105 val prems' = map (transform_prem ctxt pred_names) prems |
105 |
|
106 val tac1 = resolve_tac prems' |
106 val tac1 = resolve_tac prems' |
107 val tac2 = EVERY' [ rtac pi_intro_rule, |
107 val tac2 = EVERY' [ rtac pi_intro_rule, |
108 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
108 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
109 val tac3 = EVERY' [ rtac pi_intro_rule, |
109 val tac3 = EVERY' [ rtac pi_intro_rule, |
110 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems'] |
110 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, |
|
111 simp_tac simps2, resolve_tac prems'] |
111 in |
112 in |
112 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
113 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
113 end) ctxt |
114 end) ctxt |
114 end |
115 end |
115 |
116 |