src/HOL/Finite_Set.thy
author haftmann
Mon Apr 27 10:11:44 2009 +0200 (2009-04-27)
changeset 31001 7e6ffd8f51a9
parent 30863 5dc392a59bb7
child 31017 2c227493ea56
permissions -rw-r--r--
cleaned up theory power further
     1 (*  Title:      HOL/Finite_Set.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* Finite sets *}
     7 
     8 theory Finite_Set
     9 imports Nat Product_Type Power
    10 begin
    11 
    12 subsection {* Definition and basic properties *}
    13 
    14 inductive finite :: "'a set => bool"
    15   where
    16     emptyI [simp, intro!]: "finite {}"
    17   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
    18 
    19 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    20   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    21   shows "\<exists>a::'a. a \<notin> A"
    22 proof -
    23   from assms have "A \<noteq> UNIV" by blast
    24   thus ?thesis by blast
    25 qed
    26 
    27 lemma finite_induct [case_names empty insert, induct set: finite]:
    28   "finite F ==>
    29     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    30   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    31 proof -
    32   assume "P {}" and
    33     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    34   assume "finite F"
    35   thus "P F"
    36   proof induct
    37     show "P {}" by fact
    38     fix x F assume F: "finite F" and P: "P F"
    39     show "P (insert x F)"
    40     proof cases
    41       assume "x \<in> F"
    42       hence "insert x F = F" by (rule insert_absorb)
    43       with P show ?thesis by (simp only:)
    44     next
    45       assume "x \<notin> F"
    46       from F this P show ?thesis by (rule insert)
    47     qed
    48   qed
    49 qed
    50 
    51 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
    52 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
    53  \<lbrakk> \<And>x. P{x};
    54    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    55  \<Longrightarrow> P F"
    56 using fin
    57 proof induct
    58   case empty thus ?case by simp
    59 next
    60   case (insert x F)
    61   show ?case
    62   proof cases
    63     assume "F = {}"
    64     thus ?thesis using `P {x}` by simp
    65   next
    66     assume "F \<noteq> {}"
    67     thus ?thesis using insert by blast
    68   qed
    69 qed
    70 
    71 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    72   assumes "finite F" and "F \<subseteq> A"
    73     and empty: "P {}"
    74     and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    75   shows "P F"
    76 proof -
    77   from `finite F` and `F \<subseteq> A`
    78   show ?thesis
    79   proof induct
    80     show "P {}" by fact
    81   next
    82     fix x F
    83     assume "finite F" and "x \<notin> F" and
    84       P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    85     show "P (insert x F)"
    86     proof (rule insert)
    87       from i show "x \<in> A" by blast
    88       from i have "F \<subseteq> A" by blast
    89       with P show "P F" .
    90       show "finite F" by fact
    91       show "x \<notin> F" by fact
    92     qed
    93   qed
    94 qed
    95 
    96 text{* A finite choice principle. Does not need the SOME choice operator. *}
    97 lemma finite_set_choice:
    98   "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
    99 proof (induct set: finite)
   100   case empty thus ?case by simp
   101 next
   102   case (insert a A)
   103   then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
   104   show ?case (is "EX f. ?P f")
   105   proof
   106     show "?P(%x. if x = a then b else f x)" using f ab by auto
   107   qed
   108 qed
   109 
   110 
   111 text{* Finite sets are the images of initial segments of natural numbers: *}
   112 
   113 lemma finite_imp_nat_seg_image_inj_on:
   114   assumes fin: "finite A" 
   115   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
   116 using fin
   117 proof induct
   118   case empty
   119   show ?case  
   120   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 
   121   qed
   122 next
   123   case (insert a A)
   124   have notinA: "a \<notin> A" by fact
   125   from insert.hyps obtain n f
   126     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
   127   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
   128         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
   129     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
   130   thus ?case by blast
   131 qed
   132 
   133 lemma nat_seg_image_imp_finite:
   134   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
   135 proof (induct n)
   136   case 0 thus ?case by simp
   137 next
   138   case (Suc n)
   139   let ?B = "f ` {i. i < n}"
   140   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
   141   show ?case
   142   proof cases
   143     assume "\<exists>k<n. f n = f k"
   144     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
   145     thus ?thesis using finB by simp
   146   next
   147     assume "\<not>(\<exists> k<n. f n = f k)"
   148     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
   149     thus ?thesis using finB by simp
   150   qed
   151 qed
   152 
   153 lemma finite_conv_nat_seg_image:
   154   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
   155 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
   156 
   157 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
   158 by(fastsimp simp: finite_conv_nat_seg_image)
   159 
   160 
   161 subsubsection{* Finiteness and set theoretic constructions *}
   162 
   163 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
   164 by (induct set: finite) simp_all
   165 
   166 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
   167   -- {* Every subset of a finite set is finite. *}
   168 proof -
   169   assume "finite B"
   170   thus "!!A. A \<subseteq> B ==> finite A"
   171   proof induct
   172     case empty
   173     thus ?case by simp
   174   next
   175     case (insert x F A)
   176     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
   177     show "finite A"
   178     proof cases
   179       assume x: "x \<in> A"
   180       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
   181       with r have "finite (A - {x})" .
   182       hence "finite (insert x (A - {x}))" ..
   183       also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
   184       finally show ?thesis .
   185     next
   186       show "A \<subseteq> F ==> ?thesis" by fact
   187       assume "x \<notin> A"
   188       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   189     qed
   190   qed
   191 qed
   192 
   193 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   194 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   195 
   196 lemma finite_Collect_disjI[simp]:
   197   "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
   198 by(simp add:Collect_disj_eq)
   199 
   200 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   201   -- {* The converse obviously fails. *}
   202 by (blast intro: finite_subset)
   203 
   204 lemma finite_Collect_conjI [simp, intro]:
   205   "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
   206   -- {* The converse obviously fails. *}
   207 by(simp add:Collect_conj_eq)
   208 
   209 lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
   210 by(simp add: le_eq_less_or_eq)
   211 
   212 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   213   apply (subst insert_is_Un)
   214   apply (simp only: finite_Un, blast)
   215   done
   216 
   217 lemma finite_Union[simp, intro]:
   218  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
   219 by (induct rule:finite_induct) simp_all
   220 
   221 lemma finite_empty_induct:
   222   assumes "finite A"
   223     and "P A"
   224     and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   225   shows "P {}"
   226 proof -
   227   have "P (A - A)"
   228   proof -
   229     {
   230       fix c b :: "'a set"
   231       assume c: "finite c" and b: "finite b"
   232 	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   233       have "c \<subseteq> b ==> P (b - c)"
   234 	using c
   235       proof induct
   236 	case empty
   237 	from P1 show ?case by simp
   238       next
   239 	case (insert x F)
   240 	have "P (b - F - {x})"
   241 	proof (rule P2)
   242           from _ b show "finite (b - F)" by (rule finite_subset) blast
   243           from insert show "x \<in> b - F" by simp
   244           from insert show "P (b - F)" by simp
   245 	qed
   246 	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   247 	finally show ?case .
   248       qed
   249     }
   250     then show ?thesis by this (simp_all add: assms)
   251   qed
   252   then show ?thesis by simp
   253 qed
   254 
   255 lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
   256 by (rule Diff_subset [THEN finite_subset])
   257 
   258 lemma finite_Diff2 [simp]:
   259   assumes "finite B" shows "finite (A - B) = finite A"
   260 proof -
   261   have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
   262   also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
   263   finally show ?thesis ..
   264 qed
   265 
   266 lemma finite_compl[simp]:
   267   "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
   268 by(simp add:Compl_eq_Diff_UNIV)
   269 
   270 lemma finite_Collect_not[simp]:
   271   "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
   272 by(simp add:Collect_neg_eq)
   273 
   274 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   275   apply (subst Diff_insert)
   276   apply (case_tac "a : A - B")
   277    apply (rule finite_insert [symmetric, THEN trans])
   278    apply (subst insert_Diff, simp_all)
   279   done
   280 
   281 
   282 text {* Image and Inverse Image over Finite Sets *}
   283 
   284 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   285   -- {* The image of a finite set is finite. *}
   286   by (induct set: finite) simp_all
   287 
   288 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   289   apply (frule finite_imageI)
   290   apply (erule finite_subset, assumption)
   291   done
   292 
   293 lemma finite_range_imageI:
   294     "finite (range g) ==> finite (range (%x. f (g x)))"
   295   apply (drule finite_imageI, simp add: range_composition)
   296   done
   297 
   298 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   299 proof -
   300   have aux: "!!A. finite (A - {}) = finite A" by simp
   301   fix B :: "'a set"
   302   assume "finite B"
   303   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   304     apply induct
   305      apply simp
   306     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   307      apply clarify
   308      apply (simp (no_asm_use) add: inj_on_def)
   309      apply (blast dest!: aux [THEN iffD1], atomize)
   310     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   311     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   312     apply (rule_tac x = xa in bexI)
   313      apply (simp_all add: inj_on_image_set_diff)
   314     done
   315 qed (rule refl)
   316 
   317 
   318 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   319   -- {* The inverse image of a singleton under an injective function
   320          is included in a singleton. *}
   321   apply (auto simp add: inj_on_def)
   322   apply (blast intro: the_equality [symmetric])
   323   done
   324 
   325 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   326   -- {* The inverse image of a finite set under an injective function
   327          is finite. *}
   328   apply (induct set: finite)
   329    apply simp_all
   330   apply (subst vimage_insert)
   331   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   332   done
   333 
   334 
   335 text {* The finite UNION of finite sets *}
   336 
   337 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   338   by (induct set: finite) simp_all
   339 
   340 text {*
   341   Strengthen RHS to
   342   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   343 
   344   We'd need to prove
   345   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   346   by induction. *}
   347 
   348 lemma finite_UN [simp]:
   349   "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   350 by (blast intro: finite_UN_I finite_subset)
   351 
   352 lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
   353   finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
   354 apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
   355  apply auto
   356 done
   357 
   358 lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
   359   finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
   360 apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
   361  apply auto
   362 done
   363 
   364 
   365 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
   366 by (simp add: Plus_def)
   367 
   368 text {* Sigma of finite sets *}
   369 
   370 lemma finite_SigmaI [simp]:
   371     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   372   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   373 
   374 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   375     finite (A <*> B)"
   376   by (rule finite_SigmaI)
   377 
   378 lemma finite_Prod_UNIV:
   379     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   380   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   381    apply (erule ssubst)
   382    apply (erule finite_SigmaI, auto)
   383   done
   384 
   385 lemma finite_cartesian_productD1:
   386      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
   387 apply (auto simp add: finite_conv_nat_seg_image) 
   388 apply (drule_tac x=n in spec) 
   389 apply (drule_tac x="fst o f" in spec) 
   390 apply (auto simp add: o_def) 
   391  prefer 2 apply (force dest!: equalityD2) 
   392 apply (drule equalityD1) 
   393 apply (rename_tac y x)
   394 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   395  prefer 2 apply force
   396 apply clarify
   397 apply (rule_tac x=k in image_eqI, auto)
   398 done
   399 
   400 lemma finite_cartesian_productD2:
   401      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
   402 apply (auto simp add: finite_conv_nat_seg_image) 
   403 apply (drule_tac x=n in spec) 
   404 apply (drule_tac x="snd o f" in spec) 
   405 apply (auto simp add: o_def) 
   406  prefer 2 apply (force dest!: equalityD2) 
   407 apply (drule equalityD1)
   408 apply (rename_tac x y)
   409 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   410  prefer 2 apply force
   411 apply clarify
   412 apply (rule_tac x=k in image_eqI, auto)
   413 done
   414 
   415 
   416 text {* The powerset of a finite set *}
   417 
   418 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   419 proof
   420   assume "finite (Pow A)"
   421   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   422   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   423 next
   424   assume "finite A"
   425   thus "finite (Pow A)"
   426     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   427 qed
   428 
   429 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
   430 by(simp add: Pow_def[symmetric])
   431 
   432 
   433 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   434 by(blast intro: finite_subset[OF subset_Pow_Union])
   435 
   436 
   437 subsection {* Class @{text finite}  *}
   438 
   439 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
   440 class finite =
   441   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
   442 setup {* Sign.parent_path *}
   443 hide const finite
   444 
   445 context finite
   446 begin
   447 
   448 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   449   by (rule subset_UNIV finite_UNIV finite_subset)+
   450 
   451 end
   452 
   453 lemma UNIV_unit [noatp]:
   454   "UNIV = {()}" by auto
   455 
   456 instance unit :: finite
   457   by default (simp add: UNIV_unit)
   458 
   459 lemma UNIV_bool [noatp]:
   460   "UNIV = {False, True}" by auto
   461 
   462 instance bool :: finite
   463   by default (simp add: UNIV_bool)
   464 
   465 instance * :: (finite, finite) finite
   466   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
   467 
   468 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   469   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   470 
   471 instance "fun" :: (finite, finite) finite
   472 proof
   473   show "finite (UNIV :: ('a => 'b) set)"
   474   proof (rule finite_imageD)
   475     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
   476     have "range ?graph \<subseteq> Pow UNIV" by simp
   477     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
   478       by (simp only: finite_Pow_iff finite)
   479     ultimately show "finite (range ?graph)"
   480       by (rule finite_subset)
   481     show "inj ?graph" by (rule inj_graph)
   482   qed
   483 qed
   484 
   485 instance "+" :: (finite, finite) finite
   486   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
   487 
   488 
   489 subsection {* A fold functional for finite sets *}
   490 
   491 text {* The intended behaviour is
   492 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
   493 if @{text f} is ``left-commutative'':
   494 *}
   495 
   496 locale fun_left_comm =
   497   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
   498   assumes fun_left_comm: "f x (f y z) = f y (f x z)"
   499 begin
   500 
   501 text{* On a functional level it looks much nicer: *}
   502 
   503 lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
   504 by (simp add: fun_left_comm expand_fun_eq)
   505 
   506 end
   507 
   508 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
   509 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where
   510   emptyI [intro]: "fold_graph f z {} z" |
   511   insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y
   512       \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
   513 
   514 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
   515 
   516 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
   517 [code del]: "fold f z A = (THE y. fold_graph f z A y)"
   518 
   519 text{*A tempting alternative for the definiens is
   520 @{term "if finite A then THE y. fold_graph f z A y else e"}.
   521 It allows the removal of finiteness assumptions from the theorems
   522 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
   523 The proofs become ugly. It is not worth the effort. (???) *}
   524 
   525 
   526 lemma Diff1_fold_graph:
   527   "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
   528 by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
   529 
   530 lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
   531 by (induct set: fold_graph) auto
   532 
   533 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
   534 by (induct set: finite) auto
   535 
   536 
   537 subsubsection{*From @{const fold_graph} to @{term fold}*}
   538 
   539 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   540   by (auto simp add: less_Suc_eq) 
   541 
   542 lemma insert_image_inj_on_eq:
   543      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
   544         inj_on h {i. i < Suc m}|] 
   545       ==> A = h ` {i. i < m}"
   546 apply (auto simp add: image_less_Suc inj_on_def)
   547 apply (blast intro: less_trans) 
   548 done
   549 
   550 lemma insert_inj_onE:
   551   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
   552       and inj_on: "inj_on h {i::nat. i<n}"
   553   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
   554 proof (cases n)
   555   case 0 thus ?thesis using aA by auto
   556 next
   557   case (Suc m)
   558   have nSuc: "n = Suc m" by fact
   559   have mlessn: "m<n" by (simp add: nSuc)
   560   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   561   let ?hm = "Fun.swap k m h"
   562   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
   563     by (simp add: inj_on_swap_iff inj_on)
   564   show ?thesis
   565   proof (intro exI conjI)
   566     show "inj_on ?hm {i. i < m}" using inj_hm
   567       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   568     show "m<n" by (rule mlessn)
   569     show "A = ?hm ` {i. i < m}" 
   570     proof (rule insert_image_inj_on_eq)
   571       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
   572       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   573       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   574 	using aA hkeq nSuc klessn
   575 	by (auto simp add: swap_def image_less_Suc fun_upd_image 
   576 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
   577     qed
   578   qed
   579 qed
   580 
   581 context fun_left_comm
   582 begin
   583 
   584 lemma fold_graph_determ_aux:
   585   "A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n}
   586    \<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x'
   587    \<Longrightarrow> x' = x"
   588 proof (induct n arbitrary: A x x' h rule: less_induct)
   589   case (less n)
   590   have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m}
   591       \<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x
   592       \<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact
   593   have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'"
   594     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
   595   show ?case
   596   proof (rule fold_graph.cases [OF Afoldx])
   597     assume "A = {}" and "x = z"
   598     with Afoldx' show "x' = x" by auto
   599   next
   600     fix B b u
   601     assume AbB: "A = insert b B" and x: "x = f b u"
   602       and notinB: "b \<notin> B" and Bu: "fold_graph f z B u"
   603     show "x'=x" 
   604     proof (rule fold_graph.cases [OF Afoldx'])
   605       assume "A = {}" and "x' = z"
   606       with AbB show "x' = x" by blast
   607     next
   608       fix C c v
   609       assume AcC: "A = insert c C" and x': "x' = f c v"
   610         and notinC: "c \<notin> C" and Cv: "fold_graph f z C v"
   611       from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   612       from insert_inj_onE [OF Beq notinB injh]
   613       obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   614         and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto 
   615       from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   616       from insert_inj_onE [OF Ceq notinC injh]
   617       obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   618         and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto 
   619       show "x'=x"
   620       proof cases
   621         assume "b=c"
   622 	then moreover have "B = C" using AbB AcC notinB notinC by auto
   623 	ultimately show ?thesis  using Bu Cv x x' IH [OF lessC Ceq inj_onC]
   624           by auto
   625       next
   626 	assume diff: "b \<noteq> c"
   627 	let ?D = "B - {c}"
   628 	have B: "B = insert c ?D" and C: "C = insert b ?D"
   629 	  using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   630 	have "finite A" by(rule fold_graph_imp_finite [OF Afoldx])
   631 	with AbB have "finite ?D" by simp
   632 	then obtain d where Dfoldd: "fold_graph f z ?D d"
   633 	  using finite_imp_fold_graph by iprover
   634 	moreover have cinB: "c \<in> B" using B by auto
   635 	ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph)
   636 	hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   637         moreover have "f b d = v"
   638 	proof (rule IH[OF lessC Ceq inj_onC Cv])
   639 	  show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp
   640 	qed
   641 	ultimately show ?thesis
   642           using fun_left_comm [of c b] x x' by (auto simp add: o_def)
   643       qed
   644     qed
   645   qed
   646 qed
   647 
   648 lemma fold_graph_determ:
   649   "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
   650 apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   651 apply (blast intro: fold_graph_determ_aux [rule_format])
   652 done
   653 
   654 lemma fold_equality:
   655   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
   656 by (unfold fold_def) (blast intro: fold_graph_determ)
   657 
   658 text{* The base case for @{text fold}: *}
   659 
   660 lemma (in -) fold_empty [simp]: "fold f z {} = z"
   661 by (unfold fold_def) blast
   662 
   663 text{* The various recursion equations for @{const fold}: *}
   664 
   665 lemma fold_insert_aux: "x \<notin> A
   666   \<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow>
   667       (\<exists>y. fold_graph f z A y \<and> v = f x y)"
   668 apply auto
   669 apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE])
   670  apply (fastsimp dest: fold_graph_imp_finite)
   671 apply (blast intro: fold_graph_determ)
   672 done
   673 
   674 lemma fold_insert [simp]:
   675   "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
   676 apply (simp add: fold_def fold_insert_aux)
   677 apply (rule the_equality)
   678  apply (auto intro: finite_imp_fold_graph
   679         cong add: conj_cong simp add: fold_def[symmetric] fold_equality)
   680 done
   681 
   682 lemma fold_fun_comm:
   683   "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
   684 proof (induct rule: finite_induct)
   685   case empty then show ?case by simp
   686 next
   687   case (insert y A) then show ?case
   688     by (simp add: fun_left_comm[of x])
   689 qed
   690 
   691 lemma fold_insert2:
   692   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
   693 by (simp add: fold_insert fold_fun_comm)
   694 
   695 lemma fold_rec:
   696 assumes "finite A" and "x \<in> A"
   697 shows "fold f z A = f x (fold f z (A - {x}))"
   698 proof -
   699   have A: "A = insert x (A - {x})" using `x \<in> A` by blast
   700   then have "fold f z A = fold f z (insert x (A - {x}))" by simp
   701   also have "\<dots> = f x (fold f z (A - {x}))"
   702     by (rule fold_insert) (simp add: `finite A`)+
   703   finally show ?thesis .
   704 qed
   705 
   706 lemma fold_insert_remove:
   707   assumes "finite A"
   708   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
   709 proof -
   710   from `finite A` have "finite (insert x A)" by auto
   711   moreover have "x \<in> insert x A" by auto
   712   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
   713     by (rule fold_rec)
   714   then show ?thesis by simp
   715 qed
   716 
   717 end
   718 
   719 text{* A simplified version for idempotent functions: *}
   720 
   721 locale fun_left_comm_idem = fun_left_comm +
   722   assumes fun_left_idem: "f x (f x z) = f x z"
   723 begin
   724 
   725 text{* The nice version: *}
   726 lemma fun_comp_idem : "f x o f x = f x"
   727 by (simp add: fun_left_idem expand_fun_eq)
   728 
   729 lemma fold_insert_idem:
   730   assumes fin: "finite A"
   731   shows "fold f z (insert x A) = f x (fold f z A)"
   732 proof cases
   733   assume "x \<in> A"
   734   then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert)
   735   then show ?thesis using assms by (simp add:fun_left_idem)
   736 next
   737   assume "x \<notin> A" then show ?thesis using assms by simp
   738 qed
   739 
   740 declare fold_insert[simp del] fold_insert_idem[simp]
   741 
   742 lemma fold_insert_idem2:
   743   "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
   744 by(simp add:fold_fun_comm)
   745 
   746 end
   747 
   748 subsubsection{* The derived combinator @{text fold_image} *}
   749 
   750 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
   751 where "fold_image f g = fold (%x y. f (g x) y)"
   752 
   753 lemma fold_image_empty[simp]: "fold_image f g z {} = z"
   754 by(simp add:fold_image_def)
   755 
   756 context ab_semigroup_mult
   757 begin
   758 
   759 lemma fold_image_insert[simp]:
   760 assumes "finite A" and "a \<notin> A"
   761 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
   762 proof -
   763   interpret I: fun_left_comm "%x y. (g x) * y"
   764     by unfold_locales (simp add: mult_ac)
   765   show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
   766 qed
   767 
   768 (*
   769 lemma fold_commute:
   770   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
   771   apply (induct set: finite)
   772    apply simp
   773   apply (simp add: mult_left_commute [of x])
   774   done
   775 
   776 lemma fold_nest_Un_Int:
   777   "finite A ==> finite B
   778     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
   779   apply (induct set: finite)
   780    apply simp
   781   apply (simp add: fold_commute Int_insert_left insert_absorb)
   782   done
   783 
   784 lemma fold_nest_Un_disjoint:
   785   "finite A ==> finite B ==> A Int B = {}
   786     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
   787   by (simp add: fold_nest_Un_Int)
   788 *)
   789 
   790 lemma fold_image_reindex:
   791 assumes fin: "finite A"
   792 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
   793 using fin apply induct
   794  apply simp
   795 apply simp
   796 done
   797 
   798 (*
   799 text{*
   800   Fusion theorem, as described in Graham Hutton's paper,
   801   A Tutorial on the Universality and Expressiveness of Fold,
   802   JFP 9:4 (355-372), 1999.
   803 *}
   804 
   805 lemma fold_fusion:
   806   assumes "ab_semigroup_mult g"
   807   assumes fin: "finite A"
   808     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   809   shows "h (fold g j w A) = fold times j (h w) A"
   810 proof -
   811   class_interpret ab_semigroup_mult [g] by fact
   812   show ?thesis using fin hyp by (induct set: finite) simp_all
   813 qed
   814 *)
   815 
   816 lemma fold_image_cong:
   817   "finite A \<Longrightarrow>
   818   (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
   819 apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C")
   820  apply simp
   821 apply (erule finite_induct, simp)
   822 apply (simp add: subset_insert_iff, clarify)
   823 apply (subgoal_tac "finite C")
   824  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   825 apply (subgoal_tac "C = insert x (C - {x})")
   826  prefer 2 apply blast
   827 apply (erule ssubst)
   828 apply (drule spec)
   829 apply (erule (1) notE impE)
   830 apply (simp add: Ball_def del: insert_Diff_single)
   831 done
   832 
   833 end
   834 
   835 context comm_monoid_mult
   836 begin
   837 
   838 lemma fold_image_Un_Int:
   839   "finite A ==> finite B ==>
   840     fold_image times g 1 A * fold_image times g 1 B =
   841     fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"
   842 by (induct set: finite) 
   843    (auto simp add: mult_ac insert_absorb Int_insert_left)
   844 
   845 corollary fold_Un_disjoint:
   846   "finite A ==> finite B ==> A Int B = {} ==>
   847    fold_image times g 1 (A Un B) =
   848    fold_image times g 1 A * fold_image times g 1 B"
   849 by (simp add: fold_image_Un_Int)
   850 
   851 lemma fold_image_UN_disjoint:
   852   "\<lbrakk> finite I; ALL i:I. finite (A i);
   853      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   854    \<Longrightarrow> fold_image times g 1 (UNION I A) =
   855        fold_image times (%i. fold_image times g 1 (A i)) 1 I"
   856 apply (induct set: finite, simp, atomize)
   857 apply (subgoal_tac "ALL i:F. x \<noteq> i")
   858  prefer 2 apply blast
   859 apply (subgoal_tac "A x Int UNION F A = {}")
   860  prefer 2 apply blast
   861 apply (simp add: fold_Un_disjoint)
   862 done
   863 
   864 lemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   865   fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A =
   866   fold_image times (split g) 1 (SIGMA x:A. B x)"
   867 apply (subst Sigma_def)
   868 apply (subst fold_image_UN_disjoint, assumption, simp)
   869  apply blast
   870 apply (erule fold_image_cong)
   871 apply (subst fold_image_UN_disjoint, simp, simp)
   872  apply blast
   873 apply simp
   874 done
   875 
   876 lemma fold_image_distrib: "finite A \<Longrightarrow>
   877    fold_image times (%x. g x * h x) 1 A =
   878    fold_image times g 1 A *  fold_image times h 1 A"
   879 by (erule finite_induct) (simp_all add: mult_ac)
   880 
   881 lemma fold_image_related: 
   882   assumes Re: "R e e" 
   883   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   884   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   885   shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"
   886   using fS by (rule finite_subset_induct) (insert assms, auto)
   887 
   888 lemma  fold_image_eq_general:
   889   assumes fS: "finite S"
   890   and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" 
   891   and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
   892   shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"
   893 proof-
   894   from h f12 have hS: "h ` S = S'" by auto
   895   {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
   896     from f12 h H  have "x = y" by auto }
   897   hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
   898   from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
   899   from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp
   900   also have "\<dots> = fold_image (op *) (f2 o h) e S" 
   901     using fold_image_reindex[OF fS hinj, of f2 e] .
   902   also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]
   903     by blast
   904   finally show ?thesis ..
   905 qed
   906 
   907 lemma fold_image_eq_general_inverses:
   908   assumes fS: "finite S" 
   909   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   910   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
   911   shows "fold_image (op *) f e S = fold_image (op *) g e T"
   912   (* metis solves it, but not yet available here *)
   913   apply (rule fold_image_eq_general[OF fS, of T h g f e])
   914   apply (rule ballI)
   915   apply (frule kh)
   916   apply (rule ex1I[])
   917   apply blast
   918   apply clarsimp
   919   apply (drule hk) apply simp
   920   apply (rule sym)
   921   apply (erule conjunct1[OF conjunct2[OF hk]])
   922   apply (rule ballI)
   923   apply (drule  hk)
   924   apply blast
   925   done
   926 
   927 end
   928 
   929 subsection {* Generalized summation over a set *}
   930 
   931 interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
   932   proof qed (auto intro: add_assoc add_commute)
   933 
   934 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   935 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
   936 
   937 abbreviation
   938   Setsum  ("\<Sum>_" [1000] 999) where
   939   "\<Sum>A == setsum (%x. x) A"
   940 
   941 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   942 written @{text"\<Sum>x\<in>A. e"}. *}
   943 
   944 syntax
   945   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   946 syntax (xsymbols)
   947   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   948 syntax (HTML output)
   949   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   950 
   951 translations -- {* Beware of argument permutation! *}
   952   "SUM i:A. b" == "CONST setsum (%i. b) A"
   953   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   954 
   955 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   956  @{text"\<Sum>x|P. e"}. *}
   957 
   958 syntax
   959   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   960 syntax (xsymbols)
   961   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   962 syntax (HTML output)
   963   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   964 
   965 translations
   966   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   967   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   968 
   969 print_translation {*
   970 let
   971   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   972     if x<>y then raise Match
   973     else let val x' = Syntax.mark_bound x
   974              val t' = subst_bound(x',t)
   975              val P' = subst_bound(x',P)
   976          in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   977 in [("setsum", setsum_tr')] end
   978 *}
   979 
   980 
   981 lemma setsum_empty [simp]: "setsum f {} = 0"
   982 by (simp add: setsum_def)
   983 
   984 lemma setsum_insert [simp]:
   985   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   986 by (simp add: setsum_def)
   987 
   988 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   989 by (simp add: setsum_def)
   990 
   991 lemma setsum_reindex:
   992      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   993 by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
   994 
   995 lemma setsum_reindex_id:
   996      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   997 by (auto simp add: setsum_reindex)
   998 
   999 lemma setsum_reindex_nonzero: 
  1000   assumes fS: "finite S"
  1001   and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
  1002   shows "setsum h (f ` S) = setsum (h o f) S"
  1003 using nz
  1004 proof(induct rule: finite_induct[OF fS])
  1005   case 1 thus ?case by simp
  1006 next
  1007   case (2 x F) 
  1008   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
  1009     then obtain y where y: "y \<in> F" "f x = f y" by auto 
  1010     from "2.hyps" y have xy: "x \<noteq> y" by auto
  1011     
  1012     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
  1013     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
  1014     also have "\<dots> = setsum (h o f) (insert x F)" 
  1015       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
  1016       using h0 
  1017       apply simp
  1018       apply (rule "2.hyps"(3))
  1019       apply (rule_tac y="y" in  "2.prems")
  1020       apply simp_all
  1021       done
  1022     finally have ?case .}
  1023   moreover
  1024   {assume fxF: "f x \<notin> f ` F"
  1025     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
  1026       using fxF "2.hyps" by simp 
  1027     also have "\<dots> = setsum (h o f) (insert x F)"
  1028       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
  1029       apply simp
  1030       apply (rule cong[OF refl[of "op + (h (f x))"]])
  1031       apply (rule "2.hyps"(3))
  1032       apply (rule_tac y="y" in  "2.prems")
  1033       apply simp_all
  1034       done
  1035     finally have ?case .}
  1036   ultimately show ?case by blast
  1037 qed
  1038 
  1039 lemma setsum_cong:
  1040   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
  1041 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
  1042 
  1043 lemma strong_setsum_cong[cong]:
  1044   "A = B ==> (!!x. x:B =simp=> f x = g x)
  1045    ==> setsum (%x. f x) A = setsum (%x. g x) B"
  1046 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
  1047 
  1048 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
  1049 by (rule setsum_cong[OF refl], auto);
  1050 
  1051 lemma setsum_reindex_cong:
  1052    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
  1053     ==> setsum h B = setsum g A"
  1054 by (simp add: setsum_reindex cong: setsum_cong)
  1055 
  1056 
  1057 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
  1058 apply (clarsimp simp: setsum_def)
  1059 apply (erule finite_induct, auto)
  1060 done
  1061 
  1062 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
  1063 by(simp add:setsum_cong)
  1064 
  1065 lemma setsum_Un_Int: "finite A ==> finite B ==>
  1066   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
  1067   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
  1068 by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
  1069 
  1070 lemma setsum_Un_disjoint: "finite A ==> finite B
  1071   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
  1072 by (subst setsum_Un_Int [symmetric], auto)
  1073 
  1074 lemma setsum_mono_zero_left: 
  1075   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1076   and z: "\<forall>i \<in> T - S. f i = 0"
  1077   shows "setsum f S = setsum f T"
  1078 proof-
  1079   have eq: "T = S \<union> (T - S)" using ST by blast
  1080   have d: "S \<inter> (T - S) = {}" using ST by blast
  1081   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1082   show ?thesis 
  1083   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
  1084 qed
  1085 
  1086 lemma setsum_mono_zero_right: 
  1087   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
  1088 by(blast intro!: setsum_mono_zero_left[symmetric])
  1089 
  1090 lemma setsum_mono_zero_cong_left: 
  1091   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1092   and z: "\<forall>i \<in> T - S. g i = 0"
  1093   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  1094   shows "setsum f S = setsum g T"
  1095 proof-
  1096   have eq: "T = S \<union> (T - S)" using ST by blast
  1097   have d: "S \<inter> (T - S) = {}" using ST by blast
  1098   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1099   show ?thesis 
  1100     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
  1101 qed
  1102 
  1103 lemma setsum_mono_zero_cong_right: 
  1104   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1105   and z: "\<forall>i \<in> T - S. f i = 0"
  1106   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  1107   shows "setsum f T = setsum g S"
  1108 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
  1109 
  1110 lemma setsum_delta: 
  1111   assumes fS: "finite S"
  1112   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
  1113 proof-
  1114   let ?f = "(\<lambda>k. if k=a then b k else 0)"
  1115   {assume a: "a \<notin> S"
  1116     hence "\<forall> k\<in> S. ?f k = 0" by simp
  1117     hence ?thesis  using a by simp}
  1118   moreover 
  1119   {assume a: "a \<in> S"
  1120     let ?A = "S - {a}"
  1121     let ?B = "{a}"
  1122     have eq: "S = ?A \<union> ?B" using a by blast 
  1123     have dj: "?A \<inter> ?B = {}" by simp
  1124     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1125     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
  1126       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1127       by simp
  1128     then have ?thesis  using a by simp}
  1129   ultimately show ?thesis by blast
  1130 qed
  1131 lemma setsum_delta': 
  1132   assumes fS: "finite S" shows 
  1133   "setsum (\<lambda>k. if a = k then b k else 0) S = 
  1134      (if a\<in> S then b a else 0)"
  1135   using setsum_delta[OF fS, of a b, symmetric] 
  1136   by (auto intro: setsum_cong)
  1137 
  1138 lemma setsum_restrict_set:
  1139   assumes fA: "finite A"
  1140   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
  1141 proof-
  1142   from fA have fab: "finite (A \<inter> B)" by auto
  1143   have aba: "A \<inter> B \<subseteq> A" by blast
  1144   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
  1145   from setsum_mono_zero_left[OF fA aba, of ?g]
  1146   show ?thesis by simp
  1147 qed
  1148 
  1149 lemma setsum_cases:
  1150   assumes fA: "finite A"
  1151   shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
  1152          setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
  1153 proof-
  1154   have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}" 
  1155     by blast+
  1156   from fA 
  1157   have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
  1158   let ?g = "\<lambda>x. if x \<in> B then f x else g x"
  1159   from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
  1160   show ?thesis by simp
  1161 qed
  1162 
  1163 
  1164 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
  1165   the lhs need not be, since UNION I A could still be finite.*)
  1166 lemma setsum_UN_disjoint:
  1167     "finite I ==> (ALL i:I. finite (A i)) ==>
  1168         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1169       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
  1170 by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
  1171 
  1172 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
  1173 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
  1174 lemma setsum_Union_disjoint:
  1175   "[| (ALL A:C. finite A);
  1176       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
  1177    ==> setsum f (Union C) = setsum (setsum f) C"
  1178 apply (cases "finite C") 
  1179  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
  1180   apply (frule setsum_UN_disjoint [of C id f])
  1181  apply (unfold Union_def id_def, assumption+)
  1182 done
  1183 
  1184 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
  1185   the rhs need not be, since SIGMA A B could still be finite.*)
  1186 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1187     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1188 by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
  1189 
  1190 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1191 lemma setsum_cartesian_product: 
  1192    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
  1193 apply (cases "finite A") 
  1194  apply (cases "finite B") 
  1195   apply (simp add: setsum_Sigma)
  1196  apply (cases "A={}", simp)
  1197  apply (simp) 
  1198 apply (auto simp add: setsum_def
  1199             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1200 done
  1201 
  1202 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
  1203 by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
  1204 
  1205 
  1206 subsubsection {* Properties in more restricted classes of structures *}
  1207 
  1208 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
  1209 apply (case_tac "finite A")
  1210  prefer 2 apply (simp add: setsum_def)
  1211 apply (erule rev_mp)
  1212 apply (erule finite_induct, auto)
  1213 done
  1214 
  1215 lemma setsum_eq_0_iff [simp]:
  1216     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
  1217 by (induct set: finite) auto
  1218 
  1219 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
  1220   (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
  1221 apply(erule finite_induct)
  1222 apply (auto simp add:add_is_1)
  1223 done
  1224 
  1225 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
  1226 
  1227 lemma setsum_Un_nat: "finite A ==> finite B ==>
  1228   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
  1229   -- {* For the natural numbers, we have subtraction. *}
  1230 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
  1231 
  1232 lemma setsum_Un: "finite A ==> finite B ==>
  1233   (setsum f (A Un B) :: 'a :: ab_group_add) =
  1234    setsum f A + setsum f B - setsum f (A Int B)"
  1235 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
  1236 
  1237 lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
  1238   apply (induct set: finite)
  1239   apply simp by (auto simp add: fold_image_insert)
  1240 
  1241 lemma (in comm_monoid_mult) fold_image_Un_one:
  1242   assumes fS: "finite S" and fT: "finite T"
  1243   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
  1244   shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
  1245 proof-
  1246   have "fold_image op * f 1 (S \<inter> T) = 1" 
  1247     apply (rule fold_image_1)
  1248     using fS fT I0 by auto 
  1249   with fold_image_Un_Int[OF fS fT] show ?thesis by simp
  1250 qed
  1251 
  1252 lemma setsum_eq_general_reverses:
  1253   assumes fS: "finite S" and fT: "finite T"
  1254   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
  1255   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
  1256   shows "setsum f S = setsum g T"
  1257   apply (simp add: setsum_def fS fT)
  1258   apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
  1259   apply (erule kh)
  1260   apply (erule hk)
  1261   done
  1262 
  1263 
  1264 
  1265 lemma setsum_Un_zero:  
  1266   assumes fS: "finite S" and fT: "finite T"
  1267   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
  1268   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
  1269   using fS fT
  1270   apply (simp add: setsum_def)
  1271   apply (rule comm_monoid_add.fold_image_Un_one)
  1272   using I0 by auto
  1273 
  1274 
  1275 lemma setsum_UNION_zero: 
  1276   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
  1277   and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
  1278   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
  1279   using fSS f0
  1280 proof(induct rule: finite_induct[OF fS])
  1281   case 1 thus ?case by simp
  1282 next
  1283   case (2 T F)
  1284   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
  1285     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
  1286   from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
  1287   from "2.prems" TF fTF
  1288   show ?case 
  1289     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
  1290 qed
  1291 
  1292 
  1293 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
  1294   (if a:A then setsum f A - f a else setsum f A)"
  1295 apply (case_tac "finite A")
  1296  prefer 2 apply (simp add: setsum_def)
  1297 apply (erule finite_induct)
  1298  apply (auto simp add: insert_Diff_if)
  1299 apply (drule_tac a = a in mk_disjoint_insert, auto)
  1300 done
  1301 
  1302 lemma setsum_diff1: "finite A \<Longrightarrow>
  1303   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1304   (if a:A then setsum f A - f a else setsum f A)"
  1305 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1306 
  1307 lemma setsum_diff1'[rule_format]:
  1308   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
  1309 apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
  1310 apply (auto simp add: insert_Diff_if add_ac)
  1311 done
  1312 
  1313 (* By Jeremy Siek: *)
  1314 
  1315 lemma setsum_diff_nat: 
  1316 assumes "finite B" and "B \<subseteq> A"
  1317 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1318 using assms
  1319 proof induct
  1320   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1321 next
  1322   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1323     and xFinA: "insert x F \<subseteq> A"
  1324     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1325   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1326   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1327     by (simp add: setsum_diff1_nat)
  1328   from xFinA have "F \<subseteq> A" by simp
  1329   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1330   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1331     by simp
  1332   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1333   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1334     by simp
  1335   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1336   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1337     by simp
  1338   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1339 qed
  1340 
  1341 lemma setsum_diff:
  1342   assumes le: "finite A" "B \<subseteq> A"
  1343   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1344 proof -
  1345   from le have finiteB: "finite B" using finite_subset by auto
  1346   show ?thesis using finiteB le
  1347   proof induct
  1348     case empty
  1349     thus ?case by auto
  1350   next
  1351     case (insert x F)
  1352     thus ?case using le finiteB 
  1353       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1354   qed
  1355 qed
  1356 
  1357 lemma setsum_mono:
  1358   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1359   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1360 proof (cases "finite K")
  1361   case True
  1362   thus ?thesis using le
  1363   proof induct
  1364     case empty
  1365     thus ?case by simp
  1366   next
  1367     case insert
  1368     thus ?case using add_mono by fastsimp
  1369   qed
  1370 next
  1371   case False
  1372   thus ?thesis
  1373     by (simp add: setsum_def)
  1374 qed
  1375 
  1376 lemma setsum_strict_mono:
  1377   fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1378   assumes "finite A"  "A \<noteq> {}"
  1379     and "!!x. x:A \<Longrightarrow> f x < g x"
  1380   shows "setsum f A < setsum g A"
  1381   using prems
  1382 proof (induct rule: finite_ne_induct)
  1383   case singleton thus ?case by simp
  1384 next
  1385   case insert thus ?case by (auto simp: add_strict_mono)
  1386 qed
  1387 
  1388 lemma setsum_negf:
  1389   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1390 proof (cases "finite A")
  1391   case True thus ?thesis by (induct set: finite) auto
  1392 next
  1393   case False thus ?thesis by (simp add: setsum_def)
  1394 qed
  1395 
  1396 lemma setsum_subtractf:
  1397   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1398     setsum f A - setsum g A"
  1399 proof (cases "finite A")
  1400   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1401 next
  1402   case False thus ?thesis by (simp add: setsum_def)
  1403 qed
  1404 
  1405 lemma setsum_nonneg:
  1406   assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1407   shows "0 \<le> setsum f A"
  1408 proof (cases "finite A")
  1409   case True thus ?thesis using nn
  1410   proof induct
  1411     case empty then show ?case by simp
  1412   next
  1413     case (insert x F)
  1414     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
  1415     with insert show ?case by simp
  1416   qed
  1417 next
  1418   case False thus ?thesis by (simp add: setsum_def)
  1419 qed
  1420 
  1421 lemma setsum_nonpos:
  1422   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
  1423   shows "setsum f A \<le> 0"
  1424 proof (cases "finite A")
  1425   case True thus ?thesis using np
  1426   proof induct
  1427     case empty then show ?case by simp
  1428   next
  1429     case (insert x F)
  1430     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
  1431     with insert show ?case by simp
  1432   qed
  1433 next
  1434   case False thus ?thesis by (simp add: setsum_def)
  1435 qed
  1436 
  1437 lemma setsum_mono2:
  1438 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1439 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1440 shows "setsum f A \<le> setsum f B"
  1441 proof -
  1442   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1443     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1444   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1445     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1446   also have "A \<union> (B-A) = B" using sub by blast
  1447   finally show ?thesis .
  1448 qed
  1449 
  1450 lemma setsum_mono3: "finite B ==> A <= B ==> 
  1451     ALL x: B - A. 
  1452       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
  1453         setsum f A <= setsum f B"
  1454   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
  1455   apply (erule ssubst)
  1456   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
  1457   apply simp
  1458   apply (rule add_left_mono)
  1459   apply (erule setsum_nonneg)
  1460   apply (subst setsum_Un_disjoint [THEN sym])
  1461   apply (erule finite_subset, assumption)
  1462   apply (rule finite_subset)
  1463   prefer 2
  1464   apply assumption
  1465   apply auto
  1466   apply (rule setsum_cong)
  1467   apply auto
  1468 done
  1469 
  1470 lemma setsum_right_distrib: 
  1471   fixes f :: "'a => ('b::semiring_0)"
  1472   shows "r * setsum f A = setsum (%n. r * f n) A"
  1473 proof (cases "finite A")
  1474   case True
  1475   thus ?thesis
  1476   proof induct
  1477     case empty thus ?case by simp
  1478   next
  1479     case (insert x A) thus ?case by (simp add: right_distrib)
  1480   qed
  1481 next
  1482   case False thus ?thesis by (simp add: setsum_def)
  1483 qed
  1484 
  1485 lemma setsum_left_distrib:
  1486   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
  1487 proof (cases "finite A")
  1488   case True
  1489   then show ?thesis
  1490   proof induct
  1491     case empty thus ?case by simp
  1492   next
  1493     case (insert x A) thus ?case by (simp add: left_distrib)
  1494   qed
  1495 next
  1496   case False thus ?thesis by (simp add: setsum_def)
  1497 qed
  1498 
  1499 lemma setsum_divide_distrib:
  1500   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
  1501 proof (cases "finite A")
  1502   case True
  1503   then show ?thesis
  1504   proof induct
  1505     case empty thus ?case by simp
  1506   next
  1507     case (insert x A) thus ?case by (simp add: add_divide_distrib)
  1508   qed
  1509 next
  1510   case False thus ?thesis by (simp add: setsum_def)
  1511 qed
  1512 
  1513 lemma setsum_abs[iff]: 
  1514   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1515   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1516 proof (cases "finite A")
  1517   case True
  1518   thus ?thesis
  1519   proof induct
  1520     case empty thus ?case by simp
  1521   next
  1522     case (insert x A)
  1523     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1524   qed
  1525 next
  1526   case False thus ?thesis by (simp add: setsum_def)
  1527 qed
  1528 
  1529 lemma setsum_abs_ge_zero[iff]: 
  1530   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1531   shows "0 \<le> setsum (%i. abs(f i)) A"
  1532 proof (cases "finite A")
  1533   case True
  1534   thus ?thesis
  1535   proof induct
  1536     case empty thus ?case by simp
  1537   next
  1538     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
  1539   qed
  1540 next
  1541   case False thus ?thesis by (simp add: setsum_def)
  1542 qed
  1543 
  1544 lemma abs_setsum_abs[simp]: 
  1545   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1546   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1547 proof (cases "finite A")
  1548   case True
  1549   thus ?thesis
  1550   proof induct
  1551     case empty thus ?case by simp
  1552   next
  1553     case (insert a A)
  1554     hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
  1555     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1556     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
  1557       by (simp del: abs_of_nonneg)
  1558     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1559     finally show ?case .
  1560   qed
  1561 next
  1562   case False thus ?thesis by (simp add: setsum_def)
  1563 qed
  1564 
  1565 
  1566 text {* Commuting outer and inner summation *}
  1567 
  1568 lemma swap_inj_on:
  1569   "inj_on (%(i, j). (j, i)) (A \<times> B)"
  1570   by (unfold inj_on_def) fast
  1571 
  1572 lemma swap_product:
  1573   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
  1574   by (simp add: split_def image_def) blast
  1575 
  1576 lemma setsum_commute:
  1577   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
  1578 proof (simp add: setsum_cartesian_product)
  1579   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
  1580     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
  1581     (is "?s = _")
  1582     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
  1583     apply (simp add: split_def)
  1584     done
  1585   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
  1586     (is "_ = ?t")
  1587     apply (simp add: swap_product)
  1588     done
  1589   finally show "?s = ?t" .
  1590 qed
  1591 
  1592 lemma setsum_product:
  1593   fixes f :: "'a => ('b::semiring_0)"
  1594   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
  1595   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
  1596 
  1597 
  1598 subsection {* Generalized product over a set *}
  1599 
  1600 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1601 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
  1602 
  1603 abbreviation
  1604   Setprod  ("\<Prod>_" [1000] 999) where
  1605   "\<Prod>A == setprod (%x. x) A"
  1606 
  1607 syntax
  1608   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1609 syntax (xsymbols)
  1610   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1611 syntax (HTML output)
  1612   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1613 
  1614 translations -- {* Beware of argument permutation! *}
  1615   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1616   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1617 
  1618 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1619  @{text"\<Prod>x|P. e"}. *}
  1620 
  1621 syntax
  1622   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1623 syntax (xsymbols)
  1624   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1625 syntax (HTML output)
  1626   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1627 
  1628 translations
  1629   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1630   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1631 
  1632 
  1633 lemma setprod_empty [simp]: "setprod f {} = 1"
  1634 by (auto simp add: setprod_def)
  1635 
  1636 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1637     setprod f (insert a A) = f a * setprod f A"
  1638 by (simp add: setprod_def)
  1639 
  1640 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1641 by (simp add: setprod_def)
  1642 
  1643 lemma setprod_reindex:
  1644    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1645 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
  1646 
  1647 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1648 by (auto simp add: setprod_reindex)
  1649 
  1650 lemma setprod_cong:
  1651   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1652 by(fastsimp simp: setprod_def intro: fold_image_cong)
  1653 
  1654 lemma strong_setprod_cong[cong]:
  1655   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1656 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
  1657 
  1658 lemma setprod_reindex_cong: "inj_on f A ==>
  1659     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1660 by (frule setprod_reindex, simp)
  1661 
  1662 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
  1663   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  1664   shows "setprod h B = setprod g A"
  1665 proof-
  1666     have "setprod h B = setprod (h o f) A"
  1667       by (simp add: B setprod_reindex[OF i, of h])
  1668     then show ?thesis apply simp
  1669       apply (rule setprod_cong)
  1670       apply simp
  1671       by (simp add: eq)
  1672 qed
  1673 
  1674 lemma setprod_Un_one:  
  1675   assumes fS: "finite S" and fT: "finite T"
  1676   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
  1677   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
  1678   using fS fT
  1679   apply (simp add: setprod_def)
  1680   apply (rule fold_image_Un_one)
  1681   using I0 by auto
  1682 
  1683 
  1684 lemma setprod_1: "setprod (%i. 1) A = 1"
  1685 apply (case_tac "finite A")
  1686 apply (erule finite_induct, auto simp add: mult_ac)
  1687 done
  1688 
  1689 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1690 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1691 apply (erule ssubst, rule setprod_1)
  1692 apply (rule setprod_cong, auto)
  1693 done
  1694 
  1695 lemma setprod_Un_Int: "finite A ==> finite B
  1696     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1697 by(simp add: setprod_def fold_image_Un_Int[symmetric])
  1698 
  1699 lemma setprod_Un_disjoint: "finite A ==> finite B
  1700   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1701 by (subst setprod_Un_Int [symmetric], auto)
  1702 
  1703 lemma setprod_mono_one_left: 
  1704   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1705   and z: "\<forall>i \<in> T - S. f i = 1"
  1706   shows "setprod f S = setprod f T"
  1707 proof-
  1708   have eq: "T = S \<union> (T - S)" using ST by blast
  1709   have d: "S \<inter> (T - S) = {}" using ST by blast
  1710   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1711   show ?thesis
  1712   by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
  1713 qed
  1714 
  1715 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
  1716 
  1717 lemma setprod_delta: 
  1718   assumes fS: "finite S"
  1719   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  1720 proof-
  1721   let ?f = "(\<lambda>k. if k=a then b k else 1)"
  1722   {assume a: "a \<notin> S"
  1723     hence "\<forall> k\<in> S. ?f k = 1" by simp
  1724     hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
  1725   moreover 
  1726   {assume a: "a \<in> S"
  1727     let ?A = "S - {a}"
  1728     let ?B = "{a}"
  1729     have eq: "S = ?A \<union> ?B" using a by blast 
  1730     have dj: "?A \<inter> ?B = {}" by simp
  1731     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1732     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
  1733     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1734       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1735       by simp
  1736     then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
  1737   ultimately show ?thesis by blast
  1738 qed
  1739 
  1740 lemma setprod_delta': 
  1741   assumes fS: "finite S" shows 
  1742   "setprod (\<lambda>k. if a = k then b k else 1) S = 
  1743      (if a\<in> S then b a else 1)"
  1744   using setprod_delta[OF fS, of a b, symmetric] 
  1745   by (auto intro: setprod_cong)
  1746 
  1747 
  1748 lemma setprod_UN_disjoint:
  1749     "finite I ==> (ALL i:I. finite (A i)) ==>
  1750         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1751       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1752 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
  1753 
  1754 lemma setprod_Union_disjoint:
  1755   "[| (ALL A:C. finite A);
  1756       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1757    ==> setprod f (Union C) = setprod (setprod f) C"
  1758 apply (cases "finite C") 
  1759  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1760   apply (frule setprod_UN_disjoint [of C id f])
  1761  apply (unfold Union_def id_def, assumption+)
  1762 done
  1763 
  1764 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1765     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1766     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1767 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
  1768 
  1769 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1770 lemma setprod_cartesian_product: 
  1771      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1772 apply (cases "finite A") 
  1773  apply (cases "finite B") 
  1774   apply (simp add: setprod_Sigma)
  1775  apply (cases "A={}", simp)
  1776  apply (simp add: setprod_1) 
  1777 apply (auto simp add: setprod_def
  1778             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1779 done
  1780 
  1781 lemma setprod_timesf:
  1782      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1783 by(simp add:setprod_def fold_image_distrib)
  1784 
  1785 
  1786 subsubsection {* Properties in more restricted classes of structures *}
  1787 
  1788 lemma setprod_eq_1_iff [simp]:
  1789   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1790 by (induct set: finite) auto
  1791 
  1792 lemma setprod_zero:
  1793      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1794 apply (induct set: finite, force, clarsimp)
  1795 apply (erule disjE, auto)
  1796 done
  1797 
  1798 lemma setprod_nonneg [rule_format]:
  1799    "(ALL x: A. (0::'a::ordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1800 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  1801 
  1802 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_semidom) < f x)
  1803   --> 0 < setprod f A"
  1804 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  1805 
  1806 lemma setprod_zero_iff[simp]: "finite A ==> 
  1807   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1808   (EX x: A. f x = 0)"
  1809 by (erule finite_induct, auto simp:no_zero_divisors)
  1810 
  1811 lemma setprod_pos_nat:
  1812   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1813 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1814 
  1815 lemma setprod_pos_nat_iff[simp]:
  1816   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1817 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1818 
  1819 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1820   (setprod f (A Un B) :: 'a ::{field})
  1821    = setprod f A * setprod f B / setprod f (A Int B)"
  1822 by (subst setprod_Un_Int [symmetric], auto)
  1823 
  1824 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1825   (setprod f (A - {a}) :: 'a :: {field}) =
  1826   (if a:A then setprod f A / f a else setprod f A)"
  1827 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1828 
  1829 lemma setprod_inversef: "finite A ==>
  1830   ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1831   setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1832 by (erule finite_induct) auto
  1833 
  1834 lemma setprod_dividef:
  1835    "[|finite A;
  1836       \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1837     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1838 apply (subgoal_tac
  1839          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1840 apply (erule ssubst)
  1841 apply (subst divide_inverse)
  1842 apply (subst setprod_timesf)
  1843 apply (subst setprod_inversef, assumption+, rule refl)
  1844 apply (rule setprod_cong, rule refl)
  1845 apply (subst divide_inverse, auto)
  1846 done
  1847 
  1848 lemma setprod_dvd_setprod [rule_format]: 
  1849     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1850   apply (cases "finite A")
  1851   apply (induct set: finite)
  1852   apply (auto simp add: dvd_def)
  1853   apply (rule_tac x = "k * ka" in exI)
  1854   apply (simp add: algebra_simps)
  1855 done
  1856 
  1857 lemma setprod_dvd_setprod_subset:
  1858   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1859   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1860   apply (unfold dvd_def, blast)
  1861   apply (subst setprod_Un_disjoint [symmetric])
  1862   apply (auto elim: finite_subset intro: setprod_cong)
  1863 done
  1864 
  1865 lemma setprod_dvd_setprod_subset2:
  1866   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1867       setprod f A dvd setprod g B"
  1868   apply (rule dvd_trans)
  1869   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1870   apply (erule (1) setprod_dvd_setprod_subset)
  1871 done
  1872 
  1873 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1874     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1875 by (induct set: finite) (auto intro: dvd_mult)
  1876 
  1877 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1878     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1879   apply (cases "finite A")
  1880   apply (induct set: finite)
  1881   apply auto
  1882 done
  1883 
  1884 
  1885 subsection {* Finite cardinality *}
  1886 
  1887 text {* This definition, although traditional, is ugly to work with:
  1888 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1889 But now that we have @{text setsum} things are easy:
  1890 *}
  1891 
  1892 definition card :: "'a set \<Rightarrow> nat"
  1893 where "card A = setsum (\<lambda>x. 1) A"
  1894 
  1895 lemma card_empty [simp]: "card {} = 0"
  1896 by (simp add: card_def)
  1897 
  1898 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1899 by (simp add: card_def)
  1900 
  1901 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1902 by (simp add: card_def)
  1903 
  1904 lemma card_insert_disjoint [simp]:
  1905   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1906 by(simp add: card_def)
  1907 
  1908 lemma card_insert_if:
  1909   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1910 by (simp add: insert_absorb)
  1911 
  1912 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
  1913 apply auto
  1914 apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1915 done
  1916 
  1917 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1918 by auto
  1919 
  1920 
  1921 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1922 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1923 apply(simp del:insert_Diff_single)
  1924 done
  1925 
  1926 lemma card_Diff_singleton:
  1927   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1928 by (simp add: card_Suc_Diff1 [symmetric])
  1929 
  1930 lemma card_Diff_singleton_if:
  1931   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1932 by (simp add: card_Diff_singleton)
  1933 
  1934 lemma card_Diff_insert[simp]:
  1935 assumes "finite A" and "a:A" and "a ~: B"
  1936 shows "card(A - insert a B) = card(A - B) - 1"
  1937 proof -
  1938   have "A - insert a B = (A - B) - {a}" using assms by blast
  1939   then show ?thesis using assms by(simp add:card_Diff_singleton)
  1940 qed
  1941 
  1942 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1943 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
  1944 
  1945 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1946 by (simp add: card_insert_if)
  1947 
  1948 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1949 by (simp add: card_def setsum_mono2)
  1950 
  1951 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1952 apply (induct set: finite, simp, clarify)
  1953 apply (subgoal_tac "finite A & A - {x} <= F")
  1954  prefer 2 apply (blast intro: finite_subset, atomize)
  1955 apply (drule_tac x = "A - {x}" in spec)
  1956 apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1957 apply (case_tac "card A", auto)
  1958 done
  1959 
  1960 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1961 apply (simp add: psubset_eq linorder_not_le [symmetric])
  1962 apply (blast dest: card_seteq)
  1963 done
  1964 
  1965 lemma card_Un_Int: "finite A ==> finite B
  1966     ==> card A + card B = card (A Un B) + card (A Int B)"
  1967 by(simp add:card_def setsum_Un_Int)
  1968 
  1969 lemma card_Un_disjoint: "finite A ==> finite B
  1970     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1971 by (simp add: card_Un_Int)
  1972 
  1973 lemma card_Diff_subset:
  1974   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1975 by(simp add:card_def setsum_diff_nat)
  1976 
  1977 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1978 apply (rule Suc_less_SucD)
  1979 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
  1980 done
  1981 
  1982 lemma card_Diff2_less:
  1983   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1984 apply (case_tac "x = y")
  1985  apply (simp add: card_Diff1_less del:card_Diff_insert)
  1986 apply (rule less_trans)
  1987  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
  1988 done
  1989 
  1990 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1991 apply (case_tac "x : A")
  1992  apply (simp_all add: card_Diff1_less less_imp_le)
  1993 done
  1994 
  1995 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1996 by (erule psubsetI, blast)
  1997 
  1998 lemma insert_partition:
  1999   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  2000   \<Longrightarrow> x \<inter> \<Union> F = {}"
  2001 by auto
  2002 
  2003 text{* main cardinality theorem *}
  2004 lemma card_partition [rule_format]:
  2005   "finite C ==>
  2006      finite (\<Union> C) -->
  2007      (\<forall>c\<in>C. card c = k) -->
  2008      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
  2009      k * card(C) = card (\<Union> C)"
  2010 apply (erule finite_induct, simp)
  2011 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  2012        finite_subset [of _ "\<Union> (insert x F)"])
  2013 done
  2014 
  2015 
  2016 text{*The form of a finite set of given cardinality*}
  2017 
  2018 lemma card_eq_SucD:
  2019 assumes "card A = Suc k"
  2020 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
  2021 proof -
  2022   have fin: "finite A" using assms by (auto intro: ccontr)
  2023   moreover have "card A \<noteq> 0" using assms by auto
  2024   ultimately obtain b where b: "b \<in> A" by auto
  2025   show ?thesis
  2026   proof (intro exI conjI)
  2027     show "A = insert b (A-{b})" using b by blast
  2028     show "b \<notin> A - {b}" by blast
  2029     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
  2030       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
  2031   qed
  2032 qed
  2033 
  2034 lemma card_Suc_eq:
  2035   "(card A = Suc k) =
  2036    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
  2037 apply(rule iffI)
  2038  apply(erule card_eq_SucD)
  2039 apply(auto)
  2040 apply(subst card_insert)
  2041  apply(auto intro:ccontr)
  2042 done
  2043 
  2044 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  2045 apply (cases "finite A")
  2046 apply (erule finite_induct)
  2047 apply (auto simp add: algebra_simps)
  2048 done
  2049 
  2050 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
  2051 apply (erule finite_induct)
  2052 apply (auto simp add: power_Suc)
  2053 done
  2054 
  2055 lemma setprod_gen_delta:
  2056   assumes fS: "finite S"
  2057   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)"
  2058 proof-
  2059   let ?f = "(\<lambda>k. if k=a then b k else c)"
  2060   {assume a: "a \<notin> S"
  2061     hence "\<forall> k\<in> S. ?f k = c" by simp
  2062     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
  2063   moreover 
  2064   {assume a: "a \<in> S"
  2065     let ?A = "S - {a}"
  2066     let ?B = "{a}"
  2067     have eq: "S = ?A \<union> ?B" using a by blast 
  2068     have dj: "?A \<inter> ?B = {}" by simp
  2069     from fS have fAB: "finite ?A" "finite ?B" by auto  
  2070     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  2071       apply (rule setprod_cong) by auto
  2072     have cA: "card ?A = card S - 1" using fS a by auto
  2073     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  2074     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  2075       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  2076       by simp
  2077     then have ?thesis using a cA
  2078       by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
  2079   ultimately show ?thesis by blast
  2080 qed
  2081 
  2082 
  2083 lemma setsum_bounded:
  2084   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
  2085   shows "setsum f A \<le> of_nat(card A) * K"
  2086 proof (cases "finite A")
  2087   case True
  2088   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  2089 next
  2090   case False thus ?thesis by (simp add: setsum_def)
  2091 qed
  2092 
  2093 
  2094 subsubsection {* Cardinality of unions *}
  2095 
  2096 lemma card_UN_disjoint:
  2097   "finite I ==> (ALL i:I. finite (A i)) ==>
  2098    (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
  2099    ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  2100 apply (simp add: card_def del: setsum_constant)
  2101 apply (subgoal_tac
  2102          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  2103 apply (simp add: setsum_UN_disjoint del: setsum_constant)
  2104 apply (simp cong: setsum_cong)
  2105 done
  2106 
  2107 lemma card_Union_disjoint:
  2108   "finite C ==> (ALL A:C. finite A) ==>
  2109    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  2110    ==> card (Union C) = setsum card C"
  2111 apply (frule card_UN_disjoint [of C id])
  2112 apply (unfold Union_def id_def, assumption+)
  2113 done
  2114 
  2115 
  2116 subsubsection {* Cardinality of image *}
  2117 
  2118 text{*The image of a finite set can be expressed using @{term fold_image}.*}
  2119 lemma image_eq_fold_image:
  2120   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
  2121 proof (induct rule: finite_induct)
  2122   case empty then show ?case by simp
  2123 next
  2124   interpret ab_semigroup_mult "op Un"
  2125     proof qed auto
  2126   case insert 
  2127   then show ?case by simp
  2128 qed
  2129 
  2130 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  2131 apply (induct set: finite)
  2132  apply simp
  2133 apply (simp add: le_SucI finite_imageI card_insert_if)
  2134 done
  2135 
  2136 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  2137 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  2138 
  2139 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  2140 by (simp add: card_seteq card_image)
  2141 
  2142 lemma eq_card_imp_inj_on:
  2143   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  2144 apply (induct rule:finite_induct)
  2145 apply simp
  2146 apply(frule card_image_le[where f = f])
  2147 apply(simp add:card_insert_if split:if_splits)
  2148 done
  2149 
  2150 lemma inj_on_iff_eq_card:
  2151   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  2152 by(blast intro: card_image eq_card_imp_inj_on)
  2153 
  2154 
  2155 lemma card_inj_on_le:
  2156   "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  2157 apply (subgoal_tac "finite A") 
  2158  apply (force intro: card_mono simp add: card_image [symmetric])
  2159 apply (blast intro: finite_imageD dest: finite_subset) 
  2160 done
  2161 
  2162 lemma card_bij_eq:
  2163   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  2164      finite A; finite B |] ==> card A = card B"
  2165 by (auto intro: le_anti_sym card_inj_on_le)
  2166 
  2167 
  2168 subsubsection {* Cardinality of products *}
  2169 
  2170 (*
  2171 lemma SigmaI_insert: "y \<notin> A ==>
  2172   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  2173   by auto
  2174 *)
  2175 
  2176 lemma card_SigmaI [simp]:
  2177   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  2178   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  2179 by(simp add:card_def setsum_Sigma del:setsum_constant)
  2180 
  2181 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  2182 apply (cases "finite A") 
  2183 apply (cases "finite B") 
  2184 apply (auto simp add: card_eq_0_iff
  2185             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  2186 done
  2187 
  2188 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  2189 by (simp add: card_cartesian_product)
  2190 
  2191 
  2192 subsubsection {* Cardinality of sums *}
  2193 
  2194 lemma card_Plus:
  2195   assumes "finite A" and "finite B"
  2196   shows "card (A <+> B) = card A + card B"
  2197 proof -
  2198   have "Inl`A \<inter> Inr`B = {}" by fast
  2199   with assms show ?thesis
  2200     unfolding Plus_def
  2201     by (simp add: card_Un_disjoint card_image)
  2202 qed
  2203 
  2204 
  2205 subsubsection {* Cardinality of the Powerset *}
  2206 
  2207 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  2208 apply (induct set: finite)
  2209  apply (simp_all add: Pow_insert)
  2210 apply (subst card_Un_disjoint, blast)
  2211   apply (blast intro: finite_imageI, blast)
  2212 apply (subgoal_tac "inj_on (insert x) (Pow F)")
  2213  apply (simp add: card_image Pow_insert)
  2214 apply (unfold inj_on_def)
  2215 apply (blast elim!: equalityE)
  2216 done
  2217 
  2218 text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
  2219 
  2220 lemma dvd_partition:
  2221   "finite (Union C) ==>
  2222     ALL c : C. k dvd card c ==>
  2223     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  2224   k dvd card (Union C)"
  2225 apply(frule finite_UnionD)
  2226 apply(rotate_tac -1)
  2227 apply (induct set: finite, simp_all, clarify)
  2228 apply (subst card_Un_disjoint)
  2229    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  2230 done
  2231 
  2232 
  2233 subsubsection {* Relating injectivity and surjectivity *}
  2234 
  2235 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
  2236 apply(rule eq_card_imp_inj_on, assumption)
  2237 apply(frule finite_imageI)
  2238 apply(drule (1) card_seteq)
  2239  apply(erule card_image_le)
  2240 apply simp
  2241 done
  2242 
  2243 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
  2244 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
  2245 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
  2246 
  2247 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
  2248 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
  2249 by(fastsimp simp:surj_def dest!: endo_inj_surj)
  2250 
  2251 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
  2252 proof
  2253   assume "finite(UNIV::nat set)"
  2254   with finite_UNIV_inj_surj[of Suc]
  2255   show False by simp (blast dest: Suc_neq_Zero surjD)
  2256 qed
  2257 
  2258 lemma infinite_UNIV_char_0:
  2259   "\<not> finite (UNIV::'a::semiring_char_0 set)"
  2260 proof
  2261   assume "finite (UNIV::'a set)"
  2262   with subset_UNIV have "finite (range of_nat::'a set)"
  2263     by (rule finite_subset)
  2264   moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
  2265     by (simp add: inj_on_def)
  2266   ultimately have "finite (UNIV::nat set)"
  2267     by (rule finite_imageD)
  2268   then show "False"
  2269     by (simp add: infinite_UNIV_nat)
  2270 qed
  2271 
  2272 subsection{* A fold functional for non-empty sets *}
  2273 
  2274 text{* Does not require start value. *}
  2275 
  2276 inductive
  2277   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
  2278   for f :: "'a => 'a => 'a"
  2279 where
  2280   fold1Set_insertI [intro]:
  2281    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
  2282 
  2283 constdefs
  2284   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  2285   "fold1 f A == THE x. fold1Set f A x"
  2286 
  2287 lemma fold1Set_nonempty:
  2288   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
  2289 by(erule fold1Set.cases, simp_all)
  2290 
  2291 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
  2292 
  2293 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
  2294 
  2295 
  2296 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
  2297 by (blast intro: fold_graph.intros elim: fold_graph.cases)
  2298 
  2299 lemma fold1_singleton [simp]: "fold1 f {a} = a"
  2300 by (unfold fold1_def) blast
  2301 
  2302 lemma finite_nonempty_imp_fold1Set:
  2303   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
  2304 apply (induct A rule: finite_induct)
  2305 apply (auto dest: finite_imp_fold_graph [of _ f])
  2306 done
  2307 
  2308 text{*First, some lemmas about @{const fold_graph}.*}
  2309 
  2310 context ab_semigroup_mult
  2311 begin
  2312 
  2313 lemma fun_left_comm: "fun_left_comm(op *)"
  2314 by unfold_locales (simp add: mult_ac)
  2315 
  2316 lemma fold_graph_insert_swap:
  2317 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
  2318 shows "fold_graph times z (insert b A) (z * y)"
  2319 proof -
  2320   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2321 from assms show ?thesis
  2322 proof (induct rule: fold_graph.induct)
  2323   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
  2324 next
  2325   case (insertI x A y)
  2326     have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
  2327       using insertI by force  --{*how does @{term id} get unfolded?*}
  2328     thus ?case by (simp add: insert_commute mult_ac)
  2329 qed
  2330 qed
  2331 
  2332 lemma fold_graph_permute_diff:
  2333 assumes fold: "fold_graph times b A x"
  2334 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A-{a})) x"
  2335 using fold
  2336 proof (induct rule: fold_graph.induct)
  2337   case emptyI thus ?case by simp
  2338 next
  2339   case (insertI x A y)
  2340   have "a = x \<or> a \<in> A" using insertI by simp
  2341   thus ?case
  2342   proof
  2343     assume "a = x"
  2344     with insertI show ?thesis
  2345       by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)
  2346   next
  2347     assume ainA: "a \<in> A"
  2348     hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"
  2349       using insertI by force
  2350     moreover
  2351     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  2352       using ainA insertI by blast
  2353     ultimately show ?thesis by simp
  2354   qed
  2355 qed
  2356 
  2357 lemma fold1_eq_fold:
  2358 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
  2359 proof -
  2360   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2361   from assms show ?thesis
  2362 apply (simp add: fold1_def fold_def)
  2363 apply (rule the_equality)
  2364 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
  2365 apply (rule sym, clarify)
  2366 apply (case_tac "Aa=A")
  2367  apply (best intro: the_equality fold_graph_determ)
  2368 apply (subgoal_tac "fold_graph times a A x")
  2369  apply (best intro: the_equality fold_graph_determ)
  2370 apply (subgoal_tac "insert aa (Aa - {a}) = A")
  2371  prefer 2 apply (blast elim: equalityE)
  2372 apply (auto dest: fold_graph_permute_diff [where a=a])
  2373 done
  2374 qed
  2375 
  2376 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  2377 apply safe
  2378  apply simp
  2379  apply (drule_tac x=x in spec)
  2380  apply (drule_tac x="A-{x}" in spec, auto)
  2381 done
  2382 
  2383 lemma fold1_insert:
  2384   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  2385   shows "fold1 times (insert x A) = x * fold1 times A"
  2386 proof -
  2387   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2388   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
  2389     by (auto simp add: nonempty_iff)
  2390   with A show ?thesis
  2391     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
  2392 qed
  2393 
  2394 end
  2395 
  2396 context ab_semigroup_idem_mult
  2397 begin
  2398 
  2399 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
  2400 apply unfold_locales
  2401  apply (simp add: mult_ac)
  2402 apply (simp add: mult_idem mult_assoc[symmetric])
  2403 done
  2404 
  2405 
  2406 lemma fold1_insert_idem [simp]:
  2407   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  2408   shows "fold1 times (insert x A) = x * fold1 times A"
  2409 proof -
  2410   interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2411     by (rule fun_left_comm_idem)
  2412   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
  2413     by (auto simp add: nonempty_iff)
  2414   show ?thesis
  2415   proof cases
  2416     assume "a = x"
  2417     thus ?thesis
  2418     proof cases
  2419       assume "A' = {}"
  2420       with prems show ?thesis by (simp add: mult_idem)
  2421     next
  2422       assume "A' \<noteq> {}"
  2423       with prems show ?thesis
  2424 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
  2425     qed
  2426   next
  2427     assume "a \<noteq> x"
  2428     with prems show ?thesis
  2429       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  2430   qed
  2431 qed
  2432 
  2433 lemma hom_fold1_commute:
  2434 assumes hom: "!!x y. h (x * y) = h x * h y"
  2435 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
  2436 using N proof (induct rule: finite_ne_induct)
  2437   case singleton thus ?case by simp
  2438 next
  2439   case (insert n N)
  2440   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
  2441   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
  2442   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
  2443   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
  2444     using insert by(simp)
  2445   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  2446   finally show ?case .
  2447 qed
  2448 
  2449 end
  2450 
  2451 
  2452 text{* Now the recursion rules for definitions: *}
  2453 
  2454 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
  2455 by(simp add:fold1_singleton)
  2456 
  2457 lemma (in ab_semigroup_mult) fold1_insert_def:
  2458   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2459 by (simp add:fold1_insert)
  2460 
  2461 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
  2462   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2463 by simp
  2464 
  2465 subsubsection{* Determinacy for @{term fold1Set} *}
  2466 
  2467 (*Not actually used!!*)
  2468 (*
  2469 context ab_semigroup_mult
  2470 begin
  2471 
  2472 lemma fold_graph_permute:
  2473   "[|fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A|]
  2474    ==> fold_graph times id a (insert b A) x"
  2475 apply (cases "a=b") 
  2476 apply (auto dest: fold_graph_permute_diff) 
  2477 done
  2478 
  2479 lemma fold1Set_determ:
  2480   "fold1Set times A x ==> fold1Set times A y ==> y = x"
  2481 proof (clarify elim!: fold1Set.cases)
  2482   fix A x B y a b
  2483   assume Ax: "fold_graph times id a A x"
  2484   assume By: "fold_graph times id b B y"
  2485   assume anotA:  "a \<notin> A"
  2486   assume bnotB:  "b \<notin> B"
  2487   assume eq: "insert a A = insert b B"
  2488   show "y=x"
  2489   proof cases
  2490     assume same: "a=b"
  2491     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  2492     thus ?thesis using Ax By same by (blast intro: fold_graph_determ)
  2493   next
  2494     assume diff: "a\<noteq>b"
  2495     let ?D = "B - {a}"
  2496     have B: "B = insert a ?D" and A: "A = insert b ?D"
  2497      and aB: "a \<in> B" and bA: "b \<in> A"
  2498       using eq anotA bnotB diff by (blast elim!:equalityE)+
  2499     with aB bnotB By
  2500     have "fold_graph times id a (insert b ?D) y" 
  2501       by (auto intro: fold_graph_permute simp add: insert_absorb)
  2502     moreover
  2503     have "fold_graph times id a (insert b ?D) x"
  2504       by (simp add: A [symmetric] Ax) 
  2505     ultimately show ?thesis by (blast intro: fold_graph_determ) 
  2506   qed
  2507 qed
  2508 
  2509 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
  2510   by (unfold fold1_def) (blast intro: fold1Set_determ)
  2511 
  2512 end
  2513 *)
  2514 
  2515 declare
  2516   empty_fold_graphE [rule del]  fold_graph.intros [rule del]
  2517   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  2518   -- {* No more proofs involve these relations. *}
  2519 
  2520 subsubsection {* Lemmas about @{text fold1} *}
  2521 
  2522 context ab_semigroup_mult
  2523 begin
  2524 
  2525 lemma fold1_Un:
  2526 assumes A: "finite A" "A \<noteq> {}"
  2527 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2528        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2529 using A by (induct rule: finite_ne_induct)
  2530   (simp_all add: fold1_insert mult_assoc)
  2531 
  2532 lemma fold1_in:
  2533   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
  2534   shows "fold1 times A \<in> A"
  2535 using A
  2536 proof (induct rule:finite_ne_induct)
  2537   case singleton thus ?case by simp
  2538 next
  2539   case insert thus ?case using elem by (force simp add:fold1_insert)
  2540 qed
  2541 
  2542 end
  2543 
  2544 lemma (in ab_semigroup_idem_mult) fold1_Un2:
  2545 assumes A: "finite A" "A \<noteq> {}"
  2546 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2547        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2548 using A
  2549 proof(induct rule:finite_ne_induct)
  2550   case singleton thus ?case by simp
  2551 next
  2552   case insert thus ?case by (simp add: mult_assoc)
  2553 qed
  2554 
  2555 
  2556 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
  2557 
  2558 text{*
  2559   As an application of @{text fold1} we define infimum
  2560   and supremum in (not necessarily complete!) lattices
  2561   over (non-empty) sets by means of @{text fold1}.
  2562 *}
  2563 
  2564 context lower_semilattice
  2565 begin
  2566 
  2567 lemma ab_semigroup_idem_mult_inf:
  2568   "ab_semigroup_idem_mult inf"
  2569   proof qed (rule inf_assoc inf_commute inf_idem)+
  2570 
  2571 lemma below_fold1_iff:
  2572   assumes "finite A" "A \<noteq> {}"
  2573   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2574 proof -
  2575   interpret ab_semigroup_idem_mult inf
  2576     by (rule ab_semigroup_idem_mult_inf)
  2577   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  2578 qed
  2579 
  2580 lemma fold1_belowI:
  2581   assumes "finite A"
  2582     and "a \<in> A"
  2583   shows "fold1 inf A \<le> a"
  2584 proof -
  2585   from assms have "A \<noteq> {}" by auto
  2586   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  2587   proof (induct rule: finite_ne_induct)
  2588     case singleton thus ?case by simp
  2589   next
  2590     interpret ab_semigroup_idem_mult inf
  2591       by (rule ab_semigroup_idem_mult_inf)
  2592     case (insert x F)
  2593     from insert(5) have "a = x \<or> a \<in> F" by simp
  2594     thus ?case
  2595     proof
  2596       assume "a = x" thus ?thesis using insert
  2597         by (simp add: mult_ac)
  2598     next
  2599       assume "a \<in> F"
  2600       hence bel: "fold1 inf F \<le> a" by (rule insert)
  2601       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  2602         using insert by (simp add: mult_ac)
  2603       also have "inf (fold1 inf F) a = fold1 inf F"
  2604         using bel by (auto intro: antisym)
  2605       also have "inf x \<dots> = fold1 inf (insert x F)"
  2606         using insert by (simp add: mult_ac)
  2607       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  2608       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  2609       ultimately show ?thesis by simp
  2610     qed
  2611   qed
  2612 qed
  2613 
  2614 end
  2615 
  2616 lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
  2617   "ab_semigroup_idem_mult sup"
  2618   by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
  2619     (rule dual_lattice)
  2620 
  2621 context lattice
  2622 begin
  2623 
  2624 definition
  2625   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
  2626 where
  2627   "Inf_fin = fold1 inf"
  2628 
  2629 definition
  2630   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
  2631 where
  2632   "Sup_fin = fold1 sup"
  2633 
  2634 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  2635 apply(unfold Sup_fin_def Inf_fin_def)
  2636 apply(subgoal_tac "EX a. a:A")
  2637 prefer 2 apply blast
  2638 apply(erule exE)
  2639 apply(rule order_trans)
  2640 apply(erule (1) fold1_belowI)
  2641 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
  2642 done
  2643 
  2644 lemma sup_Inf_absorb [simp]:
  2645   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  2646 apply(subst sup_commute)
  2647 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  2648 done
  2649 
  2650 lemma inf_Sup_absorb [simp]:
  2651   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  2652 by (simp add: Sup_fin_def inf_absorb1
  2653   lower_semilattice.fold1_belowI [OF dual_lattice])
  2654 
  2655 end
  2656 
  2657 context distrib_lattice
  2658 begin
  2659 
  2660 lemma sup_Inf1_distrib:
  2661   assumes "finite A"
  2662     and "A \<noteq> {}"
  2663   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  2664 proof -
  2665   interpret ab_semigroup_idem_mult inf
  2666     by (rule ab_semigroup_idem_mult_inf)
  2667   from assms show ?thesis
  2668     by (simp add: Inf_fin_def image_def
  2669       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  2670         (rule arg_cong [where f="fold1 inf"], blast)
  2671 qed
  2672 
  2673 lemma sup_Inf2_distrib:
  2674   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2675   shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
  2676 using A proof (induct rule: finite_ne_induct)
  2677   case singleton thus ?case
  2678     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
  2679 next
  2680   interpret ab_semigroup_idem_mult inf
  2681     by (rule ab_semigroup_idem_mult_inf)
  2682   case (insert x A)
  2683   have finB: "finite {sup x b |b. b \<in> B}"
  2684     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  2685   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  2686   proof -
  2687     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  2688       by blast
  2689     thus ?thesis by(simp add: insert(1) B(1))
  2690   qed
  2691   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2692   have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
  2693     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
  2694   also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
  2695   also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
  2696     using insert by(simp add:sup_Inf1_distrib[OF B])
  2697   also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
  2698     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  2699     using B insert
  2700     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  2701   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2702     by blast
  2703   finally show ?case .
  2704 qed
  2705 
  2706 lemma inf_Sup1_distrib:
  2707   assumes "finite A" and "A \<noteq> {}"
  2708   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  2709 proof -
  2710   interpret ab_semigroup_idem_mult sup
  2711     by (rule ab_semigroup_idem_mult_sup)
  2712   from assms show ?thesis
  2713     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  2714       (rule arg_cong [where f="fold1 sup"], blast)
  2715 qed
  2716 
  2717 lemma inf_Sup2_distrib:
  2718   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2719   shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
  2720 using A proof (induct rule: finite_ne_induct)
  2721   case singleton thus ?case
  2722     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
  2723 next
  2724   case (insert x A)
  2725   have finB: "finite {inf x b |b. b \<in> B}"
  2726     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  2727   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  2728   proof -
  2729     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  2730       by blast
  2731     thus ?thesis by(simp add: insert(1) B(1))
  2732   qed
  2733   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2734   interpret ab_semigroup_idem_mult sup
  2735     by (rule ab_semigroup_idem_mult_sup)
  2736   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
  2737     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
  2738   also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
  2739   also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
  2740     using insert by(simp add:inf_Sup1_distrib[OF B])
  2741   also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
  2742     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  2743     using B insert
  2744     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  2745   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2746     by blast
  2747   finally show ?case .
  2748 qed
  2749 
  2750 end
  2751 
  2752 context complete_lattice
  2753 begin
  2754 
  2755 text {*
  2756   Coincidence on finite sets in complete lattices:
  2757 *}
  2758 
  2759 lemma Inf_fin_Inf:
  2760   assumes "finite A" and "A \<noteq> {}"
  2761   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  2762 proof -
  2763     interpret ab_semigroup_idem_mult inf
  2764     by (rule ab_semigroup_idem_mult_inf)
  2765   from assms show ?thesis
  2766   unfolding Inf_fin_def by (induct A set: finite)
  2767     (simp_all add: Inf_insert_simp)
  2768 qed
  2769 
  2770 lemma Sup_fin_Sup:
  2771   assumes "finite A" and "A \<noteq> {}"
  2772   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  2773 proof -
  2774   interpret ab_semigroup_idem_mult sup
  2775     by (rule ab_semigroup_idem_mult_sup)
  2776   from assms show ?thesis
  2777   unfolding Sup_fin_def by (induct A set: finite)
  2778     (simp_all add: Sup_insert_simp)
  2779 qed
  2780 
  2781 end
  2782 
  2783 
  2784 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
  2785 
  2786 text{*
  2787   As an application of @{text fold1} we define minimum
  2788   and maximum in (not necessarily complete!) linear orders
  2789   over (non-empty) sets by means of @{text fold1}.
  2790 *}
  2791 
  2792 context linorder
  2793 begin
  2794 
  2795 lemma ab_semigroup_idem_mult_min:
  2796   "ab_semigroup_idem_mult min"
  2797   proof qed (auto simp add: min_def)
  2798 
  2799 lemma ab_semigroup_idem_mult_max:
  2800   "ab_semigroup_idem_mult max"
  2801   proof qed (auto simp add: max_def)
  2802 
  2803 lemma min_lattice:
  2804   "lower_semilattice (op \<le>) (op <) min"
  2805   proof qed (auto simp add: min_def)
  2806 
  2807 lemma max_lattice:
  2808   "lower_semilattice (op \<ge>) (op >) max"
  2809   proof qed (auto simp add: max_def)
  2810 
  2811 lemma dual_max:
  2812   "ord.max (op \<ge>) = min"
  2813   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
  2814 
  2815 lemma dual_min:
  2816   "ord.min (op \<ge>) = max"
  2817   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
  2818 
  2819 lemma strict_below_fold1_iff:
  2820   assumes "finite A" and "A \<noteq> {}"
  2821   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2822 proof -
  2823   interpret ab_semigroup_idem_mult min
  2824     by (rule ab_semigroup_idem_mult_min)
  2825   from assms show ?thesis
  2826   by (induct rule: finite_ne_induct)
  2827     (simp_all add: fold1_insert)
  2828 qed
  2829 
  2830 lemma fold1_below_iff:
  2831   assumes "finite A" and "A \<noteq> {}"
  2832   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2833 proof -
  2834   interpret ab_semigroup_idem_mult min
  2835     by (rule ab_semigroup_idem_mult_min)
  2836   from assms show ?thesis
  2837   by (induct rule: finite_ne_induct)
  2838     (simp_all add: fold1_insert min_le_iff_disj)
  2839 qed
  2840 
  2841 lemma fold1_strict_below_iff:
  2842   assumes "finite A" and "A \<noteq> {}"
  2843   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2844 proof -
  2845   interpret ab_semigroup_idem_mult min
  2846     by (rule ab_semigroup_idem_mult_min)
  2847   from assms show ?thesis
  2848   by (induct rule: finite_ne_induct)
  2849     (simp_all add: fold1_insert min_less_iff_disj)
  2850 qed
  2851 
  2852 lemma fold1_antimono:
  2853   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  2854   shows "fold1 min B \<le> fold1 min A"
  2855 proof cases
  2856   assume "A = B" thus ?thesis by simp
  2857 next
  2858   interpret ab_semigroup_idem_mult min
  2859     by (rule ab_semigroup_idem_mult_min)
  2860   assume "A \<noteq> B"
  2861   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  2862   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  2863   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  2864   proof -
  2865     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  2866     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  2867     moreover have "(B-A) \<noteq> {}" using prems by blast
  2868     moreover have "A Int (B-A) = {}" using prems by blast
  2869     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  2870   qed
  2871   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  2872   finally show ?thesis .
  2873 qed
  2874 
  2875 definition
  2876   Min :: "'a set \<Rightarrow> 'a"
  2877 where
  2878   "Min = fold1 min"
  2879 
  2880 definition
  2881   Max :: "'a set \<Rightarrow> 'a"
  2882 where
  2883   "Max = fold1 max"
  2884 
  2885 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
  2886 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
  2887 
  2888 lemma Min_insert [simp]:
  2889   assumes "finite A" and "A \<noteq> {}"
  2890   shows "Min (insert x A) = min x (Min A)"
  2891 proof -
  2892   interpret ab_semigroup_idem_mult min
  2893     by (rule ab_semigroup_idem_mult_min)
  2894   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
  2895 qed
  2896 
  2897 lemma Max_insert [simp]:
  2898   assumes "finite A" and "A \<noteq> {}"
  2899   shows "Max (insert x A) = max x (Max A)"
  2900 proof -
  2901   interpret ab_semigroup_idem_mult max
  2902     by (rule ab_semigroup_idem_mult_max)
  2903   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
  2904 qed
  2905 
  2906 lemma Min_in [simp]:
  2907   assumes "finite A" and "A \<noteq> {}"
  2908   shows "Min A \<in> A"
  2909 proof -
  2910   interpret ab_semigroup_idem_mult min
  2911     by (rule ab_semigroup_idem_mult_min)
  2912   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
  2913 qed
  2914 
  2915 lemma Max_in [simp]:
  2916   assumes "finite A" and "A \<noteq> {}"
  2917   shows "Max A \<in> A"
  2918 proof -
  2919   interpret ab_semigroup_idem_mult max
  2920     by (rule ab_semigroup_idem_mult_max)
  2921   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
  2922 qed
  2923 
  2924 lemma Min_Un:
  2925   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2926   shows "Min (A \<union> B) = min (Min A) (Min B)"
  2927 proof -
  2928   interpret ab_semigroup_idem_mult min
  2929     by (rule ab_semigroup_idem_mult_min)
  2930   from assms show ?thesis
  2931     by (simp add: Min_def fold1_Un2)
  2932 qed
  2933 
  2934 lemma Max_Un:
  2935   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2936   shows "Max (A \<union> B) = max (Max A) (Max B)"
  2937 proof -
  2938   interpret ab_semigroup_idem_mult max
  2939     by (rule ab_semigroup_idem_mult_max)
  2940   from assms show ?thesis
  2941     by (simp add: Max_def fold1_Un2)
  2942 qed
  2943 
  2944 lemma hom_Min_commute:
  2945   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  2946     and "finite N" and "N \<noteq> {}"
  2947   shows "h (Min N) = Min (h ` N)"
  2948 proof -
  2949   interpret ab_semigroup_idem_mult min
  2950     by (rule ab_semigroup_idem_mult_min)
  2951   from assms show ?thesis
  2952     by (simp add: Min_def hom_fold1_commute)
  2953 qed
  2954 
  2955 lemma hom_Max_commute:
  2956   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  2957     and "finite N" and "N \<noteq> {}"
  2958   shows "h (Max N) = Max (h ` N)"
  2959 proof -
  2960   interpret ab_semigroup_idem_mult max
  2961     by (rule ab_semigroup_idem_mult_max)
  2962   from assms show ?thesis
  2963     by (simp add: Max_def hom_fold1_commute [of h])
  2964 qed
  2965 
  2966 lemma Min_le [simp]:
  2967   assumes "finite A" and "x \<in> A"
  2968   shows "Min A \<le> x"
  2969 proof -
  2970   interpret lower_semilattice "op \<le>" "op <" min
  2971     by (rule min_lattice)
  2972   from assms show ?thesis by (simp add: Min_def fold1_belowI)
  2973 qed
  2974 
  2975 lemma Max_ge [simp]:
  2976   assumes "finite A" and "x \<in> A"
  2977   shows "x \<le> Max A"
  2978 proof -
  2979   interpret lower_semilattice "op \<ge>" "op >" max
  2980     by (rule max_lattice)
  2981   from assms show ?thesis by (simp add: Max_def fold1_belowI)
  2982 qed
  2983 
  2984 lemma Min_ge_iff [simp, noatp]:
  2985   assumes "finite A" and "A \<noteq> {}"
  2986   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2987 proof -
  2988   interpret lower_semilattice "op \<le>" "op <" min
  2989     by (rule min_lattice)
  2990   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
  2991 qed
  2992 
  2993 lemma Max_le_iff [simp, noatp]:
  2994   assumes "finite A" and "A \<noteq> {}"
  2995   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2996 proof -
  2997   interpret lower_semilattice "op \<ge>" "op >" max
  2998     by (rule max_lattice)
  2999   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
  3000 qed
  3001 
  3002 lemma Min_gr_iff [simp, noatp]:
  3003   assumes "finite A" and "A \<noteq> {}"
  3004   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  3005 proof -
  3006   interpret lower_semilattice "op \<le>" "op <" min
  3007     by (rule min_lattice)
  3008   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
  3009 qed
  3010 
  3011 lemma Max_less_iff [simp, noatp]:
  3012   assumes "finite A" and "A \<noteq> {}"
  3013   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  3014 proof -
  3015   note Max = Max_def
  3016   interpret linorder "op \<ge>" "op >"
  3017     by (rule dual_linorder)
  3018   from assms show ?thesis
  3019     by (simp add: Max strict_below_fold1_iff [folded dual_max])
  3020 qed
  3021 
  3022 lemma Min_le_iff [noatp]:
  3023   assumes "finite A" and "A \<noteq> {}"
  3024   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  3025 proof -
  3026   interpret lower_semilattice "op \<le>" "op <" min
  3027     by (rule min_lattice)
  3028   from assms show ?thesis
  3029     by (simp add: Min_def fold1_below_iff)
  3030 qed
  3031 
  3032 lemma Max_ge_iff [noatp]:
  3033   assumes "finite A" and "A \<noteq> {}"
  3034   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  3035 proof -
  3036   note Max = Max_def
  3037   interpret linorder "op \<ge>" "op >"
  3038     by (rule dual_linorder)
  3039   from assms show ?thesis
  3040     by (simp add: Max fold1_below_iff [folded dual_max])
  3041 qed
  3042 
  3043 lemma Min_less_iff [noatp]:
  3044   assumes "finite A" and "A \<noteq> {}"
  3045   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  3046 proof -
  3047   interpret lower_semilattice "op \<le>" "op <" min
  3048     by (rule min_lattice)
  3049   from assms show ?thesis
  3050     by (simp add: Min_def fold1_strict_below_iff)
  3051 qed
  3052 
  3053 lemma Max_gr_iff [noatp]:
  3054   assumes "finite A" and "A \<noteq> {}"
  3055   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  3056 proof -
  3057   note Max = Max_def
  3058   interpret linorder "op \<ge>" "op >"
  3059     by (rule dual_linorder)
  3060   from assms show ?thesis
  3061     by (simp add: Max fold1_strict_below_iff [folded dual_max])
  3062 qed
  3063 
  3064 lemma Min_eqI:
  3065   assumes "finite A"
  3066   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  3067     and "x \<in> A"
  3068   shows "Min A = x"
  3069 proof (rule antisym)
  3070   from `x \<in> A` have "A \<noteq> {}" by auto
  3071   with assms show "Min A \<ge> x" by simp
  3072 next
  3073   from assms show "x \<ge> Min A" by simp
  3074 qed
  3075 
  3076 lemma Max_eqI:
  3077   assumes "finite A"
  3078   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  3079     and "x \<in> A"
  3080   shows "Max A = x"
  3081 proof (rule antisym)
  3082   from `x \<in> A` have "A \<noteq> {}" by auto
  3083   with assms show "Max A \<le> x" by simp
  3084 next
  3085   from assms show "x \<le> Max A" by simp
  3086 qed
  3087 
  3088 lemma Min_antimono:
  3089   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  3090   shows "Min N \<le> Min M"
  3091 proof -
  3092   interpret distrib_lattice "op \<le>" "op <" min max
  3093     by (rule distrib_lattice_min_max)
  3094   from assms show ?thesis by (simp add: Min_def fold1_antimono)
  3095 qed
  3096 
  3097 lemma Max_mono:
  3098   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  3099   shows "Max M \<le> Max N"
  3100 proof -
  3101   note Max = Max_def
  3102   interpret linorder "op \<ge>" "op >"
  3103     by (rule dual_linorder)
  3104   from assms show ?thesis
  3105     by (simp add: Max fold1_antimono [folded dual_max])
  3106 qed
  3107 
  3108 lemma finite_linorder_induct[consumes 1, case_names empty insert]:
  3109  "finite A \<Longrightarrow> P {} \<Longrightarrow>
  3110   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
  3111   \<Longrightarrow> P A"
  3112 proof (induct A rule: measure_induct_rule[where f=card])
  3113   fix A :: "'a set"
  3114   assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
  3115                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
  3116                   \<Longrightarrow> P B"
  3117   and "finite A" and "P {}"
  3118   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
  3119   show "P A"
  3120   proof (cases "A = {}")
  3121     assume "A = {}" thus "P A" using `P {}` by simp
  3122   next
  3123     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
  3124     assume "A \<noteq> {}"
  3125     with `finite A` have "Max A : A" by auto
  3126     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
  3127     note card_Diff1_less[OF `finite A` `Max A : A`]
  3128     moreover have "finite ?B" using `finite A` by simp
  3129     ultimately have "P ?B" using `P {}` step IH by blast
  3130     moreover have "\<forall>a\<in>?B. a < Max A"
  3131       using Max_ge [OF `finite A`] by fastsimp
  3132     ultimately show "P A"
  3133       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
  3134   qed
  3135 qed
  3136 
  3137 end
  3138 
  3139 context ordered_ab_semigroup_add
  3140 begin
  3141 
  3142 lemma add_Min_commute:
  3143   fixes k
  3144   assumes "finite N" and "N \<noteq> {}"
  3145   shows "k + Min N = Min {k + m | m. m \<in> N}"
  3146 proof -
  3147   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  3148     by (simp add: min_def not_le)
  3149       (blast intro: antisym less_imp_le add_left_mono)
  3150   with assms show ?thesis
  3151     using hom_Min_commute [of "plus k" N]
  3152     by simp (blast intro: arg_cong [where f = Min])
  3153 qed
  3154 
  3155 lemma add_Max_commute:
  3156   fixes k
  3157   assumes "finite N" and "N \<noteq> {}"
  3158   shows "k + Max N = Max {k + m | m. m \<in> N}"
  3159 proof -
  3160   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  3161     by (simp add: max_def not_le)
  3162       (blast intro: antisym less_imp_le add_left_mono)
  3163   with assms show ?thesis
  3164     using hom_Max_commute [of "plus k" N]
  3165     by simp (blast intro: arg_cong [where f = Max])
  3166 qed
  3167 
  3168 end
  3169 
  3170 end