src/HOL/Finite_Set.thy
author paulson
Thu Feb 10 16:03:18 2005 +0100 (2005-02-10)
changeset 15521 1ffd04343ac9
parent 15520 0ed33cd8f238
child 15526 748ebc63b807
permissions -rw-r--r--
non-inductive fold1Set proofs
     1 (*  Title:      HOL/Finite_Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4                 Additions by Jeremy Avigad in Feb 2004
     5 *)
     6 
     7 header {* Finite sets *}
     8 
     9 theory Finite_Set
    10 imports Divides Power Inductive Lattice_Locales
    11 begin
    12 
    13 subsection {* Definition and basic properties *}
    14 
    15 consts Finites :: "'a set set"
    16 syntax
    17   finite :: "'a set => bool"
    18 translations
    19   "finite A" == "A : Finites"
    20 
    21 inductive Finites
    22   intros
    23     emptyI [simp, intro!]: "{} : Finites"
    24     insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    25 
    26 axclass finite \<subseteq> type
    27   finite: "finite UNIV"
    28 
    29 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    30   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    31   shows "\<exists>a::'a. a \<notin> A"
    32 proof -
    33   from prems have "A \<noteq> UNIV" by blast
    34   thus ?thesis by blast
    35 qed
    36 
    37 lemma finite_induct [case_names empty insert, induct set: Finites]:
    38   "finite F ==>
    39     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    40   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    41 proof -
    42   assume "P {}" and
    43     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
    44   assume "finite F"
    45   thus "P F"
    46   proof induct
    47     show "P {}" .
    48     fix x F assume F: "finite F" and P: "P F"
    49     show "P (insert x F)"
    50     proof cases
    51       assume "x \<in> F"
    52       hence "insert x F = F" by (rule insert_absorb)
    53       with P show ?thesis by (simp only:)
    54     next
    55       assume "x \<notin> F"
    56       from F this P show ?thesis by (rule insert)
    57     qed
    58   qed
    59 qed
    60 
    61 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
    62 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
    63  \<lbrakk> \<And>x. P{x};
    64    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    65  \<Longrightarrow> P F"
    66 using fin
    67 proof induct
    68   case empty thus ?case by simp
    69 next
    70   case (insert x F)
    71   show ?case
    72   proof cases
    73     assume "F = {}" thus ?thesis using insert(4) by simp
    74   next
    75     assume "F \<noteq> {}" thus ?thesis using insert by blast
    76   qed
    77 qed
    78 
    79 lemma finite_subset_induct [consumes 2, case_names empty insert]:
    80   "finite F ==> F \<subseteq> A ==>
    81     P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    82     P F"
    83 proof -
    84   assume "P {}" and insert:
    85     "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    86   assume "finite F"
    87   thus "F \<subseteq> A ==> P F"
    88   proof induct
    89     show "P {}" .
    90     fix x F assume "finite F" and "x \<notin> F"
    91       and P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
    92     show "P (insert x F)"
    93     proof (rule insert)
    94       from i show "x \<in> A" by blast
    95       from i have "F \<subseteq> A" by blast
    96       with P show "P F" .
    97     qed
    98   qed
    99 qed
   100 
   101 text{* Finite sets are the images of initial segments of natural numbers: *}
   102 
   103 lemma finite_imp_nat_seg_image_inj_on:
   104   assumes fin: "finite A" 
   105   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
   106 using fin
   107 proof induct
   108   case empty
   109   show ?case  
   110   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 
   111   qed
   112 next
   113   case (insert a A)
   114   have notinA: "a \<notin> A" .
   115   from insert.hyps obtain n f
   116     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
   117   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
   118         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
   119     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
   120   thus ?case by blast
   121 qed
   122 
   123 lemma nat_seg_image_imp_finite:
   124   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
   125 proof (induct n)
   126   case 0 thus ?case by simp
   127 next
   128   case (Suc n)
   129   let ?B = "f ` {i. i < n}"
   130   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
   131   show ?case
   132   proof cases
   133     assume "\<exists>k<n. f n = f k"
   134     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
   135     thus ?thesis using finB by simp
   136   next
   137     assume "\<not>(\<exists> k<n. f n = f k)"
   138     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
   139     thus ?thesis using finB by simp
   140   qed
   141 qed
   142 
   143 lemma finite_conv_nat_seg_image:
   144   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
   145 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
   146 
   147 subsubsection{* Finiteness and set theoretic constructions *}
   148 
   149 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
   150   -- {* The union of two finite sets is finite. *}
   151   by (induct set: Finites) simp_all
   152 
   153 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
   154   -- {* Every subset of a finite set is finite. *}
   155 proof -
   156   assume "finite B"
   157   thus "!!A. A \<subseteq> B ==> finite A"
   158   proof induct
   159     case empty
   160     thus ?case by simp
   161   next
   162     case (insert x F A)
   163     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" .
   164     show "finite A"
   165     proof cases
   166       assume x: "x \<in> A"
   167       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
   168       with r have "finite (A - {x})" .
   169       hence "finite (insert x (A - {x}))" ..
   170       also have "insert x (A - {x}) = A" by (rule insert_Diff)
   171       finally show ?thesis .
   172     next
   173       show "A \<subseteq> F ==> ?thesis" .
   174       assume "x \<notin> A"
   175       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
   176     qed
   177   qed
   178 qed
   179 
   180 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   181   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
   182 
   183 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
   184   -- {* The converse obviously fails. *}
   185   by (blast intro: finite_subset)
   186 
   187 lemma finite_insert [simp]: "finite (insert a A) = finite A"
   188   apply (subst insert_is_Un)
   189   apply (simp only: finite_Un, blast)
   190   done
   191 
   192 lemma finite_Union[simp, intro]:
   193  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
   194 by (induct rule:finite_induct) simp_all
   195 
   196 lemma finite_empty_induct:
   197   "finite A ==>
   198   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
   199 proof -
   200   assume "finite A"
   201     and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
   202   have "P (A - A)"
   203   proof -
   204     fix c b :: "'a set"
   205     presume c: "finite c" and b: "finite b"
   206       and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
   207     from c show "c \<subseteq> b ==> P (b - c)"
   208     proof induct
   209       case empty
   210       from P1 show ?case by simp
   211     next
   212       case (insert x F)
   213       have "P (b - F - {x})"
   214       proof (rule P2)
   215         from _ b show "finite (b - F)" by (rule finite_subset) blast
   216         from insert show "x \<in> b - F" by simp
   217         from insert show "P (b - F)" by simp
   218       qed
   219       also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
   220       finally show ?case .
   221     qed
   222   next
   223     show "A \<subseteq> A" ..
   224   qed
   225   thus "P {}" by simp
   226 qed
   227 
   228 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
   229   by (rule Diff_subset [THEN finite_subset])
   230 
   231 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
   232   apply (subst Diff_insert)
   233   apply (case_tac "a : A - B")
   234    apply (rule finite_insert [symmetric, THEN trans])
   235    apply (subst insert_Diff, simp_all)
   236   done
   237 
   238 
   239 text {* Image and Inverse Image over Finite Sets *}
   240 
   241 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   242   -- {* The image of a finite set is finite. *}
   243   by (induct set: Finites) simp_all
   244 
   245 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
   246   apply (frule finite_imageI)
   247   apply (erule finite_subset, assumption)
   248   done
   249 
   250 lemma finite_range_imageI:
   251     "finite (range g) ==> finite (range (%x. f (g x)))"
   252   apply (drule finite_imageI, simp)
   253   done
   254 
   255 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
   256 proof -
   257   have aux: "!!A. finite (A - {}) = finite A" by simp
   258   fix B :: "'a set"
   259   assume "finite B"
   260   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
   261     apply induct
   262      apply simp
   263     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
   264      apply clarify
   265      apply (simp (no_asm_use) add: inj_on_def)
   266      apply (blast dest!: aux [THEN iffD1], atomize)
   267     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
   268     apply (frule subsetD [OF equalityD2 insertI1], clarify)
   269     apply (rule_tac x = xa in bexI)
   270      apply (simp_all add: inj_on_image_set_diff)
   271     done
   272 qed (rule refl)
   273 
   274 
   275 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   276   -- {* The inverse image of a singleton under an injective function
   277          is included in a singleton. *}
   278   apply (auto simp add: inj_on_def)
   279   apply (blast intro: the_equality [symmetric])
   280   done
   281 
   282 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   283   -- {* The inverse image of a finite set under an injective function
   284          is finite. *}
   285   apply (induct set: Finites, simp_all)
   286   apply (subst vimage_insert)
   287   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   288   done
   289 
   290 
   291 text {* The finite UNION of finite sets *}
   292 
   293 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
   294   by (induct set: Finites) simp_all
   295 
   296 text {*
   297   Strengthen RHS to
   298   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   299 
   300   We'd need to prove
   301   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   302   by induction. *}
   303 
   304 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   305   by (blast intro: finite_UN_I finite_subset)
   306 
   307 
   308 text {* Sigma of finite sets *}
   309 
   310 lemma finite_SigmaI [simp]:
   311     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
   312   by (unfold Sigma_def) (blast intro!: finite_UN_I)
   313 
   314 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   315     finite (A <*> B)"
   316   by (rule finite_SigmaI)
   317 
   318 lemma finite_Prod_UNIV:
   319     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
   320   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
   321    apply (erule ssubst)
   322    apply (erule finite_SigmaI, auto)
   323   done
   324 
   325 lemma finite_cartesian_productD1:
   326      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
   327 apply (auto simp add: finite_conv_nat_seg_image) 
   328 apply (drule_tac x=n in spec) 
   329 apply (drule_tac x="fst o f" in spec) 
   330 apply (auto simp add: o_def) 
   331  prefer 2 apply (force dest!: equalityD2) 
   332 apply (drule equalityD1) 
   333 apply (rename_tac y x)
   334 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   335  prefer 2 apply force
   336 apply clarify
   337 apply (rule_tac x=k in image_eqI, auto)
   338 done
   339 
   340 lemma finite_cartesian_productD2:
   341      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
   342 apply (auto simp add: finite_conv_nat_seg_image) 
   343 apply (drule_tac x=n in spec) 
   344 apply (drule_tac x="snd o f" in spec) 
   345 apply (auto simp add: o_def) 
   346  prefer 2 apply (force dest!: equalityD2) 
   347 apply (drule equalityD1)
   348 apply (rename_tac x y)
   349 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)") 
   350  prefer 2 apply force
   351 apply clarify
   352 apply (rule_tac x=k in image_eqI, auto)
   353 done
   354 
   355 
   356 instance unit :: finite
   357 proof
   358   have "finite {()}" by simp
   359   also have "{()} = UNIV" by auto
   360   finally show "finite (UNIV :: unit set)" .
   361 qed
   362 
   363 instance * :: (finite, finite) finite
   364 proof
   365   show "finite (UNIV :: ('a \<times> 'b) set)"
   366   proof (rule finite_Prod_UNIV)
   367     show "finite (UNIV :: 'a set)" by (rule finite)
   368     show "finite (UNIV :: 'b set)" by (rule finite)
   369   qed
   370 qed
   371 
   372 
   373 text {* The powerset of a finite set *}
   374 
   375 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
   376 proof
   377   assume "finite (Pow A)"
   378   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
   379   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
   380 next
   381   assume "finite A"
   382   thus "finite (Pow A)"
   383     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
   384 qed
   385 
   386 
   387 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
   388 by(blast intro: finite_subset[OF subset_Pow_Union])
   389 
   390 
   391 lemma finite_converse [iff]: "finite (r^-1) = finite r"
   392   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   393    apply simp
   394    apply (rule iffI)
   395     apply (erule finite_imageD [unfolded inj_on_def])
   396     apply (simp split add: split_split)
   397    apply (erule finite_imageI)
   398   apply (simp add: converse_def image_def, auto)
   399   apply (rule bexI)
   400    prefer 2 apply assumption
   401   apply simp
   402   done
   403 
   404 
   405 text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
   406 Ehmety) *}
   407 
   408 lemma finite_Field: "finite r ==> finite (Field r)"
   409   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   410   apply (induct set: Finites)
   411    apply (auto simp add: Field_def Domain_insert Range_insert)
   412   done
   413 
   414 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   415   apply clarify
   416   apply (erule trancl_induct)
   417    apply (auto simp add: Field_def)
   418   done
   419 
   420 lemma finite_trancl: "finite (r^+) = finite r"
   421   apply auto
   422    prefer 2
   423    apply (rule trancl_subset_Field2 [THEN finite_subset])
   424    apply (rule finite_SigmaI)
   425     prefer 3
   426     apply (blast intro: r_into_trancl' finite_subset)
   427    apply (auto simp add: finite_Field)
   428   done
   429 
   430 
   431 subsection {* A fold functional for finite sets *}
   432 
   433 text {* The intended behaviour is
   434 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"}
   435 if @{text f} is associative-commutative. For an application of @{text fold}
   436 se the definitions of sums and products over finite sets.
   437 *}
   438 
   439 consts
   440   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
   441 
   442 inductive "foldSet f g z"
   443 intros
   444 emptyI [intro]: "({}, z) : foldSet f g z"
   445 insertI [intro]:
   446      "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
   447       \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
   448 
   449 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
   450 
   451 constdefs
   452   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   453   "fold f g z A == THE x. (A, x) : foldSet f g z"
   454 
   455 text{*A tempting alternative for the definiens is
   456 @{term "if finite A then THE x. (A, x) : foldSet f g e else e"}.
   457 It allows the removal of finiteness assumptions from the theorems
   458 @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}.
   459 The proofs become ugly, with @{text rule_format}. It is not worth the effort.*}
   460 
   461 
   462 lemma Diff1_foldSet:
   463   "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z"
   464 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   465 
   466 lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A"
   467   by (induct set: foldSet) auto
   468 
   469 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z"
   470   by (induct set: Finites) auto
   471 
   472 
   473 subsubsection {* Commutative monoids *}
   474 
   475 locale ACf =
   476   fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   477   assumes commute: "x \<cdot> y = y \<cdot> x"
   478     and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   479 
   480 locale ACe = ACf +
   481   fixes e :: 'a
   482   assumes ident [simp]: "x \<cdot> e = x"
   483 
   484 locale ACIf = ACf +
   485   assumes idem: "x \<cdot> x = x"
   486 
   487 lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   488 proof -
   489   have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   490   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   491   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   492   finally show ?thesis .
   493 qed
   494 
   495 lemmas (in ACf) AC = assoc commute left_commute
   496 
   497 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
   498 proof -
   499   have "x \<cdot> e = x" by (rule ident)
   500   thus ?thesis by (subst commute)
   501 qed
   502 
   503 lemma (in ACIf) idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y"
   504 proof -
   505   have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc)
   506   also have "\<dots> = x \<cdot> y" by(simp add:idem)
   507   finally show ?thesis .
   508 qed
   509 
   510 lemmas (in ACIf) ACI = AC idem idem2
   511 
   512 text{* Instantiation of locales: *}
   513 
   514 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
   515 by(fastsimp intro: ACf.intro add_assoc add_commute)
   516 
   517 lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
   518 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
   519 
   520 
   521 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
   522 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
   523 
   524 lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
   525 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
   526 
   527 
   528 subsubsection{*From @{term foldSet} to @{term fold}*}
   529 
   530 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   531 by (auto simp add: less_Suc_eq) 
   532 
   533 lemma insert_image_inj_on_eq:
   534      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
   535         inj_on h {i. i < Suc m}|] 
   536       ==> A = h ` {i. i < m}"
   537 apply (auto simp add: image_less_Suc inj_on_def)
   538 apply (blast intro: less_trans) 
   539 done
   540 
   541 lemma insert_inj_onE:
   542   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
   543       and inj_on: "inj_on h {i::nat. i<n}"
   544   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
   545 proof (cases n)
   546   case 0 thus ?thesis using aA by auto
   547 next
   548   case (Suc m)
   549   have nSuc: "n = Suc m" . 
   550   have mlessn: "m<n" by (simp add: nSuc)
   551   have "a \<in> h ` {i. i < n}" using aA by blast
   552   then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
   553   let ?hm = "swap k m h"
   554   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
   555     by (simp add: inj_on_swap_iff inj_on)
   556   show ?thesis
   557   proof (intro exI conjI)
   558     show "inj_on ?hm {i. i < m}" using inj_hm
   559       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   560     show "m<n" by (rule mlessn)
   561     show "A = ?hm ` {i. i < m}" 
   562     proof (rule insert_image_inj_on_eq)
   563       show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
   564       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   565       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   566 	using aA hkeq nSuc klessn
   567 	by (auto simp add: swap_def image_less_Suc fun_upd_image 
   568 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
   569     qed
   570   qed
   571 qed
   572 
   573 lemma (in ACf) foldSet_determ_aux:
   574   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   575                 (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
   576    \<Longrightarrow> x' = x"
   577 proof (induct n rule: less_induct)
   578   case (less n)
   579     have IH: "!!m h A x x'. 
   580                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   581                 (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" .
   582     have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z"
   583      and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
   584     show ?case
   585     proof (rule foldSet.cases [OF Afoldx])
   586       assume "(A, x) = ({}, z)"
   587       with Afoldx' show "x' = x" by blast
   588     next
   589       fix B b u
   590       assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B"
   591          and Bu: "(B,u) \<in> foldSet f g z"
   592       hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto
   593       show "x'=x" 
   594       proof (rule foldSet.cases [OF Afoldx'])
   595         assume "(A, x') = ({}, z)"
   596         with AbB show "x' = x" by blast
   597       next
   598 	fix C c v
   599 	assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C"
   600 	   and Cv: "(C,v) \<in> foldSet f g z"
   601 	hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto
   602 	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   603         from insert_inj_onE [OF Beq notinB injh]
   604         obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   605                      and Beq: "B = hB ` {i. i < mB}"
   606                      and lessB: "mB < n" by auto 
   607 	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   608         from insert_inj_onE [OF Ceq notinC injh]
   609         obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   610                        and Ceq: "C = hC ` {i. i < mC}"
   611                        and lessC: "mC < n" by auto 
   612 	show "x'=x"
   613 	proof cases
   614           assume "b=c"
   615 	  then moreover have "B = C" using AbB AcC notinB notinC by auto
   616 	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
   617             by auto
   618 	next
   619 	  assume diff: "b \<noteq> c"
   620 	  let ?D = "B - {c}"
   621 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   622 	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   623 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   624 	  with AbB have "finite ?D" by simp
   625 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   626 	    using finite_imp_foldSet by rules
   627 	  moreover have cinB: "c \<in> B" using B by auto
   628 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   629 	    by(rule Diff1_foldSet)
   630 	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   631           moreover have "g b \<cdot> d = v"
   632 	  proof (rule IH[OF lessC Ceq inj_onC Cv])
   633 	    show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   634 	      by fastsimp
   635 	  qed
   636 	  ultimately show ?thesis using x x' by (auto simp: AC)
   637 	qed
   638       qed
   639     qed
   640   qed
   641 
   642 
   643 lemma (in ACf) foldSet_determ:
   644   "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x"
   645 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   646 apply (blast intro: foldSet_determ_aux [rule_format])
   647 done
   648 
   649 lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
   650   by (unfold fold_def) (blast intro: foldSet_determ)
   651 
   652 text{* The base case for @{text fold}: *}
   653 
   654 lemma fold_empty [simp]: "fold f g z {} = z"
   655   by (unfold fold_def) blast
   656 
   657 lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   658     ((insert x A, v) : foldSet f g z) =
   659     (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
   660   apply auto
   661   apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   662    apply (fastsimp dest: foldSet_imp_finite)
   663   apply (blast intro: foldSet_determ)
   664   done
   665 
   666 text{* The recursion equation for @{text fold}: *}
   667 
   668 lemma (in ACf) fold_insert[simp]:
   669     "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
   670   apply (unfold fold_def)
   671   apply (simp add: fold_insert_aux)
   672   apply (rule the_equality)
   673   apply (auto intro: finite_imp_foldSet
   674     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   675   done
   676 
   677 
   678 text{* A simplified version for idempotent functions: *}
   679 
   680 lemma (in ACIf) fold_insert_idem:
   681 assumes finA: "finite A"
   682 shows "fold f g z (insert a A) = g a \<cdot> fold f g z A"
   683 proof cases
   684   assume "a \<in> A"
   685   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   686     by(blast dest: mk_disjoint_insert)
   687   show ?thesis
   688   proof -
   689     from finA A have finB: "finite B" by(blast intro: finite_subset)
   690     have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
   691     also have "\<dots> = (g a) \<cdot> (fold f g z B)"
   692       using finB disj by simp
   693     also have "\<dots> = g a \<cdot> fold f g z A"
   694       using A finB disj by(simp add:idem assoc[symmetric])
   695     finally show ?thesis .
   696   qed
   697 next
   698   assume "a \<notin> A"
   699   with finA show ?thesis by simp
   700 qed
   701 
   702 lemma (in ACIf) foldI_conv_id:
   703   "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
   704 by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
   705 
   706 subsubsection{*Lemmas about @{text fold}*}
   707 
   708 lemma (in ACf) fold_commute:
   709   "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
   710   apply (induct set: Finites, simp)
   711   apply (simp add: left_commute [of x])
   712   done
   713 
   714 lemma (in ACf) fold_nest_Un_Int:
   715   "finite A ==> finite B
   716     ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   717   apply (induct set: Finites, simp)
   718   apply (simp add: fold_commute Int_insert_left insert_absorb)
   719   done
   720 
   721 lemma (in ACf) fold_nest_Un_disjoint:
   722   "finite A ==> finite B ==> A Int B = {}
   723     ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
   724   by (simp add: fold_nest_Un_Int)
   725 
   726 lemma (in ACf) fold_reindex:
   727 assumes fin: "finite A"
   728 shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
   729 using fin apply induct
   730  apply simp
   731 apply simp
   732 done
   733 
   734 lemma (in ACe) fold_Un_Int:
   735   "finite A ==> finite B ==>
   736     fold f g e A \<cdot> fold f g e B =
   737     fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   738   apply (induct set: Finites, simp)
   739   apply (simp add: AC insert_absorb Int_insert_left)
   740   done
   741 
   742 corollary (in ACe) fold_Un_disjoint:
   743   "finite A ==> finite B ==> A Int B = {} ==>
   744     fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   745   by (simp add: fold_Un_Int)
   746 
   747 lemma (in ACe) fold_UN_disjoint:
   748   "\<lbrakk> finite I; ALL i:I. finite (A i);
   749      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   750    \<Longrightarrow> fold f g e (UNION I A) =
   751        fold f (%i. fold f g e (A i)) e I"
   752   apply (induct set: Finites, simp, atomize)
   753   apply (subgoal_tac "ALL i:F. x \<noteq> i")
   754    prefer 2 apply blast
   755   apply (subgoal_tac "A x Int UNION F A = {}")
   756    prefer 2 apply blast
   757   apply (simp add: fold_Un_disjoint)
   758   done
   759 
   760 text{*Fusion theorem, as described in
   761 Graham Hutton's paper,
   762 A Tutorial on the Universality and Expressiveness of Fold,
   763 JFP 9:4 (355-372), 1999.*}
   764 lemma (in ACf) fold_fusion:
   765       includes ACf g
   766       shows
   767 	"finite A ==> 
   768 	 (!!x y. h (g x y) = f x (h y)) ==>
   769          h (fold g j w A) = fold f j (h w) A"
   770   by (induct set: Finites, simp_all)
   771 
   772 lemma (in ACf) fold_cong:
   773   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   774   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
   775    apply simp
   776   apply (erule finite_induct, simp)
   777   apply (simp add: subset_insert_iff, clarify)
   778   apply (subgoal_tac "finite C")
   779    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   780   apply (subgoal_tac "C = insert x (C - {x})")
   781    prefer 2 apply blast
   782   apply (erule ssubst)
   783   apply (drule spec)
   784   apply (erule (1) notE impE)
   785   apply (simp add: Ball_def del: insert_Diff_single)
   786   done
   787 
   788 lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   789   fold f (%x. fold f (g x) e (B x)) e A =
   790   fold f (split g) e (SIGMA x:A. B x)"
   791 apply (subst Sigma_def)
   792 apply (subst fold_UN_disjoint, assumption, simp)
   793  apply blast
   794 apply (erule fold_cong)
   795 apply (subst fold_UN_disjoint, simp, simp)
   796  apply blast
   797 apply simp
   798 done
   799 
   800 lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   801    fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   802 apply (erule finite_induct, simp)
   803 apply (simp add:AC)
   804 done
   805 
   806 
   807 subsection {* Generalized summation over a set *}
   808 
   809 constdefs
   810   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   811   "setsum f A == if finite A then fold (op +) f 0 A else 0"
   812 
   813 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   814 written @{text"\<Sum>x\<in>A. e"}. *}
   815 
   816 syntax
   817   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   818 syntax (xsymbols)
   819   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   820 syntax (HTML output)
   821   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   822 
   823 translations -- {* Beware of argument permutation! *}
   824   "SUM i:A. b" == "setsum (%i. b) A"
   825   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   826 
   827 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   828  @{text"\<Sum>x|P. e"}. *}
   829 
   830 syntax
   831   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   832 syntax (xsymbols)
   833   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   834 syntax (HTML output)
   835   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   836 
   837 translations
   838   "SUM x|P. t" => "setsum (%x. t) {x. P}"
   839   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   840 
   841 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *}
   842 
   843 syntax
   844   "_Setsum" :: "'a set => 'a::comm_monoid_mult"  ("\<Sum>_" [1000] 999)
   845 
   846 parse_translation {*
   847   let
   848     fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
   849   in [("_Setsum", Setsum_tr)] end;
   850 *}
   851 
   852 print_translation {*
   853 let
   854   fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A
   855     | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   856        if x<>y then raise Match
   857        else let val x' = Syntax.mark_bound x
   858                 val t' = subst_bound(x',t)
   859                 val P' = subst_bound(x',P)
   860             in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
   861 in
   862 [("setsum", setsum_tr')]
   863 end
   864 *}
   865 
   866 lemma setsum_empty [simp]: "setsum f {} = 0"
   867   by (simp add: setsum_def)
   868 
   869 lemma setsum_insert [simp]:
   870     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   871   by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
   872 
   873 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   874   by (simp add: setsum_def)
   875 
   876 lemma setsum_reindex:
   877      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   878 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
   879 
   880 lemma setsum_reindex_id:
   881      "inj_on f B ==> setsum f B = setsum id (f ` B)"
   882 by (auto simp add: setsum_reindex)
   883 
   884 lemma setsum_cong:
   885   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   886 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
   887 
   888 lemma setsum_reindex_cong:
   889      "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
   890       ==> setsum h B = setsum g A"
   891   by (simp add: setsum_reindex cong: setsum_cong)
   892 
   893 lemma setsum_0: "setsum (%i. 0) A = 0"
   894 apply (clarsimp simp: setsum_def)
   895 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
   896 done
   897 
   898 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   899   apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
   900   apply (erule ssubst, rule setsum_0)
   901   apply (rule setsum_cong, auto)
   902   done
   903 
   904 lemma setsum_Un_Int: "finite A ==> finite B ==>
   905   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   906   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   907 by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
   908 
   909 lemma setsum_Un_disjoint: "finite A ==> finite B
   910   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   911 by (subst setsum_Un_Int [symmetric], auto)
   912 
   913 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   914   the lhs need not be, since UNION I A could still be finite.*)
   915 lemma setsum_UN_disjoint:
   916     "finite I ==> (ALL i:I. finite (A i)) ==>
   917         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   918       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   919 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
   920 
   921 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   922 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   923 lemma setsum_Union_disjoint:
   924   "[| (ALL A:C. finite A);
   925       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   926    ==> setsum f (Union C) = setsum (setsum f) C"
   927 apply (cases "finite C") 
   928  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   929   apply (frule setsum_UN_disjoint [of C id f])
   930  apply (unfold Union_def id_def, assumption+)
   931 done
   932 
   933 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   934   the rhs need not be, since SIGMA A B could still be finite.*)
   935 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   936     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   937     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   938 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
   939 
   940 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   941 lemma setsum_cartesian_product: 
   942    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
   943 apply (cases "finite A") 
   944  apply (cases "finite B") 
   945   apply (simp add: setsum_Sigma)
   946  apply (cases "A={}", simp)
   947  apply (simp add: setsum_0) 
   948 apply (auto simp add: setsum_def
   949             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   950 done
   951 
   952 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   953 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
   954 
   955 
   956 subsubsection {* Properties in more restricted classes of structures *}
   957 
   958 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   959   apply (case_tac "finite A")
   960    prefer 2 apply (simp add: setsum_def)
   961   apply (erule rev_mp)
   962   apply (erule finite_induct, auto)
   963   done
   964 
   965 lemma setsum_eq_0_iff [simp]:
   966     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   967   by (induct set: Finites) auto
   968 
   969 lemma setsum_Un_nat: "finite A ==> finite B ==>
   970     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   971   -- {* For the natural numbers, we have subtraction. *}
   972   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   973 
   974 lemma setsum_Un: "finite A ==> finite B ==>
   975     (setsum f (A Un B) :: 'a :: ab_group_add) =
   976       setsum f A + setsum f B - setsum f (A Int B)"
   977   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   978 
   979 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   980     (if a:A then setsum f A - f a else setsum f A)"
   981   apply (case_tac "finite A")
   982    prefer 2 apply (simp add: setsum_def)
   983   apply (erule finite_induct)
   984    apply (auto simp add: insert_Diff_if)
   985   apply (drule_tac a = a in mk_disjoint_insert, auto)
   986   done
   987 
   988 lemma setsum_diff1: "finite A \<Longrightarrow>
   989   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   990   (if a:A then setsum f A - f a else setsum f A)"
   991   by (erule finite_induct) (auto simp add: insert_Diff_if)
   992 
   993 (* By Jeremy Siek: *)
   994 
   995 lemma setsum_diff_nat: 
   996   assumes finB: "finite B"
   997   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   998 using finB
   999 proof (induct)
  1000   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1001 next
  1002   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1003     and xFinA: "insert x F \<subseteq> A"
  1004     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1005   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1006   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1007     by (simp add: setsum_diff1_nat)
  1008   from xFinA have "F \<subseteq> A" by simp
  1009   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1010   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1011     by simp
  1012   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1013   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1014     by simp
  1015   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1016   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1017     by simp
  1018   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1019 qed
  1020 
  1021 lemma setsum_diff:
  1022   assumes le: "finite A" "B \<subseteq> A"
  1023   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1024 proof -
  1025   from le have finiteB: "finite B" using finite_subset by auto
  1026   show ?thesis using finiteB le
  1027     proof (induct)
  1028       case empty
  1029       thus ?case by auto
  1030     next
  1031       case (insert x F)
  1032       thus ?case using le finiteB 
  1033 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1034     qed
  1035   qed
  1036 
  1037 lemma setsum_mono:
  1038   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1039   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1040 proof (cases "finite K")
  1041   case True
  1042   thus ?thesis using le
  1043   proof (induct)
  1044     case empty
  1045     thus ?case by simp
  1046   next
  1047     case insert
  1048     thus ?case using add_mono 
  1049       by force
  1050   qed
  1051 next
  1052   case False
  1053   thus ?thesis
  1054     by (simp add: setsum_def)
  1055 qed
  1056 
  1057 lemma setsum_mono2_nat:
  1058   assumes fin: "finite B" and sub: "A \<subseteq> B"
  1059 shows "setsum f A \<le> (setsum f B :: nat)"
  1060 proof -
  1061   have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
  1062   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1063     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1064   also have "A \<union> (B-A) = B" using sub by blast
  1065   finally show ?thesis .
  1066 qed
  1067 
  1068 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
  1069   - setsum f A"
  1070   by (induct set: Finites, auto)
  1071 
  1072 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1073   setsum f A - setsum g A"
  1074   by (simp add: diff_minus setsum_addf setsum_negf)
  1075 
  1076 lemma setsum_nonneg: "[| finite A;
  1077     \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
  1078     0 \<le> setsum f A";
  1079   apply (induct set: Finites, auto)
  1080   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1081   apply (blast intro: add_mono)
  1082   done
  1083 
  1084 lemma setsum_nonpos: "[| finite A;
  1085     \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
  1086     setsum f A \<le> 0";
  1087   apply (induct set: Finites, auto)
  1088   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1089   apply (blast intro: add_mono)
  1090   done
  1091 
  1092 lemma setsum_mult: 
  1093   fixes f :: "'a => ('b::semiring_0_cancel)"
  1094   shows "r * setsum f A = setsum (%n. r * f n) A"
  1095 proof (cases "finite A")
  1096   case True
  1097   thus ?thesis
  1098   proof (induct)
  1099     case empty thus ?case by simp
  1100   next
  1101     case (insert x A) thus ?case by (simp add: right_distrib)
  1102   qed
  1103 next
  1104   case False thus ?thesis by (simp add: setsum_def)
  1105 qed
  1106 
  1107 lemma setsum_abs: 
  1108   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1109   assumes fin: "finite A" 
  1110   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1111 using fin 
  1112 proof (induct) 
  1113   case empty thus ?case by simp
  1114 next
  1115   case (insert x A)
  1116   thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1117 qed
  1118 
  1119 lemma setsum_abs_ge_zero: 
  1120   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1121   assumes fin: "finite A" 
  1122   shows "0 \<le> setsum (%i. abs(f i)) A"
  1123 using fin 
  1124 proof (induct) 
  1125   case empty thus ?case by simp
  1126 next
  1127   case (insert x A) thus ?case by (auto intro: order_trans)
  1128 qed
  1129 
  1130 
  1131 subsection {* Generalized product over a set *}
  1132 
  1133 constdefs
  1134   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1135   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1136 
  1137 syntax
  1138   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_:_. _)" [0, 51, 10] 10)
  1139 
  1140 syntax (xsymbols)
  1141   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1142 syntax (HTML output)
  1143   "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1144 translations
  1145   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
  1146 
  1147 syntax
  1148   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1149 
  1150 parse_translation {*
  1151   let
  1152     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1153   in [("_Setprod", Setprod_tr)] end;
  1154 *}
  1155 print_translation {*
  1156 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1157     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1158 in
  1159 [("setprod", setprod_tr')]
  1160 end
  1161 *}
  1162 
  1163 
  1164 lemma setprod_empty [simp]: "setprod f {} = 1"
  1165   by (auto simp add: setprod_def)
  1166 
  1167 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1168     setprod f (insert a A) = f a * setprod f A"
  1169 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
  1170 
  1171 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1172   by (simp add: setprod_def)
  1173 
  1174 lemma setprod_reindex:
  1175      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1176 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
  1177 
  1178 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1179 by (auto simp add: setprod_reindex)
  1180 
  1181 lemma setprod_cong:
  1182   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1183 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
  1184 
  1185 lemma setprod_reindex_cong: "inj_on f A ==>
  1186     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1187   by (frule setprod_reindex, simp)
  1188 
  1189 
  1190 lemma setprod_1: "setprod (%i. 1) A = 1"
  1191   apply (case_tac "finite A")
  1192   apply (erule finite_induct, auto simp add: mult_ac)
  1193   done
  1194 
  1195 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1196   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1197   apply (erule ssubst, rule setprod_1)
  1198   apply (rule setprod_cong, auto)
  1199   done
  1200 
  1201 lemma setprod_Un_Int: "finite A ==> finite B
  1202     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1203 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
  1204 
  1205 lemma setprod_Un_disjoint: "finite A ==> finite B
  1206   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1207 by (subst setprod_Un_Int [symmetric], auto)
  1208 
  1209 lemma setprod_UN_disjoint:
  1210     "finite I ==> (ALL i:I. finite (A i)) ==>
  1211         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1212       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1213 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
  1214 
  1215 lemma setprod_Union_disjoint:
  1216   "[| (ALL A:C. finite A);
  1217       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1218    ==> setprod f (Union C) = setprod (setprod f) C"
  1219 apply (cases "finite C") 
  1220  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1221   apply (frule setprod_UN_disjoint [of C id f])
  1222  apply (unfold Union_def id_def, assumption+)
  1223 done
  1224 
  1225 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1226     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
  1227     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
  1228 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
  1229 
  1230 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1231 lemma setprod_cartesian_product: 
  1232      "(\<Prod>x:A. (\<Prod>y: B. f x y)) = (\<Prod>z:(A <*> B). f (fst z) (snd z))"
  1233 apply (cases "finite A") 
  1234  apply (cases "finite B") 
  1235   apply (simp add: setprod_Sigma)
  1236  apply (cases "A={}", simp)
  1237  apply (simp add: setprod_1) 
  1238 apply (auto simp add: setprod_def
  1239             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1240 done
  1241 
  1242 lemma setprod_timesf:
  1243      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1244 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
  1245 
  1246 
  1247 subsubsection {* Properties in more restricted classes of structures *}
  1248 
  1249 lemma setprod_eq_1_iff [simp]:
  1250     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1251   by (induct set: Finites) auto
  1252 
  1253 lemma setprod_zero:
  1254      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1255   apply (induct set: Finites, force, clarsimp)
  1256   apply (erule disjE, auto)
  1257   done
  1258 
  1259 lemma setprod_nonneg [rule_format]:
  1260      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1261   apply (case_tac "finite A")
  1262   apply (induct set: Finites, force, clarsimp)
  1263   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1264   apply (rule mult_mono, assumption+)
  1265   apply (auto simp add: setprod_def)
  1266   done
  1267 
  1268 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1269      --> 0 < setprod f A"
  1270   apply (case_tac "finite A")
  1271   apply (induct set: Finites, force, clarsimp)
  1272   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1273   apply (rule mult_strict_mono, assumption+)
  1274   apply (auto simp add: setprod_def)
  1275   done
  1276 
  1277 lemma setprod_nonzero [rule_format]:
  1278     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1279       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1280   apply (erule finite_induct, auto)
  1281   done
  1282 
  1283 lemma setprod_zero_eq:
  1284     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1285      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1286   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1287   done
  1288 
  1289 lemma setprod_nonzero_field:
  1290     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1291   apply (rule setprod_nonzero, auto)
  1292   done
  1293 
  1294 lemma setprod_zero_eq_field:
  1295     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1296   apply (rule setprod_zero_eq, auto)
  1297   done
  1298 
  1299 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1300     (setprod f (A Un B) :: 'a ::{field})
  1301       = setprod f A * setprod f B / setprod f (A Int B)"
  1302   apply (subst setprod_Un_Int [symmetric], auto)
  1303   apply (subgoal_tac "finite (A Int B)")
  1304   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1305   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1306   done
  1307 
  1308 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1309     (setprod f (A - {a}) :: 'a :: {field}) =
  1310       (if a:A then setprod f A / f a else setprod f A)"
  1311   apply (erule finite_induct)
  1312    apply (auto simp add: insert_Diff_if)
  1313   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1314   apply (erule ssubst)
  1315   apply (subst times_divide_eq_right [THEN sym])
  1316   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1317   done
  1318 
  1319 lemma setprod_inversef: "finite A ==>
  1320     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1321       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1322   apply (erule finite_induct)
  1323   apply (simp, simp)
  1324   done
  1325 
  1326 lemma setprod_dividef:
  1327      "[|finite A;
  1328         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1329       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1330   apply (subgoal_tac
  1331          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1332   apply (erule ssubst)
  1333   apply (subst divide_inverse)
  1334   apply (subst setprod_timesf)
  1335   apply (subst setprod_inversef, assumption+, rule refl)
  1336   apply (rule setprod_cong, rule refl)
  1337   apply (subst divide_inverse, auto)
  1338   done
  1339 
  1340 subsection {* Finite cardinality *}
  1341 
  1342 text {* This definition, although traditional, is ugly to work with:
  1343 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1344 But now that we have @{text setsum} things are easy:
  1345 *}
  1346 
  1347 constdefs
  1348   card :: "'a set => nat"
  1349   "card A == setsum (%x. 1::nat) A"
  1350 
  1351 lemma card_empty [simp]: "card {} = 0"
  1352   by (simp add: card_def)
  1353 
  1354 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1355   by (simp add: card_def)
  1356 
  1357 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1358 by (simp add: card_def)
  1359 
  1360 lemma card_insert_disjoint [simp]:
  1361   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1362 by(simp add: card_def ACf.fold_insert[OF ACf_add])
  1363 
  1364 lemma card_insert_if:
  1365     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1366   by (simp add: insert_absorb)
  1367 
  1368 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1369   apply auto
  1370   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1371   done
  1372 
  1373 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1374 by auto
  1375 
  1376 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1377 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1378 apply(simp del:insert_Diff_single)
  1379 done
  1380 
  1381 lemma card_Diff_singleton:
  1382     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1383   by (simp add: card_Suc_Diff1 [symmetric])
  1384 
  1385 lemma card_Diff_singleton_if:
  1386     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1387   by (simp add: card_Diff_singleton)
  1388 
  1389 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1390   by (simp add: card_insert_if card_Suc_Diff1)
  1391 
  1392 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1393   by (simp add: card_insert_if)
  1394 
  1395 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1396 by (simp add: card_def setsum_mono2_nat)
  1397 
  1398 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1399   apply (induct set: Finites, simp, clarify)
  1400   apply (subgoal_tac "finite A & A - {x} <= F")
  1401    prefer 2 apply (blast intro: finite_subset, atomize)
  1402   apply (drule_tac x = "A - {x}" in spec)
  1403   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1404   apply (case_tac "card A", auto)
  1405   done
  1406 
  1407 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1408   apply (simp add: psubset_def linorder_not_le [symmetric])
  1409   apply (blast dest: card_seteq)
  1410   done
  1411 
  1412 lemma card_Un_Int: "finite A ==> finite B
  1413     ==> card A + card B = card (A Un B) + card (A Int B)"
  1414 by(simp add:card_def setsum_Un_Int)
  1415 
  1416 lemma card_Un_disjoint: "finite A ==> finite B
  1417     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1418   by (simp add: card_Un_Int)
  1419 
  1420 lemma card_Diff_subset:
  1421   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1422 by(simp add:card_def setsum_diff_nat)
  1423 
  1424 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1425   apply (rule Suc_less_SucD)
  1426   apply (simp add: card_Suc_Diff1)
  1427   done
  1428 
  1429 lemma card_Diff2_less:
  1430     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1431   apply (case_tac "x = y")
  1432    apply (simp add: card_Diff1_less)
  1433   apply (rule less_trans)
  1434    prefer 2 apply (auto intro!: card_Diff1_less)
  1435   done
  1436 
  1437 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1438   apply (case_tac "x : A")
  1439    apply (simp_all add: card_Diff1_less less_imp_le)
  1440   done
  1441 
  1442 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1443 by (erule psubsetI, blast)
  1444 
  1445 lemma insert_partition:
  1446   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1447   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1448 by auto
  1449 
  1450 (* main cardinality theorem *)
  1451 lemma card_partition [rule_format]:
  1452      "finite C ==>  
  1453         finite (\<Union> C) -->  
  1454         (\<forall>c\<in>C. card c = k) -->   
  1455         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1456         k * card(C) = card (\<Union> C)"
  1457 apply (erule finite_induct, simp)
  1458 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1459        finite_subset [of _ "\<Union> (insert x F)"])
  1460 done
  1461 
  1462 
  1463 lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
  1464   -- {* Generalized to any @{text comm_semiring_1_cancel} in
  1465         @{text IntDef} as @{text setsum_constant}. *}
  1466 apply (cases "finite A") 
  1467 apply (erule finite_induct, auto)
  1468 done
  1469 
  1470 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
  1471   apply (erule finite_induct)
  1472   apply (auto simp add: power_Suc)
  1473   done
  1474 
  1475 
  1476 subsubsection {* Cardinality of unions *}
  1477 
  1478 lemma card_UN_disjoint:
  1479     "finite I ==> (ALL i:I. finite (A i)) ==>
  1480         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1481       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1482   apply (simp add: card_def)
  1483   apply (subgoal_tac
  1484            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1485   apply (simp add: setsum_UN_disjoint)
  1486   apply (simp add: setsum_constant_nat cong: setsum_cong)
  1487   done
  1488 
  1489 lemma card_Union_disjoint:
  1490   "finite C ==> (ALL A:C. finite A) ==>
  1491         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1492       card (Union C) = setsum card C"
  1493   apply (frule card_UN_disjoint [of C id])
  1494   apply (unfold Union_def id_def, assumption+)
  1495   done
  1496 
  1497 subsubsection {* Cardinality of image *}
  1498 
  1499 text{*The image of a finite set can be expressed using @{term fold}.*}
  1500 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1501   apply (erule finite_induct, simp)
  1502   apply (subst ACf.fold_insert) 
  1503   apply (auto simp add: ACf_def) 
  1504   done
  1505 
  1506 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1507   apply (induct set: Finites, simp)
  1508   apply (simp add: le_SucI finite_imageI card_insert_if)
  1509   done
  1510 
  1511 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1512 by(simp add:card_def setsum_reindex o_def)
  1513 
  1514 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1515   by (simp add: card_seteq card_image)
  1516 
  1517 lemma eq_card_imp_inj_on:
  1518   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1519 apply (induct rule:finite_induct, simp)
  1520 apply(frule card_image_le[where f = f])
  1521 apply(simp add:card_insert_if split:if_splits)
  1522 done
  1523 
  1524 lemma inj_on_iff_eq_card:
  1525   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1526 by(blast intro: card_image eq_card_imp_inj_on)
  1527 
  1528 
  1529 lemma card_inj_on_le:
  1530     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1531 apply (subgoal_tac "finite A") 
  1532  apply (force intro: card_mono simp add: card_image [symmetric])
  1533 apply (blast intro: finite_imageD dest: finite_subset) 
  1534 done
  1535 
  1536 lemma card_bij_eq:
  1537     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1538        finite A; finite B |] ==> card A = card B"
  1539   by (auto intro: le_anti_sym card_inj_on_le)
  1540 
  1541 
  1542 subsubsection {* Cardinality of products *}
  1543 
  1544 (*
  1545 lemma SigmaI_insert: "y \<notin> A ==>
  1546   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1547   by auto
  1548 *)
  1549 
  1550 lemma card_SigmaI [simp]:
  1551   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1552   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1553 by(simp add:card_def setsum_Sigma)
  1554 
  1555 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1556 apply (cases "finite A") 
  1557 apply (cases "finite B") 
  1558   apply (simp add: setsum_constant_nat) 
  1559 apply (auto simp add: card_eq_0_iff
  1560             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1561 done
  1562 
  1563 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1564 by (simp add: card_cartesian_product) 
  1565 
  1566 
  1567 
  1568 subsubsection {* Cardinality of the Powerset *}
  1569 
  1570 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1571   apply (induct set: Finites)
  1572    apply (simp_all add: Pow_insert)
  1573   apply (subst card_Un_disjoint, blast)
  1574     apply (blast intro: finite_imageI, blast)
  1575   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1576    apply (simp add: card_image Pow_insert)
  1577   apply (unfold inj_on_def)
  1578   apply (blast elim!: equalityE)
  1579   done
  1580 
  1581 text {* Relates to equivalence classes.  Based on a theorem of
  1582 F. Kammüller's.  *}
  1583 
  1584 lemma dvd_partition:
  1585   "finite (Union C) ==>
  1586     ALL c : C. k dvd card c ==>
  1587     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1588   k dvd card (Union C)"
  1589 apply(frule finite_UnionD)
  1590 apply(rotate_tac -1)
  1591   apply (induct set: Finites, simp_all, clarify)
  1592   apply (subst card_Un_disjoint)
  1593   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1594   done
  1595 
  1596 
  1597 subsubsection {* Theorems about @{text "choose"} *}
  1598 
  1599 text {*
  1600   \medskip Basic theorem about @{text "choose"}.  By Florian
  1601   Kamm\"uller, tidied by LCP.
  1602 *}
  1603 
  1604 lemma card_s_0_eq_empty:
  1605     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
  1606   apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
  1607   apply (simp cong add: rev_conj_cong)
  1608   done
  1609 
  1610 lemma choose_deconstruct: "finite M ==> x \<notin> M
  1611   ==> {s. s <= insert x M & card(s) = Suc k}
  1612        = {s. s <= M & card(s) = Suc k} Un
  1613          {s. EX t. t <= M & card(t) = k & s = insert x t}"
  1614   apply safe
  1615    apply (auto intro: finite_subset [THEN card_insert_disjoint])
  1616   apply (drule_tac x = "xa - {x}" in spec)
  1617   apply (subgoal_tac "x \<notin> xa", auto)
  1618   apply (erule rev_mp, subst card_Diff_singleton)
  1619   apply (auto intro: finite_subset)
  1620   done
  1621 
  1622 text{*There are as many subsets of @{term A} having cardinality @{term k}
  1623  as there are sets obtained from the former by inserting a fixed element
  1624  @{term x} into each.*}
  1625 lemma constr_bij:
  1626    "[|finite A; x \<notin> A|] ==>
  1627     card {B. EX C. C <= A & card(C) = k & B = insert x C} =
  1628     card {B. B <= A & card(B) = k}"
  1629   apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
  1630        apply (auto elim!: equalityE simp add: inj_on_def)
  1631     apply (subst Diff_insert0, auto)
  1632    txt {* finiteness of the two sets *}
  1633    apply (rule_tac [2] B = "Pow (A)" in finite_subset)
  1634    apply (rule_tac B = "Pow (insert x A)" in finite_subset)
  1635    apply fast+
  1636   done
  1637 
  1638 text {*
  1639   Main theorem: combinatorial statement about number of subsets of a set.
  1640 *}
  1641 
  1642 lemma n_sub_lemma:
  1643   "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1644   apply (induct k)
  1645    apply (simp add: card_s_0_eq_empty, atomize)
  1646   apply (rotate_tac -1, erule finite_induct)
  1647    apply (simp_all (no_asm_simp) cong add: conj_cong
  1648      add: card_s_0_eq_empty choose_deconstruct)
  1649   apply (subst card_Un_disjoint)
  1650      prefer 4 apply (force simp add: constr_bij)
  1651     prefer 3 apply force
  1652    prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
  1653      finite_subset [of _ "Pow (insert x F)", standard])
  1654   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
  1655   done
  1656 
  1657 theorem n_subsets:
  1658     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
  1659   by (simp add: n_sub_lemma)
  1660 
  1661 
  1662 subsection{* A fold functional for non-empty sets *}
  1663 
  1664 text{* Does not require start value. *}
  1665 
  1666 consts
  1667   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1668 
  1669 inductive "fold1Set f"
  1670 intros
  1671   fold1Set_insertI [intro]:
  1672    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1673 
  1674 constdefs
  1675   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1676   "fold1 f A == THE x. (A, x) : fold1Set f"
  1677 
  1678 lemma fold1Set_nonempty:
  1679  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1680 by(erule fold1Set.cases, simp_all) 
  1681 
  1682 
  1683 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1684 
  1685 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1686 
  1687 
  1688 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1689   by (blast intro: foldSet.intros elim: foldSet.cases)
  1690 
  1691 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1692   by (unfold fold1_def) blast
  1693 
  1694 lemma finite_nonempty_imp_fold1Set:
  1695   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1696 apply (induct A rule: finite_induct)
  1697 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1698 done
  1699 
  1700 text{*First, some lemmas about @{term foldSet}.*}
  1701 
  1702 lemma (in ACf) foldSet_insert_swap:
  1703 assumes fold: "(A,y) \<in> foldSet f id b"
  1704 shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1705 using fold
  1706 proof (induct rule: foldSet.induct)
  1707   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1708 next
  1709   case (insertI A x y)
  1710     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1711       using insertI by force  --{*how does @{term id} get unfolded?*}
  1712     thus ?case by (simp add: insert_commute AC)
  1713 qed
  1714 
  1715 lemma (in ACf) foldSet_permute_diff:
  1716 assumes fold: "(A,x) \<in> foldSet f id b"
  1717 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1718 using fold
  1719 proof (induct rule: foldSet.induct)
  1720   case emptyI thus ?case by simp
  1721 next
  1722   case (insertI A x y)
  1723   have "a = x \<or> a \<in> A" using insertI by simp
  1724   thus ?case
  1725   proof
  1726     assume "a = x"
  1727     with insertI show ?thesis
  1728       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
  1729   next
  1730     assume ainA: "a \<in> A"
  1731     hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1732       using insertI by (force simp: id_def)
  1733     moreover
  1734     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1735       using ainA insertI by blast
  1736     ultimately show ?thesis by (simp add: id_def)
  1737   qed
  1738 qed
  1739 
  1740 lemma (in ACf) fold1_eq_fold:
  1741      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1742 apply (simp add: fold1_def fold_def) 
  1743 apply (rule the_equality)
  1744 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1745 apply (rule sym, clarify)
  1746 apply (case_tac "Aa=A")
  1747  apply (best intro: the_equality foldSet_determ)  
  1748 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1749  apply (best intro: the_equality foldSet_determ)  
  1750 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1751  prefer 2 apply (blast elim: equalityE) 
  1752 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1753 done
  1754 
  1755 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  1756 apply safe
  1757 apply simp 
  1758 apply (drule_tac x=x in spec)
  1759 apply (drule_tac x="A-{x}" in spec, auto) 
  1760 done
  1761 
  1762 lemma (in ACf) fold1_insert:
  1763   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  1764   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1765 proof -
  1766   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
  1767     by (auto simp add: nonempty_iff)
  1768   with A show ?thesis
  1769     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
  1770 qed
  1771 
  1772 lemma (in ACIf) fold1_insert_idem [simp]:
  1773   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  1774   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1775 proof -
  1776   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
  1777     by (auto simp add: nonempty_iff)
  1778   show ?thesis
  1779   proof cases
  1780     assume "a = x"
  1781     thus ?thesis 
  1782     proof cases
  1783       assume "A' = {}"
  1784       with prems show ?thesis by (simp add: idem) 
  1785     next
  1786       assume "A' \<noteq> {}"
  1787       with prems show ?thesis
  1788 	by (simp add: fold1_insert assoc [symmetric] idem) 
  1789     qed
  1790   next
  1791     assume "a \<noteq> x"
  1792     with prems show ?thesis
  1793       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  1794   qed
  1795 qed
  1796 
  1797 
  1798 text{* Now the recursion rules for definitions: *}
  1799 
  1800 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1801 by(simp add:fold1_singleton)
  1802 
  1803 lemma (in ACf) fold1_insert_def:
  1804   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1805 by(simp add:fold1_insert)
  1806 
  1807 lemma (in ACIf) fold1_insert_idem_def:
  1808   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1809 by(simp add:fold1_insert_idem)
  1810 
  1811 subsubsection{* Determinacy for @{term fold1Set} *}
  1812 
  1813 text{*Not actually used!!*}
  1814 
  1815 lemma (in ACf) foldSet_permute:
  1816   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1817    ==> (insert b A, x) \<in> foldSet f id a"
  1818 apply (case_tac "a=b") 
  1819 apply (auto dest: foldSet_permute_diff) 
  1820 done
  1821 
  1822 lemma (in ACf) fold1Set_determ:
  1823   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1824 proof (clarify elim!: fold1Set.cases)
  1825   fix A x B y a b
  1826   assume Ax: "(A, x) \<in> foldSet f id a"
  1827   assume By: "(B, y) \<in> foldSet f id b"
  1828   assume anotA:  "a \<notin> A"
  1829   assume bnotB:  "b \<notin> B"
  1830   assume eq: "insert a A = insert b B"
  1831   show "y=x"
  1832   proof cases
  1833     assume same: "a=b"
  1834     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1835     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1836   next
  1837     assume diff: "a\<noteq>b"
  1838     let ?D = "B - {a}"
  1839     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1840      and aB: "a \<in> B" and bA: "b \<in> A"
  1841       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1842     with aB bnotB By
  1843     have "(insert b ?D, y) \<in> foldSet f id a" 
  1844       by (auto intro: foldSet_permute simp add: insert_absorb)
  1845     moreover
  1846     have "(insert b ?D, x) \<in> foldSet f id a"
  1847       by (simp add: A [symmetric] Ax) 
  1848     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1849   qed
  1850 qed
  1851 
  1852 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1853   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1854 
  1855 declare
  1856   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1857   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1858   -- {* No more proves involve these relations. *}
  1859 
  1860 subsubsection{* Semi-Lattices *}
  1861 
  1862 locale ACIfSL = ACIf +
  1863   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1864   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1865 
  1866 locale ACIfSLlin = ACIfSL +
  1867   assumes lin: "x\<cdot>y \<in> {x,y}"
  1868 
  1869 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1870 by(simp add: below_def idem)
  1871 
  1872 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1873 proof
  1874   assume "x \<sqsubseteq> y \<cdot> z"
  1875   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1876   have "x \<cdot> y = x"
  1877   proof -
  1878     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1879     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1880     also have "\<dots> = x" by(rule xyzx)
  1881     finally show ?thesis .
  1882   qed
  1883   moreover have "x \<cdot> z = x"
  1884   proof -
  1885     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  1886     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1887     also have "\<dots> = x" by(rule xyzx)
  1888     finally show ?thesis .
  1889   qed
  1890   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  1891 next
  1892   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  1893   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  1894   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  1895   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  1896   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  1897   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  1898 qed
  1899 
  1900 lemma (in ACIfSLlin) above_f_conv:
  1901  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  1902 proof
  1903   assume a: "x \<cdot> y \<sqsubseteq> z"
  1904   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  1905   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1906   proof
  1907     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1908   next
  1909     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1910   qed
  1911 next
  1912   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1913   thus "x \<cdot> y \<sqsubseteq> z"
  1914   proof
  1915     assume a: "x \<sqsubseteq> z"
  1916     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  1917     also have "x \<cdot> z = x" using a by(simp add:below_def)
  1918     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1919   next
  1920     assume a: "y \<sqsubseteq> z"
  1921     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1922     also have "y \<cdot> z = y" using a by(simp add:below_def)
  1923     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1924   qed
  1925 qed
  1926 
  1927 
  1928 subsubsection{* Lemmas about @{text fold1} *}
  1929 
  1930 lemma (in ACf) fold1_Un:
  1931 assumes A: "finite A" "A \<noteq> {}"
  1932 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  1933        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1934 using A
  1935 proof(induct rule:finite_ne_induct)
  1936   case singleton thus ?case by(simp add:fold1_insert)
  1937 next
  1938   case insert thus ?case by (simp add:fold1_insert assoc)
  1939 qed
  1940 
  1941 lemma (in ACIf) fold1_Un2:
  1942 assumes A: "finite A" "A \<noteq> {}"
  1943 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  1944        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1945 using A
  1946 proof(induct rule:finite_ne_induct)
  1947   case singleton thus ?case by(simp add:fold1_insert_idem)
  1948 next
  1949   case insert thus ?case by (simp add:fold1_insert_idem assoc)
  1950 qed
  1951 
  1952 lemma (in ACf) fold1_in:
  1953   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  1954   shows "fold1 f A \<in> A"
  1955 using A
  1956 proof (induct rule:finite_ne_induct)
  1957   case singleton thus ?case by simp
  1958 next
  1959   case insert thus ?case using elem by (force simp add:fold1_insert)
  1960 qed
  1961 
  1962 lemma (in ACIfSL) below_fold1_iff:
  1963 assumes A: "finite A" "A \<noteq> {}"
  1964 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  1965 using A
  1966 by(induct rule:finite_ne_induct) simp_all
  1967 
  1968 lemma (in ACIfSL) fold1_belowI:
  1969 assumes A: "finite A" "A \<noteq> {}"
  1970 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  1971 using A
  1972 proof (induct rule:finite_ne_induct)
  1973   case singleton thus ?case by simp
  1974 next
  1975   case (insert x F)
  1976   from insert(5) have "a = x \<or> a \<in> F" by simp
  1977   thus ?case
  1978   proof
  1979     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  1980   next
  1981     assume "a \<in> F"
  1982     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  1983     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  1984       using insert by(simp add:below_def ACI)
  1985     also have "fold1 f F \<cdot> a = fold1 f F"
  1986       using bel  by(simp add:below_def ACI)
  1987     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  1988       using insert by(simp add:below_def ACI)
  1989     finally show ?thesis  by(simp add:below_def)
  1990   qed
  1991 qed
  1992 
  1993 lemma (in ACIfSLlin) fold1_below_iff:
  1994 assumes A: "finite A" "A \<noteq> {}"
  1995 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  1996 using A
  1997 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  1998 
  1999 
  2000 subsubsection{* Lattices *}
  2001 
  2002 locale Lattice = lattice +
  2003   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2004   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2005   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2006 
  2007 locale Distrib_Lattice = distrib_lattice + Lattice
  2008 
  2009 text{* Lattices are semilattices *}
  2010 
  2011 lemma (in Lattice) ACf_inf: "ACf inf"
  2012 by(blast intro: ACf.intro inf_commute inf_assoc)
  2013 
  2014 lemma (in Lattice) ACf_sup: "ACf sup"
  2015 by(blast intro: ACf.intro sup_commute sup_assoc)
  2016 
  2017 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2018 apply(rule ACIf.intro)
  2019 apply(rule ACf_inf)
  2020 apply(rule ACIf_axioms.intro)
  2021 apply(rule inf_idem)
  2022 done
  2023 
  2024 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2025 apply(rule ACIf.intro)
  2026 apply(rule ACf_sup)
  2027 apply(rule ACIf_axioms.intro)
  2028 apply(rule sup_idem)
  2029 done
  2030 
  2031 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2032 apply(rule ACIfSL.intro)
  2033 apply(rule ACf_inf)
  2034 apply(rule ACIf.axioms[OF ACIf_inf])
  2035 apply(rule ACIfSL_axioms.intro)
  2036 apply(rule iffI)
  2037  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2038 apply(erule subst)
  2039 apply(rule inf_le2)
  2040 done
  2041 
  2042 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2043 apply(rule ACIfSL.intro)
  2044 apply(rule ACf_sup)
  2045 apply(rule ACIf.axioms[OF ACIf_sup])
  2046 apply(rule ACIfSL_axioms.intro)
  2047 apply(rule iffI)
  2048  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2049 apply(erule subst)
  2050 apply(rule sup_ge2)
  2051 done
  2052 
  2053 
  2054 subsubsection{* Fold laws in lattices *}
  2055 
  2056 lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2057 apply(unfold Sup_def Inf_def)
  2058 apply(subgoal_tac "EX a. a:A")
  2059 prefer 2 apply blast
  2060 apply(erule exE)
  2061 apply(rule trans)
  2062 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2063 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2064 done
  2065 
  2066 lemma (in Lattice) sup_Inf_absorb:
  2067   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2068 apply(subst sup_commute)
  2069 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2070 done
  2071 
  2072 lemma (in Lattice) inf_Sup_absorb:
  2073   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2074 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2075 
  2076 
  2077 lemma (in Distrib_Lattice) sup_Inf1_distrib:
  2078 assumes A: "finite A" "A \<noteq> {}"
  2079 shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2080 using A
  2081 proof (induct rule: finite_ne_induct)
  2082   case singleton thus ?case by(simp add:Inf_def)
  2083 next
  2084   case (insert y A)
  2085   have fin: "finite {x \<squnion> a |a. a \<in> A}"
  2086     by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
  2087   have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
  2088     using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
  2089   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
  2090   also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
  2091   also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
  2092     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def fin])
  2093   also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
  2094     by blast
  2095   finally show ?case .
  2096 qed
  2097 
  2098 lemma (in Distrib_Lattice) sup_Inf2_distrib:
  2099 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2100 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2101 using A
  2102 proof (induct rule: finite_ne_induct)
  2103   case singleton thus ?case
  2104     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2105 next
  2106   case (insert x A)
  2107   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2108     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
  2109   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2110   proof -
  2111     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2112       by blast
  2113     thus ?thesis by(simp add: insert(1) B(1))
  2114   qed
  2115   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2116   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2117     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
  2118   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2119   also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2120     using insert by(simp add:sup_Inf1_distrib[OF B])
  2121   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2122     (is "_ = \<Sqinter>?M")
  2123     using B insert
  2124     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2125   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2126     by blast
  2127   finally show ?case .
  2128 qed
  2129 
  2130 
  2131 subsection{*Min and Max*}
  2132 
  2133 text{* As an application of @{text fold1} we define the minimal and
  2134 maximal element of a (non-empty) set over a linear order. *}
  2135 
  2136 constdefs
  2137   Min :: "('a::linorder)set => 'a"
  2138   "Min  ==  fold1 min"
  2139 
  2140   Max :: "('a::linorder)set => 'a"
  2141   "Max  ==  fold1 max"
  2142 
  2143 
  2144 text{* Before we can do anything, we need to show that @{text min} and
  2145 @{text max} are ACI and the ordering is linear: *}
  2146 
  2147 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2148 apply(rule ACf.intro)
  2149 apply(auto simp:min_def)
  2150 done
  2151 
  2152 lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2153 apply(rule ACIf.intro[OF ACf_min])
  2154 apply(rule ACIf_axioms.intro)
  2155 apply(auto simp:min_def)
  2156 done
  2157 
  2158 lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2159 apply(rule ACf.intro)
  2160 apply(auto simp:max_def)
  2161 done
  2162 
  2163 lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2164 apply(rule ACIf.intro[OF ACf_max])
  2165 apply(rule ACIf_axioms.intro)
  2166 apply(auto simp:max_def)
  2167 done
  2168 
  2169 lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
  2170 apply(rule ACIfSL.intro)
  2171 apply(rule ACf_min)
  2172 apply(rule ACIf.axioms[OF ACIf_min])
  2173 apply(rule ACIfSL_axioms.intro)
  2174 apply(auto simp:min_def)
  2175 done
  2176 
  2177 lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
  2178 apply(rule ACIfSLlin.intro)
  2179 apply(rule ACf_min)
  2180 apply(rule ACIf.axioms[OF ACIf_min])
  2181 apply(rule ACIfSL.axioms[OF ACIfSL_min])
  2182 apply(rule ACIfSLlin_axioms.intro)
  2183 apply(auto simp:min_def)
  2184 done
  2185 
  2186 lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
  2187 apply(rule ACIfSL.intro)
  2188 apply(rule ACf_max)
  2189 apply(rule ACIf.axioms[OF ACIf_max])
  2190 apply(rule ACIfSL_axioms.intro)
  2191 apply(auto simp:max_def)
  2192 done
  2193 
  2194 lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
  2195 apply(rule ACIfSLlin.intro)
  2196 apply(rule ACf_max)
  2197 apply(rule ACIf.axioms[OF ACIf_max])
  2198 apply(rule ACIfSL.axioms[OF ACIfSL_max])
  2199 apply(rule ACIfSLlin_axioms.intro)
  2200 apply(auto simp:max_def)
  2201 done
  2202 
  2203 lemma partial_order_order:
  2204  "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
  2205 apply(rule partial_order.intro)
  2206 apply(simp_all)
  2207 done
  2208 
  2209 lemma lower_semilattice_lin_min:
  2210   "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2211 apply(rule lower_semilattice.intro)
  2212 apply(rule partial_order_order)
  2213 apply(rule lower_semilattice_axioms.intro)
  2214 apply(simp add:min_def linorder_not_le order_less_imp_le)
  2215 apply(simp add:min_def linorder_not_le order_less_imp_le)
  2216 apply(simp add:min_def linorder_not_le order_less_imp_le)
  2217 done
  2218 
  2219 lemma upper_semilattice_lin_min:
  2220   "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2221 apply(rule upper_semilattice.intro)
  2222 apply(rule partial_order_order)
  2223 apply(rule upper_semilattice_axioms.intro)
  2224 apply(simp add: max_def linorder_not_le order_less_imp_le)
  2225 apply(simp add: max_def linorder_not_le order_less_imp_le)
  2226 apply(simp add: max_def linorder_not_le order_less_imp_le)
  2227 done
  2228 
  2229 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
  2230 apply(rule Lattice.intro)
  2231 apply(rule partial_order_order)
  2232 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
  2233 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min])
  2234 done
  2235 
  2236 lemma Distrib_Lattice_min_max:
  2237  "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
  2238 apply(rule Distrib_Lattice.intro)
  2239 apply(rule partial_order_order)
  2240 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
  2241 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min])
  2242 apply(rule distrib_lattice_axioms.intro)
  2243 apply(rule_tac x=x and y=y in linorder_le_cases)
  2244 apply(rule_tac x=x and y=z in linorder_le_cases)
  2245 apply(rule_tac x=y and y=z in linorder_le_cases)
  2246 apply(simp add:min_def max_def)
  2247 apply(simp add:min_def max_def)
  2248 apply(rule_tac x=y and y=z in linorder_le_cases)
  2249 apply(simp add:min_def max_def)
  2250 apply(simp add:min_def max_def)
  2251 apply(rule_tac x=x and y=z in linorder_le_cases)
  2252 apply(rule_tac x=y and y=z in linorder_le_cases)
  2253 apply(simp add:min_def max_def)
  2254 apply(simp add:min_def max_def)
  2255 apply(rule_tac x=y and y=z in linorder_le_cases)
  2256 apply(simp add:min_def max_def)
  2257 apply(simp add:min_def max_def)
  2258 done
  2259 
  2260 text{* Now we instantiate the recursion equations and declare them
  2261 simplification rules: *}
  2262 
  2263 declare
  2264   fold1_singleton_def[OF Min_def, simp]
  2265   ACIf.fold1_insert_idem_def[OF ACIf_min Min_def, simp]
  2266   fold1_singleton_def[OF Max_def, simp]
  2267   ACIf.fold1_insert_idem_def[OF ACIf_max Max_def, simp]
  2268 
  2269 text{* Now we instantiate some @{text fold1} properties: *}
  2270 
  2271 lemma Min_in [simp]:
  2272   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2273 using ACf.fold1_in[OF ACf_min]
  2274 by(fastsimp simp: Min_def min_def)
  2275 
  2276 lemma Max_in [simp]:
  2277   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2278 using ACf.fold1_in[OF ACf_max]
  2279 by(fastsimp simp: Max_def max_def)
  2280 
  2281 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2282 by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
  2283 
  2284 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2285 by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
  2286 
  2287 lemma Min_ge_iff[simp]:
  2288   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2289 by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min])
  2290 
  2291 lemma Max_le_iff[simp]:
  2292   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2293 by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max])
  2294 
  2295 lemma Min_le_iff:
  2296   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2297 by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
  2298 
  2299 lemma Max_ge_iff:
  2300   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2301 by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
  2302 
  2303 lemma Min_le_Max:
  2304   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
  2305 by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
  2306 
  2307 lemma max_Min2_distrib:
  2308   "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
  2309   max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
  2310 by(simp add: Min_def Distrib_Lattice.sup_Inf2_distrib[OF Distrib_Lattice_min_max])
  2311 
  2312 end