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