src/HOL/Finite_Set.thy
 author obua Tue Nov 23 18:58:59 2004 +0100 (2004-11-23) changeset 15318 e9669e0d6452 parent 15315 a358e31572d9 child 15327 0230a10582d3 permissions -rw-r--r--
prettier proof of setsum_diff
```     1 (*  Title:      HOL/Finite_Set.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
```
```     4                 Additions by Jeremy Avigad in Feb 2004
```
```     5 *)
```
```     6
```
```     7 header {* Finite sets *}
```
```     8
```
```     9 theory Finite_Set
```
```    10 imports Divides Power Inductive
```
```    11 begin
```
```    12
```
```    13 subsection {* Collection of finite sets *}
```
```    14
```
```    15 consts Finites :: "'a set set"
```
```    16 syntax
```
```    17   finite :: "'a set => bool"
```
```    18 translations
```
```    19   "finite A" == "A : Finites"
```
```    20
```
```    21 inductive Finites
```
```    22   intros
```
```    23     emptyI [simp, intro!]: "{} : Finites"
```
```    24     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
```
```    25
```
```    26 axclass finite \<subseteq> type
```
```    27   finite: "finite UNIV"
```
```    28
```
```    29 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
```
```    30   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
```
```    31   shows "\<exists>a::'a. a \<notin> A"
```
```    32 proof -
```
```    33   from prems have "A \<noteq> UNIV" by blast
```
```    34   thus ?thesis by blast
```
```    35 qed
```
```    36
```
```    37 lemma finite_induct [case_names empty insert, induct set: Finites]:
```
```    38   "finite F ==>
```
```    39     P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
```
```    40   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
```
```    41 proof -
```
```    42   assume "P {}" and
```
```    43     insert: "!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
```
```    44   assume "finite F"
```
```    45   thus "P F"
```
```    46   proof induct
```
```    47     show "P {}" .
```
```    48     fix F x assume F: "finite F" and P: "P F"
```
```    49     show "P (insert x F)"
```
```    50     proof cases
```
```    51       assume "x \<in> F"
```
```    52       hence "insert x F = F" by (rule insert_absorb)
```
```    53       with P show ?thesis by (simp only:)
```
```    54     next
```
```    55       assume "x \<notin> F"
```
```    56       from F this P show ?thesis by (rule insert)
```
```    57     qed
```
```    58   qed
```
```    59 qed
```
```    60
```
```    61 lemma finite_subset_induct [consumes 2, case_names empty insert]:
```
```    62   "finite F ==> F \<subseteq> A ==>
```
```    63     P {} ==> (!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
```
```    64     P F"
```
```    65 proof -
```
```    66   assume "P {}" and insert:
```
```    67     "!!F a. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
```
```    68   assume "finite F"
```
```    69   thus "F \<subseteq> A ==> P F"
```
```    70   proof induct
```
```    71     show "P {}" .
```
```    72     fix F x assume "finite F" and "x \<notin> F"
```
```    73       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
```
```    74     show "P (insert x F)"
```
```    75     proof (rule insert)
```
```    76       from i show "x \<in> A" by blast
```
```    77       from i have "F \<subseteq> A" by blast
```
```    78       with P show "P F" .
```
```    79     qed
```
```    80   qed
```
```    81 qed
```
```    82
```
```    83 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
```
```    84   -- {* The union of two finite sets is finite. *}
```
```    85   by (induct set: Finites) simp_all
```
```    86
```
```    87 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
```
```    88   -- {* Every subset of a finite set is finite. *}
```
```    89 proof -
```
```    90   assume "finite B"
```
```    91   thus "!!A. A \<subseteq> B ==> finite A"
```
```    92   proof induct
```
```    93     case empty
```
```    94     thus ?case by simp
```
```    95   next
```
```    96     case (insert F x A)
```
```    97     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
```
```    98     show "finite A"
```
```    99     proof cases
```
```   100       assume x: "x \<in> A"
```
```   101       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
```
```   102       with r have "finite (A - {x})" .
```
```   103       hence "finite (insert x (A - {x}))" ..
```
```   104       also have "insert x (A - {x}) = A" by (rule insert_Diff)
```
```   105       finally show ?thesis .
```
```   106     next
```
```   107       show "A \<subseteq> F ==> ?thesis" .
```
```   108       assume "x \<notin> A"
```
```   109       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
```
```   110     qed
```
```   111   qed
```
```   112 qed
```
```   113
```
```   114 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
```
```   115   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
```
```   116
```
```   117 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
```
```   118   -- {* The converse obviously fails. *}
```
```   119   by (blast intro: finite_subset)
```
```   120
```
```   121 lemma finite_insert [simp]: "finite (insert a A) = finite A"
```
```   122   apply (subst insert_is_Un)
```
```   123   apply (simp only: finite_Un, blast)
```
```   124   done
```
```   125
```
```   126 lemma finite_Union[simp, intro]:
```
```   127  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
```
```   128 by (induct rule:finite_induct) simp_all
```
```   129
```
```   130 lemma finite_empty_induct:
```
```   131   "finite A ==>
```
```   132   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
```
```   133 proof -
```
```   134   assume "finite A"
```
```   135     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
```
```   136   have "P (A - A)"
```
```   137   proof -
```
```   138     fix c b :: "'a set"
```
```   139     presume c: "finite c" and b: "finite b"
```
```   140       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
```
```   141     from c show "c \<subseteq> b ==> P (b - c)"
```
```   142     proof induct
```
```   143       case empty
```
```   144       from P1 show ?case by simp
```
```   145     next
```
```   146       case (insert F x)
```
```   147       have "P (b - F - {x})"
```
```   148       proof (rule P2)
```
```   149         from _ b show "finite (b - F)" by (rule finite_subset) blast
```
```   150         from insert show "x \<in> b - F" by simp
```
```   151         from insert show "P (b - F)" by simp
```
```   152       qed
```
```   153       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
```
```   154       finally show ?case .
```
```   155     qed
```
```   156   next
```
```   157     show "A \<subseteq> A" ..
```
```   158   qed
```
```   159   thus "P {}" by simp
```
```   160 qed
```
```   161
```
```   162 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
```
```   163   by (rule Diff_subset [THEN finite_subset])
```
```   164
```
```   165 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
```
```   166   apply (subst Diff_insert)
```
```   167   apply (case_tac "a : A - B")
```
```   168    apply (rule finite_insert [symmetric, THEN trans])
```
```   169    apply (subst insert_Diff, simp_all)
```
```   170   done
```
```   171
```
```   172
```
```   173 subsubsection {* Image and Inverse Image over Finite Sets *}
```
```   174
```
```   175 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
```
```   176   -- {* The image of a finite set is finite. *}
```
```   177   by (induct set: Finites) simp_all
```
```   178
```
```   179 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
```
```   180   apply (frule finite_imageI)
```
```   181   apply (erule finite_subset, assumption)
```
```   182   done
```
```   183
```
```   184 lemma finite_range_imageI:
```
```   185     "finite (range g) ==> finite (range (%x. f (g x)))"
```
```   186   apply (drule finite_imageI, simp)
```
```   187   done
```
```   188
```
```   189 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
```
```   190 proof -
```
```   191   have aux: "!!A. finite (A - {}) = finite A" by simp
```
```   192   fix B :: "'a set"
```
```   193   assume "finite B"
```
```   194   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
```
```   195     apply induct
```
```   196      apply simp
```
```   197     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
```
```   198      apply clarify
```
```   199      apply (simp (no_asm_use) add: inj_on_def)
```
```   200      apply (blast dest!: aux [THEN iffD1], atomize)
```
```   201     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
```
```   202     apply (frule subsetD [OF equalityD2 insertI1], clarify)
```
```   203     apply (rule_tac x = xa in bexI)
```
```   204      apply (simp_all add: inj_on_image_set_diff)
```
```   205     done
```
```   206 qed (rule refl)
```
```   207
```
```   208
```
```   209 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
```
```   210   -- {* The inverse image of a singleton under an injective function
```
```   211          is included in a singleton. *}
```
```   212   apply (auto simp add: inj_on_def)
```
```   213   apply (blast intro: the_equality [symmetric])
```
```   214   done
```
```   215
```
```   216 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
```
```   217   -- {* The inverse image of a finite set under an injective function
```
```   218          is finite. *}
```
```   219   apply (induct set: Finites, simp_all)
```
```   220   apply (subst vimage_insert)
```
```   221   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
```
```   222   done
```
```   223
```
```   224
```
```   225 subsubsection {* The finite UNION of finite sets *}
```
```   226
```
```   227 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
```
```   228   by (induct set: Finites) simp_all
```
```   229
```
```   230 text {*
```
```   231   Strengthen RHS to
```
```   232   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
```
```   233
```
```   234   We'd need to prove
```
```   235   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
```
```   236   by induction. *}
```
```   237
```
```   238 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
```
```   239   by (blast intro: finite_UN_I finite_subset)
```
```   240
```
```   241
```
```   242 subsubsection {* Sigma of finite sets *}
```
```   243
```
```   244 lemma finite_SigmaI [simp]:
```
```   245     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
```
```   246   by (unfold Sigma_def) (blast intro!: finite_UN_I)
```
```   247
```
```   248 lemma finite_Prod_UNIV:
```
```   249     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
```
```   250   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
```
```   251    apply (erule ssubst)
```
```   252    apply (erule finite_SigmaI, auto)
```
```   253   done
```
```   254
```
```   255 instance unit :: finite
```
```   256 proof
```
```   257   have "finite {()}" by simp
```
```   258   also have "{()} = UNIV" by auto
```
```   259   finally show "finite (UNIV :: unit set)" .
```
```   260 qed
```
```   261
```
```   262 instance * :: (finite, finite) finite
```
```   263 proof
```
```   264   show "finite (UNIV :: ('a \<times> 'b) set)"
```
```   265   proof (rule finite_Prod_UNIV)
```
```   266     show "finite (UNIV :: 'a set)" by (rule finite)
```
```   267     show "finite (UNIV :: 'b set)" by (rule finite)
```
```   268   qed
```
```   269 qed
```
```   270
```
```   271
```
```   272 subsubsection {* The powerset of a finite set *}
```
```   273
```
```   274 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
```
```   275 proof
```
```   276   assume "finite (Pow A)"
```
```   277   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
```
```   278   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
```
```   279 next
```
```   280   assume "finite A"
```
```   281   thus "finite (Pow A)"
```
```   282     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
```
```   283 qed
```
```   284
```
```   285 lemma finite_converse [iff]: "finite (r^-1) = finite r"
```
```   286   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
```
```   287    apply simp
```
```   288    apply (rule iffI)
```
```   289     apply (erule finite_imageD [unfolded inj_on_def])
```
```   290     apply (simp split add: split_split)
```
```   291    apply (erule finite_imageI)
```
```   292   apply (simp add: converse_def image_def, auto)
```
```   293   apply (rule bexI)
```
```   294    prefer 2 apply assumption
```
```   295   apply simp
```
```   296   done
```
```   297
```
```   298
```
```   299 subsubsection {* Finiteness of transitive closure *}
```
```   300
```
```   301 text {* (Thanks to Sidi Ehmety) *}
```
```   302
```
```   303 lemma finite_Field: "finite r ==> finite (Field r)"
```
```   304   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
```
```   305   apply (induct set: Finites)
```
```   306    apply (auto simp add: Field_def Domain_insert Range_insert)
```
```   307   done
```
```   308
```
```   309 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
```
```   310   apply clarify
```
```   311   apply (erule trancl_induct)
```
```   312    apply (auto simp add: Field_def)
```
```   313   done
```
```   314
```
```   315 lemma finite_trancl: "finite (r^+) = finite r"
```
```   316   apply auto
```
```   317    prefer 2
```
```   318    apply (rule trancl_subset_Field2 [THEN finite_subset])
```
```   319    apply (rule finite_SigmaI)
```
```   320     prefer 3
```
```   321     apply (blast intro: r_into_trancl' finite_subset)
```
```   322    apply (auto simp add: finite_Field)
```
```   323   done
```
```   324
```
```   325 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
```
```   326     finite (A <*> B)"
```
```   327   by (rule finite_SigmaI)
```
```   328
```
```   329
```
```   330 subsection {* Finite cardinality *}
```
```   331
```
```   332 text {*
```
```   333   This definition, although traditional, is ugly to work with: @{text
```
```   334   "card A == LEAST n. EX f. A = {f i | i. i < n}"}.  Therefore we have
```
```   335   switched to an inductive one:
```
```   336 *}
```
```   337
```
```   338 consts cardR :: "('a set \<times> nat) set"
```
```   339
```
```   340 inductive cardR
```
```   341   intros
```
```   342     EmptyI: "({}, 0) : cardR"
```
```   343     InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR"
```
```   344
```
```   345 constdefs
```
```   346   card :: "'a set => nat"
```
```   347   "card A == THE n. (A, n) : cardR"
```
```   348
```
```   349 inductive_cases cardR_emptyE: "({}, n) : cardR"
```
```   350 inductive_cases cardR_insertE: "(insert a A,n) : cardR"
```
```   351
```
```   352 lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)"
```
```   353   by (induct set: cardR) simp_all
```
```   354
```
```   355 lemma cardR_determ_aux1:
```
```   356     "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
```
```   357   apply (induct set: cardR, auto)
```
```   358   apply (simp add: insert_Diff_if, auto)
```
```   359   apply (drule cardR_SucD)
```
```   360   apply (blast intro!: cardR.intros)
```
```   361   done
```
```   362
```
```   363 lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR"
```
```   364   by (drule cardR_determ_aux1) auto
```
```   365
```
```   366 lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)"
```
```   367   apply (induct set: cardR)
```
```   368    apply (safe elim!: cardR_emptyE cardR_insertE)
```
```   369   apply (rename_tac B b m)
```
```   370   apply (case_tac "a = b")
```
```   371    apply (subgoal_tac "A = B")
```
```   372     prefer 2 apply (blast elim: equalityE, blast)
```
```   373   apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
```
```   374    prefer 2
```
```   375    apply (rule_tac x = "A Int B" in exI)
```
```   376    apply (blast elim: equalityE)
```
```   377   apply (frule_tac A = B in cardR_SucD)
```
```   378   apply (blast intro!: cardR.intros dest!: cardR_determ_aux2)
```
```   379   done
```
```   380
```
```   381 lemma cardR_imp_finite: "(A, n) : cardR ==> finite A"
```
```   382   by (induct set: cardR) simp_all
```
```   383
```
```   384 lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR"
```
```   385   by (induct set: Finites) (auto intro!: cardR.intros)
```
```   386
```
```   387 lemma card_equality: "(A,n) : cardR ==> card A = n"
```
```   388   by (unfold card_def) (blast intro: cardR_determ)
```
```   389
```
```   390 lemma card_empty [simp]: "card {} = 0"
```
```   391   by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE)
```
```   392
```
```   393 lemma card_insert_disjoint [simp]:
```
```   394   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
```
```   395 proof -
```
```   396   assume x: "x \<notin> A"
```
```   397   hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)"
```
```   398     apply (auto intro!: cardR.intros)
```
```   399     apply (rule_tac A1 = A in finite_imp_cardR [THEN exE])
```
```   400      apply (force dest: cardR_imp_finite)
```
```   401     apply (blast intro!: cardR.intros intro: cardR_determ)
```
```   402     done
```
```   403   assume "finite A"
```
```   404   thus ?thesis
```
```   405     apply (simp add: card_def aux)
```
```   406     apply (rule the_equality)
```
```   407      apply (auto intro: finite_imp_cardR
```
```   408        cong: conj_cong simp: card_def [symmetric] card_equality)
```
```   409     done
```
```   410 qed
```
```   411
```
```   412 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
```
```   413   apply auto
```
```   414   apply (drule_tac a = x in mk_disjoint_insert, clarify)
```
```   415   apply (rotate_tac -1, auto)
```
```   416   done
```
```   417
```
```   418 lemma card_insert_if:
```
```   419     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
```
```   420   by (simp add: insert_absorb)
```
```   421
```
```   422 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
```
```   423 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
```
```   424 apply(simp del:insert_Diff_single)
```
```   425 done
```
```   426
```
```   427 lemma card_Diff_singleton:
```
```   428     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
```
```   429   by (simp add: card_Suc_Diff1 [symmetric])
```
```   430
```
```   431 lemma card_Diff_singleton_if:
```
```   432     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
```
```   433   by (simp add: card_Diff_singleton)
```
```   434
```
```   435 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
```
```   436   by (simp add: card_insert_if card_Suc_Diff1)
```
```   437
```
```   438 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
```
```   439   by (simp add: card_insert_if)
```
```   440
```
```   441 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
```
```   442   apply (induct set: Finites, simp, clarify)
```
```   443   apply (subgoal_tac "finite A & A - {x} <= F")
```
```   444    prefer 2 apply (blast intro: finite_subset, atomize)
```
```   445   apply (drule_tac x = "A - {x}" in spec)
```
```   446   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
```
```   447   apply (case_tac "card A", auto)
```
```   448   done
```
```   449
```
```   450 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
```
```   451   apply (simp add: psubset_def linorder_not_le [symmetric])
```
```   452   apply (blast dest: card_seteq)
```
```   453   done
```
```   454
```
```   455 lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
```
```   456   apply (case_tac "A = B", simp)
```
```   457   apply (simp add: linorder_not_less [symmetric])
```
```   458   apply (blast dest: card_seteq intro: order_less_imp_le)
```
```   459   done
```
```   460
```
```   461 lemma card_Un_Int: "finite A ==> finite B
```
```   462     ==> card A + card B = card (A Un B) + card (A Int B)"
```
```   463   apply (induct set: Finites, simp)
```
```   464   apply (simp add: insert_absorb Int_insert_left)
```
```   465   done
```
```   466
```
```   467 lemma card_Un_disjoint: "finite A ==> finite B
```
```   468     ==> A Int B = {} ==> card (A Un B) = card A + card B"
```
```   469   by (simp add: card_Un_Int)
```
```   470
```
```   471 lemma card_Diff_subset:
```
```   472     "finite A ==> B <= A ==> card A - card B = card (A - B)"
```
```   473   apply (subgoal_tac "(A - B) Un B = A")
```
```   474    prefer 2 apply blast
```
```   475   apply (rule nat_add_right_cancel [THEN iffD1])
```
```   476   apply (rule card_Un_disjoint [THEN subst])
```
```   477      apply (erule_tac [4] ssubst)
```
```   478      prefer 3 apply blast
```
```   479     apply (simp_all add: add_commute not_less_iff_le
```
```   480       add_diff_inverse card_mono finite_subset)
```
```   481   done
```
```   482
```
```   483 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
```
```   484   apply (rule Suc_less_SucD)
```
```   485   apply (simp add: card_Suc_Diff1)
```
```   486   done
```
```   487
```
```   488 lemma card_Diff2_less:
```
```   489     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
```
```   490   apply (case_tac "x = y")
```
```   491    apply (simp add: card_Diff1_less)
```
```   492   apply (rule less_trans)
```
```   493    prefer 2 apply (auto intro!: card_Diff1_less)
```
```   494   done
```
```   495
```
```   496 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
```
```   497   apply (case_tac "x : A")
```
```   498    apply (simp_all add: card_Diff1_less less_imp_le)
```
```   499   done
```
```   500
```
```   501 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
```
```   502 by (erule psubsetI, blast)
```
```   503
```
```   504 lemma insert_partition:
```
```   505      "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|]
```
```   506       ==> x \<inter> \<Union> F = {}"
```
```   507 by auto
```
```   508
```
```   509 (* main cardinality theorem *)
```
```   510 lemma card_partition [rule_format]:
```
```   511      "finite C ==>
```
```   512         finite (\<Union> C) -->
```
```   513         (\<forall>c\<in>C. card c = k) -->
```
```   514         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
```
```   515         k * card(C) = card (\<Union> C)"
```
```   516 apply (erule finite_induct, simp)
```
```   517 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
```
```   518        finite_subset [of _ "\<Union> (insert x F)"])
```
```   519 done
```
```   520
```
```   521
```
```   522 subsubsection {* Cardinality of image *}
```
```   523
```
```   524 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
```
```   525   apply (induct set: Finites, simp)
```
```   526   apply (simp add: le_SucI finite_imageI card_insert_if)
```
```   527   done
```
```   528
```
```   529 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
```
```   530 by (induct set: Finites, simp_all)
```
```   531
```
```   532 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
```
```   533   by (simp add: card_seteq card_image)
```
```   534
```
```   535 lemma eq_card_imp_inj_on:
```
```   536   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
```
```   537 apply(induct rule:finite_induct)
```
```   538  apply simp
```
```   539 apply(frule card_image_le[where f = f])
```
```   540 apply(simp add:card_insert_if split:if_splits)
```
```   541 done
```
```   542
```
```   543 lemma inj_on_iff_eq_card:
```
```   544   "finite A ==> inj_on f A = (card(f ` A) = card A)"
```
```   545 by(blast intro: card_image eq_card_imp_inj_on)
```
```   546
```
```   547
```
```   548 subsubsection {* Cardinality of the Powerset *}
```
```   549
```
```   550 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
```
```   551   apply (induct set: Finites)
```
```   552    apply (simp_all add: Pow_insert)
```
```   553   apply (subst card_Un_disjoint, blast)
```
```   554     apply (blast intro: finite_imageI, blast)
```
```   555   apply (subgoal_tac "inj_on (insert x) (Pow F)")
```
```   556    apply (simp add: card_image Pow_insert)
```
```   557   apply (unfold inj_on_def)
```
```   558   apply (blast elim!: equalityE)
```
```   559   done
```
```   560
```
```   561 text {*
```
```   562   \medskip Relates to equivalence classes.  Based on a theorem of
```
```   563   F. Kammüller's.  The @{prop "finite C"} premise is redundant.
```
```   564 *}
```
```   565
```
```   566 lemma dvd_partition:
```
```   567   "finite C ==> finite (Union C) ==>
```
```   568     ALL c : C. k dvd card c ==>
```
```   569     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
```
```   570   k dvd card (Union C)"
```
```   571   apply (induct set: Finites, simp_all, clarify)
```
```   572   apply (subst card_Un_disjoint)
```
```   573   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
```
```   574   done
```
```   575
```
```   576
```
```   577 subsection {* A fold functional for finite sets *}
```
```   578
```
```   579 text {*
```
```   580   For @{text n} non-negative we have @{text "fold f e {x1, ..., xn} =
```
```   581   f x1 (... (f xn e))"} where @{text f} is at least left-commutative.
```
```   582 *}
```
```   583
```
```   584 consts
```
```   585   foldSet :: "('b => 'a => 'a) => 'a => ('b set \<times> 'a) set"
```
```   586
```
```   587 inductive "foldSet f e"
```
```   588   intros
```
```   589     emptyI [intro]: "({}, e) : foldSet f e"
```
```   590     insertI [intro]: "x \<notin> A ==> (A, y) : foldSet f e ==> (insert x A, f x y) : foldSet f e"
```
```   591
```
```   592 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f e"
```
```   593
```
```   594 constdefs
```
```   595   fold :: "('b => 'a => 'a) => 'a => 'b set => 'a"
```
```   596   "fold f e A == THE x. (A, x) : foldSet f e"
```
```   597
```
```   598 lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
```
```   599 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
```
```   600
```
```   601 lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
```
```   602   by (induct set: foldSet) auto
```
```   603
```
```   604 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f e"
```
```   605   by (induct set: Finites) auto
```
```   606
```
```   607
```
```   608 subsubsection {* Left-commutative operations *}
```
```   609
```
```   610 locale LC =
```
```   611   fixes f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
```
```   612   assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
```
```   613
```
```   614 lemma (in LC) foldSet_determ_aux:
```
```   615   "ALL A x. card A < n --> (A, x) : foldSet f e -->
```
```   616     (ALL y. (A, y) : foldSet f e --> y = x)"
```
```   617   apply (induct n)
```
```   618    apply (auto simp add: less_Suc_eq)
```
```   619   apply (erule foldSet.cases, blast)
```
```   620   apply (erule foldSet.cases, blast, clarify)
```
```   621   txt {* force simplification of @{text "card A < card (insert ...)"}. *}
```
```   622   apply (erule rev_mp)
```
```   623   apply (simp add: less_Suc_eq_le)
```
```   624   apply (rule impI)
```
```   625   apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
```
```   626    apply (subgoal_tac "Aa = Ab")
```
```   627     prefer 2 apply (blast elim!: equalityE, blast)
```
```   628   txt {* case @{prop "xa \<notin> xb"}. *}
```
```   629   apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
```
```   630    prefer 2 apply (blast elim!: equalityE, clarify)
```
```   631   apply (subgoal_tac "Aa = insert xb Ab - {xa}")
```
```   632    prefer 2 apply blast
```
```   633   apply (subgoal_tac "card Aa <= card Ab")
```
```   634    prefer 2
```
```   635    apply (rule Suc_le_mono [THEN subst])
```
```   636    apply (simp add: card_Suc_Diff1)
```
```   637   apply (rule_tac A1 = "Aa - {xb}" and f1 = f in finite_imp_foldSet [THEN exE])
```
```   638   apply (blast intro: foldSet_imp_finite finite_Diff)
```
```   639   apply (frule (1) Diff1_foldSet)
```
```   640   apply (subgoal_tac "ya = f xb x")
```
```   641    prefer 2 apply (blast del: equalityCE)
```
```   642   apply (subgoal_tac "(Ab - {xa}, x) : foldSet f e")
```
```   643    prefer 2 apply simp
```
```   644   apply (subgoal_tac "yb = f xa x")
```
```   645    prefer 2 apply (blast del: equalityCE dest: Diff1_foldSet)
```
```   646   apply (simp (no_asm_simp) add: left_commute)
```
```   647   done
```
```   648
```
```   649 lemma (in LC) foldSet_determ: "(A, x) : foldSet f e ==> (A, y) : foldSet f e ==> y = x"
```
```   650   by (blast intro: foldSet_determ_aux [rule_format])
```
```   651
```
```   652 lemma (in LC) fold_equality: "(A, y) : foldSet f e ==> fold f e A = y"
```
```   653   by (unfold fold_def) (blast intro: foldSet_determ)
```
```   654
```
```   655 lemma fold_empty [simp]: "fold f e {} = e"
```
```   656   by (unfold fold_def) blast
```
```   657
```
```   658 lemma (in LC) fold_insert_aux: "x \<notin> A ==>
```
```   659     ((insert x A, v) : foldSet f e) =
```
```   660     (EX y. (A, y) : foldSet f e & v = f x y)"
```
```   661   apply auto
```
```   662   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
```
```   663    apply (fastsimp dest: foldSet_imp_finite)
```
```   664   apply (blast intro: foldSet_determ)
```
```   665   done
```
```   666
```
```   667 lemma (in LC) fold_insert:
```
```   668     "finite A ==> x \<notin> A ==> fold f e (insert x A) = f x (fold f e A)"
```
```   669   apply (unfold fold_def)
```
```   670   apply (simp add: fold_insert_aux)
```
```   671   apply (rule the_equality)
```
```   672   apply (auto intro: finite_imp_foldSet
```
```   673     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
```
```   674   done
```
```   675
```
```   676 lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
```
```   677   apply (induct set: Finites, simp)
```
```   678   apply (simp add: left_commute fold_insert)
```
```   679   done
```
```   680
```
```   681 lemma (in LC) fold_nest_Un_Int:
```
```   682   "finite A ==> finite B
```
```   683     ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
```
```   684   apply (induct set: Finites, simp)
```
```   685   apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
```
```   686   done
```
```   687
```
```   688 lemma (in LC) fold_nest_Un_disjoint:
```
```   689   "finite A ==> finite B ==> A Int B = {}
```
```   690     ==> fold f e (A Un B) = fold f (fold f e B) A"
```
```   691   by (simp add: fold_nest_Un_Int)
```
```   692
```
```   693 declare foldSet_imp_finite [simp del]
```
```   694     empty_foldSetE [rule del]  foldSet.intros [rule del]
```
```   695   -- {* Delete rules to do with @{text foldSet} relation. *}
```
```   696
```
```   697
```
```   698
```
```   699 subsubsection {* Commutative monoids *}
```
```   700
```
```   701 text {*
```
```   702   We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
```
```   703   instead of @{text "'b => 'a => 'a"}.
```
```   704 *}
```
```   705
```
```   706 locale ACe =
```
```   707   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
```
```   708     and e :: 'a
```
```   709   assumes ident [simp]: "x \<cdot> e = x"
```
```   710     and commute: "x \<cdot> y = y \<cdot> x"
```
```   711     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
```
```   712
```
```   713 lemma (in ACe) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
```
```   714 proof -
```
```   715   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
```
```   716   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
```
```   717   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
```
```   718   finally show ?thesis .
```
```   719 qed
```
```   720
```
```   721 lemmas (in ACe) AC = assoc commute left_commute
```
```   722
```
```   723 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
```
```   724 proof -
```
```   725   have "x \<cdot> e = x" by (rule ident)
```
```   726   thus ?thesis by (subst commute)
```
```   727 qed
```
```   728
```
```   729 lemma (in ACe) fold_Un_Int:
```
```   730   "finite A ==> finite B ==>
```
```   731     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
```
```   732   apply (induct set: Finites, simp)
```
```   733   apply (simp add: AC insert_absorb Int_insert_left
```
```   734     LC.fold_insert [OF LC.intro])
```
```   735   done
```
```   736
```
```   737 lemma (in ACe) fold_Un_disjoint:
```
```   738   "finite A ==> finite B ==> A Int B = {} ==>
```
```   739     fold f e (A Un B) = fold f e A \<cdot> fold f e B"
```
```   740   by (simp add: fold_Un_Int)
```
```   741
```
```   742 lemma (in ACe) fold_Un_disjoint2:
```
```   743   "finite A ==> finite B ==> A Int B = {} ==>
```
```   744     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
```
```   745 proof -
```
```   746   assume b: "finite B"
```
```   747   assume "finite A"
```
```   748   thus "A Int B = {} ==>
```
```   749     fold (f o g) e (A Un B) = fold (f o g) e A \<cdot> fold (f o g) e B"
```
```   750   proof induct
```
```   751     case empty
```
```   752     thus ?case by simp
```
```   753   next
```
```   754     case (insert F x)
```
```   755     have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
```
```   756       by simp
```
```   757     also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
```
```   758       by (rule LC.fold_insert [OF LC.intro])
```
```   759         (insert b insert, auto simp add: left_commute)
```
```   760     also from insert have "fold (f o g) e (F \<union> B) =
```
```   761       fold (f o g) e F \<cdot> fold (f o g) e B" by blast
```
```   762     also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
```
```   763       by (simp add: AC)
```
```   764     also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
```
```   765       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
```
```   766         auto simp add: left_commute)
```
```   767     finally show ?case .
```
```   768   qed
```
```   769 qed
```
```   770
```
```   771
```
```   772 subsection {* Generalized summation over a set *}
```
```   773
```
```   774 constdefs
```
```   775   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
```
```   776   "setsum f A == if finite A then fold (op + o f) 0 A else 0"
```
```   777
```
```   778 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
```
```   779 written @{text"\<Sum>x\<in>A. e"}. *}
```
```   780
```
```   781 syntax
```
```   782   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
```
```   783 syntax (xsymbols)
```
```   784   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```   785 syntax (HTML output)
```
```   786   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```   787
```
```   788 translations -- {* Beware of argument permutation! *}
```
```   789   "SUM i:A. b" == "setsum (%i. b) A"
```
```   790   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
```
```   791
```
```   792 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
```
```   793  @{text"\<Sum>x|P. e"}. *}
```
```   794
```
```   795 syntax
```
```   796   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
```
```   797 syntax (xsymbols)
```
```   798   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```   799 syntax (HTML output)
```
```   800   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```   801
```
```   802 translations
```
```   803   "SUM x|P. t" => "setsum (%x. t) {x. P}"
```
```   804   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
```
```   805
```
```   806 print_translation {*
```
```   807 let
```
```   808   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
```
```   809     (if x<>y then raise Match
```
```   810      else let val x' = Syntax.mark_bound x
```
```   811               val t' = subst_bound(x',t)
```
```   812               val P' = subst_bound(x',P)
```
```   813           in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end)
```
```   814 in
```
```   815 [("setsum", setsum_tr')]
```
```   816 end
```
```   817 *}
```
```   818
```
```   819 text{* As Jeremy Avigad notes, setprod needs the same treatment \dots *}
```
```   820
```
```   821 lemma setsum_empty [simp]: "setsum f {} = 0"
```
```   822   by (simp add: setsum_def)
```
```   823
```
```   824 lemma setsum_insert [simp]:
```
```   825     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
```
```   826   by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
```
```   827
```
```   828 lemma setsum_reindex [rule_format]:
```
```   829      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
```
```   830 by (rule finite_induct, auto)
```
```   831
```
```   832 lemma setsum_reindex_id:
```
```   833      "finite B ==> inj_on f B ==> setsum f B = setsum id (f ` B)"
```
```   834 by (auto simp add: setsum_reindex id_o)
```
```   835
```
```   836 lemma setsum_cong:
```
```   837   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
```
```   838   apply (case_tac "finite B")
```
```   839    prefer 2 apply (simp add: setsum_def, simp)
```
```   840   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
```
```   841    apply simp
```
```   842   apply (erule finite_induct, simp)
```
```   843   apply (simp add: subset_insert_iff, clarify)
```
```   844   apply (subgoal_tac "finite C")
```
```   845    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```   846   apply (subgoal_tac "C = insert x (C - {x})")
```
```   847    prefer 2 apply blast
```
```   848   apply (erule ssubst)
```
```   849   apply (drule spec)
```
```   850   apply (erule (1) notE impE)
```
```   851   apply (simp add: Ball_def del:insert_Diff_single)
```
```   852   done
```
```   853
```
```   854 lemma setsum_reindex_cong:
```
```   855      "[|finite A; inj_on f A; B = f ` A; !!a. g a = h (f a)|]
```
```   856       ==> setsum h B = setsum g A"
```
```   857   by (simp add: setsum_reindex cong: setsum_cong)
```
```   858
```
```   859 lemma setsum_0: "setsum (%i. 0) A = 0"
```
```   860   apply (case_tac "finite A")
```
```   861    prefer 2 apply (simp add: setsum_def)
```
```   862   apply (erule finite_induct, auto)
```
```   863   done
```
```   864
```
```   865 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
```
```   866   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
```
```   867   apply (erule ssubst, rule setsum_0)
```
```   868   apply (rule setsum_cong, auto)
```
```   869   done
```
```   870
```
```   871 lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
```
```   872   -- {* Could allow many @{text "card"} proofs to be simplified. *}
```
```   873   by (induct set: Finites) auto
```
```   874
```
```   875 lemma setsum_Un_Int: "finite A ==> finite B
```
```   876     ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
```
```   877   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
```
```   878   apply (induct set: Finites, simp)
```
```   879   apply (simp add: add_ac Int_insert_left insert_absorb)
```
```   880   done
```
```   881
```
```   882 lemma setsum_Un_disjoint: "finite A ==> finite B
```
```   883   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
```
```   884   apply (subst setsum_Un_Int [symmetric], auto)
```
```   885   done
```
```   886
```
```   887 lemma setsum_UN_disjoint:
```
```   888     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```   889         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```   890       setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
```
```   891   apply (induct set: Finites, simp, atomize)
```
```   892   apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```   893    prefer 2 apply blast
```
```   894   apply (subgoal_tac "A x Int UNION F A = {}")
```
```   895    prefer 2 apply blast
```
```   896   apply (simp add: setsum_Un_disjoint)
```
```   897   done
```
```   898
```
```   899 lemma setsum_Union_disjoint:
```
```   900   "finite C ==> (ALL A:C. finite A) ==>
```
```   901         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```   902       setsum f (Union C) = setsum (setsum f) C"
```
```   903   apply (frule setsum_UN_disjoint [of C id f])
```
```   904   apply (unfold Union_def id_def, assumption+)
```
```   905   done
```
```   906
```
```   907 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```   908     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
```
```   909     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
```
```   910   apply (subst Sigma_def)
```
```   911   apply (subst setsum_UN_disjoint)
```
```   912   apply assumption
```
```   913   apply (rule ballI)
```
```   914   apply (drule_tac x = i in bspec, assumption)
```
```   915   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
```
```   916   apply (rule finite_surj)
```
```   917   apply auto
```
```   918   apply (rule setsum_cong, rule refl)
```
```   919   apply (subst setsum_UN_disjoint)
```
```   920   apply (erule bspec, assumption)
```
```   921   apply auto
```
```   922   done
```
```   923
```
```   924 lemma setsum_cartesian_product: "finite A ==> finite B ==>
```
```   925     (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) =
```
```   926     (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
```
```   927   by (erule setsum_Sigma, auto);
```
```   928
```
```   929 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
```
```   930   apply (case_tac "finite A")
```
```   931    prefer 2 apply (simp add: setsum_def)
```
```   932   apply (erule finite_induct, auto)
```
```   933   apply (simp add: add_ac)
```
```   934   done
```
```   935
```
```   936 subsubsection {* Properties in more restricted classes of structures *}
```
```   937
```
```   938 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
```
```   939   apply (case_tac "finite A")
```
```   940    prefer 2 apply (simp add: setsum_def)
```
```   941   apply (erule rev_mp)
```
```   942   apply (erule finite_induct, auto)
```
```   943   done
```
```   944
```
```   945 lemma setsum_eq_0_iff [simp]:
```
```   946     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
```
```   947   by (induct set: Finites) auto
```
```   948
```
```   949 lemma setsum_constant_nat:
```
```   950     "finite A ==> (\<Sum>x\<in>A. y) = (card A) * y"
```
```   951   -- {* Generalized to any @{text comm_semiring_1_cancel} in
```
```   952         @{text IntDef} as @{text setsum_constant}. *}
```
```   953   by (erule finite_induct, auto)
```
```   954
```
```   955 lemma setsum_Un: "finite A ==> finite B ==>
```
```   956     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
```
```   957   -- {* For the natural numbers, we have subtraction. *}
```
```   958   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
```
```   959
```
```   960 lemma setsum_Un_ring: "finite A ==> finite B ==>
```
```   961     (setsum f (A Un B) :: 'a :: ab_group_add) =
```
```   962       setsum f A + setsum f B - setsum f (A Int B)"
```
```   963   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
```
```   964
```
```   965 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
```
```   966     (if a:A then setsum f A - f a else setsum f A)"
```
```   967   apply (case_tac "finite A")
```
```   968    prefer 2 apply (simp add: setsum_def)
```
```   969   apply (erule finite_induct)
```
```   970    apply (auto simp add: insert_Diff_if)
```
```   971   apply (drule_tac a = a in mk_disjoint_insert, auto)
```
```   972   done
```
```   973
```
```   974 lemma setsum_diff1: "finite A \<Longrightarrow>
```
```   975   (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) =
```
```   976   (if a:A then setsum f A - f a else setsum f A)"
```
```   977   by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```   978
```
```   979 (* By Jeremy Siek: *)
```
```   980
```
```   981 lemma setsum_diff_nat:
```
```   982   assumes finB: "finite B"
```
```   983   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
```
```   984 using finB
```
```   985 proof (induct)
```
```   986   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
```
```   987 next
```
```   988   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
```
```   989     and xFinA: "insert x F \<subseteq> A"
```
```   990     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
```
```   991   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
```
```   992   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
```
```   993     by (simp add: setsum_diff1_nat)
```
```   994   from xFinA have "F \<subseteq> A" by simp
```
```   995   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
```
```   996   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
```
```   997     by simp
```
```   998   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
```
```   999   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
```
```  1000     by simp
```
```  1001   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
```
```  1002   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
```
```  1003     by simp
```
```  1004   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
```
```  1005 qed
```
```  1006
```
```  1007 lemma setsum_diff:
```
```  1008   assumes le: "finite A" "B \<subseteq> A"
```
```  1009   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
```
```  1010 proof -
```
```  1011   from le have finiteB: "finite B" using finite_subset by auto
```
```  1012   show ?thesis using finiteB le
```
```  1013     proof (induct)
```
```  1014       case empty
```
```  1015       thus ?case by auto
```
```  1016     next
```
```  1017       case (insert F x)
```
```  1018       thus ?case using le finiteB
```
```  1019 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
```
```  1020     qed
```
```  1021   qed
```
```  1022
```
```  1023 lemma setsum_mono:
```
```  1024   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
```
```  1025   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
```
```  1026 proof (cases "finite K")
```
```  1027   case True
```
```  1028   thus ?thesis using le
```
```  1029   proof (induct)
```
```  1030     case empty
```
```  1031     thus ?case by simp
```
```  1032   next
```
```  1033     case insert
```
```  1034     thus ?case using add_mono
```
```  1035       by force
```
```  1036   qed
```
```  1037 next
```
```  1038   case False
```
```  1039   thus ?thesis
```
```  1040     by (simp add: setsum_def)
```
```  1041 qed
```
```  1042
```
```  1043 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
```
```  1044   - setsum f A"
```
```  1045   by (induct set: Finites, auto)
```
```  1046
```
```  1047 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
```
```  1048   setsum f A - setsum g A"
```
```  1049   by (simp add: diff_minus setsum_addf setsum_negf)
```
```  1050
```
```  1051 lemma setsum_nonneg: "[| finite A;
```
```  1052     \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
```
```  1053     0 \<le> setsum f A";
```
```  1054   apply (induct set: Finites, auto)
```
```  1055   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
```
```  1056   apply (blast intro: add_mono)
```
```  1057   done
```
```  1058
```
```  1059 lemma setsum_nonpos: "[| finite A;
```
```  1060     \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
```
```  1061     setsum f A \<le> 0";
```
```  1062   apply (induct set: Finites, auto)
```
```  1063   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
```
```  1064   apply (blast intro: add_mono)
```
```  1065   done
```
```  1066
```
```  1067 lemma setsum_mult:
```
```  1068   fixes f :: "'a => ('b::semiring_0_cancel)"
```
```  1069   shows "r * setsum f A = setsum (%n. r * f n) A"
```
```  1070 proof (cases "finite A")
```
```  1071   case True
```
```  1072   thus ?thesis
```
```  1073   proof (induct)
```
```  1074     case empty thus ?case by simp
```
```  1075   next
```
```  1076     case (insert A x) thus ?case by (simp add: right_distrib)
```
```  1077   qed
```
```  1078 next
```
```  1079   case False thus ?thesis by (simp add: setsum_def)
```
```  1080 qed
```
```  1081
```
```  1082 lemma setsum_abs:
```
```  1083   fixes f :: "'a => ('b::lordered_ab_group_abs)"
```
```  1084   assumes fin: "finite A"
```
```  1085   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
```
```  1086 using fin
```
```  1087 proof (induct)
```
```  1088   case empty thus ?case by simp
```
```  1089 next
```
```  1090   case (insert A x)
```
```  1091   thus ?case by (auto intro: abs_triangle_ineq order_trans)
```
```  1092 qed
```
```  1093
```
```  1094 lemma setsum_abs_ge_zero:
```
```  1095   fixes f :: "'a => ('b::lordered_ab_group_abs)"
```
```  1096   assumes fin: "finite A"
```
```  1097   shows "0 \<le> setsum (%i. abs(f i)) A"
```
```  1098 using fin
```
```  1099 proof (induct)
```
```  1100   case empty thus ?case by simp
```
```  1101 next
```
```  1102   case (insert A x) thus ?case by (auto intro: order_trans)
```
```  1103 qed
```
```  1104
```
```  1105 subsubsection {* Cardinality of unions and Sigma sets *}
```
```  1106
```
```  1107 lemma card_UN_disjoint:
```
```  1108     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1109         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1110       card (UNION I A) = setsum (%i. card (A i)) I"
```
```  1111   apply (subst card_eq_setsum)
```
```  1112   apply (subst finite_UN, assumption+)
```
```  1113   apply (subgoal_tac
```
```  1114            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
```
```  1115   apply (simp add: setsum_UN_disjoint)
```
```  1116   apply (simp add: setsum_constant_nat cong: setsum_cong)
```
```  1117   done
```
```  1118
```
```  1119 lemma card_Union_disjoint:
```
```  1120   "finite C ==> (ALL A:C. finite A) ==>
```
```  1121         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```  1122       card (Union C) = setsum card C"
```
```  1123   apply (frule card_UN_disjoint [of C id])
```
```  1124   apply (unfold Union_def id_def, assumption+)
```
```  1125   done
```
```  1126
```
```  1127 lemma SigmaI_insert: "y \<notin> A ==>
```
```  1128   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
```
```  1129   by auto
```
```  1130
```
```  1131 lemma card_cartesian_product_singleton: "finite A ==>
```
```  1132     card({x} <*> A) = card(A)"
```
```  1133   apply (subgoal_tac "inj_on (%y .(x,y)) A")
```
```  1134   apply (frule card_image, assumption)
```
```  1135   apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
```
```  1136   apply (auto simp add: inj_on_def)
```
```  1137   done
```
```  1138
```
```  1139 lemma card_SigmaI [rule_format,simp]: "finite A ==>
```
```  1140   (ALL a:A. finite (B a)) -->
```
```  1141   card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
```
```  1142   apply (erule finite_induct, auto)
```
```  1143   apply (subst SigmaI_insert, assumption)
```
```  1144   apply (subst card_Un_disjoint)
```
```  1145   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
```
```  1146   done
```
```  1147
```
```  1148 lemma card_cartesian_product:
```
```  1149      "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)"
```
```  1150   by (simp add: setsum_constant_nat)
```
```  1151
```
```  1152
```
```  1153
```
```  1154 subsection {* Generalized product over a set *}
```
```  1155
```
```  1156 constdefs
```
```  1157   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
```
```  1158   "setprod f A == if finite A then fold (op * o f) 1 A else 1"
```
```  1159
```
```  1160 syntax
```
```  1161   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
```
```  1162
```
```  1163 syntax (xsymbols)
```
```  1164   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1165 syntax (HTML output)
```
```  1166   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1167 translations
```
```  1168   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
```
```  1169
```
```  1170 lemma setprod_empty [simp]: "setprod f {} = 1"
```
```  1171   by (auto simp add: setprod_def)
```
```  1172
```
```  1173 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
```
```  1174     setprod f (insert a A) = f a * setprod f A"
```
```  1175   by (auto simp add: setprod_def LC_def LC.fold_insert
```
```  1176       mult_left_commute)
```
```  1177
```
```  1178 lemma setprod_reindex [rule_format]:
```
```  1179      "finite B ==> inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
```
```  1180 by (rule finite_induct, auto)
```
```  1181
```
```  1182 lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
```
```  1183     setprod f B = setprod id (f ` B)"
```
```  1184 by (auto simp add: setprod_reindex id_o)
```
```  1185
```
```  1186 lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
```
```  1187     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
```
```  1188   by (frule setprod_reindex, assumption, simp)
```
```  1189
```
```  1190 lemma setprod_cong:
```
```  1191   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
```
```  1192   apply (case_tac "finite B")
```
```  1193    prefer 2 apply (simp add: setprod_def, simp)
```
```  1194   apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
```
```  1195    apply simp
```
```  1196   apply (erule finite_induct, simp)
```
```  1197   apply (simp add: subset_insert_iff, clarify)
```
```  1198   apply (subgoal_tac "finite C")
```
```  1199    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```  1200   apply (subgoal_tac "C = insert x (C - {x})")
```
```  1201    prefer 2 apply blast
```
```  1202   apply (erule ssubst)
```
```  1203   apply (drule spec)
```
```  1204   apply (erule (1) notE impE)
```
```  1205   apply (simp add: Ball_def del:insert_Diff_single)
```
```  1206   done
```
```  1207
```
```  1208 lemma setprod_1: "setprod (%i. 1) A = 1"
```
```  1209   apply (case_tac "finite A")
```
```  1210   apply (erule finite_induct, auto simp add: mult_ac)
```
```  1211   apply (simp add: setprod_def)
```
```  1212   done
```
```  1213
```
```  1214 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
```
```  1215   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
```
```  1216   apply (erule ssubst, rule setprod_1)
```
```  1217   apply (rule setprod_cong, auto)
```
```  1218   done
```
```  1219
```
```  1220 lemma setprod_Un_Int: "finite A ==> finite B
```
```  1221     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
```
```  1222   apply (induct set: Finites, simp)
```
```  1223   apply (simp add: mult_ac insert_absorb)
```
```  1224   apply (simp add: mult_ac Int_insert_left insert_absorb)
```
```  1225   done
```
```  1226
```
```  1227 lemma setprod_Un_disjoint: "finite A ==> finite B
```
```  1228   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
```
```  1229   apply (subst setprod_Un_Int [symmetric], auto simp add: mult_ac)
```
```  1230   done
```
```  1231
```
```  1232 lemma setprod_UN_disjoint:
```
```  1233     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1234         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1235       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
```
```  1236   apply (induct set: Finites, simp, atomize)
```
```  1237   apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```  1238    prefer 2 apply blast
```
```  1239   apply (subgoal_tac "A x Int UNION F A = {}")
```
```  1240    prefer 2 apply blast
```
```  1241   apply (simp add: setprod_Un_disjoint)
```
```  1242   done
```
```  1243
```
```  1244 lemma setprod_Union_disjoint:
```
```  1245   "finite C ==> (ALL A:C. finite A) ==>
```
```  1246         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```  1247       setprod f (Union C) = setprod (setprod f) C"
```
```  1248   apply (frule setprod_UN_disjoint [of C id f])
```
```  1249   apply (unfold Union_def id_def, assumption+)
```
```  1250   done
```
```  1251
```
```  1252 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1253     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
```
```  1254     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
```
```  1255   apply (subst Sigma_def)
```
```  1256   apply (subst setprod_UN_disjoint)
```
```  1257   apply assumption
```
```  1258   apply (rule ballI)
```
```  1259   apply (drule_tac x = i in bspec, assumption)
```
```  1260   apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
```
```  1261   apply (rule finite_surj)
```
```  1262   apply auto
```
```  1263   apply (rule setprod_cong, rule refl)
```
```  1264   apply (subst setprod_UN_disjoint)
```
```  1265   apply (erule bspec, assumption)
```
```  1266   apply auto
```
```  1267   done
```
```  1268
```
```  1269 lemma setprod_cartesian_product: "finite A ==> finite B ==>
```
```  1270     (\<Prod>x:A. (\<Prod>y: B. f x y)) =
```
```  1271     (\<Prod>z:(A <*> B). f (fst z) (snd z))"
```
```  1272   by (erule setprod_Sigma, auto)
```
```  1273
```
```  1274 lemma setprod_timesf: "setprod (%x. f x * g x) A =
```
```  1275     (setprod f A * setprod g A)"
```
```  1276   apply (case_tac "finite A")
```
```  1277    prefer 2 apply (simp add: setprod_def mult_ac)
```
```  1278   apply (erule finite_induct, auto)
```
```  1279   apply (simp add: mult_ac)
```
```  1280   done
```
```  1281
```
```  1282 subsubsection {* Properties in more restricted classes of structures *}
```
```  1283
```
```  1284 lemma setprod_eq_1_iff [simp]:
```
```  1285     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
```
```  1286   by (induct set: Finites) auto
```
```  1287
```
```  1288 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
```
```  1289   apply (erule finite_induct)
```
```  1290   apply (auto simp add: power_Suc)
```
```  1291   done
```
```  1292
```
```  1293 lemma setprod_zero:
```
```  1294      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
```
```  1295   apply (induct set: Finites, force, clarsimp)
```
```  1296   apply (erule disjE, auto)
```
```  1297   done
```
```  1298
```
```  1299 lemma setprod_nonneg [rule_format]:
```
```  1300      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
```
```  1301   apply (case_tac "finite A")
```
```  1302   apply (induct set: Finites, force, clarsimp)
```
```  1303   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
```
```  1304   apply (rule mult_mono, assumption+)
```
```  1305   apply (auto simp add: setprod_def)
```
```  1306   done
```
```  1307
```
```  1308 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
```
```  1309      --> 0 < setprod f A"
```
```  1310   apply (case_tac "finite A")
```
```  1311   apply (induct set: Finites, force, clarsimp)
```
```  1312   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
```
```  1313   apply (rule mult_strict_mono, assumption+)
```
```  1314   apply (auto simp add: setprod_def)
```
```  1315   done
```
```  1316
```
```  1317 lemma setprod_nonzero [rule_format]:
```
```  1318     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
```
```  1319       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
```
```  1320   apply (erule finite_induct, auto)
```
```  1321   done
```
```  1322
```
```  1323 lemma setprod_zero_eq:
```
```  1324     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
```
```  1325      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
```
```  1326   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
```
```  1327   done
```
```  1328
```
```  1329 lemma setprod_nonzero_field:
```
```  1330     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
```
```  1331   apply (rule setprod_nonzero, auto)
```
```  1332   done
```
```  1333
```
```  1334 lemma setprod_zero_eq_field:
```
```  1335     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
```
```  1336   apply (rule setprod_zero_eq, auto)
```
```  1337   done
```
```  1338
```
```  1339 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
```
```  1340     (setprod f (A Un B) :: 'a ::{field})
```
```  1341       = setprod f A * setprod f B / setprod f (A Int B)"
```
```  1342   apply (subst setprod_Un_Int [symmetric], auto)
```
```  1343   apply (subgoal_tac "finite (A Int B)")
```
```  1344   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
```
```  1345   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
```
```  1346   done
```
```  1347
```
```  1348 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
```
```  1349     (setprod f (A - {a}) :: 'a :: {field}) =
```
```  1350       (if a:A then setprod f A / f a else setprod f A)"
```
```  1351   apply (erule finite_induct)
```
```  1352    apply (auto simp add: insert_Diff_if)
```
```  1353   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
```
```  1354   apply (erule ssubst)
```
```  1355   apply (subst times_divide_eq_right [THEN sym])
```
```  1356   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
```
```  1357   done
```
```  1358
```
```  1359 lemma setprod_inversef: "finite A ==>
```
```  1360     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
```
```  1361       setprod (inverse \<circ> f) A = inverse (setprod f A)"
```
```  1362   apply (erule finite_induct)
```
```  1363   apply (simp, simp)
```
```  1364   done
```
```  1365
```
```  1366 lemma setprod_dividef:
```
```  1367      "[|finite A;
```
```  1368         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
```
```  1369       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
```
```  1370   apply (subgoal_tac
```
```  1371          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
```
```  1372   apply (erule ssubst)
```
```  1373   apply (subst divide_inverse)
```
```  1374   apply (subst setprod_timesf)
```
```  1375   apply (subst setprod_inversef, assumption+, rule refl)
```
```  1376   apply (rule setprod_cong, rule refl)
```
```  1377   apply (subst divide_inverse, auto)
```
```  1378   done
```
```  1379
```
```  1380
```
```  1381 subsection{* Min and Max of finite linearly ordered sets *}
```
```  1382
```
```  1383 text{* Seemed easier to define directly than via fold. *}
```
```  1384
```
```  1385 lemma ex_Max: fixes S :: "('a::linorder)set"
```
```  1386   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
```
```  1387 using fin
```
```  1388 proof (induct)
```
```  1389   case empty thus ?case by simp
```
```  1390 next
```
```  1391   case (insert S x)
```
```  1392   show ?case
```
```  1393   proof (cases)
```
```  1394     assume "S = {}" thus ?thesis by simp
```
```  1395   next
```
```  1396     assume nonempty: "S \<noteq> {}"
```
```  1397     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
```
```  1398     show ?thesis
```
```  1399     proof (cases)
```
```  1400       assume "x \<le> m" thus ?thesis using m by blast
```
```  1401     next
```
```  1402       assume "~ x \<le> m" thus ?thesis using m
```
```  1403         by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
```
```  1404     qed
```
```  1405   qed
```
```  1406 qed
```
```  1407
```
```  1408 lemma ex_Min: fixes S :: "('a::linorder)set"
```
```  1409   assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
```
```  1410 using fin
```
```  1411 proof (induct)
```
```  1412   case empty thus ?case by simp
```
```  1413 next
```
```  1414   case (insert S x)
```
```  1415   show ?case
```
```  1416   proof (cases)
```
```  1417     assume "S = {}" thus ?thesis by simp
```
```  1418   next
```
```  1419     assume nonempty: "S \<noteq> {}"
```
```  1420     then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
```
```  1421     show ?thesis
```
```  1422     proof (cases)
```
```  1423       assume "m \<le> x" thus ?thesis using m by blast
```
```  1424     next
```
```  1425       assume "~ m \<le> x" thus ?thesis using m
```
```  1426         by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
```
```  1427     qed
```
```  1428   qed
```
```  1429 qed
```
```  1430
```
```  1431 constdefs
```
```  1432   Min :: "('a::linorder)set => 'a"
```
```  1433   "Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
```
```  1434
```
```  1435   Max :: "('a::linorder)set => 'a"
```
```  1436   "Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
```
```  1437
```
```  1438 lemma Min [simp]:
```
```  1439   assumes a: "finite S"  "S \<noteq> {}"
```
```  1440   shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
```
```  1441 proof (unfold Min_def, rule theI')
```
```  1442   show "\<exists>!m. ?P m"
```
```  1443   proof (rule ex_ex1I)
```
```  1444     show "\<exists>m. ?P m" using ex_Min[OF a] by blast
```
```  1445   next
```
```  1446     fix m1 m2 assume "?P m1" and "?P m2"
```
```  1447     thus "m1 = m2" by (blast dest: order_antisym)
```
```  1448   qed
```
```  1449 qed
```
```  1450
```
```  1451 lemma Max [simp]:
```
```  1452   assumes a: "finite S"  "S \<noteq> {}"
```
```  1453   shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
```
```  1454 proof (unfold Max_def, rule theI')
```
```  1455   show "\<exists>!m. ?P m"
```
```  1456   proof (rule ex_ex1I)
```
```  1457     show "\<exists>m. ?P m" using ex_Max[OF a] by blast
```
```  1458   next
```
```  1459     fix m1 m2 assume "?P m1" "?P m2"
```
```  1460     thus "m1 = m2" by (blast dest: order_antisym)
```
```  1461   qed
```
```  1462 qed
```
```  1463
```
```  1464
```
```  1465 subsection {* Theorems about @{text "choose"} *}
```
```  1466
```
```  1467 text {*
```
```  1468   \medskip Basic theorem about @{text "choose"}.  By Florian
```
```  1469   Kamm\"uller, tidied by LCP.
```
```  1470 *}
```
```  1471
```
```  1472 lemma card_s_0_eq_empty:
```
```  1473     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
```
```  1474   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
```
```  1475   apply (simp cong add: rev_conj_cong)
```
```  1476   done
```
```  1477
```
```  1478 lemma choose_deconstruct: "finite M ==> x \<notin> M
```
```  1479   ==> {s. s <= insert x M & card(s) = Suc k}
```
```  1480        = {s. s <= M & card(s) = Suc k} Un
```
```  1481          {s. EX t. t <= M & card(t) = k & s = insert x t}"
```
```  1482   apply safe
```
```  1483    apply (auto intro: finite_subset [THEN card_insert_disjoint])
```
```  1484   apply (drule_tac x = "xa - {x}" in spec)
```
```  1485   apply (subgoal_tac "x \<notin> xa", auto)
```
```  1486   apply (erule rev_mp, subst card_Diff_singleton)
```
```  1487   apply (auto intro: finite_subset)
```
```  1488   done
```
```  1489
```
```  1490 lemma card_inj_on_le:
```
```  1491     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
```
```  1492 apply (subgoal_tac "finite A")
```
```  1493  apply (force intro: card_mono simp add: card_image [symmetric])
```
```  1494 apply (blast intro: finite_imageD dest: finite_subset)
```
```  1495 done
```
```  1496
```
```  1497 lemma card_bij_eq:
```
```  1498     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
```
```  1499        finite A; finite B |] ==> card A = card B"
```
```  1500   by (auto intro: le_anti_sym card_inj_on_le)
```
```  1501
```
```  1502 text{*There are as many subsets of @{term A} having cardinality @{term k}
```
```  1503  as there are sets obtained from the former by inserting a fixed element
```
```  1504  @{term x} into each.*}
```
```  1505 lemma constr_bij:
```
```  1506    "[|finite A; x \<notin> A|] ==>
```
```  1507     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
```
```  1508     card {B. B <= A & card(B) = k}"
```
```  1509   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
```
```  1510        apply (auto elim!: equalityE simp add: inj_on_def)
```
```  1511     apply (subst Diff_insert0, auto)
```
```  1512    txt {* finiteness of the two sets *}
```
```  1513    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
```
```  1514    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
```
```  1515    apply fast+
```
```  1516   done
```
```  1517
```
```  1518 text {*
```
```  1519   Main theorem: combinatorial statement about number of subsets of a set.
```
```  1520 *}
```
```  1521
```
```  1522 lemma n_sub_lemma:
```
```  1523   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
```
```  1524   apply (induct k)
```
```  1525    apply (simp add: card_s_0_eq_empty, atomize)
```
```  1526   apply (rotate_tac -1, erule finite_induct)
```
```  1527    apply (simp_all (no_asm_simp) cong add: conj_cong
```
```  1528      add: card_s_0_eq_empty choose_deconstruct)
```
```  1529   apply (subst card_Un_disjoint)
```
```  1530      prefer 4 apply (force simp add: constr_bij)
```
```  1531     prefer 3 apply force
```
```  1532    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
```
```  1533      finite_subset [of _ "Pow (insert x F)", standard])
```
```  1534   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
```
```  1535   done
```
```  1536
```
```  1537 theorem n_subsets:
```
```  1538     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
```
```  1539   by (simp add: n_sub_lemma)
```
```  1540
```
```  1541 end
```