equal
deleted
inserted
replaced
74 apply (rule_tac x="-pi" in exI) |
74 apply (rule_tac x="-pi" in exI) |
75 by auto |
75 by auto |
76 |
76 |
77 ML {* |
77 ML {* |
78 fun symp_tac induct inj eqvt ctxt = |
78 fun symp_tac induct inj eqvt ctxt = |
79 rel_indtac induct THEN_ALL_NEW |
79 rtac induct THEN_ALL_NEW |
80 simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac |
80 simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac |
81 THEN_ALL_NEW |
81 THEN_ALL_NEW |
82 REPEAT o etac @{thm exi_neg} |
82 REPEAT o etac @{thm exi_neg} |
83 THEN_ALL_NEW |
83 THEN_ALL_NEW |
84 split_conj_tac THEN_ALL_NEW |
84 split_conj_tac THEN_ALL_NEW |
109 ) |
109 ) |
110 *} |
110 *} |
111 |
111 |
112 ML {* |
112 ML {* |
113 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
113 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
114 rel_indtac induct THEN_ALL_NEW |
114 rtac induct THEN_ALL_NEW |
115 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
115 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
116 asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW |
116 asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW |
117 split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac |
117 split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac |
118 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
118 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
119 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
119 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
220 (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) |
220 (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) |
221 end |
221 end |
222 *} |
222 *} |
223 |
223 |
224 ML {* |
224 ML {* |
225 fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW ( |
225 fun fs_tac induct supports = rtac induct THEN_ALL_NEW ( |
226 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
226 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
227 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
227 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
228 supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) |
228 supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) |
229 *} |
229 *} |
230 |
230 |
315 done |
315 done |
316 |
316 |
317 |
317 |
318 ML {* |
318 ML {* |
319 fun supp_eq_tac ind fv perm eqiff ctxt = |
319 fun supp_eq_tac ind fv perm eqiff ctxt = |
320 rel_indtac ind THEN_ALL_NEW |
320 rtac ind THEN_ALL_NEW |
321 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
321 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
322 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW |
322 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW |
323 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
323 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
324 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
324 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
325 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
325 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |