src/HOL/Finite_Set.thy
author berghofe
Fri Jul 01 13:51:11 2005 +0200 (2005-07-01)
changeset 16632 ad2895beef79
parent 16550 e14b89d6ef13
child 16733 236dfafbeb63
permissions -rw-r--r--
Added strong_setsum_cong and strong_setprod_cong.
     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:
   895   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setsum f A = setsum g B"
   896 by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
   897 
   898 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
   899   by (rule setsum_cong[OF refl], auto);
   900 
   901 lemma setsum_reindex_cong:
   902      "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   903       ==> setsum h B = setsum g A"
   904   by (simp add: setsum_reindex cong: setsum_cong)
   905 
   906 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
   907 apply (clarsimp simp: setsum_def)
   908 apply (erule finite_induct, auto)
   909 done
   910 
   911 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
   912 by(simp add:setsum_cong)
   913 
   914 lemma setsum_Un_Int: "finite A ==> finite B ==>
   915   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   916   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   917 by(simp add: setsum_def AC_add.fold_Un_Int [symmetric])
   918 
   919 lemma setsum_Un_disjoint: "finite A ==> finite B
   920   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   921 by (subst setsum_Un_Int [symmetric], auto)
   922 
   923 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   924   the lhs need not be, since UNION I A could still be finite.*)
   925 lemma setsum_UN_disjoint:
   926     "finite I ==> (ALL i:I. finite (A i)) ==>
   927         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   928       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   929 by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong)
   930 
   931 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   932 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   933 lemma setsum_Union_disjoint:
   934   "[| (ALL A:C. finite A);
   935       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   936    ==> setsum f (Union C) = setsum (setsum f) C"
   937 apply (cases "finite C") 
   938  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   939   apply (frule setsum_UN_disjoint [of C id f])
   940  apply (unfold Union_def id_def, assumption+)
   941 done
   942 
   943 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   944   the rhs need not be, since SIGMA A B could still be finite.*)
   945 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   946     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   947     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   948 by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
   949 
   950 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   951 lemma setsum_cartesian_product: 
   952    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
   953 apply (cases "finite A") 
   954  apply (cases "finite B") 
   955   apply (simp add: setsum_Sigma)
   956  apply (cases "A={}", simp)
   957  apply (simp) 
   958 apply (auto simp add: setsum_def
   959             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   960 done
   961 
   962 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   963 by(simp add:setsum_def AC_add.fold_distrib)
   964 
   965 
   966 subsubsection {* Properties in more restricted classes of structures *}
   967 
   968 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   969   apply (case_tac "finite A")
   970    prefer 2 apply (simp add: setsum_def)
   971   apply (erule rev_mp)
   972   apply (erule finite_induct, auto)
   973   done
   974 
   975 lemma setsum_eq_0_iff [simp]:
   976     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   977   by (induct set: Finites) auto
   978 
   979 lemma setsum_Un_nat: "finite A ==> finite B ==>
   980     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   981   -- {* For the natural numbers, we have subtraction. *}
   982   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   983 
   984 lemma setsum_Un: "finite A ==> finite B ==>
   985     (setsum f (A Un B) :: 'a :: ab_group_add) =
   986       setsum f A + setsum f B - setsum f (A Int B)"
   987   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   988 
   989 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   990     (if a:A then setsum f A - f a else setsum f A)"
   991   apply (case_tac "finite A")
   992    prefer 2 apply (simp add: setsum_def)
   993   apply (erule finite_induct)
   994    apply (auto simp add: insert_Diff_if)
   995   apply (drule_tac a = a in mk_disjoint_insert, auto)
   996   done
   997 
   998 lemma setsum_diff1: "finite A \<Longrightarrow>
   999   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1000   (if a:A then setsum f A - f a else setsum f A)"
  1001   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1002 
  1003 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)"
  1004   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))"])
  1005   apply (auto simp add: insert_Diff_if add_ac)
  1006   done
  1007 
  1008 (* By Jeremy Siek: *)
  1009 
  1010 lemma setsum_diff_nat: 
  1011   assumes finB: "finite B"
  1012   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1013 using finB
  1014 proof (induct)
  1015   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1016 next
  1017   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1018     and xFinA: "insert x F \<subseteq> A"
  1019     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1020   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1021   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1022     by (simp add: setsum_diff1_nat)
  1023   from xFinA have "F \<subseteq> A" by simp
  1024   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1025   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1026     by simp
  1027   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1028   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1029     by simp
  1030   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1031   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1032     by simp
  1033   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1034 qed
  1035 
  1036 lemma setsum_diff:
  1037   assumes le: "finite A" "B \<subseteq> A"
  1038   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1039 proof -
  1040   from le have finiteB: "finite B" using finite_subset by auto
  1041   show ?thesis using finiteB le
  1042     proof (induct)
  1043       case empty
  1044       thus ?case by auto
  1045     next
  1046       case (insert x F)
  1047       thus ?case using le finiteB 
  1048 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1049     qed
  1050   qed
  1051 
  1052 lemma setsum_mono:
  1053   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1054   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1055 proof (cases "finite K")
  1056   case True
  1057   thus ?thesis using le
  1058   proof (induct)
  1059     case empty
  1060     thus ?case by simp
  1061   next
  1062     case insert
  1063     thus ?case using add_mono 
  1064       by force
  1065   qed
  1066 next
  1067   case False
  1068   thus ?thesis
  1069     by (simp add: setsum_def)
  1070 qed
  1071 
  1072 lemma setsum_strict_mono:
  1073 fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1074 assumes fin_ne: "finite A"  "A \<noteq> {}"
  1075 shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
  1076 using fin_ne
  1077 proof (induct rule: finite_ne_induct)
  1078   case singleton thus ?case by simp
  1079 next
  1080   case insert thus ?case by (auto simp: add_strict_mono)
  1081 qed
  1082 
  1083 lemma setsum_negf:
  1084  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1085 proof (cases "finite A")
  1086   case True thus ?thesis by (induct set: Finites, auto)
  1087 next
  1088   case False thus ?thesis by (simp add: setsum_def)
  1089 qed
  1090 
  1091 lemma setsum_subtractf:
  1092  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1093   setsum f A - setsum g A"
  1094 proof (cases "finite A")
  1095   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1096 next
  1097   case False thus ?thesis by (simp add: setsum_def)
  1098 qed
  1099 
  1100 lemma setsum_nonneg:
  1101 assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1102 shows "0 \<le> setsum f A"
  1103 proof (cases "finite A")
  1104   case True thus ?thesis using nn
  1105   apply (induct set: Finites, auto)
  1106   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1107   apply (blast intro: add_mono)
  1108   done
  1109 next
  1110   case False thus ?thesis by (simp add: setsum_def)
  1111 qed
  1112 
  1113 lemma setsum_nonpos:
  1114 assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
  1115 shows "setsum f A \<le> 0"
  1116 proof (cases "finite A")
  1117   case True thus ?thesis using np
  1118   apply (induct set: Finites, auto)
  1119   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1120   apply (blast intro: add_mono)
  1121   done
  1122 next
  1123   case False thus ?thesis by (simp add: setsum_def)
  1124 qed
  1125 
  1126 lemma setsum_mono2:
  1127 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1128 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1129 shows "setsum f A \<le> setsum f B"
  1130 proof -
  1131   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1132     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1133   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1134     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1135   also have "A \<union> (B-A) = B" using sub by blast
  1136   finally show ?thesis .
  1137 qed
  1138 
  1139 (* FIXME: this is distributitivty, name as such! *)
  1140 
  1141 lemma setsum_mult: 
  1142   fixes f :: "'a => ('b::semiring_0_cancel)"
  1143   shows "r * setsum f A = setsum (%n. r * f n) A"
  1144 proof (cases "finite A")
  1145   case True
  1146   thus ?thesis
  1147   proof (induct)
  1148     case empty thus ?case by simp
  1149   next
  1150     case (insert x A) thus ?case by (simp add: right_distrib)
  1151   qed
  1152 next
  1153   case False thus ?thesis by (simp add: setsum_def)
  1154 qed
  1155 
  1156 lemma setsum_abs[iff]: 
  1157   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1158   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1159 proof (cases "finite A")
  1160   case True
  1161   thus ?thesis
  1162   proof (induct)
  1163     case empty thus ?case by simp
  1164   next
  1165     case (insert x A)
  1166     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1167   qed
  1168 next
  1169   case False thus ?thesis by (simp add: setsum_def)
  1170 qed
  1171 
  1172 lemma setsum_abs_ge_zero[iff]: 
  1173   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1174   shows "0 \<le> setsum (%i. abs(f i)) A"
  1175 proof (cases "finite A")
  1176   case True
  1177   thus ?thesis
  1178   proof (induct)
  1179     case empty thus ?case by simp
  1180   next
  1181     case (insert x A) thus ?case by (auto intro: order_trans)
  1182   qed
  1183 next
  1184   case False thus ?thesis by (simp add: setsum_def)
  1185 qed
  1186 
  1187 lemma abs_setsum_abs[simp]: 
  1188   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1189   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1190 proof (cases "finite A")
  1191   case True
  1192   thus ?thesis
  1193   proof (induct)
  1194     case empty thus ?case by simp
  1195   next
  1196     case (insert a A)
  1197     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
  1198     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1199     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
  1200     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1201     finally show ?case .
  1202   qed
  1203 next
  1204   case False thus ?thesis by (simp add: setsum_def)
  1205 qed
  1206 
  1207 
  1208 subsection {* Generalized product over a set *}
  1209 
  1210 constdefs
  1211   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1212   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1213 
  1214 syntax
  1215   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1216 syntax (xsymbols)
  1217   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1218 syntax (HTML output)
  1219   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1220 
  1221 translations -- {* Beware of argument permutation! *}
  1222   "PROD i:A. b" == "setprod (%i. b) A" 
  1223   "\<Prod>i\<in>A. b" == "setprod (%i. b) A" 
  1224 
  1225 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1226  @{text"\<Prod>x|P. e"}. *}
  1227 
  1228 syntax
  1229   "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1230 syntax (xsymbols)
  1231   "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1232 syntax (HTML output)
  1233   "_qsetprod" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1234 
  1235 translations
  1236   "PROD x|P. t" => "setprod (%x. t) {x. P}"
  1237   "\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
  1238 
  1239 text{* Finally we abbreviate @{term"\<Prod>x\<in>A. x"} by @{text"\<Prod>A"}. *}
  1240 
  1241 syntax
  1242   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1243 
  1244 parse_translation {*
  1245   let
  1246     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1247   in [("_Setprod", Setprod_tr)] end;
  1248 *}
  1249 print_translation {*
  1250 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1251     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1252 in
  1253 [("setprod", setprod_tr')]
  1254 end
  1255 *}
  1256 
  1257 
  1258 lemma setprod_empty [simp]: "setprod f {} = 1"
  1259   by (auto simp add: setprod_def)
  1260 
  1261 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1262     setprod f (insert a A) = f a * setprod f A"
  1263 by (simp add: setprod_def)
  1264 
  1265 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1266   by (simp add: setprod_def)
  1267 
  1268 lemma setprod_reindex:
  1269      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1270 by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
  1271 
  1272 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1273 by (auto simp add: setprod_reindex)
  1274 
  1275 lemma setprod_cong:
  1276   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1277 by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
  1278 
  1279 lemma strong_setprod_cong:
  1280   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1281 by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
  1282 
  1283 lemma setprod_reindex_cong: "inj_on f A ==>
  1284     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1285   by (frule setprod_reindex, simp)
  1286 
  1287 
  1288 lemma setprod_1: "setprod (%i. 1) A = 1"
  1289   apply (case_tac "finite A")
  1290   apply (erule finite_induct, auto simp add: mult_ac)
  1291   done
  1292 
  1293 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1294   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1295   apply (erule ssubst, rule setprod_1)
  1296   apply (rule setprod_cong, auto)
  1297   done
  1298 
  1299 lemma setprod_Un_Int: "finite A ==> finite B
  1300     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1301 by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
  1302 
  1303 lemma setprod_Un_disjoint: "finite A ==> finite B
  1304   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1305 by (subst setprod_Un_Int [symmetric], auto)
  1306 
  1307 lemma setprod_UN_disjoint:
  1308     "finite I ==> (ALL i:I. finite (A i)) ==>
  1309         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1310       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1311 by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
  1312 
  1313 lemma setprod_Union_disjoint:
  1314   "[| (ALL A:C. finite A);
  1315       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1316    ==> setprod f (Union C) = setprod (setprod f) C"
  1317 apply (cases "finite C") 
  1318  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1319   apply (frule setprod_UN_disjoint [of C id f])
  1320  apply (unfold Union_def id_def, assumption+)
  1321 done
  1322 
  1323 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1324     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1325     (\<Prod>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
  1326 by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
  1327 
  1328 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1329 lemma setprod_cartesian_product: 
  1330      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>z\<in>(A <*> B). f (fst z) (snd z))"
  1331 apply (cases "finite A") 
  1332  apply (cases "finite B") 
  1333   apply (simp add: setprod_Sigma)
  1334  apply (cases "A={}", simp)
  1335  apply (simp add: setprod_1) 
  1336 apply (auto simp add: setprod_def
  1337             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1338 done
  1339 
  1340 lemma setprod_timesf:
  1341      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1342 by(simp add:setprod_def AC_mult.fold_distrib)
  1343 
  1344 
  1345 subsubsection {* Properties in more restricted classes of structures *}
  1346 
  1347 lemma setprod_eq_1_iff [simp]:
  1348     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1349   by (induct set: Finites) auto
  1350 
  1351 lemma setprod_zero:
  1352      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1353   apply (induct set: Finites, force, clarsimp)
  1354   apply (erule disjE, auto)
  1355   done
  1356 
  1357 lemma setprod_nonneg [rule_format]:
  1358      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1359   apply (case_tac "finite A")
  1360   apply (induct set: Finites, force, clarsimp)
  1361   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1362   apply (rule mult_mono, assumption+)
  1363   apply (auto simp add: setprod_def)
  1364   done
  1365 
  1366 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1367      --> 0 < setprod f A"
  1368   apply (case_tac "finite A")
  1369   apply (induct set: Finites, force, clarsimp)
  1370   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1371   apply (rule mult_strict_mono, assumption+)
  1372   apply (auto simp add: setprod_def)
  1373   done
  1374 
  1375 lemma setprod_nonzero [rule_format]:
  1376     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1377       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1378   apply (erule finite_induct, auto)
  1379   done
  1380 
  1381 lemma setprod_zero_eq:
  1382     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1383      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1384   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1385   done
  1386 
  1387 lemma setprod_nonzero_field:
  1388     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1389   apply (rule setprod_nonzero, auto)
  1390   done
  1391 
  1392 lemma setprod_zero_eq_field:
  1393     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1394   apply (rule setprod_zero_eq, auto)
  1395   done
  1396 
  1397 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1398     (setprod f (A Un B) :: 'a ::{field})
  1399       = setprod f A * setprod f B / setprod f (A Int B)"
  1400   apply (subst setprod_Un_Int [symmetric], auto)
  1401   apply (subgoal_tac "finite (A Int B)")
  1402   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1403   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1404   done
  1405 
  1406 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1407     (setprod f (A - {a}) :: 'a :: {field}) =
  1408       (if a:A then setprod f A / f a else setprod f A)"
  1409   apply (erule finite_induct)
  1410    apply (auto simp add: insert_Diff_if)
  1411   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1412   apply (erule ssubst)
  1413   apply (subst times_divide_eq_right [THEN sym])
  1414   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1415   done
  1416 
  1417 lemma setprod_inversef: "finite A ==>
  1418     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1419       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1420   apply (erule finite_induct)
  1421   apply (simp, simp)
  1422   done
  1423 
  1424 lemma setprod_dividef:
  1425      "[|finite A;
  1426         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1427       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1428   apply (subgoal_tac
  1429          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1430   apply (erule ssubst)
  1431   apply (subst divide_inverse)
  1432   apply (subst setprod_timesf)
  1433   apply (subst setprod_inversef, assumption+, rule refl)
  1434   apply (rule setprod_cong, rule refl)
  1435   apply (subst divide_inverse, auto)
  1436   done
  1437 
  1438 subsection {* Finite cardinality *}
  1439 
  1440 text {* This definition, although traditional, is ugly to work with:
  1441 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1442 But now that we have @{text setsum} things are easy:
  1443 *}
  1444 
  1445 constdefs
  1446   card :: "'a set => nat"
  1447   "card A == setsum (%x. 1::nat) A"
  1448 
  1449 lemma card_empty [simp]: "card {} = 0"
  1450   by (simp add: card_def)
  1451 
  1452 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1453   by (simp add: card_def)
  1454 
  1455 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1456 by (simp add: card_def)
  1457 
  1458 lemma card_insert_disjoint [simp]:
  1459   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1460 by(simp add: card_def)
  1461 
  1462 lemma card_insert_if:
  1463     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1464   by (simp add: insert_absorb)
  1465 
  1466 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1467   apply auto
  1468   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1469   done
  1470 
  1471 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1472 by auto
  1473 
  1474 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1475 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1476 apply(simp del:insert_Diff_single)
  1477 done
  1478 
  1479 lemma card_Diff_singleton:
  1480     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1481   by (simp add: card_Suc_Diff1 [symmetric])
  1482 
  1483 lemma card_Diff_singleton_if:
  1484     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1485   by (simp add: card_Diff_singleton)
  1486 
  1487 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1488   by (simp add: card_insert_if card_Suc_Diff1)
  1489 
  1490 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1491   by (simp add: card_insert_if)
  1492 
  1493 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1494 by (simp add: card_def setsum_mono2)
  1495 
  1496 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1497   apply (induct set: Finites, simp, clarify)
  1498   apply (subgoal_tac "finite A & A - {x} <= F")
  1499    prefer 2 apply (blast intro: finite_subset, atomize)
  1500   apply (drule_tac x = "A - {x}" in spec)
  1501   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1502   apply (case_tac "card A", auto)
  1503   done
  1504 
  1505 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1506   apply (simp add: psubset_def linorder_not_le [symmetric])
  1507   apply (blast dest: card_seteq)
  1508   done
  1509 
  1510 lemma card_Un_Int: "finite A ==> finite B
  1511     ==> card A + card B = card (A Un B) + card (A Int B)"
  1512 by(simp add:card_def setsum_Un_Int)
  1513 
  1514 lemma card_Un_disjoint: "finite A ==> finite B
  1515     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1516   by (simp add: card_Un_Int)
  1517 
  1518 lemma card_Diff_subset:
  1519   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1520 by(simp add:card_def setsum_diff_nat)
  1521 
  1522 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1523   apply (rule Suc_less_SucD)
  1524   apply (simp add: card_Suc_Diff1)
  1525   done
  1526 
  1527 lemma card_Diff2_less:
  1528     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1529   apply (case_tac "x = y")
  1530    apply (simp add: card_Diff1_less)
  1531   apply (rule less_trans)
  1532    prefer 2 apply (auto intro!: card_Diff1_less)
  1533   done
  1534 
  1535 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1536   apply (case_tac "x : A")
  1537    apply (simp_all add: card_Diff1_less less_imp_le)
  1538   done
  1539 
  1540 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1541 by (erule psubsetI, blast)
  1542 
  1543 lemma insert_partition:
  1544   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1545   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1546 by auto
  1547 
  1548 (* main cardinality theorem *)
  1549 lemma card_partition [rule_format]:
  1550      "finite C ==>  
  1551         finite (\<Union> C) -->  
  1552         (\<forall>c\<in>C. card c = k) -->   
  1553         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1554         k * card(C) = card (\<Union> C)"
  1555 apply (erule finite_induct, simp)
  1556 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1557        finite_subset [of _ "\<Union> (insert x F)"])
  1558 done
  1559 
  1560 
  1561 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  1562 apply (cases "finite A")
  1563 apply (erule finite_induct)
  1564 apply (auto simp add: ring_distrib add_ac)
  1565 done
  1566 
  1567 
  1568 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)"
  1569   apply (erule finite_induct)
  1570   apply (auto simp add: power_Suc)
  1571   done
  1572 
  1573 lemma setsum_bounded:
  1574   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
  1575   shows "setsum f A \<le> of_nat(card A) * K"
  1576 proof (cases "finite A")
  1577   case True
  1578   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1579 next
  1580   case False thus ?thesis by (simp add: setsum_def)
  1581 qed
  1582 
  1583 
  1584 subsubsection {* Cardinality of unions *}
  1585 
  1586 lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
  1587 by(induct n, auto)
  1588 
  1589 lemma card_UN_disjoint:
  1590     "finite I ==> (ALL i:I. finite (A i)) ==>
  1591         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1592       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1593   apply (simp add: card_def del: setsum_constant)
  1594   apply (subgoal_tac
  1595            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1596   apply (simp add: setsum_UN_disjoint del: setsum_constant)
  1597   apply (simp cong: setsum_cong)
  1598   done
  1599 
  1600 lemma card_Union_disjoint:
  1601   "finite C ==> (ALL A:C. finite A) ==>
  1602         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1603       card (Union C) = setsum card C"
  1604   apply (frule card_UN_disjoint [of C id])
  1605   apply (unfold Union_def id_def, assumption+)
  1606   done
  1607 
  1608 subsubsection {* Cardinality of image *}
  1609 
  1610 text{*The image of a finite set can be expressed using @{term fold}.*}
  1611 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1612   apply (erule finite_induct, simp)
  1613   apply (subst ACf.fold_insert) 
  1614   apply (auto simp add: ACf_def) 
  1615   done
  1616 
  1617 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1618   apply (induct set: Finites, simp)
  1619   apply (simp add: le_SucI finite_imageI card_insert_if)
  1620   done
  1621 
  1622 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1623 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  1624 
  1625 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1626   by (simp add: card_seteq card_image)
  1627 
  1628 lemma eq_card_imp_inj_on:
  1629   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1630 apply (induct rule:finite_induct, simp)
  1631 apply(frule card_image_le[where f = f])
  1632 apply(simp add:card_insert_if split:if_splits)
  1633 done
  1634 
  1635 lemma inj_on_iff_eq_card:
  1636   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1637 by(blast intro: card_image eq_card_imp_inj_on)
  1638 
  1639 
  1640 lemma card_inj_on_le:
  1641     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1642 apply (subgoal_tac "finite A") 
  1643  apply (force intro: card_mono simp add: card_image [symmetric])
  1644 apply (blast intro: finite_imageD dest: finite_subset) 
  1645 done
  1646 
  1647 lemma card_bij_eq:
  1648     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1649        finite A; finite B |] ==> card A = card B"
  1650   by (auto intro: le_anti_sym card_inj_on_le)
  1651 
  1652 
  1653 subsubsection {* Cardinality of products *}
  1654 
  1655 (*
  1656 lemma SigmaI_insert: "y \<notin> A ==>
  1657   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1658   by auto
  1659 *)
  1660 
  1661 lemma card_SigmaI [simp]:
  1662   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1663   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1664 by(simp add:card_def setsum_Sigma del:setsum_constant)
  1665 
  1666 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1667 apply (cases "finite A") 
  1668 apply (cases "finite B") 
  1669 apply (auto simp add: card_eq_0_iff
  1670             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1671 done
  1672 
  1673 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1674 by (simp add: card_cartesian_product)
  1675 
  1676 
  1677 
  1678 subsubsection {* Cardinality of the Powerset *}
  1679 
  1680 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1681   apply (induct set: Finites)
  1682    apply (simp_all add: Pow_insert)
  1683   apply (subst card_Un_disjoint, blast)
  1684     apply (blast intro: finite_imageI, blast)
  1685   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1686    apply (simp add: card_image Pow_insert)
  1687   apply (unfold inj_on_def)
  1688   apply (blast elim!: equalityE)
  1689   done
  1690 
  1691 text {* Relates to equivalence classes.  Based on a theorem of
  1692 F. Kammüller's.  *}
  1693 
  1694 lemma dvd_partition:
  1695   "finite (Union C) ==>
  1696     ALL c : C. k dvd card c ==>
  1697     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1698   k dvd card (Union C)"
  1699 apply(frule finite_UnionD)
  1700 apply(rotate_tac -1)
  1701   apply (induct set: Finites, simp_all, clarify)
  1702   apply (subst card_Un_disjoint)
  1703   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1704   done
  1705 
  1706 
  1707 subsubsection {* Theorems about @{text "choose"} *}
  1708 
  1709 text {*
  1710   \medskip Basic theorem about @{text "choose"}.  By Florian
  1711   Kamm\"uller, tidied by LCP.
  1712 *}
  1713 
  1714 lemma card_s_0_eq_empty:
  1715     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1716   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1717   apply (simp cong add: rev_conj_cong)
  1718   done
  1719 
  1720 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1721   ==> {s. s <= insert x M & card(s) = Suc k}
  1722        = {s. s <= M & card(s) = Suc k} Un
  1723          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1724   apply safe
  1725    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1726   apply (drule_tac x = "xa - {x}" in spec)
  1727   apply (subgoal_tac "x \<notin> xa", auto)
  1728   apply (erule rev_mp, subst card_Diff_singleton)
  1729   apply (auto intro: finite_subset)
  1730   done
  1731 
  1732 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1733  as there are sets obtained from the former by inserting a fixed element
  1734  @{term x} into each.*}
  1735 lemma constr_bij:
  1736    "[|finite A; x \<notin> A|] ==>
  1737     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1738     card {B. B <= A & card(B) = k}"
  1739   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1740        apply (auto elim!: equalityE simp add: inj_on_def)
  1741     apply (subst Diff_insert0, auto)
  1742    txt {* finiteness of the two sets *}
  1743    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1744    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1745    apply fast+
  1746   done
  1747 
  1748 text {*
  1749   Main theorem: combinatorial statement about number of subsets of a set.
  1750 *}
  1751 
  1752 lemma n_sub_lemma:
  1753   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1754   apply (induct k)
  1755    apply (simp add: card_s_0_eq_empty, atomize)
  1756   apply (rotate_tac -1, erule finite_induct)
  1757    apply (simp_all (no_asm_simp) cong add: conj_cong
  1758      add: card_s_0_eq_empty choose_deconstruct)
  1759   apply (subst card_Un_disjoint)
  1760      prefer 4 apply (force simp add: constr_bij)
  1761     prefer 3 apply force
  1762    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1763      finite_subset [of _ "Pow (insert x F)", standard])
  1764   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1765   done
  1766 
  1767 theorem n_subsets:
  1768     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1769   by (simp add: n_sub_lemma)
  1770 
  1771 
  1772 subsection{* A fold functional for non-empty sets *}
  1773 
  1774 text{* Does not require start value. *}
  1775 
  1776 consts
  1777   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1778 
  1779 inductive "fold1Set f"
  1780 intros
  1781   fold1Set_insertI [intro]:
  1782    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1783 
  1784 constdefs
  1785   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1786   "fold1 f A == THE x. (A, x) : fold1Set f"
  1787 
  1788 lemma fold1Set_nonempty:
  1789  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1790 by(erule fold1Set.cases, simp_all) 
  1791 
  1792 
  1793 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1794 
  1795 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1796 
  1797 
  1798 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1799   by (blast intro: foldSet.intros elim: foldSet.cases)
  1800 
  1801 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1802   by (unfold fold1_def) blast
  1803 
  1804 lemma finite_nonempty_imp_fold1Set:
  1805   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1806 apply (induct A rule: finite_induct)
  1807 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1808 done
  1809 
  1810 text{*First, some lemmas about @{term foldSet}.*}
  1811 
  1812 lemma (in ACf) foldSet_insert_swap:
  1813 assumes fold: "(A,y) \<in> foldSet f id b"
  1814 shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1815 using fold
  1816 proof (induct rule: foldSet.induct)
  1817   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1818 next
  1819   case (insertI A x y)
  1820     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1821       using insertI by force  --{*how does @{term id} get unfolded?*}
  1822     thus ?case by (simp add: insert_commute AC)
  1823 qed
  1824 
  1825 lemma (in ACf) foldSet_permute_diff:
  1826 assumes fold: "(A,x) \<in> foldSet f id b"
  1827 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1828 using fold
  1829 proof (induct rule: foldSet.induct)
  1830   case emptyI thus ?case by simp
  1831 next
  1832   case (insertI A x y)
  1833   have "a = x \<or> a \<in> A" using insertI by simp
  1834   thus ?case
  1835   proof
  1836     assume "a = x"
  1837     with insertI show ?thesis
  1838       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
  1839   next
  1840     assume ainA: "a \<in> A"
  1841     hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1842       using insertI by (force simp: id_def)
  1843     moreover
  1844     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1845       using ainA insertI by blast
  1846     ultimately show ?thesis by (simp add: id_def)
  1847   qed
  1848 qed
  1849 
  1850 lemma (in ACf) fold1_eq_fold:
  1851      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1852 apply (simp add: fold1_def fold_def) 
  1853 apply (rule the_equality)
  1854 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1855 apply (rule sym, clarify)
  1856 apply (case_tac "Aa=A")
  1857  apply (best intro: the_equality foldSet_determ)  
  1858 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1859  apply (best intro: the_equality foldSet_determ)  
  1860 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1861  prefer 2 apply (blast elim: equalityE) 
  1862 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1863 done
  1864 
  1865 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  1866 apply safe
  1867 apply simp 
  1868 apply (drule_tac x=x in spec)
  1869 apply (drule_tac x="A-{x}" in spec, auto) 
  1870 done
  1871 
  1872 lemma (in ACf) fold1_insert:
  1873   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  1874   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1875 proof -
  1876   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
  1877     by (auto simp add: nonempty_iff)
  1878   with A show ?thesis
  1879     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
  1880 qed
  1881 
  1882 lemma (in ACIf) fold1_insert_idem [simp]:
  1883   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  1884   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1885 proof -
  1886   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
  1887     by (auto simp add: nonempty_iff)
  1888   show ?thesis
  1889   proof cases
  1890     assume "a = x"
  1891     thus ?thesis 
  1892     proof cases
  1893       assume "A' = {}"
  1894       with prems show ?thesis by (simp add: idem) 
  1895     next
  1896       assume "A' \<noteq> {}"
  1897       with prems show ?thesis
  1898 	by (simp add: fold1_insert assoc [symmetric] idem) 
  1899     qed
  1900   next
  1901     assume "a \<noteq> x"
  1902     with prems show ?thesis
  1903       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  1904   qed
  1905 qed
  1906 
  1907 
  1908 text{* Now the recursion rules for definitions: *}
  1909 
  1910 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1911 by(simp add:fold1_singleton)
  1912 
  1913 lemma (in ACf) fold1_insert_def:
  1914   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1915 by(simp add:fold1_insert)
  1916 
  1917 lemma (in ACIf) fold1_insert_idem_def:
  1918   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1919 by(simp add:fold1_insert_idem)
  1920 
  1921 subsubsection{* Determinacy for @{term fold1Set} *}
  1922 
  1923 text{*Not actually used!!*}
  1924 
  1925 lemma (in ACf) foldSet_permute:
  1926   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1927    ==> (insert b A, x) \<in> foldSet f id a"
  1928 apply (case_tac "a=b") 
  1929 apply (auto dest: foldSet_permute_diff) 
  1930 done
  1931 
  1932 lemma (in ACf) fold1Set_determ:
  1933   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1934 proof (clarify elim!: fold1Set.cases)
  1935   fix A x B y a b
  1936   assume Ax: "(A, x) \<in> foldSet f id a"
  1937   assume By: "(B, y) \<in> foldSet f id b"
  1938   assume anotA:  "a \<notin> A"
  1939   assume bnotB:  "b \<notin> B"
  1940   assume eq: "insert a A = insert b B"
  1941   show "y=x"
  1942   proof cases
  1943     assume same: "a=b"
  1944     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1945     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1946   next
  1947     assume diff: "a\<noteq>b"
  1948     let ?D = "B - {a}"
  1949     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1950      and aB: "a \<in> B" and bA: "b \<in> A"
  1951       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1952     with aB bnotB By
  1953     have "(insert b ?D, y) \<in> foldSet f id a" 
  1954       by (auto intro: foldSet_permute simp add: insert_absorb)
  1955     moreover
  1956     have "(insert b ?D, x) \<in> foldSet f id a"
  1957       by (simp add: A [symmetric] Ax) 
  1958     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1959   qed
  1960 qed
  1961 
  1962 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1963   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1964 
  1965 declare
  1966   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1967   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1968   -- {* No more proves involve these relations. *}
  1969 
  1970 subsubsection{* Semi-Lattices *}
  1971 
  1972 locale ACIfSL = ACIf +
  1973   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1974   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1975 
  1976 locale ACIfSLlin = ACIfSL +
  1977   assumes lin: "x\<cdot>y \<in> {x,y}"
  1978 
  1979 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1980 by(simp add: below_def idem)
  1981 
  1982 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1983 proof
  1984   assume "x \<sqsubseteq> y \<cdot> z"
  1985   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1986   have "x \<cdot> y = x"
  1987   proof -
  1988     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1989     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1990     also have "\<dots> = x" by(rule xyzx)
  1991     finally show ?thesis .
  1992   qed
  1993   moreover have "x \<cdot> z = x"
  1994   proof -
  1995     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  1996     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1997     also have "\<dots> = x" by(rule xyzx)
  1998     finally show ?thesis .
  1999   qed
  2000   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  2001 next
  2002   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  2003   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  2004   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  2005   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  2006   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  2007   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  2008 qed
  2009 
  2010 lemma (in ACIfSLlin) above_f_conv:
  2011  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  2012 proof
  2013   assume a: "x \<cdot> y \<sqsubseteq> z"
  2014   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  2015   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  2016   proof
  2017     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  2018   next
  2019     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  2020   qed
  2021 next
  2022   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  2023   thus "x \<cdot> y \<sqsubseteq> z"
  2024   proof
  2025     assume a: "x \<sqsubseteq> z"
  2026     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  2027     also have "x \<cdot> z = x" using a by(simp add:below_def)
  2028     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  2029   next
  2030     assume a: "y \<sqsubseteq> z"
  2031     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  2032     also have "y \<cdot> z = y" using a by(simp add:below_def)
  2033     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  2034   qed
  2035 qed
  2036 
  2037 
  2038 subsubsection{* Lemmas about @{text fold1} *}
  2039 
  2040 lemma (in ACf) fold1_Un:
  2041 assumes A: "finite A" "A \<noteq> {}"
  2042 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2043        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2044 using A
  2045 proof(induct rule:finite_ne_induct)
  2046   case singleton thus ?case by(simp add:fold1_insert)
  2047 next
  2048   case insert thus ?case by (simp add:fold1_insert assoc)
  2049 qed
  2050 
  2051 lemma (in ACIf) fold1_Un2:
  2052 assumes A: "finite A" "A \<noteq> {}"
  2053 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2054        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2055 using A
  2056 proof(induct rule:finite_ne_induct)
  2057   case singleton thus ?case by(simp add:fold1_insert_idem)
  2058 next
  2059   case insert thus ?case by (simp add:fold1_insert_idem assoc)
  2060 qed
  2061 
  2062 lemma (in ACf) fold1_in:
  2063   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  2064   shows "fold1 f A \<in> A"
  2065 using A
  2066 proof (induct rule:finite_ne_induct)
  2067   case singleton thus ?case by simp
  2068 next
  2069   case insert thus ?case using elem by (force simp add:fold1_insert)
  2070 qed
  2071 
  2072 lemma (in ACIfSL) below_fold1_iff:
  2073 assumes A: "finite A" "A \<noteq> {}"
  2074 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  2075 using A
  2076 by(induct rule:finite_ne_induct) simp_all
  2077 
  2078 lemma (in ACIfSL) fold1_belowI:
  2079 assumes A: "finite A" "A \<noteq> {}"
  2080 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  2081 using A
  2082 proof (induct rule:finite_ne_induct)
  2083   case singleton thus ?case by simp
  2084 next
  2085   case (insert x F)
  2086   from insert(5) have "a = x \<or> a \<in> F" by simp
  2087   thus ?case
  2088   proof
  2089     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  2090   next
  2091     assume "a \<in> F"
  2092     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  2093     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  2094       using insert by(simp add:below_def ACI)
  2095     also have "fold1 f F \<cdot> a = fold1 f F"
  2096       using bel  by(simp add:below_def ACI)
  2097     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  2098       using insert by(simp add:below_def ACI)
  2099     finally show ?thesis  by(simp add:below_def)
  2100   qed
  2101 qed
  2102 
  2103 lemma (in ACIfSLlin) fold1_below_iff:
  2104 assumes A: "finite A" "A \<noteq> {}"
  2105 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  2106 using A
  2107 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  2108 
  2109 
  2110 subsubsection{* Lattices *}
  2111 
  2112 locale Lattice = lattice +
  2113   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2114   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2115   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2116 
  2117 locale Distrib_Lattice = distrib_lattice + Lattice
  2118 
  2119 text{* Lattices are semilattices *}
  2120 
  2121 lemma (in Lattice) ACf_inf: "ACf inf"
  2122 by(blast intro: ACf.intro inf_commute inf_assoc)
  2123 
  2124 lemma (in Lattice) ACf_sup: "ACf sup"
  2125 by(blast intro: ACf.intro sup_commute sup_assoc)
  2126 
  2127 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2128 apply(rule ACIf.intro)
  2129 apply(rule ACf_inf)
  2130 apply(rule ACIf_axioms.intro)
  2131 apply(rule inf_idem)
  2132 done
  2133 
  2134 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2135 apply(rule ACIf.intro)
  2136 apply(rule ACf_sup)
  2137 apply(rule ACIf_axioms.intro)
  2138 apply(rule sup_idem)
  2139 done
  2140 
  2141 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2142 apply(rule ACIfSL.intro)
  2143 apply(rule ACf_inf)
  2144 apply(rule ACIf.axioms[OF ACIf_inf])
  2145 apply(rule ACIfSL_axioms.intro)
  2146 apply(rule iffI)
  2147  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2148 apply(erule subst)
  2149 apply(rule inf_le2)
  2150 done
  2151 
  2152 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2153 apply(rule ACIfSL.intro)
  2154 apply(rule ACf_sup)
  2155 apply(rule ACIf.axioms[OF ACIf_sup])
  2156 apply(rule ACIfSL_axioms.intro)
  2157 apply(rule iffI)
  2158  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2159 apply(erule subst)
  2160 apply(rule sup_ge2)
  2161 done
  2162 
  2163 
  2164 subsubsection{* Fold laws in lattices *}
  2165 
  2166 lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2167 apply(unfold Sup_def Inf_def)
  2168 apply(subgoal_tac "EX a. a:A")
  2169 prefer 2 apply blast
  2170 apply(erule exE)
  2171 apply(rule trans)
  2172 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2173 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2174 done
  2175 
  2176 lemma (in Lattice) sup_Inf_absorb[simp]:
  2177   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2178 apply(subst sup_commute)
  2179 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2180 done
  2181 
  2182 lemma (in Lattice) inf_Sup_absorb[simp]:
  2183   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2184 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2185 
  2186 
  2187 lemma (in Distrib_Lattice) sup_Inf1_distrib:
  2188 assumes A: "finite A" "A \<noteq> {}"
  2189 shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2190 using A
  2191 proof (induct rule: finite_ne_induct)
  2192   case singleton thus ?case by(simp add:Inf_def)
  2193 next
  2194   case (insert y A)
  2195   have fin: "finite {x \<squnion> a |a. a \<in> A}"
  2196     by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
  2197   have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
  2198     using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
  2199   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
  2200   also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
  2201   also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
  2202     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def fin])
  2203   also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
  2204     by blast
  2205   finally show ?case .
  2206 qed
  2207 
  2208 lemma (in Distrib_Lattice) sup_Inf2_distrib:
  2209 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2210 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2211 using A
  2212 proof (induct rule: finite_ne_induct)
  2213   case singleton thus ?case
  2214     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2215 next
  2216   case (insert x A)
  2217   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2218     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
  2219   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2220   proof -
  2221     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2222       by blast
  2223     thus ?thesis by(simp add: insert(1) B(1))
  2224   qed
  2225   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2226   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2227     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
  2228   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2229   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}"
  2230     using insert by(simp add:sup_Inf1_distrib[OF B])
  2231   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2232     (is "_ = \<Sqinter>?M")
  2233     using B insert
  2234     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2235   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2236     by blast
  2237   finally show ?case .
  2238 qed
  2239 
  2240 
  2241 subsection{*Min and Max*}
  2242 
  2243 text{* As an application of @{text fold1} we define the minimal and
  2244 maximal element of a (non-empty) set over a linear order. *}
  2245 
  2246 constdefs
  2247   Min :: "('a::linorder)set => 'a"
  2248   "Min  ==  fold1 min"
  2249 
  2250   Max :: "('a::linorder)set => 'a"
  2251   "Max  ==  fold1 max"
  2252 
  2253 
  2254 text{* Before we can do anything, we need to show that @{text min} and
  2255 @{text max} are ACI and the ordering is linear: *}
  2256 
  2257 interpretation min: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2258 apply(rule ACf.intro)
  2259 apply(auto simp:min_def)
  2260 done
  2261 
  2262 interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2263 apply(rule ACIf_axioms.intro)
  2264 apply(auto simp:min_def)
  2265 done
  2266 
  2267 interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2268 apply(rule ACf.intro)
  2269 apply(auto simp:max_def)
  2270 done
  2271 
  2272 interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2273 apply(rule ACIf_axioms.intro)
  2274 apply(auto simp:max_def)
  2275 done
  2276 
  2277 interpretation min:
  2278   ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
  2279 apply(rule ACIfSL_axioms.intro)
  2280 apply(auto simp:min_def)
  2281 done
  2282 
  2283 interpretation min:
  2284   ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
  2285 apply(rule ACIfSLlin_axioms.intro)
  2286 apply(auto simp:min_def)
  2287 done
  2288 
  2289 interpretation max:
  2290   ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
  2291 apply(rule ACIfSL_axioms.intro)
  2292 apply(auto simp:max_def)
  2293 done
  2294 
  2295 interpretation max:
  2296   ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
  2297 apply(rule ACIfSLlin_axioms.intro)
  2298 apply(auto simp:max_def)
  2299 done
  2300 
  2301 interpretation min_max:
  2302   Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2303 apply -
  2304 apply(rule Min_def)
  2305 apply(rule Max_def)
  2306 done
  2307 
  2308 
  2309 interpretation min_max:
  2310   Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2311 .
  2312 
  2313 text{* Now we instantiate the recursion equations and declare them
  2314 simplification rules: *}
  2315 
  2316 (* Making Min (resp. Max) a defined parameter of a locale suitably
  2317   extending ACIf could make the following interpretations more automatic. *)
  2318 
  2319 declare
  2320   fold1_singleton_def[OF Min_def, simp]
  2321   min.fold1_insert_idem_def[OF Min_def, simp]
  2322   fold1_singleton_def[OF Max_def, simp]
  2323   max.fold1_insert_idem_def[OF Max_def, simp]
  2324 
  2325 text{* Now we instantiate some @{text fold1} properties: *}
  2326 
  2327 lemma Min_in [simp]:
  2328   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2329 using min.fold1_in
  2330 by(fastsimp simp: Min_def min_def)
  2331 
  2332 lemma Max_in [simp]:
  2333   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2334 using max.fold1_in
  2335 by(fastsimp simp: Max_def max_def)
  2336 
  2337 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2338 by(simp add: Min_def min.fold1_belowI)
  2339 
  2340 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2341 by(simp add: Max_def max.fold1_belowI)
  2342 
  2343 lemma Min_ge_iff[simp]:
  2344   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2345 by(simp add: Min_def min.below_fold1_iff)
  2346 
  2347 lemma Max_le_iff[simp]:
  2348   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2349 by(simp add: Max_def max.below_fold1_iff)
  2350 
  2351 lemma Min_le_iff:
  2352   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2353 by(simp add: Min_def min.fold1_below_iff)
  2354 
  2355 lemma Max_ge_iff:
  2356   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2357 by(simp add: Max_def max.fold1_below_iff)
  2358 
  2359 end