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