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