757 by (etac finite_induct 1); |
757 by (etac finite_induct 1); |
758 by (auto_tac (claset(), simpset() addsimps [insert_Diff_if])); |
758 by (auto_tac (claset(), simpset() addsimps [insert_Diff_if])); |
759 by (dres_inst_tac [("a","a")] mk_disjoint_insert 1); |
759 by (dres_inst_tac [("a","a")] mk_disjoint_insert 1); |
760 by (Auto_tac); |
760 by (Auto_tac); |
761 qed_spec_mp "setsum_diff1"; |
761 qed_spec_mp "setsum_diff1"; |
|
762 |
|
763 |
|
764 (*** Basic theorem about "choose". By Florian Kammueller, tidied by LCP ***) |
|
765 |
|
766 Goal "finite S ==> (card S = 0) = (S = {})"; |
|
767 by (auto_tac (claset() addDs [card_Suc_Diff1], |
|
768 simpset())); |
|
769 qed "card_0_empty_iff"; |
|
770 |
|
771 Goal "finite A ==> card {B. B <= A & card B = 0} = 1"; |
|
772 by (asm_simp_tac (simpset() addcongs [conj_cong] |
|
773 addsimps [finite_subset RS card_0_empty_iff]) 1); |
|
774 by (simp_tac (simpset() addcongs [rev_conj_cong]) 1); |
|
775 qed "card_s_0_eq_empty"; |
|
776 |
|
777 Goal "[| finite M; x ~: M |] \ |
|
778 \ ==> {s. s <= insert x M & card(s) = Suc k} \ |
|
779 \ = {s. s <= M & card(s) = Suc k} Un \ |
|
780 \ {s. EX t. t <= M & card(t) = k & s = insert x t}"; |
|
781 by Safe_tac; |
|
782 by (auto_tac (claset() addIs [finite_subset RS card_insert_disjoint], |
|
783 simpset())); |
|
784 by (dres_inst_tac [("x","xa - {x}")] spec 1); |
|
785 by (subgoal_tac ("x ~: xa") 1); |
|
786 by Auto_tac; |
|
787 by (etac rev_mp 1 THEN stac card_Diff_singleton 1); |
|
788 by (auto_tac (claset() addIs [finite_subset], |
|
789 simpset())); |
|
790 qed "choose_deconstruct"; |
|
791 |
|
792 Goal "[| finite(A); finite(B); f : A funcset B; inj_on f A |] \ |
|
793 \ ==> card A <= card B"; |
|
794 by (auto_tac (claset() addIs [card_mono], |
|
795 simpset() addsimps [card_image RS sym, Pi_def])); |
|
796 qed "card_inj_on_le"; |
|
797 |
|
798 Goal "[| finite A; finite B; \ |
|
799 \ f: A funcset B; inj_on f A; g: B funcset A; inj_on g B |] \ |
|
800 \ ==> card(A) = card(B)"; |
|
801 by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset())); |
|
802 qed "card_bij_eq"; |
|
803 |
|
804 Goal "[| finite M; x ~: M |] \ |
|
805 \ ==> card{s. EX t. t <= M & card(t) = k & s = insert x t} = \ |
|
806 \ card {s. s <= M & card(s) = k}"; |
|
807 by (res_inst_tac |
|
808 [("f", "lam s: {s. EX t. t <= M & card t = k & s = insert x t}. s - {x}"), |
|
809 ("g","lam s: {s. s <= M & card s = k}. insert x s")] card_bij_eq 1); |
|
810 by (res_inst_tac [("B","Pow(insert x M)")] finite_subset 1); |
|
811 by (res_inst_tac [("B","Pow(M)")] finite_subset 3); |
|
812 by (TRYALL (Fast_tac)); |
|
813 by (rtac funcsetI 3); |
|
814 by (rtac funcsetI 1); |
|
815 (* arity *) |
|
816 by (auto_tac (claset() addSEs [equalityE], |
|
817 simpset() addsimps [inj_on_def, restrict_def])); |
|
818 by (stac Diff_insert0 1); |
|
819 by Auto_tac; |
|
820 qed "constr_bij"; |
|
821 |
|
822 (* Main theorem: combinatorial theorem about number of subsets of a set *) |
|
823 Goal "ALL m. k <= m --> (ALL A. finite A --> card A = m --> \ |
|
824 \ card {s. s <= A & card s = k} = (m choose k))"; |
|
825 by (induct_tac "k" 1); |
|
826 by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1); |
|
827 (* first 0 case finished *) |
|
828 by (rtac allI 1); |
|
829 (* second induction *) |
|
830 by (induct_tac "m" 1); |
|
831 by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1); |
|
832 (* snd 0 case finished *) |
|
833 (* prepare finite set induction *) |
|
834 by (rtac impI 1 THEN rtac allI 1 THEN rtac impI 1); |
|
835 (* third induction, finite sets *) |
|
836 by (etac finite_induct 1); |
|
837 by (simp_tac (simpset() addsimps [card_s_0_eq_empty]) 1); |
|
838 (** LEVEL 10 **) |
|
839 by (Clarify_tac 1); |
|
840 (* case analysis: n < na *) |
|
841 by (case_tac "n < na" 1); |
|
842 (* n < na *) |
|
843 by (stac choose_deconstruct 1); |
|
844 by (assume_tac 1); |
|
845 by (assume_tac 1); |
|
846 by (stac card_Un_disjoint 1); |
|
847 by (Force_tac 3); |
|
848 (* finite goal *) |
|
849 by (res_inst_tac [("B","Pow F")] finite_subset 1); |
|
850 by (Blast_tac 1); |
|
851 by (etac (finite_Pow_iff RS iffD2) 1); |
|
852 (* finite goal *) |
|
853 by (res_inst_tac [("B","Pow (insert x F)")] finite_subset 1); |
|
854 by (Blast_tac 1); |
|
855 by (blast_tac (claset() addIs [finite_Pow_iff RS iffD2]) 1); |
|
856 (** LEVEL 21 **) |
|
857 (* use bijection *) |
|
858 by (force_tac (claset(), simpset() addsimps [constr_bij]) 1); |
|
859 (* The remaining odd cases *) |
|
860 (* case ~ n < na: 1. na < n contradiction and 2. n = na trivial solution *) |
|
861 by (dtac (leI RS (le_eq_less_or_eq RS iffD1)) 1); |
|
862 by (etac disjE 1); |
|
863 (* contradiction for case na < n *) |
|
864 by (Force_tac 1); |
|
865 (* Second case na = n: substitution and evaluation *) |
|
866 by (Asm_full_simp_tac 1); |
|
867 by (subgoal_tac "{s. s <= insert x F & card s = Suc n} = {insert x F}" 1); |
|
868 by (auto_tac (claset(), |
|
869 simpset() addsimps [card_seteq RS equalityD2 RS subsetD])); |
|
870 qed "n_sub_lemma"; |
|
871 |
|
872 Goal "[| finite M; card(M) = n; k <= n |]\ |
|
873 \ ==> card {s. s <= M & card(s) = k} = (n choose k)"; |
|
874 by (asm_simp_tac (simpset() addsimps [n_sub_lemma]) 1); |
|
875 qed "n_subsets"; |
|
876 |