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