src/HOL/Finite_Set.thy
author nipkow
Thu Jul 07 12:39:17 2005 +0200 (2005-07-07)
changeset 16733 236dfafbeb63
parent 16632 ad2895beef79
child 16760 5c5f051aaaaa
permissions -rw-r--r--
linear arithmetic now takes "&" in assumptions apart.
     1 (*  Title:      HOL/Finite_Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4                 Additions by Jeremy Avigad in Feb 2004
     5 *)
     6 
     7 header {* Finite sets *}
     8 
     9 theory Finite_Set
    10 imports Divides Power Inductive Lattice_Locales
    11 begin
    12 
    13 subsection {* Definition and basic properties *}
    14 
    15 consts Finites :: "'a set set"
    16 syntax
    17   finite :: "'a set => bool"
    18 translations
    19   "finite A" == "A : Finites"
    20 
    21 inductive Finites
    22   intros
    23     emptyI [simp, intro!]: "{} : Finites"
    24     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    25 
    26 axclass finite \<subseteq> type
    27   finite: "finite UNIV"
    28 
    29 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    30   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    31   shows "\<exists>a::'a. a \<notin> A"
    32 proof -
    33   from prems have "A \<noteq> UNIV" by blast
    34   thus ?thesis by blast
    35 qed
    36 
    37 lemma finite_induct [case_names empty insert, induct set: Finites]:
    38   "finite F ==>
    39     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    40   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    41 proof -
    42   assume "P {}" and
    43     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    44   assume "finite F"
    45   thus "P F"
    46   proof induct
    47     show "P {}" .
    48     fix x F assume F: "finite F" and P: "P F"
    49     show "P (insert x F)"
    50     proof cases
    51       assume "x \<in> F"
    52       hence "insert x F = F" by (rule insert_absorb)
    53       with P show ?thesis by (simp only:)
    54     next
    55       assume "x \<notin> F"
    56       from F this P show ?thesis by (rule insert)
    57     qed
    58   qed
    59 qed
    60 
    61 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
    62 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
    63  \<lbrakk> \<And>x. P{x};
    64    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    65  \<Longrightarrow> P F"
    66 using fin
    67 proof induct
    68   case empty thus ?case by simp
    69 next
    70   case (insert x F)
    71   show ?case
    72   proof cases
    73     assume "F = {}" thus ?thesis using insert(4) by simp
    74   next
    75     assume "F \<noteq> {}" thus ?thesis using insert by blast
    76   qed
    77 qed
    78 
    79 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    80   "finite F ==> F \<subseteq> A ==>
    81     P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    82     P F"
    83 proof -
    84   assume "P {}" and insert:
    85     "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    86   assume "finite F"
    87   thus "F \<subseteq> A ==> P F"
    88   proof induct
    89     show "P {}" .
    90     fix x F assume "finite F" and "x \<notin> F"
    91       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    92     show "P (insert x F)"
    93     proof (rule insert)
    94       from i show "x \<in> A" by blast
    95       from i have "F \<subseteq> A" by blast
    96       with P show "P F" .
    97     qed
    98   qed
    99 qed
   100 
   101 text{* Finite sets are the images of initial segments of natural numbers: *}
   102 
   103 lemma finite_imp_nat_seg_image_inj_on:
   104   assumes fin: "finite A" 
   105   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
   106 using fin
   107 proof induct
   108   case empty
   109   show ?case  
   110   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 
   111   qed
   112 next
   113   case (insert a A)
   114   have notinA: "a \<notin> A" .
   115   from insert.hyps obtain n f
   116     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
   117   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
   118         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
   119     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
   120   thus ?case by blast
   121 qed
   122 
   123 lemma nat_seg_image_imp_finite:
   124   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
   125 proof (induct n)
   126   case 0 thus ?case by simp
   127 next
   128   case (Suc n)
   129   let ?B = "f ` {i. i < n}"
   130   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
   131   show ?case
   132   proof cases
   133     assume "\<exists>k<n. f n = f k"
   134     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
   135     thus ?thesis using finB by simp
   136   next
   137     assume "\<not>(\<exists> k<n. f n = f k)"
   138     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
   139     thus ?thesis using finB by simp
   140   qed
   141 qed
   142 
   143 lemma finite_conv_nat_seg_image:
   144   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
   145 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
   146 
   147 subsubsection{* Finiteness and set theoretic constructions *}
   148 
   149 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
   150   -- {* The union of two finite sets is finite. *}
   151   by (induct set: Finites) simp_all
   152 
   153 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
   154   -- {* Every subset of a finite set is finite. *}
   155 proof -
   156   assume "finite B"
   157   thus "!!A. A \<subseteq> B ==> finite A"
   158   proof induct
   159     case empty
   160     thus ?case by simp
   161   next
   162     case (insert x F A)
   163     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
   164     show "finite A"
   165     proof cases
   166       assume x: "x \<in> A"
   167       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
   168       with r have "finite (A - {x})" .
   169       hence "finite (insert x (A - {x}))" ..
   170       also have "insert x (A - {x}) = A" by (rule insert_Diff)
   171       finally show ?thesis .
   172     next
   173       show "A \<subseteq> F ==> ?thesis" .
   174       assume "x \<notin> A"
   175       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   176     qed
   177   qed
   178 qed
   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   "finite A ==>
   198   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
   199 proof -
   200   assume "finite A"
   201     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   202   have "P (A - A)"
   203   proof -
   204     fix c b :: "'a set"
   205     presume c: "finite c" and b: "finite b"
   206       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   207     from c show "c \<subseteq> b ==> P (b - c)"
   208     proof induct
   209       case empty
   210       from P1 show ?case by simp
   211     next
   212       case (insert x F)
   213       have "P (b - F - {x})"
   214       proof (rule P2)
   215         from _ b show "finite (b - F)" by (rule finite_subset) blast
   216         from insert show "x \<in> b - F" by simp
   217         from insert show "P (b - F)" by simp
   218       qed
   219       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   220       finally show ?case .
   221     qed
   222   next
   223     show "A \<subseteq> A" ..
   224   qed
   225   thus "P {}" by simp
   226 qed
   227 
   228 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   229   by (rule Diff_subset [THEN finite_subset])
   230 
   231 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   232   apply (subst Diff_insert)
   233   apply (case_tac "a : A - B")
   234    apply (rule finite_insert [symmetric, THEN trans])
   235    apply (subst insert_Diff, simp_all)
   236   done
   237 
   238 
   239 text {* Image and Inverse Image over Finite Sets *}
   240 
   241 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   242   -- {* The image of a finite set is finite. *}
   243   by (induct set: Finites) simp_all
   244 
   245 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   246   apply (frule finite_imageI)
   247   apply (erule finite_subset, assumption)
   248   done
   249 
   250 lemma finite_range_imageI:
   251     "finite (range g) ==> finite (range (%x. f (g x)))"
   252   apply (drule finite_imageI, simp)
   253   done
   254 
   255 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   256 proof -
   257   have aux: "!!A. finite (A - {}) = finite A" by simp
   258   fix B :: "'a set"
   259   assume "finite B"
   260   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   261     apply induct
   262      apply simp
   263     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   264      apply clarify
   265      apply (simp (no_asm_use) add: inj_on_def)
   266      apply (blast dest!: aux [THEN iffD1], atomize)
   267     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   268     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   269     apply (rule_tac x = xa in bexI)
   270      apply (simp_all add: inj_on_image_set_diff)
   271     done
   272 qed (rule refl)
   273 
   274 
   275 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   276   -- {* The inverse image of a singleton under an injective function
   277          is included in a singleton. *}
   278   apply (auto simp add: inj_on_def)
   279   apply (blast intro: the_equality [symmetric])
   280   done
   281 
   282 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   283   -- {* The inverse image of a finite set under an injective function
   284          is finite. *}
   285   apply (induct set: Finites, simp_all)
   286   apply (subst vimage_insert)
   287   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   288   done
   289 
   290 
   291 text {* The finite UNION of finite sets *}
   292 
   293 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   294   by (induct set: Finites) simp_all
   295 
   296 text {*
   297   Strengthen RHS to
   298   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   299 
   300   We'd need to prove
   301   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   302   by induction. *}
   303 
   304 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   305   by (blast intro: finite_UN_I finite_subset)
   306 
   307 
   308 text {* Sigma of finite sets *}
   309 
   310 lemma finite_SigmaI [simp]:
   311     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   312   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   313 
   314 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   315     finite (A <*> B)"
   316   by (rule finite_SigmaI)
   317 
   318 lemma finite_Prod_UNIV:
   319     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   320   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   321    apply (erule ssubst)
   322    apply (erule finite_SigmaI, auto)
   323   done
   324 
   325 lemma finite_cartesian_productD1:
   326      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
   327 apply (auto simp add: finite_conv_nat_seg_image) 
   328 apply (drule_tac x=n in spec) 
   329 apply (drule_tac x="fst o f" in spec) 
   330 apply (auto simp add: o_def) 
   331  prefer 2 apply (force dest!: equalityD2) 
   332 apply (drule equalityD1) 
   333 apply (rename_tac y x)
   334 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   335  prefer 2 apply force
   336 apply clarify
   337 apply (rule_tac x=k in image_eqI, auto)
   338 done
   339 
   340 lemma finite_cartesian_productD2:
   341      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
   342 apply (auto simp add: finite_conv_nat_seg_image) 
   343 apply (drule_tac x=n in spec) 
   344 apply (drule_tac x="snd o f" in spec) 
   345 apply (auto simp add: o_def) 
   346  prefer 2 apply (force dest!: equalityD2) 
   347 apply (drule equalityD1)
   348 apply (rename_tac x y)
   349 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   350  prefer 2 apply force
   351 apply clarify
   352 apply (rule_tac x=k in image_eqI, auto)
   353 done
   354 
   355 
   356 instance unit :: finite
   357 proof
   358   have "finite {()}" by simp
   359   also have "{()} = UNIV" by auto
   360   finally show "finite (UNIV :: unit set)" .
   361 qed
   362 
   363 instance * :: (finite, finite) finite
   364 proof
   365   show "finite (UNIV :: ('a \<times> 'b) set)"
   366   proof (rule finite_Prod_UNIV)
   367     show "finite (UNIV :: 'a set)" by (rule finite)
   368     show "finite (UNIV :: 'b set)" by (rule finite)
   369   qed
   370 qed
   371 
   372 
   373 text {* The powerset of a finite set *}
   374 
   375 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   376 proof
   377   assume "finite (Pow A)"
   378   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   379   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   380 next
   381   assume "finite A"
   382   thus "finite (Pow A)"
   383     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   384 qed
   385 
   386 
   387 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   388 by(blast intro: finite_subset[OF subset_Pow_Union])
   389 
   390 
   391 lemma finite_converse [iff]: "finite (r^-1) = finite r"
   392   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   393    apply simp
   394    apply (rule iffI)
   395     apply (erule finite_imageD [unfolded inj_on_def])
   396     apply (simp split add: split_split)
   397    apply (erule finite_imageI)
   398   apply (simp add: converse_def image_def, auto)
   399   apply (rule bexI)
   400    prefer 2 apply assumption
   401   apply simp
   402   done
   403 
   404 
   405 text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
   406 Ehmety) *}
   407 
   408 lemma finite_Field: "finite r ==> finite (Field r)"
   409   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   410   apply (induct set: Finites)
   411    apply (auto simp add: Field_def Domain_insert Range_insert)
   412   done
   413 
   414 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   415   apply clarify
   416   apply (erule trancl_induct)
   417    apply (auto simp add: Field_def)
   418   done
   419 
   420 lemma finite_trancl: "finite (r^+) = finite r"
   421   apply auto
   422    prefer 2
   423    apply (rule trancl_subset_Field2 [THEN finite_subset])
   424    apply (rule finite_SigmaI)
   425     prefer 3
   426     apply (blast intro: r_into_trancl' finite_subset)
   427    apply (auto simp add: finite_Field)
   428   done
   429 
   430 
   431 subsection {* A fold functional for finite sets *}
   432 
   433 text {* The intended behaviour is
   434 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"}
   435 if @{text f} is associative-commutative. For an application of @{text fold}
   436 se the definitions of sums and products over finite sets.
   437 *}
   438 
   439 consts
   440   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
   441 
   442 inductive "foldSet f g z"
   443 intros
   444 emptyI [intro]: "({}, z) : foldSet f g z"
   445 insertI [intro]:
   446      "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
   447       \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
   448 
   449 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
   450 
   451 constdefs
   452   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   453   "fold f g z A == THE x. (A, x) : foldSet f g z"
   454 
   455 text{*A tempting alternative for the definiens is
   456 @{term "if finite A then THE x. (A, x) : foldSet f g e else e"}.
   457 It allows the removal of finiteness assumptions from the theorems
   458 @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}.
   459 The proofs become ugly, with @{text rule_format}. It is not worth the effort.*}
   460 
   461 
   462 lemma Diff1_foldSet:
   463   "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z"
   464 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   465 
   466 lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A"
   467   by (induct set: foldSet) auto
   468 
   469 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z"
   470   by (induct set: Finites) auto
   471 
   472 
   473 subsubsection {* Commutative monoids *}
   474 
   475 locale ACf =
   476   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   477   assumes commute: "x \<cdot> y = y \<cdot> x"
   478     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   479 
   480 locale ACe = ACf +
   481   fixes e :: 'a
   482   assumes ident [simp]: "x \<cdot> e = x"
   483 
   484 locale ACIf = ACf +
   485   assumes idem: "x \<cdot> x = x"
   486 
   487 lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   488 proof -
   489   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   490   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   491   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   492   finally show ?thesis .
   493 qed
   494 
   495 lemmas (in ACf) AC = assoc commute left_commute
   496 
   497 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   498 proof -
   499   have "x \<cdot> e = x" by (rule ident)
   500   thus ?thesis by (subst commute)
   501 qed
   502 
   503 lemma (in ACIf) idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y"
   504 proof -
   505   have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc)
   506   also have "\<dots> = x \<cdot> y" by(simp add:idem)
   507   finally show ?thesis .
   508 qed
   509 
   510 lemmas (in ACIf) ACI = AC idem idem2
   511 
   512 text{* Interpretation of locales: *}
   513 
   514 interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
   515 by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
   516 
   517 interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
   518   apply -
   519    apply (fast intro: ACf.intro mult_assoc mult_commute)
   520   apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute)
   521   done
   522 
   523 
   524 subsubsection{*From @{term foldSet} to @{term fold}*}
   525 
   526 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   527 by (auto simp add: less_Suc_eq) 
   528 
   529 lemma insert_image_inj_on_eq:
   530      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
   531         inj_on h {i. i < Suc m}|] 
   532       ==> A = h ` {i. i < m}"
   533 apply (auto simp add: image_less_Suc inj_on_def)
   534 apply (blast intro: less_trans) 
   535 done
   536 
   537 lemma insert_inj_onE:
   538   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
   539       and inj_on: "inj_on h {i::nat. i<n}"
   540   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
   541 proof (cases n)
   542   case 0 thus ?thesis using aA by auto
   543 next
   544   case (Suc m)
   545   have nSuc: "n = Suc m" . 
   546   have mlessn: "m<n" by (simp add: nSuc)
   547   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   548   let ?hm = "swap k m h"
   549   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
   550     by (simp add: inj_on_swap_iff inj_on)
   551   show ?thesis
   552   proof (intro exI conjI)
   553     show "inj_on ?hm {i. i < m}" using inj_hm
   554       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   555     show "m<n" by (rule mlessn)
   556     show "A = ?hm ` {i. i < m}" 
   557     proof (rule insert_image_inj_on_eq)
   558       show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
   559       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   560       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   561 	using aA hkeq nSuc klessn
   562 	by (auto simp add: swap_def image_less_Suc fun_upd_image 
   563 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
   564     qed
   565   qed
   566 qed
   567 
   568 lemma (in ACf) foldSet_determ_aux:
   569   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   570                 (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
   571    \<Longrightarrow> x' = x"
   572 proof (induct n rule: less_induct)
   573   case (less n)
   574     have IH: "!!m h A x x'. 
   575                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   576                 (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" .
   577     have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z"
   578      and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
   579     show ?case
   580     proof (rule foldSet.cases [OF Afoldx])
   581       assume "(A, x) = ({}, z)"
   582       with Afoldx' show "x' = x" by blast
   583     next
   584       fix B b u
   585       assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B"
   586          and Bu: "(B,u) \<in> foldSet f g z"
   587       hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto
   588       show "x'=x" 
   589       proof (rule foldSet.cases [OF Afoldx'])
   590         assume "(A, x') = ({}, z)"
   591         with AbB show "x' = x" by blast
   592       next
   593 	fix C c v
   594 	assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C"
   595 	   and Cv: "(C,v) \<in> foldSet f g z"
   596 	hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto
   597 	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   598         from insert_inj_onE [OF Beq notinB injh]
   599         obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   600                      and Beq: "B = hB ` {i. i < mB}"
   601                      and lessB: "mB < n" by auto 
   602 	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   603         from insert_inj_onE [OF Ceq notinC injh]
   604         obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   605                        and Ceq: "C = hC ` {i. i < mC}"
   606                        and lessC: "mC < n" by auto 
   607 	show "x'=x"
   608 	proof cases
   609           assume "b=c"
   610 	  then moreover have "B = C" using AbB AcC notinB notinC by auto
   611 	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
   612             by auto
   613 	next
   614 	  assume diff: "b \<noteq> c"
   615 	  let ?D = "B - {c}"
   616 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   617 	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   618 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   619 	  with AbB have "finite ?D" by simp
   620 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   621 	    using finite_imp_foldSet by rules
   622 	  moreover have cinB: "c \<in> B" using B by auto
   623 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   624 	    by(rule Diff1_foldSet)
   625 	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   626           moreover have "g b \<cdot> d = v"
   627 	  proof (rule IH[OF lessC Ceq inj_onC Cv])
   628 	    show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   629 	      by fastsimp
   630 	  qed
   631 	  ultimately show ?thesis using x x' by (auto simp: AC)
   632 	qed
   633       qed
   634     qed
   635   qed
   636 
   637 
   638 lemma (in ACf) foldSet_determ:
   639   "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x"
   640 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   641 apply (blast intro: foldSet_determ_aux [rule_format])
   642 done
   643 
   644 lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
   645   by (unfold fold_def) (blast intro: foldSet_determ)
   646 
   647 text{* The base case for @{text fold}: *}
   648 
   649 lemma fold_empty [simp]: "fold f g z {} = z"
   650   by (unfold fold_def) blast
   651 
   652 lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   653     ((insert x A, v) : foldSet f g z) =
   654     (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
   655   apply auto
   656   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   657    apply (fastsimp dest: foldSet_imp_finite)
   658   apply (blast intro: foldSet_determ)
   659   done
   660 
   661 text{* The recursion equation for @{text fold}: *}
   662 
   663 lemma (in ACf) fold_insert[simp]:
   664     "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
   665   apply (unfold fold_def)
   666   apply (simp add: fold_insert_aux)
   667   apply (rule the_equality)
   668   apply (auto intro: finite_imp_foldSet
   669     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   670   done
   671 
   672 lemma (in ACf) fold_rec:
   673 assumes fin: "finite A" and a: "a:A"
   674 shows "fold f g z A = f (g a) (fold f g z (A - {a}))"
   675 proof-
   676   have A: "A = insert a (A - {a})" using a by blast
   677   hence "fold f g z A = fold f g z (insert a (A - {a}))" by simp
   678   also have "\<dots> = f (g a) (fold f g z (A - {a}))"
   679     by(rule fold_insert) (simp add:fin)+
   680   finally show ?thesis .
   681 qed
   682 
   683 
   684 text{* A simplified version for idempotent functions: *}
   685 
   686 lemma (in ACIf) fold_insert_idem:
   687 assumes finA: "finite A"
   688 shows "fold f g z (insert a A) = g a \<cdot> fold f g z A"
   689 proof cases
   690   assume "a \<in> A"
   691   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   692     by(blast dest: mk_disjoint_insert)
   693   show ?thesis
   694   proof -
   695     from finA A have finB: "finite B" by(blast intro: finite_subset)
   696     have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
   697     also have "\<dots> = (g a) \<cdot> (fold f g z B)"
   698       using finB disj by simp
   699     also have "\<dots> = g a \<cdot> fold f g z A"
   700       using A finB disj by(simp add:idem assoc[symmetric])
   701     finally show ?thesis .
   702   qed
   703 next
   704   assume "a \<notin> A"
   705   with finA show ?thesis by simp
   706 qed
   707 
   708 lemma (in ACIf) foldI_conv_id:
   709   "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
   710 by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
   711 
   712 subsubsection{*Lemmas about @{text fold}*}
   713 
   714 lemma (in ACf) fold_commute:
   715   "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
   716   apply (induct set: Finites, simp)
   717   apply (simp add: left_commute [of x])
   718   done
   719 
   720 lemma (in ACf) fold_nest_Un_Int:
   721   "finite A ==> finite B
   722     ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   723   apply (induct set: Finites, simp)
   724   apply (simp add: fold_commute Int_insert_left insert_absorb)
   725   done
   726 
   727 lemma (in ACf) fold_nest_Un_disjoint:
   728   "finite A ==> finite B ==> A Int B = {}
   729     ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
   730   by (simp add: fold_nest_Un_Int)
   731 
   732 lemma (in ACf) fold_reindex:
   733 assumes fin: "finite A"
   734 shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
   735 using fin apply induct
   736  apply simp
   737 apply simp
   738 done
   739 
   740 lemma (in ACe) fold_Un_Int:
   741   "finite A ==> finite B ==>
   742     fold f g e A \<cdot> fold f g e B =
   743     fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   744   apply (induct set: Finites, simp)
   745   apply (simp add: AC insert_absorb Int_insert_left)
   746   done
   747 
   748 corollary (in ACe) fold_Un_disjoint:
   749   "finite A ==> finite B ==> A Int B = {} ==>
   750     fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   751   by (simp add: fold_Un_Int)
   752 
   753 lemma (in ACe) fold_UN_disjoint:
   754   "\<lbrakk> finite I; ALL i:I. finite (A i);
   755      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   756    \<Longrightarrow> fold f g e (UNION I A) =
   757        fold f (%i. fold f g e (A i)) e I"
   758   apply (induct set: Finites, simp, atomize)
   759   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   760    prefer 2 apply blast
   761   apply (subgoal_tac "A x Int UNION F A = {}")
   762    prefer 2 apply blast
   763   apply (simp add: fold_Un_disjoint)
   764   done
   765 
   766 text{*Fusion theorem, as described in
   767 Graham Hutton's paper,
   768 A Tutorial on the Universality and Expressiveness of Fold,
   769 JFP 9:4 (355-372), 1999.*}
   770 lemma (in ACf) fold_fusion:
   771       includes ACf g
   772       shows
   773 	"finite A ==> 
   774 	 (!!x y. h (g x y) = f x (h y)) ==>
   775          h (fold g j w A) = fold f j (h w) A"
   776   by (induct set: Finites, simp_all)
   777 
   778 lemma (in ACf) fold_cong:
   779   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   780   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
   781    apply simp
   782   apply (erule finite_induct, simp)
   783   apply (simp add: subset_insert_iff, clarify)
   784   apply (subgoal_tac "finite C")
   785    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   786   apply (subgoal_tac "C = insert x (C - {x})")
   787    prefer 2 apply blast
   788   apply (erule ssubst)
   789   apply (drule spec)
   790   apply (erule (1) notE impE)
   791   apply (simp add: Ball_def del: insert_Diff_single)
   792   done
   793 
   794 lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   795   fold f (%x. fold f (g x) e (B x)) e A =
   796   fold f (split g) e (SIGMA x:A. B x)"
   797 apply (subst Sigma_def)
   798 apply (subst fold_UN_disjoint, assumption, simp)
   799  apply blast
   800 apply (erule fold_cong)
   801 apply (subst fold_UN_disjoint, simp, simp)
   802  apply blast
   803 apply simp
   804 done
   805 
   806 lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   807    fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   808 apply (erule finite_induct, simp)
   809 apply (simp add:AC)
   810 done
   811 
   812 
   813 subsection {* Generalized summation over a set *}
   814 
   815 constdefs
   816   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   817   "setsum f A == if finite A then fold (op +) f 0 A else 0"
   818 
   819 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   820 written @{text"\<Sum>x\<in>A. e"}. *}
   821 
   822 syntax
   823   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   824 syntax (xsymbols)
   825   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   826 syntax (HTML output)
   827   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   828 
   829 translations -- {* Beware of argument permutation! *}
   830   "SUM i:A. b" == "setsum (%i. b) A"
   831   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   832 
   833 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   834  @{text"\<Sum>x|P. e"}. *}
   835 
   836 syntax
   837   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   838 syntax (xsymbols)
   839   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   840 syntax (HTML output)
   841   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   842 
   843 translations
   844   "SUM x|P. t" => "setsum (%x. t) {x. P}"
   845   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   846 
   847 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
   848 
   849 syntax
   850   "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
   851 
   852 parse_translation {*
   853   let
   854     fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
   855   in [("_Setsum", Setsum_tr)] end;
   856 *}
   857 
   858 print_translation {*
   859 let
   860   fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
   861     | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   862        if x<>y then raise Match
   863        else let val x' = Syntax.mark_bound x
   864                 val t' = subst_bound(x',t)
   865                 val P' = subst_bound(x',P)
   866             in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   867 in
   868 [("setsum", setsum_tr')]
   869 end
   870 *}
   871 
   872 lemma setsum_empty [simp]: "setsum f {} = 0"
   873   by (simp add: setsum_def)
   874 
   875 lemma setsum_insert [simp]:
   876     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   877   by (simp add: setsum_def)
   878 
   879 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   880   by (simp add: setsum_def)
   881 
   882 lemma setsum_reindex:
   883      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   884 by(auto simp add: setsum_def AC_add.fold_reindex dest!:finite_imageD)
   885 
   886 lemma setsum_reindex_id:
   887      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   888 by (auto simp add: setsum_reindex)
   889 
   890 lemma setsum_cong:
   891   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   892 by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
   893 
   894 lemma strong_setsum_cong[cong]:
   895   "A = B ==> (!!x. x:B =simp=> f x = g x)
   896    ==> setsum (%x. f x) A = setsum (%x. g x) B"
   897 by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
   898 
   899 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
   900   by (rule setsum_cong[OF refl], auto);
   901 
   902 lemma setsum_reindex_cong:
   903      "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   904       ==> setsum h B = setsum g A"
   905   by (simp add: setsum_reindex cong: setsum_cong)
   906 
   907 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
   908 apply (clarsimp simp: setsum_def)
   909 apply (erule finite_induct, auto)
   910 done
   911 
   912 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
   913 by(simp add:setsum_cong)
   914 
   915 lemma setsum_Un_Int: "finite A ==> finite B ==>
   916   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   917   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   918 by(simp add: setsum_def AC_add.fold_Un_Int [symmetric])
   919 
   920 lemma setsum_Un_disjoint: "finite A ==> finite B
   921   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   922 by (subst setsum_Un_Int [symmetric], auto)
   923 
   924 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   925   the lhs need not be, since UNION I A could still be finite.*)
   926 lemma setsum_UN_disjoint:
   927     "finite I ==> (ALL i:I. finite (A i)) ==>
   928         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   929       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   930 by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong)
   931 
   932 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   933 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   934 lemma setsum_Union_disjoint:
   935   "[| (ALL A:C. finite A);
   936       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   937    ==> setsum f (Union C) = setsum (setsum f) C"
   938 apply (cases "finite C") 
   939  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   940   apply (frule setsum_UN_disjoint [of C id f])
   941  apply (unfold Union_def id_def, assumption+)
   942 done
   943 
   944 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   945   the rhs need not be, since SIGMA A B could still be finite.*)
   946 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   947     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   948     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   949 by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
   950 
   951 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   952 lemma setsum_cartesian_product: 
   953    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
   954 apply (cases "finite A") 
   955  apply (cases "finite B") 
   956   apply (simp add: setsum_Sigma)
   957  apply (cases "A={}", simp)
   958  apply (simp) 
   959 apply (auto simp add: setsum_def
   960             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   961 done
   962 
   963 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   964 by(simp add:setsum_def AC_add.fold_distrib)
   965 
   966 
   967 subsubsection {* Properties in more restricted classes of structures *}
   968 
   969 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   970   apply (case_tac "finite A")
   971    prefer 2 apply (simp add: setsum_def)
   972   apply (erule rev_mp)
   973   apply (erule finite_induct, auto)
   974   done
   975 
   976 lemma setsum_eq_0_iff [simp]:
   977     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   978   by (induct set: Finites) auto
   979 
   980 lemma setsum_Un_nat: "finite A ==> finite B ==>
   981     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   982   -- {* For the natural numbers, we have subtraction. *}
   983   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   984 
   985 lemma setsum_Un: "finite A ==> finite B ==>
   986     (setsum f (A Un B) :: 'a :: ab_group_add) =
   987       setsum f A + setsum f B - setsum f (A Int B)"
   988   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   989 
   990 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   991     (if a:A then setsum f A - f a else setsum f A)"
   992   apply (case_tac "finite A")
   993    prefer 2 apply (simp add: setsum_def)
   994   apply (erule finite_induct)
   995    apply (auto simp add: insert_Diff_if)
   996   apply (drule_tac a = a in mk_disjoint_insert, auto)
   997   done
   998 
   999 lemma setsum_diff1: "finite A \<Longrightarrow>
  1000   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1001   (if a:A then setsum f A - f a else setsum f A)"
  1002   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1003 
  1004 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)"
  1005   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))"])
  1006   apply (auto simp add: insert_Diff_if add_ac)
  1007   done
  1008 
  1009 (* By Jeremy Siek: *)
  1010 
  1011 lemma setsum_diff_nat: 
  1012   assumes finB: "finite B"
  1013   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1014 using finB
  1015 proof (induct)
  1016   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1017 next
  1018   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1019     and xFinA: "insert x F \<subseteq> A"
  1020     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1021   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1022   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1023     by (simp add: setsum_diff1_nat)
  1024   from xFinA have "F \<subseteq> A" by simp
  1025   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1026   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1027     by simp
  1028   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1029   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1030     by simp
  1031   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1032   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1033     by simp
  1034   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1035 qed
  1036 
  1037 lemma setsum_diff:
  1038   assumes le: "finite A" "B \<subseteq> A"
  1039   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1040 proof -
  1041   from le have finiteB: "finite B" using finite_subset by auto
  1042   show ?thesis using finiteB le
  1043     proof (induct)
  1044       case empty
  1045       thus ?case by auto
  1046     next
  1047       case (insert x F)
  1048       thus ?case using le finiteB 
  1049 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1050     qed
  1051   qed
  1052 
  1053 lemma setsum_mono:
  1054   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1055   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1056 proof (cases "finite K")
  1057   case True
  1058   thus ?thesis using le
  1059   proof (induct)
  1060     case empty
  1061     thus ?case by simp
  1062   next
  1063     case insert
  1064     thus ?case using add_mono 
  1065       by force
  1066   qed
  1067 next
  1068   case False
  1069   thus ?thesis
  1070     by (simp add: setsum_def)
  1071 qed
  1072 
  1073 lemma setsum_strict_mono:
  1074 fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1075 assumes fin_ne: "finite A"  "A \<noteq> {}"
  1076 shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
  1077 using fin_ne
  1078 proof (induct rule: finite_ne_induct)
  1079   case singleton thus ?case by simp
  1080 next
  1081   case insert thus ?case by (auto simp: add_strict_mono)
  1082 qed
  1083 
  1084 lemma setsum_negf:
  1085  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1086 proof (cases "finite A")
  1087   case True thus ?thesis by (induct set: Finites, auto)
  1088 next
  1089   case False thus ?thesis by (simp add: setsum_def)
  1090 qed
  1091 
  1092 lemma setsum_subtractf:
  1093  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1094   setsum f A - setsum g A"
  1095 proof (cases "finite A")
  1096   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1097 next
  1098   case False thus ?thesis by (simp add: setsum_def)
  1099 qed
  1100 
  1101 lemma setsum_nonneg:
  1102 assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1103 shows "0 \<le> setsum f A"
  1104 proof (cases "finite A")
  1105   case True thus ?thesis using nn
  1106   apply (induct set: Finites, auto)
  1107   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1108   apply (blast intro: add_mono)
  1109   done
  1110 next
  1111   case False thus ?thesis by (simp add: setsum_def)
  1112 qed
  1113 
  1114 lemma setsum_nonpos:
  1115 assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
  1116 shows "setsum f A \<le> 0"
  1117 proof (cases "finite A")
  1118   case True thus ?thesis using np
  1119   apply (induct set: Finites, auto)
  1120   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1121   apply (blast intro: add_mono)
  1122   done
  1123 next
  1124   case False thus ?thesis by (simp add: setsum_def)
  1125 qed
  1126 
  1127 lemma setsum_mono2:
  1128 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1129 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1130 shows "setsum f A \<le> setsum f B"
  1131 proof -
  1132   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1133     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1134   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1135     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1136   also have "A \<union> (B-A) = B" using sub by blast
  1137   finally show ?thesis .
  1138 qed
  1139 
  1140 (* FIXME: this is distributitivty, name as such! *)
  1141 
  1142 lemma setsum_mult: 
  1143   fixes f :: "'a => ('b::semiring_0_cancel)"
  1144   shows "r * setsum f A = setsum (%n. r * f n) A"
  1145 proof (cases "finite A")
  1146   case True
  1147   thus ?thesis
  1148   proof (induct)
  1149     case empty thus ?case by simp
  1150   next
  1151     case (insert x A) thus ?case by (simp add: right_distrib)
  1152   qed
  1153 next
  1154   case False thus ?thesis by (simp add: setsum_def)
  1155 qed
  1156 
  1157 lemma setsum_abs[iff]: 
  1158   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1159   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1160 proof (cases "finite A")
  1161   case True
  1162   thus ?thesis
  1163   proof (induct)
  1164     case empty thus ?case by simp
  1165   next
  1166     case (insert x A)
  1167     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1168   qed
  1169 next
  1170   case False thus ?thesis by (simp add: setsum_def)
  1171 qed
  1172 
  1173 lemma setsum_abs_ge_zero[iff]: 
  1174   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1175   shows "0 \<le> setsum (%i. abs(f i)) A"
  1176 proof (cases "finite A")
  1177   case True
  1178   thus ?thesis
  1179   proof (induct)
  1180     case empty thus ?case by simp
  1181   next
  1182     case (insert x A) thus ?case by (auto intro: order_trans)
  1183   qed
  1184 next
  1185   case False thus ?thesis by (simp add: setsum_def)
  1186 qed
  1187 
  1188 lemma abs_setsum_abs[simp]: 
  1189   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1190   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1191 proof (cases "finite A")
  1192   case True
  1193   thus ?thesis
  1194   proof (induct)
  1195     case empty thus ?case by simp
  1196   next
  1197     case (insert a A)
  1198     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
  1199     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1200     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
  1201     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1202     finally show ?case .
  1203   qed
  1204 next
  1205   case False thus ?thesis by (simp add: setsum_def)
  1206 qed
  1207 
  1208 
  1209 subsection {* Generalized product over a set *}
  1210 
  1211 constdefs
  1212   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1213   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1214 
  1215 syntax
  1216   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1217 syntax (xsymbols)
  1218   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1219 syntax (HTML output)
  1220   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1221 
  1222 translations -- {* Beware of argument permutation! *}
  1223   "PROD i:A. b" == "setprod (%i. b) A" 
  1224   "\<Prod>i\<in>A. b" == "setprod (%i. b) A" 
  1225 
  1226 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1227  @{text"\<Prod>x|P. e"}. *}
  1228 
  1229 syntax
  1230   "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1231 syntax (xsymbols)
  1232   "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1233 syntax (HTML output)
  1234   "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1235 
  1236 translations
  1237   "PROD x|P. t" => "setprod (%x. t) {x. P}"
  1238   "\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
  1239 
  1240 text{* Finally we abbreviate @{term"\<Prod>x\<in>A. x"} by @{text"\<Prod>A"}. *}
  1241 
  1242 syntax
  1243   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1244 
  1245 parse_translation {*
  1246   let
  1247     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1248   in [("_Setprod", Setprod_tr)] end;
  1249 *}
  1250 print_translation {*
  1251 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1252     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1253 in
  1254 [("setprod", setprod_tr')]
  1255 end
  1256 *}
  1257 
  1258 
  1259 lemma setprod_empty [simp]: "setprod f {} = 1"
  1260   by (auto simp add: setprod_def)
  1261 
  1262 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1263     setprod f (insert a A) = f a * setprod f A"
  1264 by (simp add: setprod_def)
  1265 
  1266 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1267   by (simp add: setprod_def)
  1268 
  1269 lemma setprod_reindex:
  1270      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1271 by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
  1272 
  1273 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1274 by (auto simp add: setprod_reindex)
  1275 
  1276 lemma setprod_cong:
  1277   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1278 by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
  1279 
  1280 lemma strong_setprod_cong:
  1281   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1282 by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
  1283 
  1284 lemma setprod_reindex_cong: "inj_on f A ==>
  1285     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1286   by (frule setprod_reindex, simp)
  1287 
  1288 
  1289 lemma setprod_1: "setprod (%i. 1) A = 1"
  1290   apply (case_tac "finite A")
  1291   apply (erule finite_induct, auto simp add: mult_ac)
  1292   done
  1293 
  1294 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1295   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1296   apply (erule ssubst, rule setprod_1)
  1297   apply (rule setprod_cong, auto)
  1298   done
  1299 
  1300 lemma setprod_Un_Int: "finite A ==> finite B
  1301     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1302 by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
  1303 
  1304 lemma setprod_Un_disjoint: "finite A ==> finite B
  1305   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1306 by (subst setprod_Un_Int [symmetric], auto)
  1307 
  1308 lemma setprod_UN_disjoint:
  1309     "finite I ==> (ALL i:I. finite (A i)) ==>
  1310         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1311       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1312 by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
  1313 
  1314 lemma setprod_Union_disjoint:
  1315   "[| (ALL A:C. finite A);
  1316       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1317    ==> setprod f (Union C) = setprod (setprod f) C"
  1318 apply (cases "finite C") 
  1319  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1320   apply (frule setprod_UN_disjoint [of C id f])
  1321  apply (unfold Union_def id_def, assumption+)
  1322 done
  1323 
  1324 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1325     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1326     (\<Prod>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
  1327 by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
  1328 
  1329 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1330 lemma setprod_cartesian_product: 
  1331      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>z\<in>(A <*> B). f (fst z) (snd z))"
  1332 apply (cases "finite A") 
  1333  apply (cases "finite B") 
  1334   apply (simp add: setprod_Sigma)
  1335  apply (cases "A={}", simp)
  1336  apply (simp add: setprod_1) 
  1337 apply (auto simp add: setprod_def
  1338             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1339 done
  1340 
  1341 lemma setprod_timesf:
  1342      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1343 by(simp add:setprod_def AC_mult.fold_distrib)
  1344 
  1345 
  1346 subsubsection {* Properties in more restricted classes of structures *}
  1347 
  1348 lemma setprod_eq_1_iff [simp]:
  1349     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1350   by (induct set: Finites) auto
  1351 
  1352 lemma setprod_zero:
  1353      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1354   apply (induct set: Finites, force, clarsimp)
  1355   apply (erule disjE, auto)
  1356   done
  1357 
  1358 lemma setprod_nonneg [rule_format]:
  1359      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1360   apply (case_tac "finite A")
  1361   apply (induct set: Finites, force, clarsimp)
  1362   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1363   apply (rule mult_mono, assumption+)
  1364   apply (auto simp add: setprod_def)
  1365   done
  1366 
  1367 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1368      --> 0 < setprod f A"
  1369   apply (case_tac "finite A")
  1370   apply (induct set: Finites, force, clarsimp)
  1371   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1372   apply (rule mult_strict_mono, assumption+)
  1373   apply (auto simp add: setprod_def)
  1374   done
  1375 
  1376 lemma setprod_nonzero [rule_format]:
  1377     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1378       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1379   apply (erule finite_induct, auto)
  1380   done
  1381 
  1382 lemma setprod_zero_eq:
  1383     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1384      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1385   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1386   done
  1387 
  1388 lemma setprod_nonzero_field:
  1389     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1390   apply (rule setprod_nonzero, auto)
  1391   done
  1392 
  1393 lemma setprod_zero_eq_field:
  1394     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1395   apply (rule setprod_zero_eq, auto)
  1396   done
  1397 
  1398 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1399     (setprod f (A Un B) :: 'a ::{field})
  1400       = setprod f A * setprod f B / setprod f (A Int B)"
  1401   apply (subst setprod_Un_Int [symmetric], auto)
  1402   apply (subgoal_tac "finite (A Int B)")
  1403   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1404   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1405   done
  1406 
  1407 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1408     (setprod f (A - {a}) :: 'a :: {field}) =
  1409       (if a:A then setprod f A / f a else setprod f A)"
  1410   apply (erule finite_induct)
  1411    apply (auto simp add: insert_Diff_if)
  1412   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1413   apply (erule ssubst)
  1414   apply (subst times_divide_eq_right [THEN sym])
  1415   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1416   done
  1417 
  1418 lemma setprod_inversef: "finite A ==>
  1419     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1420       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1421   apply (erule finite_induct)
  1422   apply (simp, simp)
  1423   done
  1424 
  1425 lemma setprod_dividef:
  1426      "[|finite A;
  1427         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1428       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1429   apply (subgoal_tac
  1430          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1431   apply (erule ssubst)
  1432   apply (subst divide_inverse)
  1433   apply (subst setprod_timesf)
  1434   apply (subst setprod_inversef, assumption+, rule refl)
  1435   apply (rule setprod_cong, rule refl)
  1436   apply (subst divide_inverse, auto)
  1437   done
  1438 
  1439 subsection {* Finite cardinality *}
  1440 
  1441 text {* This definition, although traditional, is ugly to work with:
  1442 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1443 But now that we have @{text setsum} things are easy:
  1444 *}
  1445 
  1446 constdefs
  1447   card :: "'a set => nat"
  1448   "card A == setsum (%x. 1::nat) A"
  1449 
  1450 lemma card_empty [simp]: "card {} = 0"
  1451   by (simp add: card_def)
  1452 
  1453 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1454   by (simp add: card_def)
  1455 
  1456 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1457 by (simp add: card_def)
  1458 
  1459 lemma card_insert_disjoint [simp]:
  1460   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1461 by(simp add: card_def)
  1462 
  1463 lemma card_insert_if:
  1464     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1465   by (simp add: insert_absorb)
  1466 
  1467 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1468   apply auto
  1469   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1470   done
  1471 
  1472 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1473 by auto
  1474 
  1475 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1476 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1477 apply(simp del:insert_Diff_single)
  1478 done
  1479 
  1480 lemma card_Diff_singleton:
  1481     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1482   by (simp add: card_Suc_Diff1 [symmetric])
  1483 
  1484 lemma card_Diff_singleton_if:
  1485     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1486   by (simp add: card_Diff_singleton)
  1487 
  1488 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1489   by (simp add: card_insert_if card_Suc_Diff1)
  1490 
  1491 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1492   by (simp add: card_insert_if)
  1493 
  1494 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1495 by (simp add: card_def setsum_mono2)
  1496 
  1497 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1498   apply (induct set: Finites, simp, clarify)
  1499   apply (subgoal_tac "finite A & A - {x} <= F")
  1500    prefer 2 apply (blast intro: finite_subset, atomize)
  1501   apply (drule_tac x = "A - {x}" in spec)
  1502   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1503   apply (case_tac "card A", auto)
  1504   done
  1505 
  1506 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1507   apply (simp add: psubset_def linorder_not_le [symmetric])
  1508   apply (blast dest: card_seteq)
  1509   done
  1510 
  1511 lemma card_Un_Int: "finite A ==> finite B
  1512     ==> card A + card B = card (A Un B) + card (A Int B)"
  1513 by(simp add:card_def setsum_Un_Int)
  1514 
  1515 lemma card_Un_disjoint: "finite A ==> finite B
  1516     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1517   by (simp add: card_Un_Int)
  1518 
  1519 lemma card_Diff_subset:
  1520   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1521 by(simp add:card_def setsum_diff_nat)
  1522 
  1523 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1524   apply (rule Suc_less_SucD)
  1525   apply (simp add: card_Suc_Diff1)
  1526   done
  1527 
  1528 lemma card_Diff2_less:
  1529     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1530   apply (case_tac "x = y")
  1531    apply (simp add: card_Diff1_less)
  1532   apply (rule less_trans)
  1533    prefer 2 apply (auto intro!: card_Diff1_less)
  1534   done
  1535 
  1536 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1537   apply (case_tac "x : A")
  1538    apply (simp_all add: card_Diff1_less less_imp_le)
  1539   done
  1540 
  1541 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1542 by (erule psubsetI, blast)
  1543 
  1544 lemma insert_partition:
  1545   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1546   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1547 by auto
  1548 
  1549 (* main cardinality theorem *)
  1550 lemma card_partition [rule_format]:
  1551      "finite C ==>  
  1552         finite (\<Union> C) -->  
  1553         (\<forall>c\<in>C. card c = k) -->   
  1554         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1555         k * card(C) = card (\<Union> C)"
  1556 apply (erule finite_induct, simp)
  1557 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1558        finite_subset [of _ "\<Union> (insert x F)"])
  1559 done
  1560 
  1561 
  1562 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  1563 apply (cases "finite A")
  1564 apply (erule finite_induct)
  1565 apply (auto simp add: ring_distrib add_ac)
  1566 done
  1567 
  1568 
  1569 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)"
  1570   apply (erule finite_induct)
  1571   apply (auto simp add: power_Suc)
  1572   done
  1573 
  1574 lemma setsum_bounded:
  1575   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
  1576   shows "setsum f A \<le> of_nat(card A) * K"
  1577 proof (cases "finite A")
  1578   case True
  1579   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1580 next
  1581   case False thus ?thesis by (simp add: setsum_def)
  1582 qed
  1583 
  1584 
  1585 subsubsection {* Cardinality of unions *}
  1586 
  1587 lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
  1588 by(induct n, auto)
  1589 
  1590 lemma card_UN_disjoint:
  1591     "finite I ==> (ALL i:I. finite (A i)) ==>
  1592         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1593       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1594   apply (simp add: card_def del: setsum_constant)
  1595   apply (subgoal_tac
  1596            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1597   apply (simp add: setsum_UN_disjoint del: setsum_constant)
  1598   apply (simp cong: setsum_cong)
  1599   done
  1600 
  1601 lemma card_Union_disjoint:
  1602   "finite C ==> (ALL A:C. finite A) ==>
  1603         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1604       card (Union C) = setsum card C"
  1605   apply (frule card_UN_disjoint [of C id])
  1606   apply (unfold Union_def id_def, assumption+)
  1607   done
  1608 
  1609 subsubsection {* Cardinality of image *}
  1610 
  1611 text{*The image of a finite set can be expressed using @{term fold}.*}
  1612 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1613   apply (erule finite_induct, simp)
  1614   apply (subst ACf.fold_insert) 
  1615   apply (auto simp add: ACf_def) 
  1616   done
  1617 
  1618 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1619   apply (induct set: Finites, simp)
  1620   apply (simp add: le_SucI finite_imageI card_insert_if)
  1621   done
  1622 
  1623 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1624 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  1625 
  1626 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1627   by (simp add: card_seteq card_image)
  1628 
  1629 lemma eq_card_imp_inj_on:
  1630   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1631 apply (induct rule:finite_induct, simp)
  1632 apply(frule card_image_le[where f = f])
  1633 apply(simp add:card_insert_if split:if_splits)
  1634 done
  1635 
  1636 lemma inj_on_iff_eq_card:
  1637   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1638 by(blast intro: card_image eq_card_imp_inj_on)
  1639 
  1640 
  1641 lemma card_inj_on_le:
  1642     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1643 apply (subgoal_tac "finite A") 
  1644  apply (force intro: card_mono simp add: card_image [symmetric])
  1645 apply (blast intro: finite_imageD dest: finite_subset) 
  1646 done
  1647 
  1648 lemma card_bij_eq:
  1649     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1650        finite A; finite B |] ==> card A = card B"
  1651   by (auto intro: le_anti_sym card_inj_on_le)
  1652 
  1653 
  1654 subsubsection {* Cardinality of products *}
  1655 
  1656 (*
  1657 lemma SigmaI_insert: "y \<notin> A ==>
  1658   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1659   by auto
  1660 *)
  1661 
  1662 lemma card_SigmaI [simp]:
  1663   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1664   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1665 by(simp add:card_def setsum_Sigma del:setsum_constant)
  1666 
  1667 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1668 apply (cases "finite A") 
  1669 apply (cases "finite B") 
  1670 apply (auto simp add: card_eq_0_iff
  1671             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1672 done
  1673 
  1674 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1675 by (simp add: card_cartesian_product)
  1676 
  1677 
  1678 
  1679 subsubsection {* Cardinality of the Powerset *}
  1680 
  1681 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1682   apply (induct set: Finites)
  1683    apply (simp_all add: Pow_insert)
  1684   apply (subst card_Un_disjoint, blast)
  1685     apply (blast intro: finite_imageI, blast)
  1686   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1687    apply (simp add: card_image Pow_insert)
  1688   apply (unfold inj_on_def)
  1689   apply (blast elim!: equalityE)
  1690   done
  1691 
  1692 text {* Relates to equivalence classes.  Based on a theorem of
  1693 F. Kammüller's.  *}
  1694 
  1695 lemma dvd_partition:
  1696   "finite (Union C) ==>
  1697     ALL c : C. k dvd card c ==>
  1698     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1699   k dvd card (Union C)"
  1700 apply(frule finite_UnionD)
  1701 apply(rotate_tac -1)
  1702   apply (induct set: Finites, simp_all, clarify)
  1703   apply (subst card_Un_disjoint)
  1704   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1705   done
  1706 
  1707 
  1708 subsection{* A fold functional for non-empty sets *}
  1709 
  1710 text{* Does not require start value. *}
  1711 
  1712 consts
  1713   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1714 
  1715 inductive "fold1Set f"
  1716 intros
  1717   fold1Set_insertI [intro]:
  1718    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1719 
  1720 constdefs
  1721   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1722   "fold1 f A == THE x. (A, x) : fold1Set f"
  1723 
  1724 lemma fold1Set_nonempty:
  1725  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1726 by(erule fold1Set.cases, simp_all) 
  1727 
  1728 
  1729 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1730 
  1731 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1732 
  1733 
  1734 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1735   by (blast intro: foldSet.intros elim: foldSet.cases)
  1736 
  1737 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1738   by (unfold fold1_def) blast
  1739 
  1740 lemma finite_nonempty_imp_fold1Set:
  1741   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1742 apply (induct A rule: finite_induct)
  1743 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1744 done
  1745 
  1746 text{*First, some lemmas about @{term foldSet}.*}
  1747 
  1748 lemma (in ACf) foldSet_insert_swap:
  1749 assumes fold: "(A,y) \<in> foldSet f id b"
  1750 shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1751 using fold
  1752 proof (induct rule: foldSet.induct)
  1753   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1754 next
  1755   case (insertI A x y)
  1756     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1757       using insertI by force  --{*how does @{term id} get unfolded?*}
  1758     thus ?case by (simp add: insert_commute AC)
  1759 qed
  1760 
  1761 lemma (in ACf) foldSet_permute_diff:
  1762 assumes fold: "(A,x) \<in> foldSet f id b"
  1763 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1764 using fold
  1765 proof (induct rule: foldSet.induct)
  1766   case emptyI thus ?case by simp
  1767 next
  1768   case (insertI A x y)
  1769   have "a = x \<or> a \<in> A" using insertI by simp
  1770   thus ?case
  1771   proof
  1772     assume "a = x"
  1773     with insertI show ?thesis
  1774       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
  1775   next
  1776     assume ainA: "a \<in> A"
  1777     hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1778       using insertI by (force simp: id_def)
  1779     moreover
  1780     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1781       using ainA insertI by blast
  1782     ultimately show ?thesis by (simp add: id_def)
  1783   qed
  1784 qed
  1785 
  1786 lemma (in ACf) fold1_eq_fold:
  1787      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1788 apply (simp add: fold1_def fold_def) 
  1789 apply (rule the_equality)
  1790 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1791 apply (rule sym, clarify)
  1792 apply (case_tac "Aa=A")
  1793  apply (best intro: the_equality foldSet_determ)  
  1794 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1795  apply (best intro: the_equality foldSet_determ)  
  1796 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1797  prefer 2 apply (blast elim: equalityE) 
  1798 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1799 done
  1800 
  1801 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  1802 apply safe
  1803 apply simp 
  1804 apply (drule_tac x=x in spec)
  1805 apply (drule_tac x="A-{x}" in spec, auto) 
  1806 done
  1807 
  1808 lemma (in ACf) fold1_insert:
  1809   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  1810   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1811 proof -
  1812   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
  1813     by (auto simp add: nonempty_iff)
  1814   with A show ?thesis
  1815     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
  1816 qed
  1817 
  1818 lemma (in ACIf) fold1_insert_idem [simp]:
  1819   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  1820   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1821 proof -
  1822   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
  1823     by (auto simp add: nonempty_iff)
  1824   show ?thesis
  1825   proof cases
  1826     assume "a = x"
  1827     thus ?thesis 
  1828     proof cases
  1829       assume "A' = {}"
  1830       with prems show ?thesis by (simp add: idem) 
  1831     next
  1832       assume "A' \<noteq> {}"
  1833       with prems show ?thesis
  1834 	by (simp add: fold1_insert assoc [symmetric] idem) 
  1835     qed
  1836   next
  1837     assume "a \<noteq> x"
  1838     with prems show ?thesis
  1839       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  1840   qed
  1841 qed
  1842 
  1843 
  1844 text{* Now the recursion rules for definitions: *}
  1845 
  1846 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1847 by(simp add:fold1_singleton)
  1848 
  1849 lemma (in ACf) fold1_insert_def:
  1850   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1851 by(simp add:fold1_insert)
  1852 
  1853 lemma (in ACIf) fold1_insert_idem_def:
  1854   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1855 by(simp add:fold1_insert_idem)
  1856 
  1857 subsubsection{* Determinacy for @{term fold1Set} *}
  1858 
  1859 text{*Not actually used!!*}
  1860 
  1861 lemma (in ACf) foldSet_permute:
  1862   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1863    ==> (insert b A, x) \<in> foldSet f id a"
  1864 apply (case_tac "a=b") 
  1865 apply (auto dest: foldSet_permute_diff) 
  1866 done
  1867 
  1868 lemma (in ACf) fold1Set_determ:
  1869   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1870 proof (clarify elim!: fold1Set.cases)
  1871   fix A x B y a b
  1872   assume Ax: "(A, x) \<in> foldSet f id a"
  1873   assume By: "(B, y) \<in> foldSet f id b"
  1874   assume anotA:  "a \<notin> A"
  1875   assume bnotB:  "b \<notin> B"
  1876   assume eq: "insert a A = insert b B"
  1877   show "y=x"
  1878   proof cases
  1879     assume same: "a=b"
  1880     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1881     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1882   next
  1883     assume diff: "a\<noteq>b"
  1884     let ?D = "B - {a}"
  1885     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1886      and aB: "a \<in> B" and bA: "b \<in> A"
  1887       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1888     with aB bnotB By
  1889     have "(insert b ?D, y) \<in> foldSet f id a" 
  1890       by (auto intro: foldSet_permute simp add: insert_absorb)
  1891     moreover
  1892     have "(insert b ?D, x) \<in> foldSet f id a"
  1893       by (simp add: A [symmetric] Ax) 
  1894     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1895   qed
  1896 qed
  1897 
  1898 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1899   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1900 
  1901 declare
  1902   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1903   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1904   -- {* No more proves involve these relations. *}
  1905 
  1906 subsubsection{* Semi-Lattices *}
  1907 
  1908 locale ACIfSL = ACIf +
  1909   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1910   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1911 
  1912 locale ACIfSLlin = ACIfSL +
  1913   assumes lin: "x\<cdot>y \<in> {x,y}"
  1914 
  1915 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1916 by(simp add: below_def idem)
  1917 
  1918 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1919 proof
  1920   assume "x \<sqsubseteq> y \<cdot> z"
  1921   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1922   have "x \<cdot> y = x"
  1923   proof -
  1924     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1925     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1926     also have "\<dots> = x" by(rule xyzx)
  1927     finally show ?thesis .
  1928   qed
  1929   moreover have "x \<cdot> z = x"
  1930   proof -
  1931     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  1932     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1933     also have "\<dots> = x" by(rule xyzx)
  1934     finally show ?thesis .
  1935   qed
  1936   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  1937 next
  1938   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  1939   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  1940   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  1941   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  1942   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  1943   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  1944 qed
  1945 
  1946 lemma (in ACIfSLlin) above_f_conv:
  1947  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  1948 proof
  1949   assume a: "x \<cdot> y \<sqsubseteq> z"
  1950   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  1951   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1952   proof
  1953     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1954   next
  1955     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1956   qed
  1957 next
  1958   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1959   thus "x \<cdot> y \<sqsubseteq> z"
  1960   proof
  1961     assume a: "x \<sqsubseteq> z"
  1962     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  1963     also have "x \<cdot> z = x" using a by(simp add:below_def)
  1964     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1965   next
  1966     assume a: "y \<sqsubseteq> z"
  1967     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1968     also have "y \<cdot> z = y" using a by(simp add:below_def)
  1969     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1970   qed
  1971 qed
  1972 
  1973 
  1974 subsubsection{* Lemmas about @{text fold1} *}
  1975 
  1976 lemma (in ACf) fold1_Un:
  1977 assumes A: "finite A" "A \<noteq> {}"
  1978 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  1979        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1980 using A
  1981 proof(induct rule:finite_ne_induct)
  1982   case singleton thus ?case by(simp add:fold1_insert)
  1983 next
  1984   case insert thus ?case by (simp add:fold1_insert assoc)
  1985 qed
  1986 
  1987 lemma (in ACIf) fold1_Un2:
  1988 assumes A: "finite A" "A \<noteq> {}"
  1989 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  1990        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1991 using A
  1992 proof(induct rule:finite_ne_induct)
  1993   case singleton thus ?case by(simp add:fold1_insert_idem)
  1994 next
  1995   case insert thus ?case by (simp add:fold1_insert_idem assoc)
  1996 qed
  1997 
  1998 lemma (in ACf) fold1_in:
  1999   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  2000   shows "fold1 f A \<in> A"
  2001 using A
  2002 proof (induct rule:finite_ne_induct)
  2003   case singleton thus ?case by simp
  2004 next
  2005   case insert thus ?case using elem by (force simp add:fold1_insert)
  2006 qed
  2007 
  2008 lemma (in ACIfSL) below_fold1_iff:
  2009 assumes A: "finite A" "A \<noteq> {}"
  2010 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  2011 using A
  2012 by(induct rule:finite_ne_induct) simp_all
  2013 
  2014 lemma (in ACIfSL) fold1_belowI:
  2015 assumes A: "finite A" "A \<noteq> {}"
  2016 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  2017 using A
  2018 proof (induct rule:finite_ne_induct)
  2019   case singleton thus ?case by simp
  2020 next
  2021   case (insert x F)
  2022   from insert(5) have "a = x \<or> a \<in> F" by simp
  2023   thus ?case
  2024   proof
  2025     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  2026   next
  2027     assume "a \<in> F"
  2028     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  2029     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  2030       using insert by(simp add:below_def ACI)
  2031     also have "fold1 f F \<cdot> a = fold1 f F"
  2032       using bel  by(simp add:below_def ACI)
  2033     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  2034       using insert by(simp add:below_def ACI)
  2035     finally show ?thesis  by(simp add:below_def)
  2036   qed
  2037 qed
  2038 
  2039 lemma (in ACIfSLlin) fold1_below_iff:
  2040 assumes A: "finite A" "A \<noteq> {}"
  2041 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  2042 using A
  2043 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  2044 
  2045 
  2046 subsubsection{* Lattices *}
  2047 
  2048 locale Lattice = lattice +
  2049   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2050   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2051   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2052 
  2053 locale Distrib_Lattice = distrib_lattice + Lattice
  2054 
  2055 text{* Lattices are semilattices *}
  2056 
  2057 lemma (in Lattice) ACf_inf: "ACf inf"
  2058 by(blast intro: ACf.intro inf_commute inf_assoc)
  2059 
  2060 lemma (in Lattice) ACf_sup: "ACf sup"
  2061 by(blast intro: ACf.intro sup_commute sup_assoc)
  2062 
  2063 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2064 apply(rule ACIf.intro)
  2065 apply(rule ACf_inf)
  2066 apply(rule ACIf_axioms.intro)
  2067 apply(rule inf_idem)
  2068 done
  2069 
  2070 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2071 apply(rule ACIf.intro)
  2072 apply(rule ACf_sup)
  2073 apply(rule ACIf_axioms.intro)
  2074 apply(rule sup_idem)
  2075 done
  2076 
  2077 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2078 apply(rule ACIfSL.intro)
  2079 apply(rule ACf_inf)
  2080 apply(rule ACIf.axioms[OF ACIf_inf])
  2081 apply(rule ACIfSL_axioms.intro)
  2082 apply(rule iffI)
  2083  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2084 apply(erule subst)
  2085 apply(rule inf_le2)
  2086 done
  2087 
  2088 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2089 apply(rule ACIfSL.intro)
  2090 apply(rule ACf_sup)
  2091 apply(rule ACIf.axioms[OF ACIf_sup])
  2092 apply(rule ACIfSL_axioms.intro)
  2093 apply(rule iffI)
  2094  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2095 apply(erule subst)
  2096 apply(rule sup_ge2)
  2097 done
  2098 
  2099 
  2100 subsubsection{* Fold laws in lattices *}
  2101 
  2102 lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2103 apply(unfold Sup_def Inf_def)
  2104 apply(subgoal_tac "EX a. a:A")
  2105 prefer 2 apply blast
  2106 apply(erule exE)
  2107 apply(rule trans)
  2108 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2109 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2110 done
  2111 
  2112 lemma (in Lattice) sup_Inf_absorb[simp]:
  2113   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2114 apply(subst sup_commute)
  2115 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2116 done
  2117 
  2118 lemma (in Lattice) inf_Sup_absorb[simp]:
  2119   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2120 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2121 
  2122 
  2123 lemma (in Distrib_Lattice) sup_Inf1_distrib:
  2124 assumes A: "finite A" "A \<noteq> {}"
  2125 shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2126 using A
  2127 proof (induct rule: finite_ne_induct)
  2128   case singleton thus ?case by(simp add:Inf_def)
  2129 next
  2130   case (insert y A)
  2131   have fin: "finite {x \<squnion> a |a. a \<in> A}"
  2132     by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
  2133   have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
  2134     using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
  2135   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
  2136   also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
  2137   also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
  2138     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def fin])
  2139   also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
  2140     by blast
  2141   finally show ?case .
  2142 qed
  2143 
  2144 lemma (in Distrib_Lattice) sup_Inf2_distrib:
  2145 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2146 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2147 using A
  2148 proof (induct rule: finite_ne_induct)
  2149   case singleton thus ?case
  2150     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2151 next
  2152   case (insert x A)
  2153   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2154     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
  2155   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2156   proof -
  2157     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2158       by blast
  2159     thus ?thesis by(simp add: insert(1) B(1))
  2160   qed
  2161   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2162   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2163     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
  2164   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2165   also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2166     using insert by(simp add:sup_Inf1_distrib[OF B])
  2167   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2168     (is "_ = \<Sqinter>?M")
  2169     using B insert
  2170     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2171   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2172     by blast
  2173   finally show ?case .
  2174 qed
  2175 
  2176 
  2177 subsection{*Min and Max*}
  2178 
  2179 text{* As an application of @{text fold1} we define the minimal and
  2180 maximal element of a (non-empty) set over a linear order. *}
  2181 
  2182 constdefs
  2183   Min :: "('a::linorder)set => 'a"
  2184   "Min  ==  fold1 min"
  2185 
  2186   Max :: "('a::linorder)set => 'a"
  2187   "Max  ==  fold1 max"
  2188 
  2189 
  2190 text{* Before we can do anything, we need to show that @{text min} and
  2191 @{text max} are ACI and the ordering is linear: *}
  2192 
  2193 interpretation min: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2194 apply(rule ACf.intro)
  2195 apply(auto simp:min_def)
  2196 done
  2197 
  2198 interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2199 apply(rule ACIf_axioms.intro)
  2200 apply(auto simp:min_def)
  2201 done
  2202 
  2203 interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2204 apply(rule ACf.intro)
  2205 apply(auto simp:max_def)
  2206 done
  2207 
  2208 interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2209 apply(rule ACIf_axioms.intro)
  2210 apply(auto simp:max_def)
  2211 done
  2212 
  2213 interpretation min:
  2214   ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
  2215 apply(rule ACIfSL_axioms.intro)
  2216 apply(auto simp:min_def)
  2217 done
  2218 
  2219 interpretation min:
  2220   ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
  2221 apply(rule ACIfSLlin_axioms.intro)
  2222 apply(auto simp:min_def)
  2223 done
  2224 
  2225 interpretation max:
  2226   ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
  2227 apply(rule ACIfSL_axioms.intro)
  2228 apply(auto simp:max_def)
  2229 done
  2230 
  2231 interpretation max:
  2232   ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
  2233 apply(rule ACIfSLlin_axioms.intro)
  2234 apply(auto simp:max_def)
  2235 done
  2236 
  2237 interpretation min_max:
  2238   Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2239 apply -
  2240 apply(rule Min_def)
  2241 apply(rule Max_def)
  2242 done
  2243 
  2244 
  2245 interpretation min_max:
  2246   Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2247 .
  2248 
  2249 text{* Now we instantiate the recursion equations and declare them
  2250 simplification rules: *}
  2251 
  2252 (* Making Min (resp. Max) a defined parameter of a locale suitably
  2253   extending ACIf could make the following interpretations more automatic. *)
  2254 
  2255 declare
  2256   fold1_singleton_def[OF Min_def, simp]
  2257   min.fold1_insert_idem_def[OF Min_def, simp]
  2258   fold1_singleton_def[OF Max_def, simp]
  2259   max.fold1_insert_idem_def[OF Max_def, simp]
  2260 
  2261 text{* Now we instantiate some @{text fold1} properties: *}
  2262 
  2263 lemma Min_in [simp]:
  2264   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2265 using min.fold1_in
  2266 by(fastsimp simp: Min_def min_def)
  2267 
  2268 lemma Max_in [simp]:
  2269   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2270 using max.fold1_in
  2271 by(fastsimp simp: Max_def max_def)
  2272 
  2273 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2274 by(simp add: Min_def min.fold1_belowI)
  2275 
  2276 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2277 by(simp add: Max_def max.fold1_belowI)
  2278 
  2279 lemma Min_ge_iff[simp]:
  2280   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2281 by(simp add: Min_def min.below_fold1_iff)
  2282 
  2283 lemma Max_le_iff[simp]:
  2284   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2285 by(simp add: Max_def max.below_fold1_iff)
  2286 
  2287 lemma Min_le_iff:
  2288   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2289 by(simp add: Min_def min.fold1_below_iff)
  2290 
  2291 lemma Max_ge_iff:
  2292   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2293 by(simp add: Max_def max.fold1_below_iff)
  2294 
  2295 end