src/HOL/Finite_Set.thy
author berghofe
Thu Feb 10 10:43:57 2005 +0100 (2005-02-10)
changeset 15517 3bc57d428ec1
parent 15512 ed1fa4617f52
child 15520 0ed33cd8f238
permissions -rw-r--r--
Subscripts for theorem lists now start at 1.
     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{* Instantiation of locales: *}
   513 
   514 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
   515 by(fastsimp intro: ACf.intro add_assoc add_commute)
   516 
   517 lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
   518 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
   519 
   520 
   521 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
   522 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
   523 
   524 lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
   525 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
   526 
   527 
   528 subsubsection{*From @{term foldSet} to @{term fold}*}
   529 
   530 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   531 by (auto simp add: less_Suc_eq) 
   532 
   533 lemma insert_image_inj_on_eq:
   534      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
   535         inj_on h {i. i < Suc m}|] 
   536       ==> A = h ` {i. i < m}"
   537 apply (auto simp add: image_less_Suc inj_on_def)
   538 apply (blast intro: less_trans) 
   539 done
   540 
   541 lemma insert_inj_onE:
   542   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
   543       and inj_on: "inj_on h {i::nat. i<n}"
   544   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
   545 proof (cases n)
   546   case 0 thus ?thesis using aA by auto
   547 next
   548   case (Suc m)
   549   have nSuc: "n = Suc m" . 
   550   have mlessn: "m<n" by (simp add: nSuc)
   551   have "a \<in> h ` {i. i < n}" using aA by blast
   552   then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
   553   show ?thesis
   554   proof cases
   555     assume eq: "k=m"
   556     show ?thesis
   557     proof (intro exI conjI)
   558       show "inj_on h {i::nat. i<m}" using inj_on
   559 	by (simp add: nSuc inj_on_def) 
   560       show "m<n" by (rule mlessn)
   561       show "A = h ` {i. i < m}" using aA anot nSuc hkeq eq inj_on
   562 	by (rules intro: insert_image_inj_on_eq) 
   563     qed
   564   next
   565     assume diff: "k~=m"
   566     hence klessm: "k<m" using nSuc klessn by arith
   567     have hdiff: "h k ~= h m" using diff inj_on klessn mlessn
   568 	by (auto simp add: inj_on_def) 
   569     let ?hm = "swap k m h"
   570     have inj_onhm_n: "inj_on ?hm {i. i < n}" using klessn mlessn 
   571       by (simp add: inj_on_swap_iff inj_on)
   572     hence inj_onhm_m: "inj_on ?hm {i. i < m}"
   573       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   574     show ?thesis
   575     proof (intro exI conjI)
   576       show "inj_on ?hm {i. i < m}" by (rule inj_onhm_m)
   577       show "m<n" by (simp add: nSuc)
   578       show "A = ?hm ` {i. i < m}" 
   579       proof (rule insert_image_inj_on_eq)
   580 	show "inj_on (swap k m h) {i. i < Suc m}" using inj_onhm_n
   581 	  by (simp add: nSuc)
   582         show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   583         show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   584           using aA hkeq diff hdiff nSuc
   585 	  by (auto simp add: swap_def image_less_Suc fun_upd_image klessm 
   586                              inj_on_image_set_diff [OF inj_on])
   587       qed
   588     qed
   589   qed
   590 qed
   591 
   592 lemma (in ACf) foldSet_determ_aux:
   593   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   594                 (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
   595    \<Longrightarrow> x' = x"
   596 proof (induct n rule: less_induct)
   597   case (less n)
   598     have IH: "!!m h A x x'. 
   599                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   600                 (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" .
   601     have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z"
   602      and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
   603     show ?case
   604     proof (rule foldSet.cases [OF Afoldx])
   605       assume "(A, x) = ({}, z)"
   606       with Afoldx' show "x' = x" by blast
   607     next
   608       fix B b u
   609       assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B"
   610          and Bu: "(B,u) \<in> foldSet f g z"
   611       hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto
   612       show "x'=x" 
   613       proof (rule foldSet.cases [OF Afoldx'])
   614         assume "(A, x') = ({}, z)"
   615         with AbB show "x' = x" by blast
   616       next
   617 	fix C c v
   618 	assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C"
   619 	   and Cv: "(C,v) \<in> foldSet f g z"
   620 	hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto
   621 	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   622         from insert_inj_onE [OF Beq notinB injh]
   623         obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   624                      and Beq: "B = hB ` {i. i < mB}"
   625                      and lessB: "mB < n" by auto 
   626 	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   627         from insert_inj_onE [OF Ceq notinC injh]
   628         obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   629                        and Ceq: "C = hC ` {i. i < mC}"
   630                        and lessC: "mC < n" by auto 
   631 	show "x'=x"
   632 	proof cases
   633           assume "b=c"
   634 	  then moreover have "B = C" using AbB AcC notinB notinC by auto
   635 	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
   636             by auto
   637 	next
   638 	  assume diff: "b \<noteq> c"
   639 	  let ?D = "B - {c}"
   640 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   641 	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   642 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   643 	  with AbB have "finite ?D" by simp
   644 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   645 	    using finite_imp_foldSet by rules
   646 	  moreover have cinB: "c \<in> B" using B by auto
   647 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   648 	    by(rule Diff1_foldSet)
   649 	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   650           moreover have "g b \<cdot> d = v"
   651 	  proof (rule IH[OF lessC Ceq inj_onC Cv])
   652 	    show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   653 	      by fastsimp
   654 	  qed
   655 	  ultimately show ?thesis using x x' by (auto simp: AC)
   656 	qed
   657       qed
   658     qed
   659   qed
   660 
   661 
   662 lemma (in ACf) foldSet_determ:
   663   "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x"
   664 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   665 apply (blast intro: foldSet_determ_aux [rule_format])
   666 done
   667 
   668 lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
   669   by (unfold fold_def) (blast intro: foldSet_determ)
   670 
   671 text{* The base case for @{text fold}: *}
   672 
   673 lemma fold_empty [simp]: "fold f g z {} = z"
   674   by (unfold fold_def) blast
   675 
   676 lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   677     ((insert x A, v) : foldSet f g z) =
   678     (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
   679   apply auto
   680   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   681    apply (fastsimp dest: foldSet_imp_finite)
   682   apply (blast intro: foldSet_determ)
   683   done
   684 
   685 text{* The recursion equation for @{text fold}: *}
   686 
   687 lemma (in ACf) fold_insert[simp]:
   688     "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
   689   apply (unfold fold_def)
   690   apply (simp add: fold_insert_aux)
   691   apply (rule the_equality)
   692   apply (auto intro: finite_imp_foldSet
   693     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   694   done
   695 
   696 
   697 text{* A simplified version for idempotent functions: *}
   698 
   699 lemma (in ACIf) fold_insert_idem:
   700 assumes finA: "finite A"
   701 shows "fold f g z (insert a A) = g a \<cdot> fold f g z A"
   702 proof cases
   703   assume "a \<in> A"
   704   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   705     by(blast dest: mk_disjoint_insert)
   706   show ?thesis
   707   proof -
   708     from finA A have finB: "finite B" by(blast intro: finite_subset)
   709     have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
   710     also have "\<dots> = (g a) \<cdot> (fold f g z B)"
   711       using finB disj by simp
   712     also have "\<dots> = g a \<cdot> fold f g z A"
   713       using A finB disj by(simp add:idem assoc[symmetric])
   714     finally show ?thesis .
   715   qed
   716 next
   717   assume "a \<notin> A"
   718   with finA show ?thesis by simp
   719 qed
   720 
   721 lemma (in ACIf) foldI_conv_id:
   722   "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
   723 by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
   724 
   725 subsubsection{*Lemmas about @{text fold}*}
   726 
   727 lemma (in ACf) fold_commute:
   728   "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
   729   apply (induct set: Finites, simp)
   730   apply (simp add: left_commute [of x])
   731   done
   732 
   733 lemma (in ACf) fold_nest_Un_Int:
   734   "finite A ==> finite B
   735     ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   736   apply (induct set: Finites, simp)
   737   apply (simp add: fold_commute Int_insert_left insert_absorb)
   738   done
   739 
   740 lemma (in ACf) fold_nest_Un_disjoint:
   741   "finite A ==> finite B ==> A Int B = {}
   742     ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
   743   by (simp add: fold_nest_Un_Int)
   744 
   745 lemma (in ACf) fold_reindex:
   746 assumes fin: "finite A"
   747 shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
   748 using fin apply induct
   749  apply simp
   750 apply simp
   751 done
   752 
   753 lemma (in ACe) fold_Un_Int:
   754   "finite A ==> finite B ==>
   755     fold f g e A \<cdot> fold f g e B =
   756     fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   757   apply (induct set: Finites, simp)
   758   apply (simp add: AC insert_absorb Int_insert_left)
   759   done
   760 
   761 corollary (in ACe) fold_Un_disjoint:
   762   "finite A ==> finite B ==> A Int B = {} ==>
   763     fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   764   by (simp add: fold_Un_Int)
   765 
   766 lemma (in ACe) fold_UN_disjoint:
   767   "\<lbrakk> finite I; ALL i:I. finite (A i);
   768      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   769    \<Longrightarrow> fold f g e (UNION I A) =
   770        fold f (%i. fold f g e (A i)) e I"
   771   apply (induct set: Finites, simp, atomize)
   772   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   773    prefer 2 apply blast
   774   apply (subgoal_tac "A x Int UNION F A = {}")
   775    prefer 2 apply blast
   776   apply (simp add: fold_Un_disjoint)
   777   done
   778 
   779 text{*Fusion theorem, as described in
   780 Graham Hutton's paper,
   781 A Tutorial on the Universality and Expressiveness of Fold,
   782 JFP 9:4 (355-372), 1999.*}
   783 lemma (in ACf) fold_fusion:
   784       includes ACf g
   785       shows
   786 	"finite A ==> 
   787 	 (!!x y. h (g x y) = f x (h y)) ==>
   788          h (fold g j w A) = fold f j (h w) A"
   789   by (induct set: Finites, simp_all)
   790 
   791 lemma (in ACf) fold_cong:
   792   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   793   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
   794    apply simp
   795   apply (erule finite_induct, simp)
   796   apply (simp add: subset_insert_iff, clarify)
   797   apply (subgoal_tac "finite C")
   798    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   799   apply (subgoal_tac "C = insert x (C - {x})")
   800    prefer 2 apply blast
   801   apply (erule ssubst)
   802   apply (drule spec)
   803   apply (erule (1) notE impE)
   804   apply (simp add: Ball_def del: insert_Diff_single)
   805   done
   806 
   807 lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   808   fold f (%x. fold f (g x) e (B x)) e A =
   809   fold f (split g) e (SIGMA x:A. B x)"
   810 apply (subst Sigma_def)
   811 apply (subst fold_UN_disjoint, assumption, simp)
   812  apply blast
   813 apply (erule fold_cong)
   814 apply (subst fold_UN_disjoint, simp, simp)
   815  apply blast
   816 apply simp
   817 done
   818 
   819 lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   820    fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   821 apply (erule finite_induct, simp)
   822 apply (simp add:AC)
   823 done
   824 
   825 
   826 subsection {* Generalized summation over a set *}
   827 
   828 constdefs
   829   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   830   "setsum f A == if finite A then fold (op +) f 0 A else 0"
   831 
   832 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   833 written @{text"\<Sum>x\<in>A. e"}. *}
   834 
   835 syntax
   836   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   837 syntax (xsymbols)
   838   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   839 syntax (HTML output)
   840   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   841 
   842 translations -- {* Beware of argument permutation! *}
   843   "SUM i:A. b" == "setsum (%i. b) A"
   844   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   845 
   846 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   847  @{text"\<Sum>x|P. e"}. *}
   848 
   849 syntax
   850   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   851 syntax (xsymbols)
   852   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   853 syntax (HTML output)
   854   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   855 
   856 translations
   857   "SUM x|P. t" => "setsum (%x. t) {x. P}"
   858   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   859 
   860 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
   861 
   862 syntax
   863   "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
   864 
   865 parse_translation {*
   866   let
   867     fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
   868   in [("_Setsum", Setsum_tr)] end;
   869 *}
   870 
   871 print_translation {*
   872 let
   873   fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
   874     | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   875        if x<>y then raise Match
   876        else let val x' = Syntax.mark_bound x
   877                 val t' = subst_bound(x',t)
   878                 val P' = subst_bound(x',P)
   879             in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   880 in
   881 [("setsum", setsum_tr')]
   882 end
   883 *}
   884 
   885 lemma setsum_empty [simp]: "setsum f {} = 0"
   886   by (simp add: setsum_def)
   887 
   888 lemma setsum_insert [simp]:
   889     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   890   by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
   891 
   892 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   893   by (simp add: setsum_def)
   894 
   895 lemma setsum_reindex:
   896      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   897 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
   898 
   899 lemma setsum_reindex_id:
   900      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   901 by (auto simp add: setsum_reindex)
   902 
   903 lemma setsum_cong:
   904   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   905 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
   906 
   907 lemma setsum_reindex_cong:
   908      "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
   909       ==> setsum h B = setsum g A"
   910   by (simp add: setsum_reindex cong: setsum_cong)
   911 
   912 lemma setsum_0: "setsum (%i. 0) A = 0"
   913 apply (clarsimp simp: setsum_def)
   914 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
   915 done
   916 
   917 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   918   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
   919   apply (erule ssubst, rule setsum_0)
   920   apply (rule setsum_cong, auto)
   921   done
   922 
   923 lemma setsum_Un_Int: "finite A ==> finite B ==>
   924   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   925   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   926 by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
   927 
   928 lemma setsum_Un_disjoint: "finite A ==> finite B
   929   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   930 by (subst setsum_Un_Int [symmetric], auto)
   931 
   932 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   933   the lhs need not be, since UNION I A could still be finite.*)
   934 lemma setsum_UN_disjoint:
   935     "finite I ==> (ALL i:I. finite (A i)) ==>
   936         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   937       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   938 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
   939 
   940 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   941 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   942 lemma setsum_Union_disjoint:
   943   "[| (ALL A:C. finite A);
   944       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   945    ==> setsum f (Union C) = setsum (setsum f) C"
   946 apply (cases "finite C") 
   947  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   948   apply (frule setsum_UN_disjoint [of C id f])
   949  apply (unfold Union_def id_def, assumption+)
   950 done
   951 
   952 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   953   the rhs need not be, since SIGMA A B could still be finite.*)
   954 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   955     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   956     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   957 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
   958 
   959 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   960 lemma setsum_cartesian_product: 
   961    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
   962 apply (cases "finite A") 
   963  apply (cases "finite B") 
   964   apply (simp add: setsum_Sigma)
   965  apply (cases "A={}", simp)
   966  apply (simp add: setsum_0) 
   967 apply (auto simp add: setsum_def
   968             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   969 done
   970 
   971 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   972 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
   973 
   974 
   975 subsubsection {* Properties in more restricted classes of structures *}
   976 
   977 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   978   apply (case_tac "finite A")
   979    prefer 2 apply (simp add: setsum_def)
   980   apply (erule rev_mp)
   981   apply (erule finite_induct, auto)
   982   done
   983 
   984 lemma setsum_eq_0_iff [simp]:
   985     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   986   by (induct set: Finites) auto
   987 
   988 lemma setsum_Un_nat: "finite A ==> finite B ==>
   989     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   990   -- {* For the natural numbers, we have subtraction. *}
   991   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   992 
   993 lemma setsum_Un: "finite A ==> finite B ==>
   994     (setsum f (A Un B) :: 'a :: ab_group_add) =
   995       setsum f A + setsum f B - setsum f (A Int B)"
   996   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   997 
   998 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   999     (if a:A then setsum f A - f a else setsum f A)"
  1000   apply (case_tac "finite A")
  1001    prefer 2 apply (simp add: setsum_def)
  1002   apply (erule finite_induct)
  1003    apply (auto simp add: insert_Diff_if)
  1004   apply (drule_tac a = a in mk_disjoint_insert, auto)
  1005   done
  1006 
  1007 lemma setsum_diff1: "finite A \<Longrightarrow>
  1008   (setsum f (A - {a}) :: ('a::ab_group_add)) =
  1009   (if a:A then setsum f A - f a else setsum f A)"
  1010   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1011 
  1012 (* By Jeremy Siek: *)
  1013 
  1014 lemma setsum_diff_nat: 
  1015   assumes finB: "finite B"
  1016   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
  1017 using finB
  1018 proof (induct)
  1019   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1020 next
  1021   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1022     and xFinA: "insert x F \<subseteq> A"
  1023     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1024   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1025   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1026     by (simp add: setsum_diff1_nat)
  1027   from xFinA have "F \<subseteq> A" by simp
  1028   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1029   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1030     by simp
  1031   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1032   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1033     by simp
  1034   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1035   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1036     by simp
  1037   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1038 qed
  1039 
  1040 lemma setsum_diff:
  1041   assumes le: "finite A" "B \<subseteq> A"
  1042   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1043 proof -
  1044   from le have finiteB: "finite B" using finite_subset by auto
  1045   show ?thesis using finiteB le
  1046     proof (induct)
  1047       case empty
  1048       thus ?case by auto
  1049     next
  1050       case (insert x F)
  1051       thus ?case using le finiteB 
  1052 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1053     qed
  1054   qed
  1055 
  1056 lemma setsum_mono:
  1057   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1058   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1059 proof (cases "finite K")
  1060   case True
  1061   thus ?thesis using le
  1062   proof (induct)
  1063     case empty
  1064     thus ?case by simp
  1065   next
  1066     case insert
  1067     thus ?case using add_mono 
  1068       by force
  1069   qed
  1070 next
  1071   case False
  1072   thus ?thesis
  1073     by (simp add: setsum_def)
  1074 qed
  1075 
  1076 lemma setsum_mono2_nat:
  1077   assumes fin: "finite B" and sub: "A \<subseteq> B"
  1078 shows "setsum f A \<le> (setsum f B :: nat)"
  1079 proof -
  1080   have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
  1081   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1082     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1083   also have "A \<union> (B-A) = B" using sub by blast
  1084   finally show ?thesis .
  1085 qed
  1086 
  1087 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
  1088   - setsum f A"
  1089   by (induct set: Finites, auto)
  1090 
  1091 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1092   setsum f A - setsum g A"
  1093   by (simp add: diff_minus setsum_addf setsum_negf)
  1094 
  1095 lemma setsum_nonneg: "[| finite A;
  1096     \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
  1097     0 \<le> setsum f A";
  1098   apply (induct set: Finites, auto)
  1099   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1100   apply (blast intro: add_mono)
  1101   done
  1102 
  1103 lemma setsum_nonpos: "[| finite A;
  1104     \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
  1105     setsum f A \<le> 0";
  1106   apply (induct set: Finites, auto)
  1107   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1108   apply (blast intro: add_mono)
  1109   done
  1110 
  1111 lemma setsum_mult: 
  1112   fixes f :: "'a => ('b::semiring_0_cancel)"
  1113   shows "r * setsum f A = setsum (%n. r * f n) A"
  1114 proof (cases "finite A")
  1115   case True
  1116   thus ?thesis
  1117   proof (induct)
  1118     case empty thus ?case by simp
  1119   next
  1120     case (insert x A) thus ?case by (simp add: right_distrib)
  1121   qed
  1122 next
  1123   case False thus ?thesis by (simp add: setsum_def)
  1124 qed
  1125 
  1126 lemma setsum_abs: 
  1127   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1128   assumes fin: "finite A" 
  1129   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1130 using fin 
  1131 proof (induct) 
  1132   case empty thus ?case by simp
  1133 next
  1134   case (insert x A)
  1135   thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1136 qed
  1137 
  1138 lemma setsum_abs_ge_zero: 
  1139   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1140   assumes fin: "finite A" 
  1141   shows "0 \<le> setsum (%i. abs(f i)) A"
  1142 using fin 
  1143 proof (induct) 
  1144   case empty thus ?case by simp
  1145 next
  1146   case (insert x A) thus ?case by (auto intro: order_trans)
  1147 qed
  1148 
  1149 
  1150 subsection {* Generalized product over a set *}
  1151 
  1152 constdefs
  1153   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1154   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1155 
  1156 syntax
  1157   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
  1158 
  1159 syntax (xsymbols)
  1160   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1161 syntax (HTML output)
  1162   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1163 translations
  1164   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
  1165 
  1166 syntax
  1167   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1168 
  1169 parse_translation {*
  1170   let
  1171     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1172   in [("_Setprod", Setprod_tr)] end;
  1173 *}
  1174 print_translation {*
  1175 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1176     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1177 in
  1178 [("setprod", setprod_tr')]
  1179 end
  1180 *}
  1181 
  1182 
  1183 lemma setprod_empty [simp]: "setprod f {} = 1"
  1184   by (auto simp add: setprod_def)
  1185 
  1186 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1187     setprod f (insert a A) = f a * setprod f A"
  1188 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
  1189 
  1190 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1191   by (simp add: setprod_def)
  1192 
  1193 lemma setprod_reindex:
  1194      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1195 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
  1196 
  1197 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1198 by (auto simp add: setprod_reindex)
  1199 
  1200 lemma setprod_cong:
  1201   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1202 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
  1203 
  1204 lemma setprod_reindex_cong: "inj_on f A ==>
  1205     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1206   by (frule setprod_reindex, simp)
  1207 
  1208 
  1209 lemma setprod_1: "setprod (%i. 1) A = 1"
  1210   apply (case_tac "finite A")
  1211   apply (erule finite_induct, auto simp add: mult_ac)
  1212   done
  1213 
  1214 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1215   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1216   apply (erule ssubst, rule setprod_1)
  1217   apply (rule setprod_cong, auto)
  1218   done
  1219 
  1220 lemma setprod_Un_Int: "finite A ==> finite B
  1221     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1222 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
  1223 
  1224 lemma setprod_Un_disjoint: "finite A ==> finite B
  1225   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1226 by (subst setprod_Un_Int [symmetric], auto)
  1227 
  1228 lemma setprod_UN_disjoint:
  1229     "finite I ==> (ALL i:I. finite (A i)) ==>
  1230         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1231       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1232 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
  1233 
  1234 lemma setprod_Union_disjoint:
  1235   "[| (ALL A:C. finite A);
  1236       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1237    ==> setprod f (Union C) = setprod (setprod f) C"
  1238 apply (cases "finite C") 
  1239  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1240   apply (frule setprod_UN_disjoint [of C id f])
  1241  apply (unfold Union_def id_def, assumption+)
  1242 done
  1243 
  1244 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1245     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
  1246     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
  1247 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
  1248 
  1249 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1250 lemma setprod_cartesian_product: 
  1251      "(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))"
  1252 apply (cases "finite A") 
  1253  apply (cases "finite B") 
  1254   apply (simp add: setprod_Sigma)
  1255  apply (cases "A={}", simp)
  1256  apply (simp add: setprod_1) 
  1257 apply (auto simp add: setprod_def
  1258             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1259 done
  1260 
  1261 lemma setprod_timesf:
  1262      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1263 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
  1264 
  1265 
  1266 subsubsection {* Properties in more restricted classes of structures *}
  1267 
  1268 lemma setprod_eq_1_iff [simp]:
  1269     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1270   by (induct set: Finites) auto
  1271 
  1272 lemma setprod_zero:
  1273      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1274   apply (induct set: Finites, force, clarsimp)
  1275   apply (erule disjE, auto)
  1276   done
  1277 
  1278 lemma setprod_nonneg [rule_format]:
  1279      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1280   apply (case_tac "finite A")
  1281   apply (induct set: Finites, force, clarsimp)
  1282   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1283   apply (rule mult_mono, assumption+)
  1284   apply (auto simp add: setprod_def)
  1285   done
  1286 
  1287 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1288      --> 0 < setprod f A"
  1289   apply (case_tac "finite A")
  1290   apply (induct set: Finites, force, clarsimp)
  1291   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1292   apply (rule mult_strict_mono, assumption+)
  1293   apply (auto simp add: setprod_def)
  1294   done
  1295 
  1296 lemma setprod_nonzero [rule_format]:
  1297     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1298       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1299   apply (erule finite_induct, auto)
  1300   done
  1301 
  1302 lemma setprod_zero_eq:
  1303     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1304      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1305   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1306   done
  1307 
  1308 lemma setprod_nonzero_field:
  1309     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1310   apply (rule setprod_nonzero, auto)
  1311   done
  1312 
  1313 lemma setprod_zero_eq_field:
  1314     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1315   apply (rule setprod_zero_eq, auto)
  1316   done
  1317 
  1318 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1319     (setprod f (A Un B) :: 'a ::{field})
  1320       = setprod f A * setprod f B / setprod f (A Int B)"
  1321   apply (subst setprod_Un_Int [symmetric], auto)
  1322   apply (subgoal_tac "finite (A Int B)")
  1323   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1324   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1325   done
  1326 
  1327 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1328     (setprod f (A - {a}) :: 'a :: {field}) =
  1329       (if a:A then setprod f A / f a else setprod f A)"
  1330   apply (erule finite_induct)
  1331    apply (auto simp add: insert_Diff_if)
  1332   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1333   apply (erule ssubst)
  1334   apply (subst times_divide_eq_right [THEN sym])
  1335   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1336   done
  1337 
  1338 lemma setprod_inversef: "finite A ==>
  1339     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1340       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1341   apply (erule finite_induct)
  1342   apply (simp, simp)
  1343   done
  1344 
  1345 lemma setprod_dividef:
  1346      "[|finite A;
  1347         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1348       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1349   apply (subgoal_tac
  1350          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1351   apply (erule ssubst)
  1352   apply (subst divide_inverse)
  1353   apply (subst setprod_timesf)
  1354   apply (subst setprod_inversef, assumption+, rule refl)
  1355   apply (rule setprod_cong, rule refl)
  1356   apply (subst divide_inverse, auto)
  1357   done
  1358 
  1359 subsection {* Finite cardinality *}
  1360 
  1361 text {* This definition, although traditional, is ugly to work with:
  1362 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1363 But now that we have @{text setsum} things are easy:
  1364 *}
  1365 
  1366 constdefs
  1367   card :: "'a set => nat"
  1368   "card A == setsum (%x. 1::nat) A"
  1369 
  1370 lemma card_empty [simp]: "card {} = 0"
  1371   by (simp add: card_def)
  1372 
  1373 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1374   by (simp add: card_def)
  1375 
  1376 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1377 by (simp add: card_def)
  1378 
  1379 lemma card_insert_disjoint [simp]:
  1380   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1381 by(simp add: card_def ACf.fold_insert[OF ACf_add])
  1382 
  1383 lemma card_insert_if:
  1384     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1385   by (simp add: insert_absorb)
  1386 
  1387 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1388   apply auto
  1389   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1390   done
  1391 
  1392 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1393 by auto
  1394 
  1395 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1396 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1397 apply(simp del:insert_Diff_single)
  1398 done
  1399 
  1400 lemma card_Diff_singleton:
  1401     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1402   by (simp add: card_Suc_Diff1 [symmetric])
  1403 
  1404 lemma card_Diff_singleton_if:
  1405     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1406   by (simp add: card_Diff_singleton)
  1407 
  1408 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1409   by (simp add: card_insert_if card_Suc_Diff1)
  1410 
  1411 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1412   by (simp add: card_insert_if)
  1413 
  1414 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1415 by (simp add: card_def setsum_mono2_nat)
  1416 
  1417 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1418   apply (induct set: Finites, simp, clarify)
  1419   apply (subgoal_tac "finite A & A - {x} <= F")
  1420    prefer 2 apply (blast intro: finite_subset, atomize)
  1421   apply (drule_tac x = "A - {x}" in spec)
  1422   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1423   apply (case_tac "card A", auto)
  1424   done
  1425 
  1426 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1427   apply (simp add: psubset_def linorder_not_le [symmetric])
  1428   apply (blast dest: card_seteq)
  1429   done
  1430 
  1431 lemma card_Un_Int: "finite A ==> finite B
  1432     ==> card A + card B = card (A Un B) + card (A Int B)"
  1433 by(simp add:card_def setsum_Un_Int)
  1434 
  1435 lemma card_Un_disjoint: "finite A ==> finite B
  1436     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1437   by (simp add: card_Un_Int)
  1438 
  1439 lemma card_Diff_subset:
  1440   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1441 by(simp add:card_def setsum_diff_nat)
  1442 
  1443 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1444   apply (rule Suc_less_SucD)
  1445   apply (simp add: card_Suc_Diff1)
  1446   done
  1447 
  1448 lemma card_Diff2_less:
  1449     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1450   apply (case_tac "x = y")
  1451    apply (simp add: card_Diff1_less)
  1452   apply (rule less_trans)
  1453    prefer 2 apply (auto intro!: card_Diff1_less)
  1454   done
  1455 
  1456 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1457   apply (case_tac "x : A")
  1458    apply (simp_all add: card_Diff1_less less_imp_le)
  1459   done
  1460 
  1461 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1462 by (erule psubsetI, blast)
  1463 
  1464 lemma insert_partition:
  1465   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1466   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1467 by auto
  1468 
  1469 (* main cardinality theorem *)
  1470 lemma card_partition [rule_format]:
  1471      "finite C ==>  
  1472         finite (\<Union> C) -->  
  1473         (\<forall>c\<in>C. card c = k) -->   
  1474         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1475         k * card(C) = card (\<Union> C)"
  1476 apply (erule finite_induct, simp)
  1477 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1478        finite_subset [of _ "\<Union> (insert x F)"])
  1479 done
  1480 
  1481 
  1482 lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
  1483   -- {* Generalized to any @{text comm_semiring_1_cancel} in
  1484         @{text IntDef} as @{text setsum_constant}. *}
  1485 apply (cases "finite A") 
  1486 apply (erule finite_induct, auto)
  1487 done
  1488 
  1489 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
  1490   apply (erule finite_induct)
  1491   apply (auto simp add: power_Suc)
  1492   done
  1493 
  1494 
  1495 subsubsection {* Cardinality of unions *}
  1496 
  1497 lemma card_UN_disjoint:
  1498     "finite I ==> (ALL i:I. finite (A i)) ==>
  1499         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1500       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1501   apply (simp add: card_def)
  1502   apply (subgoal_tac
  1503            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1504   apply (simp add: setsum_UN_disjoint)
  1505   apply (simp add: setsum_constant_nat cong: setsum_cong)
  1506   done
  1507 
  1508 lemma card_Union_disjoint:
  1509   "finite C ==> (ALL A:C. finite A) ==>
  1510         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1511       card (Union C) = setsum card C"
  1512   apply (frule card_UN_disjoint [of C id])
  1513   apply (unfold Union_def id_def, assumption+)
  1514   done
  1515 
  1516 subsubsection {* Cardinality of image *}
  1517 
  1518 text{*The image of a finite set can be expressed using @{term fold}.*}
  1519 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1520   apply (erule finite_induct, simp)
  1521   apply (subst ACf.fold_insert) 
  1522   apply (auto simp add: ACf_def) 
  1523   done
  1524 
  1525 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1526   apply (induct set: Finites, simp)
  1527   apply (simp add: le_SucI finite_imageI card_insert_if)
  1528   done
  1529 
  1530 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1531 by(simp add:card_def setsum_reindex o_def)
  1532 
  1533 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1534   by (simp add: card_seteq card_image)
  1535 
  1536 lemma eq_card_imp_inj_on:
  1537   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1538 apply (induct rule:finite_induct, simp)
  1539 apply(frule card_image_le[where f = f])
  1540 apply(simp add:card_insert_if split:if_splits)
  1541 done
  1542 
  1543 lemma inj_on_iff_eq_card:
  1544   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1545 by(blast intro: card_image eq_card_imp_inj_on)
  1546 
  1547 
  1548 lemma card_inj_on_le:
  1549     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1550 apply (subgoal_tac "finite A") 
  1551  apply (force intro: card_mono simp add: card_image [symmetric])
  1552 apply (blast intro: finite_imageD dest: finite_subset) 
  1553 done
  1554 
  1555 lemma card_bij_eq:
  1556     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1557        finite A; finite B |] ==> card A = card B"
  1558   by (auto intro: le_anti_sym card_inj_on_le)
  1559 
  1560 
  1561 subsubsection {* Cardinality of products *}
  1562 
  1563 (*
  1564 lemma SigmaI_insert: "y \<notin> A ==>
  1565   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1566   by auto
  1567 *)
  1568 
  1569 lemma card_SigmaI [simp]:
  1570   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1571   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1572 by(simp add:card_def setsum_Sigma)
  1573 
  1574 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1575 apply (cases "finite A") 
  1576 apply (cases "finite B") 
  1577   apply (simp add: setsum_constant_nat) 
  1578 apply (auto simp add: card_eq_0_iff
  1579             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1580 done
  1581 
  1582 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1583 by (simp add: card_cartesian_product) 
  1584 
  1585 
  1586 
  1587 subsubsection {* Cardinality of the Powerset *}
  1588 
  1589 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1590   apply (induct set: Finites)
  1591    apply (simp_all add: Pow_insert)
  1592   apply (subst card_Un_disjoint, blast)
  1593     apply (blast intro: finite_imageI, blast)
  1594   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1595    apply (simp add: card_image Pow_insert)
  1596   apply (unfold inj_on_def)
  1597   apply (blast elim!: equalityE)
  1598   done
  1599 
  1600 text {* Relates to equivalence classes.  Based on a theorem of
  1601 F. Kammüller's.  *}
  1602 
  1603 lemma dvd_partition:
  1604   "finite (Union C) ==>
  1605     ALL c : C. k dvd card c ==>
  1606     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1607   k dvd card (Union C)"
  1608 apply(frule finite_UnionD)
  1609 apply(rotate_tac -1)
  1610   apply (induct set: Finites, simp_all, clarify)
  1611   apply (subst card_Un_disjoint)
  1612   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1613   done
  1614 
  1615 
  1616 subsubsection {* Theorems about @{text "choose"} *}
  1617 
  1618 text {*
  1619   \medskip Basic theorem about @{text "choose"}.  By Florian
  1620   Kamm\"uller, tidied by LCP.
  1621 *}
  1622 
  1623 lemma card_s_0_eq_empty:
  1624     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1625   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1626   apply (simp cong add: rev_conj_cong)
  1627   done
  1628 
  1629 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1630   ==> {s. s <= insert x M & card(s) = Suc k}
  1631        = {s. s <= M & card(s) = Suc k} Un
  1632          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1633   apply safe
  1634    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1635   apply (drule_tac x = "xa - {x}" in spec)
  1636   apply (subgoal_tac "x \<notin> xa", auto)
  1637   apply (erule rev_mp, subst card_Diff_singleton)
  1638   apply (auto intro: finite_subset)
  1639   done
  1640 
  1641 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1642  as there are sets obtained from the former by inserting a fixed element
  1643  @{term x} into each.*}
  1644 lemma constr_bij:
  1645    "[|finite A; x \<notin> A|] ==>
  1646     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1647     card {B. B <= A & card(B) = k}"
  1648   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1649        apply (auto elim!: equalityE simp add: inj_on_def)
  1650     apply (subst Diff_insert0, auto)
  1651    txt {* finiteness of the two sets *}
  1652    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1653    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1654    apply fast+
  1655   done
  1656 
  1657 text {*
  1658   Main theorem: combinatorial statement about number of subsets of a set.
  1659 *}
  1660 
  1661 lemma n_sub_lemma:
  1662   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1663   apply (induct k)
  1664    apply (simp add: card_s_0_eq_empty, atomize)
  1665   apply (rotate_tac -1, erule finite_induct)
  1666    apply (simp_all (no_asm_simp) cong add: conj_cong
  1667      add: card_s_0_eq_empty choose_deconstruct)
  1668   apply (subst card_Un_disjoint)
  1669      prefer 4 apply (force simp add: constr_bij)
  1670     prefer 3 apply force
  1671    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1672      finite_subset [of _ "Pow (insert x F)", standard])
  1673   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1674   done
  1675 
  1676 theorem n_subsets:
  1677     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1678   by (simp add: n_sub_lemma)
  1679 
  1680 
  1681 subsection{* A fold functional for non-empty sets *}
  1682 
  1683 text{* Does not require start value. *}
  1684 
  1685 consts
  1686   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1687 
  1688 inductive "fold1Set f"
  1689 intros
  1690   fold1Set_insertI [intro]:
  1691    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1692 
  1693 constdefs
  1694   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1695   "fold1 f A == THE x. (A, x) : fold1Set f"
  1696 
  1697 lemma fold1Set_nonempty:
  1698  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1699 by(erule fold1Set.cases, simp_all) 
  1700 
  1701 
  1702 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1703 
  1704 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1705 
  1706 
  1707 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1708   by (blast intro: foldSet.intros elim: foldSet.cases)
  1709 
  1710 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1711   by (unfold fold1_def) blast
  1712 
  1713 lemma finite_nonempty_imp_fold1Set:
  1714   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1715 apply (induct A rule: finite_induct)
  1716 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1717 done
  1718 
  1719 text{*First, some lemmas about @{term foldSet}.*}
  1720 
  1721 
  1722 lemma (in ACf) foldSet_insert_swap:
  1723 assumes fold: "(A,y) \<in> foldSet f id b"
  1724 shows "\<lbrakk> z \<notin> A; b \<notin> A; z \<noteq> b \<rbrakk> \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1725 using fold
  1726 proof (induct rule: foldSet.induct)
  1727   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1728 next
  1729   case (insertI A x y)
  1730     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1731       using insertI by force
  1732     thus ?case by (simp add: insert_commute AC)
  1733 qed
  1734 
  1735 lemma (in ACf) foldSet_permute_diff:
  1736 assumes fold: "(A,x) \<in> foldSet f id b"
  1737 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1738 using fold
  1739 proof (induct rule: foldSet.induct)
  1740   case emptyI thus ?case by simp
  1741 next
  1742   case (insertI A x y)
  1743   show ?case
  1744   proof -
  1745     have a: "a \<in> insert x A" and b: "b \<notin> insert x A" .
  1746     from a have "a = x \<or> a \<in> A" by simp
  1747     thus "(insert b (insert x A - {a}), id x \<cdot> y) \<in> foldSet f id a"
  1748     proof
  1749       assume "a = x"
  1750       with insertI b show ?thesis by simp (blast intro: foldSet_insert_swap)
  1751     next
  1752       assume ainA: "a \<in> A"
  1753       hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1754 	using insertI b by (force simp:id_def)
  1755       moreover
  1756       have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1757 	using ainA insertI by blast
  1758       ultimately show ?thesis by simp
  1759     qed
  1760   qed
  1761 qed
  1762 
  1763 lemma (in ACf) fold1_eq_fold:
  1764      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1765 apply (simp add: fold1_def fold_def) 
  1766 apply (rule the_equality)
  1767 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1768 apply (rule sym, clarify)
  1769 apply (case_tac "Aa=A")
  1770  apply (best intro: the_equality foldSet_determ)  
  1771 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1772  apply (best intro: the_equality foldSet_determ)  
  1773 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1774  prefer 2 apply (blast elim: equalityE) 
  1775 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1776 done
  1777 
  1778 lemma (in ACf) fold1_insert:
  1779   "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  1780 apply (induct A rule: finite_induct, force)
  1781 apply (simp only: insert_commute, simp) 
  1782 apply (erule conjE) 
  1783 apply (simp add: fold1_eq_fold) 
  1784 apply (subst fold1_eq_fold, auto) 
  1785 done
  1786 
  1787 lemma (in ACIf) fold1_insert_idem [simp]:
  1788   "finite A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  1789 apply (induct A rule: finite_induct, force)
  1790 apply (case_tac "xa=x") 
  1791  prefer 2 apply (simp add: insert_commute fold1_eq_fold fold_insert_idem) 
  1792 apply (case_tac "F={}") 
  1793 apply (simp add: idem) 
  1794 apply (simp add: fold1_insert assoc [symmetric] idem) 
  1795 done
  1796 
  1797 
  1798 text{* Now the recursion rules for definitions: *}
  1799 
  1800 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1801 by(simp add:fold1_singleton)
  1802 
  1803 lemma (in ACf) fold1_insert_def:
  1804   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1805 by(simp add:fold1_insert)
  1806 
  1807 lemma (in ACIf) fold1_insert_idem_def:
  1808   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1809 by(simp add:fold1_insert_idem)
  1810 
  1811 subsubsection{* Determinacy for @{term fold1Set} *}
  1812 
  1813 text{*Not actually used!!*}
  1814 
  1815 lemma (in ACf) foldSet_permute:
  1816   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1817    ==> (insert b A, x) \<in> foldSet f id a"
  1818 apply (case_tac "a=b") 
  1819 apply (auto dest: foldSet_permute_diff) 
  1820 done
  1821 
  1822 lemma (in ACf) fold1Set_determ:
  1823   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1824 proof (clarify elim!: fold1Set.cases)
  1825   fix A x B y a b
  1826   assume Ax: "(A, x) \<in> foldSet f id a"
  1827   assume By: "(B, y) \<in> foldSet f id b"
  1828   assume anotA:  "a \<notin> A"
  1829   assume bnotB:  "b \<notin> B"
  1830   assume eq: "insert a A = insert b B"
  1831   show "y=x"
  1832   proof cases
  1833     assume same: "a=b"
  1834     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1835     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1836   next
  1837     assume diff: "a\<noteq>b"
  1838     let ?D = "B - {a}"
  1839     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1840      and aB: "a \<in> B" and bA: "b \<in> A"
  1841       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1842     with aB bnotB By
  1843     have "(insert b ?D, y) \<in> foldSet f id a" 
  1844       by (auto intro: foldSet_permute simp add: insert_absorb)
  1845     moreover
  1846     have "(insert b ?D, x) \<in> foldSet f id a"
  1847       by (simp add: A [symmetric] Ax) 
  1848     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1849   qed
  1850 qed
  1851 
  1852 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1853   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1854 
  1855 declare
  1856   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1857   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1858   -- {* No more proves involve these relations. *}
  1859 
  1860 subsubsection{* Semi-Lattices *}
  1861 
  1862 locale ACIfSL = ACIf +
  1863   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1864   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1865 
  1866 locale ACIfSLlin = ACIfSL +
  1867   assumes lin: "x\<cdot>y \<in> {x,y}"
  1868 
  1869 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1870 by(simp add: below_def idem)
  1871 
  1872 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1873 proof
  1874   assume "x \<sqsubseteq> y \<cdot> z"
  1875   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1876   have "x \<cdot> y = x"
  1877   proof -
  1878     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1879     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1880     also have "\<dots> = x" by(rule xyzx)
  1881     finally show ?thesis .
  1882   qed
  1883   moreover have "x \<cdot> z = x"
  1884   proof -
  1885     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  1886     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1887     also have "\<dots> = x" by(rule xyzx)
  1888     finally show ?thesis .
  1889   qed
  1890   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  1891 next
  1892   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  1893   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  1894   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  1895   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  1896   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  1897   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  1898 qed
  1899 
  1900 lemma (in ACIfSLlin) above_f_conv:
  1901  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  1902 proof
  1903   assume a: "x \<cdot> y \<sqsubseteq> z"
  1904   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  1905   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1906   proof
  1907     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1908   next
  1909     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1910   qed
  1911 next
  1912   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1913   thus "x \<cdot> y \<sqsubseteq> z"
  1914   proof
  1915     assume a: "x \<sqsubseteq> z"
  1916     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  1917     also have "x \<cdot> z = x" using a by(simp add:below_def)
  1918     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1919   next
  1920     assume a: "y \<sqsubseteq> z"
  1921     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1922     also have "y \<cdot> z = y" using a by(simp add:below_def)
  1923     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1924   qed
  1925 qed
  1926 
  1927 
  1928 subsubsection{* Lemmas about @{text fold1} *}
  1929 
  1930 lemma (in ACf) fold1_Un:
  1931 assumes A: "finite A" "A \<noteq> {}"
  1932 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  1933        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1934 using A
  1935 proof(induct rule:finite_ne_induct)
  1936   case singleton thus ?case by(simp add:fold1_insert)
  1937 next
  1938   case insert thus ?case by (simp add:fold1_insert assoc)
  1939 qed
  1940 
  1941 lemma (in ACIf) fold1_Un2:
  1942 assumes A: "finite A" "A \<noteq> {}"
  1943 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  1944        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1945 using A
  1946 proof(induct rule:finite_ne_induct)
  1947   case singleton thus ?case by(simp add:fold1_insert_idem)
  1948 next
  1949   case insert thus ?case by (simp add:fold1_insert_idem assoc)
  1950 qed
  1951 
  1952 lemma (in ACf) fold1_in:
  1953   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  1954   shows "fold1 f A \<in> A"
  1955 using A
  1956 proof (induct rule:finite_ne_induct)
  1957   case singleton thus ?case by simp
  1958 next
  1959   case insert thus ?case using elem by (force simp add:fold1_insert)
  1960 qed
  1961 
  1962 lemma (in ACIfSL) below_fold1_iff:
  1963 assumes A: "finite A" "A \<noteq> {}"
  1964 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  1965 using A
  1966 by(induct rule:finite_ne_induct) simp_all
  1967 
  1968 lemma (in ACIfSL) fold1_belowI:
  1969 assumes A: "finite A" "A \<noteq> {}"
  1970 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  1971 using A
  1972 proof (induct rule:finite_ne_induct)
  1973   case singleton thus ?case by simp
  1974 next
  1975   case (insert x F)
  1976   from insert(5) have "a = x \<or> a \<in> F" by simp
  1977   thus ?case
  1978   proof
  1979     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  1980   next
  1981     assume "a \<in> F"
  1982     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  1983     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  1984       using insert by(simp add:below_def ACI)
  1985     also have "fold1 f F \<cdot> a = fold1 f F"
  1986       using bel  by(simp add:below_def ACI)
  1987     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  1988       using insert by(simp add:below_def ACI)
  1989     finally show ?thesis  by(simp add:below_def)
  1990   qed
  1991 qed
  1992 
  1993 lemma (in ACIfSLlin) fold1_below_iff:
  1994 assumes A: "finite A" "A \<noteq> {}"
  1995 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  1996 using A
  1997 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  1998 
  1999 
  2000 subsubsection{* Lattices *}
  2001 
  2002 locale Lattice = lattice +
  2003   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2004   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2005   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2006 
  2007 locale Distrib_Lattice = distrib_lattice + Lattice
  2008 
  2009 text{* Lattices are semilattices *}
  2010 
  2011 lemma (in Lattice) ACf_inf: "ACf inf"
  2012 by(blast intro: ACf.intro inf_commute inf_assoc)
  2013 
  2014 lemma (in Lattice) ACf_sup: "ACf sup"
  2015 by(blast intro: ACf.intro sup_commute sup_assoc)
  2016 
  2017 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2018 apply(rule ACIf.intro)
  2019 apply(rule ACf_inf)
  2020 apply(rule ACIf_axioms.intro)
  2021 apply(rule inf_idem)
  2022 done
  2023 
  2024 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2025 apply(rule ACIf.intro)
  2026 apply(rule ACf_sup)
  2027 apply(rule ACIf_axioms.intro)
  2028 apply(rule sup_idem)
  2029 done
  2030 
  2031 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2032 apply(rule ACIfSL.intro)
  2033 apply(rule ACf_inf)
  2034 apply(rule ACIf.axioms[OF ACIf_inf])
  2035 apply(rule ACIfSL_axioms.intro)
  2036 apply(rule iffI)
  2037  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2038 apply(erule subst)
  2039 apply(rule inf_le2)
  2040 done
  2041 
  2042 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2043 apply(rule ACIfSL.intro)
  2044 apply(rule ACf_sup)
  2045 apply(rule ACIf.axioms[OF ACIf_sup])
  2046 apply(rule ACIfSL_axioms.intro)
  2047 apply(rule iffI)
  2048  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2049 apply(erule subst)
  2050 apply(rule sup_ge2)
  2051 done
  2052 
  2053 
  2054 subsubsection{* Fold laws in lattices *}
  2055 
  2056 lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2057 apply(unfold Sup_def Inf_def)
  2058 apply(subgoal_tac "EX a. a:A")
  2059 prefer 2 apply blast
  2060 apply(erule exE)
  2061 apply(rule trans)
  2062 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2063 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2064 done
  2065 
  2066 lemma (in Lattice) sup_Inf_absorb:
  2067   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2068 apply(subst sup_commute)
  2069 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2070 done
  2071 
  2072 lemma (in Lattice) inf_Sup_absorb:
  2073   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2074 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2075 
  2076 
  2077 lemma (in Distrib_Lattice) sup_Inf1_distrib:
  2078 assumes A: "finite A" "A \<noteq> {}"
  2079 shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2080 using A
  2081 proof (induct rule: finite_ne_induct)
  2082   case singleton thus ?case by(simp add:Inf_def)
  2083 next
  2084   case (insert y A)
  2085   have fin: "finite {x \<squnion> a |a. a \<in> A}"
  2086     by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
  2087   have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
  2088     using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
  2089   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
  2090   also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
  2091   also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
  2092     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def fin])
  2093   also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
  2094     by blast
  2095   finally show ?case .
  2096 qed
  2097 
  2098 lemma (in Distrib_Lattice) sup_Inf2_distrib:
  2099 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2100 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2101 using A
  2102 proof (induct rule: finite_ne_induct)
  2103   case singleton thus ?case
  2104     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2105 next
  2106   case (insert x A)
  2107   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2108     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
  2109   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2110   proof -
  2111     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2112       by blast
  2113     thus ?thesis by(simp add: insert(1) B(1))
  2114   qed
  2115   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2116   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2117     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
  2118   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2119   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}"
  2120     using insert by(simp add:sup_Inf1_distrib[OF B])
  2121   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2122     (is "_ = \<Sqinter>?M")
  2123     using B insert
  2124     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2125   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2126     by blast
  2127   finally show ?case .
  2128 qed
  2129 
  2130 
  2131 subsection{*Min and Max*}
  2132 
  2133 text{* As an application of @{text fold1} we define the minimal and
  2134 maximal element of a (non-empty) set over a linear order. *}
  2135 
  2136 constdefs
  2137   Min :: "('a::linorder)set => 'a"
  2138   "Min  ==  fold1 min"
  2139 
  2140   Max :: "('a::linorder)set => 'a"
  2141   "Max  ==  fold1 max"
  2142 
  2143 
  2144 text{* Before we can do anything, we need to show that @{text min} and
  2145 @{text max} are ACI and the ordering is linear: *}
  2146 
  2147 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2148 apply(rule ACf.intro)
  2149 apply(auto simp:min_def)
  2150 done
  2151 
  2152 lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2153 apply(rule ACIf.intro[OF ACf_min])
  2154 apply(rule ACIf_axioms.intro)
  2155 apply(auto simp:min_def)
  2156 done
  2157 
  2158 lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2159 apply(rule ACf.intro)
  2160 apply(auto simp:max_def)
  2161 done
  2162 
  2163 lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2164 apply(rule ACIf.intro[OF ACf_max])
  2165 apply(rule ACIf_axioms.intro)
  2166 apply(auto simp:max_def)
  2167 done
  2168 
  2169 lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
  2170 apply(rule ACIfSL.intro)
  2171 apply(rule ACf_min)
  2172 apply(rule ACIf.axioms[OF ACIf_min])
  2173 apply(rule ACIfSL_axioms.intro)
  2174 apply(auto simp:min_def)
  2175 done
  2176 
  2177 lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
  2178 apply(rule ACIfSLlin.intro)
  2179 apply(rule ACf_min)
  2180 apply(rule ACIf.axioms[OF ACIf_min])
  2181 apply(rule ACIfSL.axioms[OF ACIfSL_min])
  2182 apply(rule ACIfSLlin_axioms.intro)
  2183 apply(auto simp:min_def)
  2184 done
  2185 
  2186 lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
  2187 apply(rule ACIfSL.intro)
  2188 apply(rule ACf_max)
  2189 apply(rule ACIf.axioms[OF ACIf_max])
  2190 apply(rule ACIfSL_axioms.intro)
  2191 apply(auto simp:max_def)
  2192 done
  2193 
  2194 lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
  2195 apply(rule ACIfSLlin.intro)
  2196 apply(rule ACf_max)
  2197 apply(rule ACIf.axioms[OF ACIf_max])
  2198 apply(rule ACIfSL.axioms[OF ACIfSL_max])
  2199 apply(rule ACIfSLlin_axioms.intro)
  2200 apply(auto simp:max_def)
  2201 done
  2202 
  2203 lemma partial_order_order:
  2204  "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
  2205 apply(rule partial_order.intro)
  2206 apply(simp_all)
  2207 done
  2208 
  2209 lemma lower_semilattice_lin_min:
  2210   "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2211 apply(rule lower_semilattice.intro)
  2212 apply(rule partial_order_order)
  2213 apply(rule lower_semilattice_axioms.intro)
  2214 apply(simp add:min_def linorder_not_le order_less_imp_le)
  2215 apply(simp add:min_def linorder_not_le order_less_imp_le)
  2216 apply(simp add:min_def linorder_not_le order_less_imp_le)
  2217 done
  2218 
  2219 lemma upper_semilattice_lin_min:
  2220   "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2221 apply(rule upper_semilattice.intro)
  2222 apply(rule partial_order_order)
  2223 apply(rule upper_semilattice_axioms.intro)
  2224 apply(simp add: max_def linorder_not_le order_less_imp_le)
  2225 apply(simp add: max_def linorder_not_le order_less_imp_le)
  2226 apply(simp add: max_def linorder_not_le order_less_imp_le)
  2227 done
  2228 
  2229 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
  2230 apply(rule Lattice.intro)
  2231 apply(rule partial_order_order)
  2232 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
  2233 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min])
  2234 done
  2235 
  2236 lemma Distrib_Lattice_min_max:
  2237  "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
  2238 apply(rule Distrib_Lattice.intro)
  2239 apply(rule partial_order_order)
  2240 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
  2241 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min])
  2242 apply(rule distrib_lattice_axioms.intro)
  2243 apply(rule_tac x=x and y=y in linorder_le_cases)
  2244 apply(rule_tac x=x and y=z in linorder_le_cases)
  2245 apply(rule_tac x=y and y=z in linorder_le_cases)
  2246 apply(simp add:min_def max_def)
  2247 apply(simp add:min_def max_def)
  2248 apply(rule_tac x=y and y=z in linorder_le_cases)
  2249 apply(simp add:min_def max_def)
  2250 apply(simp add:min_def max_def)
  2251 apply(rule_tac x=x and y=z in linorder_le_cases)
  2252 apply(rule_tac x=y and y=z in linorder_le_cases)
  2253 apply(simp add:min_def max_def)
  2254 apply(simp add:min_def max_def)
  2255 apply(rule_tac x=y and y=z in linorder_le_cases)
  2256 apply(simp add:min_def max_def)
  2257 apply(simp add:min_def max_def)
  2258 done
  2259 
  2260 text{* Now we instantiate the recursion equations and declare them
  2261 simplification rules: *}
  2262 
  2263 declare
  2264   fold1_singleton_def[OF Min_def, simp]
  2265   ACIf.fold1_insert_idem_def[OF ACIf_min Min_def, simp]
  2266   fold1_singleton_def[OF Max_def, simp]
  2267   ACIf.fold1_insert_idem_def[OF ACIf_max Max_def, simp]
  2268 
  2269 text{* Now we instantiate some @{text fold1} properties: *}
  2270 
  2271 lemma Min_in [simp]:
  2272   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2273 using ACf.fold1_in[OF ACf_min]
  2274 by(fastsimp simp: Min_def min_def)
  2275 
  2276 lemma Max_in [simp]:
  2277   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2278 using ACf.fold1_in[OF ACf_max]
  2279 by(fastsimp simp: Max_def max_def)
  2280 
  2281 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2282 by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
  2283 
  2284 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2285 by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
  2286 
  2287 lemma Min_ge_iff[simp]:
  2288   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2289 by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min])
  2290 
  2291 lemma Max_le_iff[simp]:
  2292   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2293 by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max])
  2294 
  2295 lemma Min_le_iff:
  2296   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2297 by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
  2298 
  2299 lemma Max_ge_iff:
  2300   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2301 by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
  2302 
  2303 lemma Min_le_Max:
  2304   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
  2305 by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
  2306 
  2307 lemma max_Min2_distrib:
  2308   "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
  2309   max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
  2310 by(simp add: Min_def Distrib_Lattice.sup_Inf2_distrib[OF Distrib_Lattice_min_max])
  2311 
  2312 end