src/HOL/Finite_Set.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30325 b3ae84c6e509
child 30729 461ee3e49ad3
permissions -rw-r--r--
simplified method setup;
     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   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1088   and z: "\<forall>i \<in> T - S. f i = 0"
  1089   shows "setsum f T = setsum f S"
  1090 using setsum_mono_zero_left[OF fT ST z] by simp
  1091 
  1092 lemma setsum_mono_zero_cong_left: 
  1093   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1094   and z: "\<forall>i \<in> T - S. g i = 0"
  1095   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  1096   shows "setsum f S = setsum g T"
  1097 proof-
  1098   have eq: "T = S \<union> (T - S)" using ST by blast
  1099   have d: "S \<inter> (T - S) = {}" using ST by blast
  1100   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
  1101   show ?thesis 
  1102     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
  1103 qed
  1104 
  1105 lemma setsum_mono_zero_cong_right: 
  1106   assumes fT: "finite T" and ST: "S \<subseteq> T"
  1107   and z: "\<forall>i \<in> T - S. f i = 0"
  1108   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  1109   shows "setsum f T = setsum g S"
  1110 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
  1111 
  1112 lemma setsum_delta: 
  1113   assumes fS: "finite S"
  1114   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
  1115 proof-
  1116   let ?f = "(\<lambda>k. if k=a then b k else 0)"
  1117   {assume a: "a \<notin> S"
  1118     hence "\<forall> k\<in> S. ?f k = 0" by simp
  1119     hence ?thesis  using a by simp}
  1120   moreover 
  1121   {assume a: "a \<in> S"
  1122     let ?A = "S - {a}"
  1123     let ?B = "{a}"
  1124     have eq: "S = ?A \<union> ?B" using a by blast 
  1125     have dj: "?A \<inter> ?B = {}" by simp
  1126     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1127     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
  1128       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1129       by simp
  1130     then have ?thesis  using a by simp}
  1131   ultimately show ?thesis by blast
  1132 qed
  1133 lemma setsum_delta': 
  1134   assumes fS: "finite S" shows 
  1135   "setsum (\<lambda>k. if a = k then b k else 0) S = 
  1136      (if a\<in> S then b a else 0)"
  1137   using setsum_delta[OF fS, of a b, symmetric] 
  1138   by (auto intro: setsum_cong)
  1139 
  1140 lemma setsum_restrict_set:
  1141   assumes fA: "finite A"
  1142   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
  1143 proof-
  1144   from fA have fab: "finite (A \<inter> B)" by auto
  1145   have aba: "A \<inter> B \<subseteq> A" by blast
  1146   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
  1147   from setsum_mono_zero_left[OF fA aba, of ?g]
  1148   show ?thesis by simp
  1149 qed
  1150 
  1151 lemma setsum_cases:
  1152   assumes fA: "finite A"
  1153   shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
  1154          setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
  1155 proof-
  1156   have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}" 
  1157     by blast+
  1158   from fA 
  1159   have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
  1160   let ?g = "\<lambda>x. if x \<in> B then f x else g x"
  1161   from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
  1162   show ?thesis by simp
  1163 qed
  1164 
  1165 
  1166 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
  1167   the lhs need not be, since UNION I A could still be finite.*)
  1168 lemma setsum_UN_disjoint:
  1169     "finite I ==> (ALL i:I. finite (A i)) ==>
  1170         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1171       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
  1172 by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
  1173 
  1174 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
  1175 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
  1176 lemma setsum_Union_disjoint:
  1177   "[| (ALL A:C. finite A);
  1178       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
  1179    ==> setsum f (Union C) = setsum (setsum f) C"
  1180 apply (cases "finite C") 
  1181  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
  1182   apply (frule setsum_UN_disjoint [of C id f])
  1183  apply (unfold Union_def id_def, assumption+)
  1184 done
  1185 
  1186 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
  1187   the rhs need not be, since SIGMA A B could still be finite.*)
  1188 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1189     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1190 by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
  1191 
  1192 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1193 lemma setsum_cartesian_product: 
  1194    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
  1195 apply (cases "finite A") 
  1196  apply (cases "finite B") 
  1197   apply (simp add: setsum_Sigma)
  1198  apply (cases "A={}", simp)
  1199  apply (simp) 
  1200 apply (auto simp add: setsum_def
  1201             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1202 done
  1203 
  1204 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
  1205 by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
  1206 
  1207 
  1208 subsubsection {* Properties in more restricted classes of structures *}
  1209 
  1210 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
  1211 apply (case_tac "finite A")
  1212  prefer 2 apply (simp add: setsum_def)
  1213 apply (erule rev_mp)
  1214 apply (erule finite_induct, auto)
  1215 done
  1216 
  1217 lemma setsum_eq_0_iff [simp]:
  1218     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
  1219 by (induct set: finite) auto
  1220 
  1221 lemma setsum_Un_nat: "finite A ==> finite B ==>
  1222   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
  1223   -- {* For the natural numbers, we have subtraction. *}
  1224 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
  1225 
  1226 lemma setsum_Un: "finite A ==> finite B ==>
  1227   (setsum f (A Un B) :: 'a :: ab_group_add) =
  1228    setsum f A + setsum f B - setsum f (A Int B)"
  1229 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
  1230 
  1231 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"
  1232   apply (induct set: finite)
  1233   apply simp by (auto simp add: fold_image_insert)
  1234 
  1235 lemma (in comm_monoid_mult) fold_image_Un_one:
  1236   assumes fS: "finite S" and fT: "finite T"
  1237   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
  1238   shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
  1239 proof-
  1240   have "fold_image op * f 1 (S \<inter> T) = 1" 
  1241     apply (rule fold_image_1)
  1242     using fS fT I0 by auto 
  1243   with fold_image_Un_Int[OF fS fT] show ?thesis by simp
  1244 qed
  1245 
  1246 lemma setsum_eq_general_reverses:
  1247   assumes fS: "finite S" and fT: "finite T"
  1248   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
  1249   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
  1250   shows "setsum f S = setsum g T"
  1251   apply (simp add: setsum_def fS fT)
  1252   apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
  1253   apply (erule kh)
  1254   apply (erule hk)
  1255   done
  1256 
  1257 
  1258 
  1259 lemma setsum_Un_zero:  
  1260   assumes fS: "finite S" and fT: "finite T"
  1261   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
  1262   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
  1263   using fS fT
  1264   apply (simp add: setsum_def)
  1265   apply (rule comm_monoid_add.fold_image_Un_one)
  1266   using I0 by auto
  1267 
  1268 
  1269 lemma setsum_UNION_zero: 
  1270   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
  1271   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"
  1272   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
  1273   using fSS f0
  1274 proof(induct rule: finite_induct[OF fS])
  1275   case 1 thus ?case by simp
  1276 next
  1277   case (2 T F)
  1278   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
  1279     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
  1280   from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
  1281   from "2.prems" TF fTF
  1282   show ?case 
  1283     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
  1284 qed
  1285 
  1286 
  1287 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
  1288   (if a:A then setsum f A - f a else setsum f A)"
  1289 apply (case_tac "finite A")
  1290  prefer 2 apply (simp add: setsum_def)
  1291 apply (erule finite_induct)
  1292  apply (auto simp add: insert_Diff_if)
  1293 apply (drule_tac a = a in mk_disjoint_insert, auto)
  1294 done
  1295 
  1296 lemma setsum_diff1: "finite A \<Longrightarrow>
  1297   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1298   (if a:A then setsum f A - f a else setsum f A)"
  1299 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1300 
  1301 lemma setsum_diff1'[rule_format]:
  1302   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
  1303 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))"])
  1304 apply (auto simp add: insert_Diff_if add_ac)
  1305 done
  1306 
  1307 (* By Jeremy Siek: *)
  1308 
  1309 lemma setsum_diff_nat: 
  1310 assumes "finite B" and "B \<subseteq> A"
  1311 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1312 using assms
  1313 proof induct
  1314   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1315 next
  1316   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1317     and xFinA: "insert x F \<subseteq> A"
  1318     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1319   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1320   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1321     by (simp add: setsum_diff1_nat)
  1322   from xFinA have "F \<subseteq> A" by simp
  1323   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1324   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1325     by simp
  1326   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1327   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1328     by simp
  1329   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1330   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1331     by simp
  1332   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1333 qed
  1334 
  1335 lemma setsum_diff:
  1336   assumes le: "finite A" "B \<subseteq> A"
  1337   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1338 proof -
  1339   from le have finiteB: "finite B" using finite_subset by auto
  1340   show ?thesis using finiteB le
  1341   proof induct
  1342     case empty
  1343     thus ?case by auto
  1344   next
  1345     case (insert x F)
  1346     thus ?case using le finiteB 
  1347       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1348   qed
  1349 qed
  1350 
  1351 lemma setsum_mono:
  1352   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1353   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1354 proof (cases "finite K")
  1355   case True
  1356   thus ?thesis using le
  1357   proof induct
  1358     case empty
  1359     thus ?case by simp
  1360   next
  1361     case insert
  1362     thus ?case using add_mono by fastsimp
  1363   qed
  1364 next
  1365   case False
  1366   thus ?thesis
  1367     by (simp add: setsum_def)
  1368 qed
  1369 
  1370 lemma setsum_strict_mono:
  1371   fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1372   assumes "finite A"  "A \<noteq> {}"
  1373     and "!!x. x:A \<Longrightarrow> f x < g x"
  1374   shows "setsum f A < setsum g A"
  1375   using prems
  1376 proof (induct rule: finite_ne_induct)
  1377   case singleton thus ?case by simp
  1378 next
  1379   case insert thus ?case by (auto simp: add_strict_mono)
  1380 qed
  1381 
  1382 lemma setsum_negf:
  1383   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1384 proof (cases "finite A")
  1385   case True thus ?thesis by (induct set: finite) auto
  1386 next
  1387   case False thus ?thesis by (simp add: setsum_def)
  1388 qed
  1389 
  1390 lemma setsum_subtractf:
  1391   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1392     setsum f A - setsum g A"
  1393 proof (cases "finite A")
  1394   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1395 next
  1396   case False thus ?thesis by (simp add: setsum_def)
  1397 qed
  1398 
  1399 lemma setsum_nonneg:
  1400   assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1401   shows "0 \<le> setsum f A"
  1402 proof (cases "finite A")
  1403   case True thus ?thesis using nn
  1404   proof induct
  1405     case empty then show ?case by simp
  1406   next
  1407     case (insert x F)
  1408     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
  1409     with insert show ?case by simp
  1410   qed
  1411 next
  1412   case False thus ?thesis by (simp add: setsum_def)
  1413 qed
  1414 
  1415 lemma setsum_nonpos:
  1416   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
  1417   shows "setsum f A \<le> 0"
  1418 proof (cases "finite A")
  1419   case True thus ?thesis using np
  1420   proof induct
  1421     case empty then show ?case by simp
  1422   next
  1423     case (insert x F)
  1424     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
  1425     with insert show ?case by simp
  1426   qed
  1427 next
  1428   case False thus ?thesis by (simp add: setsum_def)
  1429 qed
  1430 
  1431 lemma setsum_mono2:
  1432 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1433 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1434 shows "setsum f A \<le> setsum f B"
  1435 proof -
  1436   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1437     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1438   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1439     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1440   also have "A \<union> (B-A) = B" using sub by blast
  1441   finally show ?thesis .
  1442 qed
  1443 
  1444 lemma setsum_mono3: "finite B ==> A <= B ==> 
  1445     ALL x: B - A. 
  1446       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
  1447         setsum f A <= setsum f B"
  1448   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
  1449   apply (erule ssubst)
  1450   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
  1451   apply simp
  1452   apply (rule add_left_mono)
  1453   apply (erule setsum_nonneg)
  1454   apply (subst setsum_Un_disjoint [THEN sym])
  1455   apply (erule finite_subset, assumption)
  1456   apply (rule finite_subset)
  1457   prefer 2
  1458   apply assumption
  1459   apply auto
  1460   apply (rule setsum_cong)
  1461   apply auto
  1462 done
  1463 
  1464 lemma setsum_right_distrib: 
  1465   fixes f :: "'a => ('b::semiring_0)"
  1466   shows "r * setsum f A = setsum (%n. r * f n) A"
  1467 proof (cases "finite A")
  1468   case True
  1469   thus ?thesis
  1470   proof induct
  1471     case empty thus ?case by simp
  1472   next
  1473     case (insert x A) thus ?case by (simp add: right_distrib)
  1474   qed
  1475 next
  1476   case False thus ?thesis by (simp add: setsum_def)
  1477 qed
  1478 
  1479 lemma setsum_left_distrib:
  1480   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
  1481 proof (cases "finite A")
  1482   case True
  1483   then show ?thesis
  1484   proof induct
  1485     case empty thus ?case by simp
  1486   next
  1487     case (insert x A) thus ?case by (simp add: left_distrib)
  1488   qed
  1489 next
  1490   case False thus ?thesis by (simp add: setsum_def)
  1491 qed
  1492 
  1493 lemma setsum_divide_distrib:
  1494   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
  1495 proof (cases "finite A")
  1496   case True
  1497   then show ?thesis
  1498   proof induct
  1499     case empty thus ?case by simp
  1500   next
  1501     case (insert x A) thus ?case by (simp add: add_divide_distrib)
  1502   qed
  1503 next
  1504   case False thus ?thesis by (simp add: setsum_def)
  1505 qed
  1506 
  1507 lemma setsum_abs[iff]: 
  1508   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1509   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1510 proof (cases "finite A")
  1511   case True
  1512   thus ?thesis
  1513   proof induct
  1514     case empty thus ?case by simp
  1515   next
  1516     case (insert x A)
  1517     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1518   qed
  1519 next
  1520   case False thus ?thesis by (simp add: setsum_def)
  1521 qed
  1522 
  1523 lemma setsum_abs_ge_zero[iff]: 
  1524   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1525   shows "0 \<le> setsum (%i. abs(f i)) A"
  1526 proof (cases "finite A")
  1527   case True
  1528   thus ?thesis
  1529   proof induct
  1530     case empty thus ?case by simp
  1531   next
  1532     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
  1533   qed
  1534 next
  1535   case False thus ?thesis by (simp add: setsum_def)
  1536 qed
  1537 
  1538 lemma abs_setsum_abs[simp]: 
  1539   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
  1540   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1541 proof (cases "finite A")
  1542   case True
  1543   thus ?thesis
  1544   proof induct
  1545     case empty thus ?case by simp
  1546   next
  1547     case (insert a A)
  1548     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
  1549     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1550     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
  1551       by (simp del: abs_of_nonneg)
  1552     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1553     finally show ?case .
  1554   qed
  1555 next
  1556   case False thus ?thesis by (simp add: setsum_def)
  1557 qed
  1558 
  1559 
  1560 text {* Commuting outer and inner summation *}
  1561 
  1562 lemma swap_inj_on:
  1563   "inj_on (%(i, j). (j, i)) (A \<times> B)"
  1564   by (unfold inj_on_def) fast
  1565 
  1566 lemma swap_product:
  1567   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
  1568   by (simp add: split_def image_def) blast
  1569 
  1570 lemma setsum_commute:
  1571   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
  1572 proof (simp add: setsum_cartesian_product)
  1573   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
  1574     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
  1575     (is "?s = _")
  1576     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
  1577     apply (simp add: split_def)
  1578     done
  1579   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
  1580     (is "_ = ?t")
  1581     apply (simp add: swap_product)
  1582     done
  1583   finally show "?s = ?t" .
  1584 qed
  1585 
  1586 lemma setsum_product:
  1587   fixes f :: "'a => ('b::semiring_0)"
  1588   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
  1589   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
  1590 
  1591 
  1592 subsection {* Generalized product over a set *}
  1593 
  1594 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1595 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
  1596 
  1597 abbreviation
  1598   Setprod  ("\<Prod>_" [1000] 999) where
  1599   "\<Prod>A == setprod (%x. x) A"
  1600 
  1601 syntax
  1602   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1603 syntax (xsymbols)
  1604   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1605 syntax (HTML output)
  1606   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1607 
  1608 translations -- {* Beware of argument permutation! *}
  1609   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1610   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1611 
  1612 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1613  @{text"\<Prod>x|P. e"}. *}
  1614 
  1615 syntax
  1616   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1617 syntax (xsymbols)
  1618   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1619 syntax (HTML output)
  1620   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1621 
  1622 translations
  1623   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1624   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1625 
  1626 
  1627 lemma setprod_empty [simp]: "setprod f {} = 1"
  1628 by (auto simp add: setprod_def)
  1629 
  1630 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1631     setprod f (insert a A) = f a * setprod f A"
  1632 by (simp add: setprod_def)
  1633 
  1634 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1635 by (simp add: setprod_def)
  1636 
  1637 lemma setprod_reindex:
  1638    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1639 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
  1640 
  1641 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1642 by (auto simp add: setprod_reindex)
  1643 
  1644 lemma setprod_cong:
  1645   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1646 by(fastsimp simp: setprod_def intro: fold_image_cong)
  1647 
  1648 lemma strong_setprod_cong:
  1649   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1650 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
  1651 
  1652 lemma setprod_reindex_cong: "inj_on f A ==>
  1653     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1654 by (frule setprod_reindex, simp)
  1655 
  1656 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
  1657   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  1658   shows "setprod h B = setprod g A"
  1659 proof-
  1660     have "setprod h B = setprod (h o f) A"
  1661       by (simp add: B setprod_reindex[OF i, of h])
  1662     then show ?thesis apply simp
  1663       apply (rule setprod_cong)
  1664       apply simp
  1665       by (erule eq[symmetric])
  1666 qed
  1667 
  1668 lemma setprod_Un_one:  
  1669   assumes fS: "finite S" and fT: "finite T"
  1670   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
  1671   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
  1672   using fS fT
  1673   apply (simp add: setprod_def)
  1674   apply (rule fold_image_Un_one)
  1675   using I0 by auto
  1676 
  1677 
  1678 lemma setprod_1: "setprod (%i. 1) A = 1"
  1679 apply (case_tac "finite A")
  1680 apply (erule finite_induct, auto simp add: mult_ac)
  1681 done
  1682 
  1683 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1684 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1685 apply (erule ssubst, rule setprod_1)
  1686 apply (rule setprod_cong, auto)
  1687 done
  1688 
  1689 lemma setprod_Un_Int: "finite A ==> finite B
  1690     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1691 by(simp add: setprod_def fold_image_Un_Int[symmetric])
  1692 
  1693 lemma setprod_Un_disjoint: "finite A ==> finite B
  1694   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1695 by (subst setprod_Un_Int [symmetric], auto)
  1696 
  1697 lemma setprod_delta: 
  1698   assumes fS: "finite S"
  1699   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  1700 proof-
  1701   let ?f = "(\<lambda>k. if k=a then b k else 1)"
  1702   {assume a: "a \<notin> S"
  1703     hence "\<forall> k\<in> S. ?f k = 1" by simp
  1704     hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
  1705   moreover 
  1706   {assume a: "a \<in> S"
  1707     let ?A = "S - {a}"
  1708     let ?B = "{a}"
  1709     have eq: "S = ?A \<union> ?B" using a by blast 
  1710     have dj: "?A \<inter> ?B = {}" by simp
  1711     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1712     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
  1713     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1714       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1715       by simp
  1716     then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
  1717   ultimately show ?thesis by blast
  1718 qed
  1719 
  1720 lemma setprod_delta': 
  1721   assumes fS: "finite S" shows 
  1722   "setprod (\<lambda>k. if a = k then b k else 1) S = 
  1723      (if a\<in> S then b a else 1)"
  1724   using setprod_delta[OF fS, of a b, symmetric] 
  1725   by (auto intro: setprod_cong)
  1726 
  1727 
  1728 lemma setprod_UN_disjoint:
  1729     "finite I ==> (ALL i:I. finite (A i)) ==>
  1730         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1731       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1732 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
  1733 
  1734 lemma setprod_Union_disjoint:
  1735   "[| (ALL A:C. finite A);
  1736       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1737    ==> setprod f (Union C) = setprod (setprod f) C"
  1738 apply (cases "finite C") 
  1739  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1740   apply (frule setprod_UN_disjoint [of C id f])
  1741  apply (unfold Union_def id_def, assumption+)
  1742 done
  1743 
  1744 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1745     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1746     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1747 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
  1748 
  1749 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1750 lemma setprod_cartesian_product: 
  1751      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1752 apply (cases "finite A") 
  1753  apply (cases "finite B") 
  1754   apply (simp add: setprod_Sigma)
  1755  apply (cases "A={}", simp)
  1756  apply (simp add: setprod_1) 
  1757 apply (auto simp add: setprod_def
  1758             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1759 done
  1760 
  1761 lemma setprod_timesf:
  1762      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1763 by(simp add:setprod_def fold_image_distrib)
  1764 
  1765 
  1766 subsubsection {* Properties in more restricted classes of structures *}
  1767 
  1768 lemma setprod_eq_1_iff [simp]:
  1769   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1770 by (induct set: finite) auto
  1771 
  1772 lemma setprod_zero:
  1773      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1774 apply (induct set: finite, force, clarsimp)
  1775 apply (erule disjE, auto)
  1776 done
  1777 
  1778 lemma setprod_nonneg [rule_format]:
  1779    "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1780 apply (case_tac "finite A")
  1781 apply (induct set: finite, force, clarsimp)
  1782 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1783 apply (rule mult_mono, assumption+)
  1784 apply (auto simp add: setprod_def)
  1785 done
  1786 
  1787 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1788   --> 0 < setprod f A"
  1789 apply (case_tac "finite A")
  1790 apply (induct set: finite, force, clarsimp)
  1791 apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1792 apply (rule mult_strict_mono, assumption+)
  1793 apply (auto simp add: setprod_def)
  1794 done
  1795 
  1796 lemma setprod_nonzero [rule_format]:
  1797   "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
  1798     finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1799 by (erule finite_induct, auto)
  1800 
  1801 lemma setprod_zero_eq:
  1802     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
  1803      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1804 by (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1805 
  1806 lemma setprod_nonzero_field:
  1807     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
  1808 by (rule setprod_nonzero, auto)
  1809 
  1810 lemma setprod_zero_eq_field:
  1811     "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
  1812 by (rule setprod_zero_eq, auto)
  1813 
  1814 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1815   (setprod f (A Un B) :: 'a ::{field})
  1816    = setprod f A * setprod f B / setprod f (A Int B)"
  1817 apply (subst setprod_Un_Int [symmetric], auto)
  1818 apply (subgoal_tac "finite (A Int B)")
  1819 apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1820 apply (subst times_divide_eq_right [THEN sym], auto)
  1821 done
  1822 
  1823 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1824   (setprod f (A - {a}) :: 'a :: {field}) =
  1825   (if a:A then setprod f A / f a else setprod f A)"
  1826 by (erule finite_induct) (auto simp add: insert_Diff_if)
  1827 
  1828 lemma setprod_inversef: "finite A ==>
  1829   ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1830   setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1831 by (erule finite_induct) auto
  1832 
  1833 lemma setprod_dividef:
  1834    "[|finite A;
  1835       \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1836     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1837 apply (subgoal_tac
  1838          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1839 apply (erule ssubst)
  1840 apply (subst divide_inverse)
  1841 apply (subst setprod_timesf)
  1842 apply (subst setprod_inversef, assumption+, rule refl)
  1843 apply (rule setprod_cong, rule refl)
  1844 apply (subst divide_inverse, auto)
  1845 done
  1846 
  1847 lemma setprod_dvd_setprod [rule_format]: 
  1848     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1849   apply (cases "finite A")
  1850   apply (induct set: finite)
  1851   apply (auto simp add: dvd_def)
  1852   apply (rule_tac x = "k * ka" in exI)
  1853   apply (simp add: algebra_simps)
  1854 done
  1855 
  1856 lemma setprod_dvd_setprod_subset:
  1857   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1858   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1859   apply (unfold dvd_def, blast)
  1860   apply (subst setprod_Un_disjoint [symmetric])
  1861   apply (auto elim: finite_subset intro: setprod_cong)
  1862 done
  1863 
  1864 lemma setprod_dvd_setprod_subset2:
  1865   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1866       setprod f A dvd setprod g B"
  1867   apply (rule dvd_trans)
  1868   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1869   apply (erule (1) setprod_dvd_setprod_subset)
  1870 done
  1871 
  1872 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1873     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1874 by (induct set: finite) (auto intro: dvd_mult)
  1875 
  1876 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1877     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1878   apply (cases "finite A")
  1879   apply (induct set: finite)
  1880   apply auto
  1881 done
  1882 
  1883 
  1884 subsection {* Finite cardinality *}
  1885 
  1886 text {* This definition, although traditional, is ugly to work with:
  1887 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1888 But now that we have @{text setsum} things are easy:
  1889 *}
  1890 
  1891 definition card :: "'a set \<Rightarrow> nat"
  1892 where "card A = setsum (\<lambda>x. 1) A"
  1893 
  1894 lemma card_empty [simp]: "card {} = 0"
  1895 by (simp add: card_def)
  1896 
  1897 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1898 by (simp add: card_def)
  1899 
  1900 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1901 by (simp add: card_def)
  1902 
  1903 lemma card_insert_disjoint [simp]:
  1904   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1905 by(simp add: card_def)
  1906 
  1907 lemma card_insert_if:
  1908   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1909 by (simp add: insert_absorb)
  1910 
  1911 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
  1912 apply auto
  1913 apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1914 done
  1915 
  1916 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1917 by auto
  1918 
  1919 
  1920 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1921 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1922 apply(simp del:insert_Diff_single)
  1923 done
  1924 
  1925 lemma card_Diff_singleton:
  1926   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1927 by (simp add: card_Suc_Diff1 [symmetric])
  1928 
  1929 lemma card_Diff_singleton_if:
  1930   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1931 by (simp add: card_Diff_singleton)
  1932 
  1933 lemma card_Diff_insert[simp]:
  1934 assumes "finite A" and "a:A" and "a ~: B"
  1935 shows "card(A - insert a B) = card(A - B) - 1"
  1936 proof -
  1937   have "A - insert a B = (A - B) - {a}" using assms by blast
  1938   then show ?thesis using assms by(simp add:card_Diff_singleton)
  1939 qed
  1940 
  1941 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1942 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
  1943 
  1944 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1945 by (simp add: card_insert_if)
  1946 
  1947 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1948 by (simp add: card_def setsum_mono2)
  1949 
  1950 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1951 apply (induct set: finite, simp, clarify)
  1952 apply (subgoal_tac "finite A & A - {x} <= F")
  1953  prefer 2 apply (blast intro: finite_subset, atomize)
  1954 apply (drule_tac x = "A - {x}" in spec)
  1955 apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1956 apply (case_tac "card A", auto)
  1957 done
  1958 
  1959 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1960 apply (simp add: psubset_eq linorder_not_le [symmetric])
  1961 apply (blast dest: card_seteq)
  1962 done
  1963 
  1964 lemma card_Un_Int: "finite A ==> finite B
  1965     ==> card A + card B = card (A Un B) + card (A Int B)"
  1966 by(simp add:card_def setsum_Un_Int)
  1967 
  1968 lemma card_Un_disjoint: "finite A ==> finite B
  1969     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1970 by (simp add: card_Un_Int)
  1971 
  1972 lemma card_Diff_subset:
  1973   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1974 by(simp add:card_def setsum_diff_nat)
  1975 
  1976 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1977 apply (rule Suc_less_SucD)
  1978 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
  1979 done
  1980 
  1981 lemma card_Diff2_less:
  1982   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1983 apply (case_tac "x = y")
  1984  apply (simp add: card_Diff1_less del:card_Diff_insert)
  1985 apply (rule less_trans)
  1986  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
  1987 done
  1988 
  1989 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1990 apply (case_tac "x : A")
  1991  apply (simp_all add: card_Diff1_less less_imp_le)
  1992 done
  1993 
  1994 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1995 by (erule psubsetI, blast)
  1996 
  1997 lemma insert_partition:
  1998   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1999   \<Longrightarrow> x \<inter> \<Union> F = {}"
  2000 by auto
  2001 
  2002 text{* main cardinality theorem *}
  2003 lemma card_partition [rule_format]:
  2004   "finite C ==>
  2005      finite (\<Union> C) -->
  2006      (\<forall>c\<in>C. card c = k) -->
  2007      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
  2008      k * card(C) = card (\<Union> C)"
  2009 apply (erule finite_induct, simp)
  2010 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  2011        finite_subset [of _ "\<Union> (insert x F)"])
  2012 done
  2013 
  2014 
  2015 text{*The form of a finite set of given cardinality*}
  2016 
  2017 lemma card_eq_SucD:
  2018 assumes "card A = Suc k"
  2019 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
  2020 proof -
  2021   have fin: "finite A" using assms by (auto intro: ccontr)
  2022   moreover have "card A \<noteq> 0" using assms by auto
  2023   ultimately obtain b where b: "b \<in> A" by auto
  2024   show ?thesis
  2025   proof (intro exI conjI)
  2026     show "A = insert b (A-{b})" using b by blast
  2027     show "b \<notin> A - {b}" by blast
  2028     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
  2029       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
  2030   qed
  2031 qed
  2032 
  2033 lemma card_Suc_eq:
  2034   "(card A = Suc k) =
  2035    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
  2036 apply(rule iffI)
  2037  apply(erule card_eq_SucD)
  2038 apply(auto)
  2039 apply(subst card_insert)
  2040  apply(auto intro:ccontr)
  2041 done
  2042 
  2043 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  2044 apply (cases "finite A")
  2045 apply (erule finite_induct)
  2046 apply (auto simp add: algebra_simps)
  2047 done
  2048 
  2049 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
  2050 apply (erule finite_induct)
  2051 apply (auto simp add: power_Suc)
  2052 done
  2053 
  2054 lemma setprod_gen_delta:
  2055   assumes fS: "finite S"
  2056   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)"
  2057 proof-
  2058   let ?f = "(\<lambda>k. if k=a then b k else c)"
  2059   {assume a: "a \<notin> S"
  2060     hence "\<forall> k\<in> S. ?f k = c" by simp
  2061     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
  2062   moreover 
  2063   {assume a: "a \<in> S"
  2064     let ?A = "S - {a}"
  2065     let ?B = "{a}"
  2066     have eq: "S = ?A \<union> ?B" using a by blast 
  2067     have dj: "?A \<inter> ?B = {}" by simp
  2068     from fS have fAB: "finite ?A" "finite ?B" by auto  
  2069     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  2070       apply (rule setprod_cong) by auto
  2071     have cA: "card ?A = card S - 1" using fS a by auto
  2072     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  2073     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  2074       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  2075       by simp
  2076     then have ?thesis using a cA
  2077       by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
  2078   ultimately show ?thesis by blast
  2079 qed
  2080 
  2081 
  2082 lemma setsum_bounded:
  2083   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
  2084   shows "setsum f A \<le> of_nat(card A) * K"
  2085 proof (cases "finite A")
  2086   case True
  2087   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  2088 next
  2089   case False thus ?thesis by (simp add: setsum_def)
  2090 qed
  2091 
  2092 
  2093 subsubsection {* Cardinality of unions *}
  2094 
  2095 lemma card_UN_disjoint:
  2096   "finite I ==> (ALL i:I. finite (A i)) ==>
  2097    (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
  2098    ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  2099 apply (simp add: card_def del: setsum_constant)
  2100 apply (subgoal_tac
  2101          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  2102 apply (simp add: setsum_UN_disjoint del: setsum_constant)
  2103 apply (simp cong: setsum_cong)
  2104 done
  2105 
  2106 lemma card_Union_disjoint:
  2107   "finite C ==> (ALL A:C. finite A) ==>
  2108    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  2109    ==> card (Union C) = setsum card C"
  2110 apply (frule card_UN_disjoint [of C id])
  2111 apply (unfold Union_def id_def, assumption+)
  2112 done
  2113 
  2114 
  2115 subsubsection {* Cardinality of image *}
  2116 
  2117 text{*The image of a finite set can be expressed using @{term fold_image}.*}
  2118 lemma image_eq_fold_image:
  2119   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
  2120 proof (induct rule: finite_induct)
  2121   case empty then show ?case by simp
  2122 next
  2123   interpret ab_semigroup_mult "op Un"
  2124     proof qed auto
  2125   case insert 
  2126   then show ?case by simp
  2127 qed
  2128 
  2129 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  2130 apply (induct set: finite)
  2131  apply simp
  2132 apply (simp add: le_SucI finite_imageI card_insert_if)
  2133 done
  2134 
  2135 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  2136 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  2137 
  2138 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  2139 by (simp add: card_seteq card_image)
  2140 
  2141 lemma eq_card_imp_inj_on:
  2142   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  2143 apply (induct rule:finite_induct)
  2144 apply simp
  2145 apply(frule card_image_le[where f = f])
  2146 apply(simp add:card_insert_if split:if_splits)
  2147 done
  2148 
  2149 lemma inj_on_iff_eq_card:
  2150   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  2151 by(blast intro: card_image eq_card_imp_inj_on)
  2152 
  2153 
  2154 lemma card_inj_on_le:
  2155   "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  2156 apply (subgoal_tac "finite A") 
  2157  apply (force intro: card_mono simp add: card_image [symmetric])
  2158 apply (blast intro: finite_imageD dest: finite_subset) 
  2159 done
  2160 
  2161 lemma card_bij_eq:
  2162   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  2163      finite A; finite B |] ==> card A = card B"
  2164 by (auto intro: le_anti_sym card_inj_on_le)
  2165 
  2166 
  2167 subsubsection {* Cardinality of products *}
  2168 
  2169 (*
  2170 lemma SigmaI_insert: "y \<notin> A ==>
  2171   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  2172   by auto
  2173 *)
  2174 
  2175 lemma card_SigmaI [simp]:
  2176   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  2177   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  2178 by(simp add:card_def setsum_Sigma del:setsum_constant)
  2179 
  2180 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  2181 apply (cases "finite A") 
  2182 apply (cases "finite B") 
  2183 apply (auto simp add: card_eq_0_iff
  2184             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  2185 done
  2186 
  2187 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  2188 by (simp add: card_cartesian_product)
  2189 
  2190 
  2191 subsubsection {* Cardinality of sums *}
  2192 
  2193 lemma card_Plus:
  2194   assumes "finite A" and "finite B"
  2195   shows "card (A <+> B) = card A + card B"
  2196 proof -
  2197   have "Inl`A \<inter> Inr`B = {}" by fast
  2198   with assms show ?thesis
  2199     unfolding Plus_def
  2200     by (simp add: card_Un_disjoint card_image)
  2201 qed
  2202 
  2203 
  2204 subsubsection {* Cardinality of the Powerset *}
  2205 
  2206 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  2207 apply (induct set: finite)
  2208  apply (simp_all add: Pow_insert)
  2209 apply (subst card_Un_disjoint, blast)
  2210   apply (blast intro: finite_imageI, blast)
  2211 apply (subgoal_tac "inj_on (insert x) (Pow F)")
  2212  apply (simp add: card_image Pow_insert)
  2213 apply (unfold inj_on_def)
  2214 apply (blast elim!: equalityE)
  2215 done
  2216 
  2217 text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
  2218 
  2219 lemma dvd_partition:
  2220   "finite (Union C) ==>
  2221     ALL c : C. k dvd card c ==>
  2222     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  2223   k dvd card (Union C)"
  2224 apply(frule finite_UnionD)
  2225 apply(rotate_tac -1)
  2226 apply (induct set: finite, simp_all, clarify)
  2227 apply (subst card_Un_disjoint)
  2228    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  2229 done
  2230 
  2231 
  2232 subsubsection {* Relating injectivity and surjectivity *}
  2233 
  2234 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
  2235 apply(rule eq_card_imp_inj_on, assumption)
  2236 apply(frule finite_imageI)
  2237 apply(drule (1) card_seteq)
  2238  apply(erule card_image_le)
  2239 apply simp
  2240 done
  2241 
  2242 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
  2243 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
  2244 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
  2245 
  2246 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
  2247 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
  2248 by(fastsimp simp:surj_def dest!: endo_inj_surj)
  2249 
  2250 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
  2251 proof
  2252   assume "finite(UNIV::nat set)"
  2253   with finite_UNIV_inj_surj[of Suc]
  2254   show False by simp (blast dest: Suc_neq_Zero surjD)
  2255 qed
  2256 
  2257 lemma infinite_UNIV_char_0:
  2258   "\<not> finite (UNIV::'a::semiring_char_0 set)"
  2259 proof
  2260   assume "finite (UNIV::'a set)"
  2261   with subset_UNIV have "finite (range of_nat::'a set)"
  2262     by (rule finite_subset)
  2263   moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
  2264     by (simp add: inj_on_def)
  2265   ultimately have "finite (UNIV::nat set)"
  2266     by (rule finite_imageD)
  2267   then show "False"
  2268     by (simp add: infinite_UNIV_nat)
  2269 qed
  2270 
  2271 subsection{* A fold functional for non-empty sets *}
  2272 
  2273 text{* Does not require start value. *}
  2274 
  2275 inductive
  2276   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
  2277   for f :: "'a => 'a => 'a"
  2278 where
  2279   fold1Set_insertI [intro]:
  2280    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
  2281 
  2282 constdefs
  2283   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  2284   "fold1 f A == THE x. fold1Set f A x"
  2285 
  2286 lemma fold1Set_nonempty:
  2287   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
  2288 by(erule fold1Set.cases, simp_all)
  2289 
  2290 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
  2291 
  2292 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
  2293 
  2294 
  2295 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
  2296 by (blast intro: fold_graph.intros elim: fold_graph.cases)
  2297 
  2298 lemma fold1_singleton [simp]: "fold1 f {a} = a"
  2299 by (unfold fold1_def) blast
  2300 
  2301 lemma finite_nonempty_imp_fold1Set:
  2302   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
  2303 apply (induct A rule: finite_induct)
  2304 apply (auto dest: finite_imp_fold_graph [of _ f])
  2305 done
  2306 
  2307 text{*First, some lemmas about @{const fold_graph}.*}
  2308 
  2309 context ab_semigroup_mult
  2310 begin
  2311 
  2312 lemma fun_left_comm: "fun_left_comm(op *)"
  2313 by unfold_locales (simp add: mult_ac)
  2314 
  2315 lemma fold_graph_insert_swap:
  2316 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
  2317 shows "fold_graph times z (insert b A) (z * y)"
  2318 proof -
  2319   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2320 from assms show ?thesis
  2321 proof (induct rule: fold_graph.induct)
  2322   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
  2323 next
  2324   case (insertI x A y)
  2325     have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
  2326       using insertI by force  --{*how does @{term id} get unfolded?*}
  2327     thus ?case by (simp add: insert_commute mult_ac)
  2328 qed
  2329 qed
  2330 
  2331 lemma fold_graph_permute_diff:
  2332 assumes fold: "fold_graph times b A x"
  2333 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A-{a})) x"
  2334 using fold
  2335 proof (induct rule: fold_graph.induct)
  2336   case emptyI thus ?case by simp
  2337 next
  2338   case (insertI x A y)
  2339   have "a = x \<or> a \<in> A" using insertI by simp
  2340   thus ?case
  2341   proof
  2342     assume "a = x"
  2343     with insertI show ?thesis
  2344       by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)
  2345   next
  2346     assume ainA: "a \<in> A"
  2347     hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"
  2348       using insertI by force
  2349     moreover
  2350     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  2351       using ainA insertI by blast
  2352     ultimately show ?thesis by simp
  2353   qed
  2354 qed
  2355 
  2356 lemma fold1_eq_fold:
  2357 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
  2358 proof -
  2359   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2360   from assms show ?thesis
  2361 apply (simp add: fold1_def fold_def)
  2362 apply (rule the_equality)
  2363 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
  2364 apply (rule sym, clarify)
  2365 apply (case_tac "Aa=A")
  2366  apply (best intro: the_equality fold_graph_determ)
  2367 apply (subgoal_tac "fold_graph times a A x")
  2368  apply (best intro: the_equality fold_graph_determ)
  2369 apply (subgoal_tac "insert aa (Aa - {a}) = A")
  2370  prefer 2 apply (blast elim: equalityE)
  2371 apply (auto dest: fold_graph_permute_diff [where a=a])
  2372 done
  2373 qed
  2374 
  2375 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  2376 apply safe
  2377  apply simp
  2378  apply (drule_tac x=x in spec)
  2379  apply (drule_tac x="A-{x}" in spec, auto)
  2380 done
  2381 
  2382 lemma fold1_insert:
  2383   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  2384   shows "fold1 times (insert x A) = x * fold1 times A"
  2385 proof -
  2386   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
  2387   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
  2388     by (auto simp add: nonempty_iff)
  2389   with A show ?thesis
  2390     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
  2391 qed
  2392 
  2393 end
  2394 
  2395 context ab_semigroup_idem_mult
  2396 begin
  2397 
  2398 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
  2399 apply unfold_locales
  2400  apply (simp add: mult_ac)
  2401 apply (simp add: mult_idem mult_assoc[symmetric])
  2402 done
  2403 
  2404 
  2405 lemma fold1_insert_idem [simp]:
  2406   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  2407   shows "fold1 times (insert x A) = x * fold1 times A"
  2408 proof -
  2409   interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2410     by (rule fun_left_comm_idem)
  2411   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
  2412     by (auto simp add: nonempty_iff)
  2413   show ?thesis
  2414   proof cases
  2415     assume "a = x"
  2416     thus ?thesis
  2417     proof cases
  2418       assume "A' = {}"
  2419       with prems show ?thesis by (simp add: mult_idem)
  2420     next
  2421       assume "A' \<noteq> {}"
  2422       with prems show ?thesis
  2423 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
  2424     qed
  2425   next
  2426     assume "a \<noteq> x"
  2427     with prems show ?thesis
  2428       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  2429   qed
  2430 qed
  2431 
  2432 lemma hom_fold1_commute:
  2433 assumes hom: "!!x y. h (x * y) = h x * h y"
  2434 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
  2435 using N proof (induct rule: finite_ne_induct)
  2436   case singleton thus ?case by simp
  2437 next
  2438   case (insert n N)
  2439   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
  2440   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
  2441   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
  2442   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
  2443     using insert by(simp)
  2444   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  2445   finally show ?case .
  2446 qed
  2447 
  2448 end
  2449 
  2450 
  2451 text{* Now the recursion rules for definitions: *}
  2452 
  2453 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
  2454 by(simp add:fold1_singleton)
  2455 
  2456 lemma (in ab_semigroup_mult) fold1_insert_def:
  2457   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2458 by (simp add:fold1_insert)
  2459 
  2460 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
  2461   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
  2462 by simp
  2463 
  2464 subsubsection{* Determinacy for @{term fold1Set} *}
  2465 
  2466 (*Not actually used!!*)
  2467 (*
  2468 context ab_semigroup_mult
  2469 begin
  2470 
  2471 lemma fold_graph_permute:
  2472   "[|fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A|]
  2473    ==> fold_graph times id a (insert b A) x"
  2474 apply (cases "a=b") 
  2475 apply (auto dest: fold_graph_permute_diff) 
  2476 done
  2477 
  2478 lemma fold1Set_determ:
  2479   "fold1Set times A x ==> fold1Set times A y ==> y = x"
  2480 proof (clarify elim!: fold1Set.cases)
  2481   fix A x B y a b
  2482   assume Ax: "fold_graph times id a A x"
  2483   assume By: "fold_graph times id b B y"
  2484   assume anotA:  "a \<notin> A"
  2485   assume bnotB:  "b \<notin> B"
  2486   assume eq: "insert a A = insert b B"
  2487   show "y=x"
  2488   proof cases
  2489     assume same: "a=b"
  2490     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  2491     thus ?thesis using Ax By same by (blast intro: fold_graph_determ)
  2492   next
  2493     assume diff: "a\<noteq>b"
  2494     let ?D = "B - {a}"
  2495     have B: "B = insert a ?D" and A: "A = insert b ?D"
  2496      and aB: "a \<in> B" and bA: "b \<in> A"
  2497       using eq anotA bnotB diff by (blast elim!:equalityE)+
  2498     with aB bnotB By
  2499     have "fold_graph times id a (insert b ?D) y" 
  2500       by (auto intro: fold_graph_permute simp add: insert_absorb)
  2501     moreover
  2502     have "fold_graph times id a (insert b ?D) x"
  2503       by (simp add: A [symmetric] Ax) 
  2504     ultimately show ?thesis by (blast intro: fold_graph_determ) 
  2505   qed
  2506 qed
  2507 
  2508 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
  2509   by (unfold fold1_def) (blast intro: fold1Set_determ)
  2510 
  2511 end
  2512 *)
  2513 
  2514 declare
  2515   empty_fold_graphE [rule del]  fold_graph.intros [rule del]
  2516   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  2517   -- {* No more proofs involve these relations. *}
  2518 
  2519 subsubsection {* Lemmas about @{text fold1} *}
  2520 
  2521 context ab_semigroup_mult
  2522 begin
  2523 
  2524 lemma fold1_Un:
  2525 assumes A: "finite A" "A \<noteq> {}"
  2526 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2527        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2528 using A by (induct rule: finite_ne_induct)
  2529   (simp_all add: fold1_insert mult_assoc)
  2530 
  2531 lemma fold1_in:
  2532   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
  2533   shows "fold1 times A \<in> A"
  2534 using A
  2535 proof (induct rule:finite_ne_induct)
  2536   case singleton thus ?case by simp
  2537 next
  2538   case insert thus ?case using elem by (force simp add:fold1_insert)
  2539 qed
  2540 
  2541 end
  2542 
  2543 lemma (in ab_semigroup_idem_mult) fold1_Un2:
  2544 assumes A: "finite A" "A \<noteq> {}"
  2545 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2546        fold1 times (A Un B) = fold1 times A * fold1 times B"
  2547 using A
  2548 proof(induct rule:finite_ne_induct)
  2549   case singleton thus ?case by simp
  2550 next
  2551   case insert thus ?case by (simp add: mult_assoc)
  2552 qed
  2553 
  2554 
  2555 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
  2556 
  2557 text{*
  2558   As an application of @{text fold1} we define infimum
  2559   and supremum in (not necessarily complete!) lattices
  2560   over (non-empty) sets by means of @{text fold1}.
  2561 *}
  2562 
  2563 context lower_semilattice
  2564 begin
  2565 
  2566 lemma ab_semigroup_idem_mult_inf:
  2567   "ab_semigroup_idem_mult inf"
  2568   proof qed (rule inf_assoc inf_commute inf_idem)+
  2569 
  2570 lemma below_fold1_iff:
  2571   assumes "finite A" "A \<noteq> {}"
  2572   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2573 proof -
  2574   interpret ab_semigroup_idem_mult inf
  2575     by (rule ab_semigroup_idem_mult_inf)
  2576   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  2577 qed
  2578 
  2579 lemma fold1_belowI:
  2580   assumes "finite A"
  2581     and "a \<in> A"
  2582   shows "fold1 inf A \<le> a"
  2583 proof -
  2584   from assms have "A \<noteq> {}" by auto
  2585   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  2586   proof (induct rule: finite_ne_induct)
  2587     case singleton thus ?case by simp
  2588   next
  2589     interpret ab_semigroup_idem_mult inf
  2590       by (rule ab_semigroup_idem_mult_inf)
  2591     case (insert x F)
  2592     from insert(5) have "a = x \<or> a \<in> F" by simp
  2593     thus ?case
  2594     proof
  2595       assume "a = x" thus ?thesis using insert
  2596         by (simp add: mult_ac)
  2597     next
  2598       assume "a \<in> F"
  2599       hence bel: "fold1 inf F \<le> a" by (rule insert)
  2600       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  2601         using insert by (simp add: mult_ac)
  2602       also have "inf (fold1 inf F) a = fold1 inf F"
  2603         using bel by (auto intro: antisym)
  2604       also have "inf x \<dots> = fold1 inf (insert x F)"
  2605         using insert by (simp add: mult_ac)
  2606       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  2607       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  2608       ultimately show ?thesis by simp
  2609     qed
  2610   qed
  2611 qed
  2612 
  2613 end
  2614 
  2615 lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
  2616   "ab_semigroup_idem_mult sup"
  2617   by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
  2618     (rule dual_lattice)
  2619 
  2620 context lattice
  2621 begin
  2622 
  2623 definition
  2624   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
  2625 where
  2626   "Inf_fin = fold1 inf"
  2627 
  2628 definition
  2629   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
  2630 where
  2631   "Sup_fin = fold1 sup"
  2632 
  2633 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  2634 apply(unfold Sup_fin_def Inf_fin_def)
  2635 apply(subgoal_tac "EX a. a:A")
  2636 prefer 2 apply blast
  2637 apply(erule exE)
  2638 apply(rule order_trans)
  2639 apply(erule (1) fold1_belowI)
  2640 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
  2641 done
  2642 
  2643 lemma sup_Inf_absorb [simp]:
  2644   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  2645 apply(subst sup_commute)
  2646 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  2647 done
  2648 
  2649 lemma inf_Sup_absorb [simp]:
  2650   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  2651 by (simp add: Sup_fin_def inf_absorb1
  2652   lower_semilattice.fold1_belowI [OF dual_lattice])
  2653 
  2654 end
  2655 
  2656 context distrib_lattice
  2657 begin
  2658 
  2659 lemma sup_Inf1_distrib:
  2660   assumes "finite A"
  2661     and "A \<noteq> {}"
  2662   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  2663 proof -
  2664   interpret ab_semigroup_idem_mult inf
  2665     by (rule ab_semigroup_idem_mult_inf)
  2666   from assms show ?thesis
  2667     by (simp add: Inf_fin_def image_def
  2668       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  2669         (rule arg_cong [where f="fold1 inf"], blast)
  2670 qed
  2671 
  2672 lemma sup_Inf2_distrib:
  2673   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2674   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}"
  2675 using A proof (induct rule: finite_ne_induct)
  2676   case singleton thus ?case
  2677     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
  2678 next
  2679   interpret ab_semigroup_idem_mult inf
  2680     by (rule ab_semigroup_idem_mult_inf)
  2681   case (insert x A)
  2682   have finB: "finite {sup x b |b. b \<in> B}"
  2683     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  2684   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  2685   proof -
  2686     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  2687       by blast
  2688     thus ?thesis by(simp add: insert(1) B(1))
  2689   qed
  2690   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2691   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)"
  2692     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
  2693   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)
  2694   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})"
  2695     using insert by(simp add:sup_Inf1_distrib[OF B])
  2696   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})"
  2697     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  2698     using B insert
  2699     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  2700   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2701     by blast
  2702   finally show ?case .
  2703 qed
  2704 
  2705 lemma inf_Sup1_distrib:
  2706   assumes "finite A" and "A \<noteq> {}"
  2707   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  2708 proof -
  2709   interpret ab_semigroup_idem_mult sup
  2710     by (rule ab_semigroup_idem_mult_sup)
  2711   from assms show ?thesis
  2712     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  2713       (rule arg_cong [where f="fold1 sup"], blast)
  2714 qed
  2715 
  2716 lemma inf_Sup2_distrib:
  2717   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2718   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}"
  2719 using A proof (induct rule: finite_ne_induct)
  2720   case singleton thus ?case
  2721     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
  2722 next
  2723   case (insert x A)
  2724   have finB: "finite {inf x b |b. b \<in> B}"
  2725     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  2726   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  2727   proof -
  2728     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  2729       by blast
  2730     thus ?thesis by(simp add: insert(1) B(1))
  2731   qed
  2732   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2733   interpret ab_semigroup_idem_mult sup
  2734     by (rule ab_semigroup_idem_mult_sup)
  2735   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)"
  2736     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
  2737   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)
  2738   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})"
  2739     using insert by(simp add:inf_Sup1_distrib[OF B])
  2740   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})"
  2741     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  2742     using B insert
  2743     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  2744   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2745     by blast
  2746   finally show ?case .
  2747 qed
  2748 
  2749 end
  2750 
  2751 context complete_lattice
  2752 begin
  2753 
  2754 text {*
  2755   Coincidence on finite sets in complete lattices:
  2756 *}
  2757 
  2758 lemma Inf_fin_Inf:
  2759   assumes "finite A" and "A \<noteq> {}"
  2760   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  2761 proof -
  2762     interpret ab_semigroup_idem_mult inf
  2763     by (rule ab_semigroup_idem_mult_inf)
  2764   from assms show ?thesis
  2765   unfolding Inf_fin_def by (induct A set: finite)
  2766     (simp_all add: Inf_insert_simp)
  2767 qed
  2768 
  2769 lemma Sup_fin_Sup:
  2770   assumes "finite A" and "A \<noteq> {}"
  2771   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  2772 proof -
  2773   interpret ab_semigroup_idem_mult sup
  2774     by (rule ab_semigroup_idem_mult_sup)
  2775   from assms show ?thesis
  2776   unfolding Sup_fin_def by (induct A set: finite)
  2777     (simp_all add: Sup_insert_simp)
  2778 qed
  2779 
  2780 end
  2781 
  2782 
  2783 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
  2784 
  2785 text{*
  2786   As an application of @{text fold1} we define minimum
  2787   and maximum in (not necessarily complete!) linear orders
  2788   over (non-empty) sets by means of @{text fold1}.
  2789 *}
  2790 
  2791 context linorder
  2792 begin
  2793 
  2794 lemma ab_semigroup_idem_mult_min:
  2795   "ab_semigroup_idem_mult min"
  2796   proof qed (auto simp add: min_def)
  2797 
  2798 lemma ab_semigroup_idem_mult_max:
  2799   "ab_semigroup_idem_mult max"
  2800   proof qed (auto simp add: max_def)
  2801 
  2802 lemma min_lattice:
  2803   "lower_semilattice (op \<le>) (op <) min"
  2804   proof qed (auto simp add: min_def)
  2805 
  2806 lemma max_lattice:
  2807   "lower_semilattice (op \<ge>) (op >) max"
  2808   proof qed (auto simp add: max_def)
  2809 
  2810 lemma dual_max:
  2811   "ord.max (op \<ge>) = min"
  2812   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
  2813 
  2814 lemma dual_min:
  2815   "ord.min (op \<ge>) = max"
  2816   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
  2817 
  2818 lemma strict_below_fold1_iff:
  2819   assumes "finite A" and "A \<noteq> {}"
  2820   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2821 proof -
  2822   interpret ab_semigroup_idem_mult min
  2823     by (rule ab_semigroup_idem_mult_min)
  2824   from assms show ?thesis
  2825   by (induct rule: finite_ne_induct)
  2826     (simp_all add: fold1_insert)
  2827 qed
  2828 
  2829 lemma fold1_below_iff:
  2830   assumes "finite A" and "A \<noteq> {}"
  2831   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2832 proof -
  2833   interpret ab_semigroup_idem_mult min
  2834     by (rule ab_semigroup_idem_mult_min)
  2835   from assms show ?thesis
  2836   by (induct rule: finite_ne_induct)
  2837     (simp_all add: fold1_insert min_le_iff_disj)
  2838 qed
  2839 
  2840 lemma fold1_strict_below_iff:
  2841   assumes "finite A" and "A \<noteq> {}"
  2842   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2843 proof -
  2844   interpret ab_semigroup_idem_mult min
  2845     by (rule ab_semigroup_idem_mult_min)
  2846   from assms show ?thesis
  2847   by (induct rule: finite_ne_induct)
  2848     (simp_all add: fold1_insert min_less_iff_disj)
  2849 qed
  2850 
  2851 lemma fold1_antimono:
  2852   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  2853   shows "fold1 min B \<le> fold1 min A"
  2854 proof cases
  2855   assume "A = B" thus ?thesis by simp
  2856 next
  2857   interpret ab_semigroup_idem_mult min
  2858     by (rule ab_semigroup_idem_mult_min)
  2859   assume "A \<noteq> B"
  2860   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  2861   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  2862   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  2863   proof -
  2864     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  2865     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  2866     moreover have "(B-A) \<noteq> {}" using prems by blast
  2867     moreover have "A Int (B-A) = {}" using prems by blast
  2868     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  2869   qed
  2870   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  2871   finally show ?thesis .
  2872 qed
  2873 
  2874 definition
  2875   Min :: "'a set \<Rightarrow> 'a"
  2876 where
  2877   "Min = fold1 min"
  2878 
  2879 definition
  2880   Max :: "'a set \<Rightarrow> 'a"
  2881 where
  2882   "Max = fold1 max"
  2883 
  2884 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
  2885 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
  2886 
  2887 lemma Min_insert [simp]:
  2888   assumes "finite A" and "A \<noteq> {}"
  2889   shows "Min (insert x A) = min x (Min A)"
  2890 proof -
  2891   interpret ab_semigroup_idem_mult min
  2892     by (rule ab_semigroup_idem_mult_min)
  2893   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
  2894 qed
  2895 
  2896 lemma Max_insert [simp]:
  2897   assumes "finite A" and "A \<noteq> {}"
  2898   shows "Max (insert x A) = max x (Max A)"
  2899 proof -
  2900   interpret ab_semigroup_idem_mult max
  2901     by (rule ab_semigroup_idem_mult_max)
  2902   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
  2903 qed
  2904 
  2905 lemma Min_in [simp]:
  2906   assumes "finite A" and "A \<noteq> {}"
  2907   shows "Min A \<in> A"
  2908 proof -
  2909   interpret ab_semigroup_idem_mult min
  2910     by (rule ab_semigroup_idem_mult_min)
  2911   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
  2912 qed
  2913 
  2914 lemma Max_in [simp]:
  2915   assumes "finite A" and "A \<noteq> {}"
  2916   shows "Max A \<in> A"
  2917 proof -
  2918   interpret ab_semigroup_idem_mult max
  2919     by (rule ab_semigroup_idem_mult_max)
  2920   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
  2921 qed
  2922 
  2923 lemma Min_Un:
  2924   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2925   shows "Min (A \<union> B) = min (Min A) (Min B)"
  2926 proof -
  2927   interpret ab_semigroup_idem_mult min
  2928     by (rule ab_semigroup_idem_mult_min)
  2929   from assms show ?thesis
  2930     by (simp add: Min_def fold1_Un2)
  2931 qed
  2932 
  2933 lemma Max_Un:
  2934   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2935   shows "Max (A \<union> B) = max (Max A) (Max B)"
  2936 proof -
  2937   interpret ab_semigroup_idem_mult max
  2938     by (rule ab_semigroup_idem_mult_max)
  2939   from assms show ?thesis
  2940     by (simp add: Max_def fold1_Un2)
  2941 qed
  2942 
  2943 lemma hom_Min_commute:
  2944   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  2945     and "finite N" and "N \<noteq> {}"
  2946   shows "h (Min N) = Min (h ` N)"
  2947 proof -
  2948   interpret ab_semigroup_idem_mult min
  2949     by (rule ab_semigroup_idem_mult_min)
  2950   from assms show ?thesis
  2951     by (simp add: Min_def hom_fold1_commute)
  2952 qed
  2953 
  2954 lemma hom_Max_commute:
  2955   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  2956     and "finite N" and "N \<noteq> {}"
  2957   shows "h (Max N) = Max (h ` N)"
  2958 proof -
  2959   interpret ab_semigroup_idem_mult max
  2960     by (rule ab_semigroup_idem_mult_max)
  2961   from assms show ?thesis
  2962     by (simp add: Max_def hom_fold1_commute [of h])
  2963 qed
  2964 
  2965 lemma Min_le [simp]:
  2966   assumes "finite A" and "x \<in> A"
  2967   shows "Min A \<le> x"
  2968 proof -
  2969   interpret lower_semilattice "op \<le>" "op <" min
  2970     by (rule min_lattice)
  2971   from assms show ?thesis by (simp add: Min_def fold1_belowI)
  2972 qed
  2973 
  2974 lemma Max_ge [simp]:
  2975   assumes "finite A" and "x \<in> A"
  2976   shows "x \<le> Max A"
  2977 proof -
  2978   interpret lower_semilattice "op \<ge>" "op >" max
  2979     by (rule max_lattice)
  2980   from assms show ?thesis by (simp add: Max_def fold1_belowI)
  2981 qed
  2982 
  2983 lemma Min_ge_iff [simp, noatp]:
  2984   assumes "finite A" and "A \<noteq> {}"
  2985   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2986 proof -
  2987   interpret lower_semilattice "op \<le>" "op <" min
  2988     by (rule min_lattice)
  2989   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
  2990 qed
  2991 
  2992 lemma Max_le_iff [simp, noatp]:
  2993   assumes "finite A" and "A \<noteq> {}"
  2994   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2995 proof -
  2996   interpret lower_semilattice "op \<ge>" "op >" max
  2997     by (rule max_lattice)
  2998   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
  2999 qed
  3000 
  3001 lemma Min_gr_iff [simp, noatp]:
  3002   assumes "finite A" and "A \<noteq> {}"
  3003   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  3004 proof -
  3005   interpret lower_semilattice "op \<le>" "op <" min
  3006     by (rule min_lattice)
  3007   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
  3008 qed
  3009 
  3010 lemma Max_less_iff [simp, noatp]:
  3011   assumes "finite A" and "A \<noteq> {}"
  3012   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  3013 proof -
  3014   note Max = Max_def
  3015   interpret linorder "op \<ge>" "op >"
  3016     by (rule dual_linorder)
  3017   from assms show ?thesis
  3018     by (simp add: Max strict_below_fold1_iff [folded dual_max])
  3019 qed
  3020 
  3021 lemma Min_le_iff [noatp]:
  3022   assumes "finite A" and "A \<noteq> {}"
  3023   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  3024 proof -
  3025   interpret lower_semilattice "op \<le>" "op <" min
  3026     by (rule min_lattice)
  3027   from assms show ?thesis
  3028     by (simp add: Min_def fold1_below_iff)
  3029 qed
  3030 
  3031 lemma Max_ge_iff [noatp]:
  3032   assumes "finite A" and "A \<noteq> {}"
  3033   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  3034 proof -
  3035   note Max = Max_def
  3036   interpret linorder "op \<ge>" "op >"
  3037     by (rule dual_linorder)
  3038   from assms show ?thesis
  3039     by (simp add: Max fold1_below_iff [folded dual_max])
  3040 qed
  3041 
  3042 lemma Min_less_iff [noatp]:
  3043   assumes "finite A" and "A \<noteq> {}"
  3044   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  3045 proof -
  3046   interpret lower_semilattice "op \<le>" "op <" min
  3047     by (rule min_lattice)
  3048   from assms show ?thesis
  3049     by (simp add: Min_def fold1_strict_below_iff)
  3050 qed
  3051 
  3052 lemma Max_gr_iff [noatp]:
  3053   assumes "finite A" and "A \<noteq> {}"
  3054   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  3055 proof -
  3056   note Max = Max_def
  3057   interpret linorder "op \<ge>" "op >"
  3058     by (rule dual_linorder)
  3059   from assms show ?thesis
  3060     by (simp add: Max fold1_strict_below_iff [folded dual_max])
  3061 qed
  3062 
  3063 lemma Min_eqI:
  3064   assumes "finite A"
  3065   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  3066     and "x \<in> A"
  3067   shows "Min A = x"
  3068 proof (rule antisym)
  3069   from `x \<in> A` have "A \<noteq> {}" by auto
  3070   with assms show "Min A \<ge> x" by simp
  3071 next
  3072   from assms show "x \<ge> Min A" by simp
  3073 qed
  3074 
  3075 lemma Max_eqI:
  3076   assumes "finite A"
  3077   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  3078     and "x \<in> A"
  3079   shows "Max A = x"
  3080 proof (rule antisym)
  3081   from `x \<in> A` have "A \<noteq> {}" by auto
  3082   with assms show "Max A \<le> x" by simp
  3083 next
  3084   from assms show "x \<le> Max A" by simp
  3085 qed
  3086 
  3087 lemma Min_antimono:
  3088   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  3089   shows "Min N \<le> Min M"
  3090 proof -
  3091   interpret distrib_lattice "op \<le>" "op <" min max
  3092     by (rule distrib_lattice_min_max)
  3093   from assms show ?thesis by (simp add: Min_def fold1_antimono)
  3094 qed
  3095 
  3096 lemma Max_mono:
  3097   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  3098   shows "Max M \<le> Max N"
  3099 proof -
  3100   note Max = Max_def
  3101   interpret linorder "op \<ge>" "op >"
  3102     by (rule dual_linorder)
  3103   from assms show ?thesis
  3104     by (simp add: Max fold1_antimono [folded dual_max])
  3105 qed
  3106 
  3107 lemma finite_linorder_induct[consumes 1, case_names empty insert]:
  3108  "finite A \<Longrightarrow> P {} \<Longrightarrow>
  3109   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
  3110   \<Longrightarrow> P A"
  3111 proof (induct A rule: measure_induct_rule[where f=card])
  3112   fix A :: "'a set"
  3113   assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
  3114                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
  3115                   \<Longrightarrow> P B"
  3116   and "finite A" and "P {}"
  3117   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
  3118   show "P A"
  3119   proof (cases "A = {}")
  3120     assume "A = {}" thus "P A" using `P {}` by simp
  3121   next
  3122     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
  3123     assume "A \<noteq> {}"
  3124     with `finite A` have "Max A : A" by auto
  3125     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
  3126     note card_Diff1_less[OF `finite A` `Max A : A`]
  3127     moreover have "finite ?B" using `finite A` by simp
  3128     ultimately have "P ?B" using `P {}` step IH by blast
  3129     moreover have "\<forall>a\<in>?B. a < Max A"
  3130       using Max_ge [OF `finite A`] by fastsimp
  3131     ultimately show "P A"
  3132       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
  3133   qed
  3134 qed
  3135 
  3136 end
  3137 
  3138 context ordered_ab_semigroup_add
  3139 begin
  3140 
  3141 lemma add_Min_commute:
  3142   fixes k
  3143   assumes "finite N" and "N \<noteq> {}"
  3144   shows "k + Min N = Min {k + m | m. m \<in> N}"
  3145 proof -
  3146   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  3147     by (simp add: min_def not_le)
  3148       (blast intro: antisym less_imp_le add_left_mono)
  3149   with assms show ?thesis
  3150     using hom_Min_commute [of "plus k" N]
  3151     by simp (blast intro: arg_cong [where f = Min])
  3152 qed
  3153 
  3154 lemma add_Max_commute:
  3155   fixes k
  3156   assumes "finite N" and "N \<noteq> {}"
  3157   shows "k + Max N = Max {k + m | m. m \<in> N}"
  3158 proof -
  3159   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  3160     by (simp add: max_def not_le)
  3161       (blast intro: antisym less_imp_le add_left_mono)
  3162   with assms show ?thesis
  3163     using hom_Max_commute [of "plus k" N]
  3164     by simp (blast intro: arg_cong [where f = Max])
  3165 qed
  3166 
  3167 end
  3168 
  3169 end