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