equal
deleted
inserted
replaced
712 ML {* |
712 ML {* |
713 fun supports_tac perm = |
713 fun supports_tac perm = |
714 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
714 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
715 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN' |
715 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN' |
716 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
716 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
717 swap_fresh_fresh fresh_atom swap_at_base_simps(3)})) |
717 swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh})) |
718 *} |
718 *} |
719 |
719 |
720 ML {* |
720 ML {* |
721 fun mk_supp ty x = |
721 fun mk_supp ty x = |
722 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
722 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
764 *} |
764 *} |
765 |
765 |
766 ML {* |
766 ML {* |
767 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
767 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
768 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
768 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
769 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom finite_insert finite.emptyI finite_Un}) |
769 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image finite_insert finite.emptyI finite_Un}) |
770 *} |
770 *} |
771 |
771 |
772 ML {* |
772 ML {* |
773 fun prove_fs ctxt induct supports tys = |
773 fun prove_fs ctxt induct supports tys = |
774 let |
774 let |