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