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