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