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