src/HOL/Finite_Set.thy
 changeset 16733 236dfafbeb63 parent 16632 ad2895beef79 child 16760 5c5f051aaaaa
```     1.1 --- a/src/HOL/Finite_Set.thy	Thu Jul 07 12:36:56 2005 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jul 07 12:39:17 2005 +0200
1.3 @@ -891,8 +891,9 @@
1.4    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
1.5  by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
1.6
1.7 -lemma strong_setsum_cong:
1.8 -  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setsum f A = setsum g B"
1.9 +lemma strong_setsum_cong[cong]:
1.10 +  "A = B ==> (!!x. x:B =simp=> f x = g x)
1.11 +   ==> setsum (%x. f x) A = setsum (%x. g x) B"
1.12  by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
1.13
1.14  lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
1.15 @@ -1704,71 +1705,6 @@
1.16    done
1.17
1.18
1.19 -subsubsection {* Theorems about @{text "choose"} *}
1.20 -
1.21 -text {*
1.22 -  \medskip Basic theorem about @{text "choose"}.  By Florian
1.23 -  Kamm\"uller, tidied by LCP.
1.24 -*}
1.25 -
1.26 -lemma card_s_0_eq_empty:
1.27 -    "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
1.29 -  apply (simp cong add: rev_conj_cong)
1.30 -  done
1.31 -
1.32 -lemma choose_deconstruct: "finite M ==> x \<notin> M
1.33 -  ==> {s. s <= insert x M & card(s) = Suc k}
1.34 -       = {s. s <= M & card(s) = Suc k} Un
1.35 -         {s. EX t. t <= M & card(t) = k & s = insert x t}"
1.36 -  apply safe
1.37 -   apply (auto intro: finite_subset [THEN card_insert_disjoint])
1.38 -  apply (drule_tac x = "xa - {x}" in spec)
1.39 -  apply (subgoal_tac "x \<notin> xa", auto)
1.40 -  apply (erule rev_mp, subst card_Diff_singleton)
1.41 -  apply (auto intro: finite_subset)
1.42 -  done
1.43 -
1.44 -text{*There are as many subsets of @{term A} having cardinality @{term k}
1.45 - as there are sets obtained from the former by inserting a fixed element
1.46 - @{term x} into each.*}
1.47 -lemma constr_bij:
1.48 -   "[|finite A; x \<notin> A|] ==>
1.49 -    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
1.50 -    card {B. B <= A & card(B) = k}"
1.51 -  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
1.52 -       apply (auto elim!: equalityE simp add: inj_on_def)
1.53 -    apply (subst Diff_insert0, auto)
1.54 -   txt {* finiteness of the two sets *}
1.55 -   apply (rule_tac [2] B = "Pow (A)" in finite_subset)
1.56 -   apply (rule_tac B = "Pow (insert x A)" in finite_subset)
1.57 -   apply fast+
1.58 -  done
1.59 -
1.60 -text {*
1.61 -  Main theorem: combinatorial statement about number of subsets of a set.
1.62 -*}
1.63 -
1.64 -lemma n_sub_lemma:
1.65 -  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
1.66 -  apply (induct k)
1.67 -   apply (simp add: card_s_0_eq_empty, atomize)
1.68 -  apply (rotate_tac -1, erule finite_induct)
1.69 -   apply (simp_all (no_asm_simp) cong add: conj_cong
1.71 -  apply (subst card_Un_disjoint)
1.72 -     prefer 4 apply (force simp add: constr_bij)
1.73 -    prefer 3 apply force
1.74 -   prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
1.75 -     finite_subset [of _ "Pow (insert x F)", standard])
1.76 -  apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
1.77 -  done
1.78 -
1.79 -theorem n_subsets:
1.80 -    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
1.81 -  by (simp add: n_sub_lemma)
1.82 -
1.83 -
1.84  subsection{* A fold functional for non-empty sets *}
1.85
1.86  text{* Does not require start value. *}
```