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