src/HOL/Finite_Set.thy
author paulson
Tue Aug 30 12:47:53 2005 +0200 (2005-08-30)
changeset 17189 b15f8e094874
parent 17149 e2b19c92ef51
child 17589 58eeffd73be1
permissions -rw-r--r--
patterns in setsum and setprod
     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" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   810 syntax (xsymbols)
   811   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   812 syntax (HTML output)
   813   "_setsum" :: "pttrn => '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" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   824 syntax (xsymbols)
   825   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   826 syntax (HTML output)
   827   "_qsetsum" :: "pttrn \<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)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   934 by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
   935 
   936 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   937 lemma setsum_cartesian_product: 
   938    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   939 apply (cases "finite A") 
   940  apply (cases "finite B") 
   941   apply (simp add: setsum_Sigma)
   942  apply (cases "A={}", simp)
   943  apply (simp) 
   944 apply (auto simp add: setsum_def
   945             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   946 done
   947 
   948 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   949 by(simp add:setsum_def AC_add.fold_distrib)
   950 
   951 
   952 subsubsection {* Properties in more restricted classes of structures *}
   953 
   954 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   955   apply (case_tac "finite A")
   956    prefer 2 apply (simp add: setsum_def)
   957   apply (erule rev_mp)
   958   apply (erule finite_induct, auto)
   959   done
   960 
   961 lemma setsum_eq_0_iff [simp]:
   962     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   963   by (induct set: Finites) auto
   964 
   965 lemma setsum_Un_nat: "finite A ==> finite B ==>
   966     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   967   -- {* For the natural numbers, we have subtraction. *}
   968   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   969 
   970 lemma setsum_Un: "finite A ==> finite B ==>
   971     (setsum f (A Un B) :: 'a :: ab_group_add) =
   972       setsum f A + setsum f B - setsum f (A Int B)"
   973   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
   974 
   975 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   976     (if a:A then setsum f A - f a else setsum f A)"
   977   apply (case_tac "finite A")
   978    prefer 2 apply (simp add: setsum_def)
   979   apply (erule finite_induct)
   980    apply (auto simp add: insert_Diff_if)
   981   apply (drule_tac a = a in mk_disjoint_insert, auto)
   982   done
   983 
   984 lemma setsum_diff1: "finite A \<Longrightarrow>
   985   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   986   (if a:A then setsum f A - f a else setsum f A)"
   987   by (erule finite_induct) (auto simp add: insert_Diff_if)
   988 
   989 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)"
   990   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))"])
   991   apply (auto simp add: insert_Diff_if add_ac)
   992   done
   993 
   994 (* By Jeremy Siek: *)
   995 
   996 lemma setsum_diff_nat: 
   997   assumes finB: "finite B"
   998   shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   999 using finB
  1000 proof (induct)
  1001   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
  1002 next
  1003   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
  1004     and xFinA: "insert x F \<subseteq> A"
  1005     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
  1006   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
  1007   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
  1008     by (simp add: setsum_diff1_nat)
  1009   from xFinA have "F \<subseteq> A" by simp
  1010   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
  1011   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
  1012     by simp
  1013   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
  1014   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
  1015     by simp
  1016   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
  1017   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
  1018     by simp
  1019   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
  1020 qed
  1021 
  1022 lemma setsum_diff:
  1023   assumes le: "finite A" "B \<subseteq> A"
  1024   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
  1025 proof -
  1026   from le have finiteB: "finite B" using finite_subset by auto
  1027   show ?thesis using finiteB le
  1028     proof (induct)
  1029       case empty
  1030       thus ?case by auto
  1031     next
  1032       case (insert x F)
  1033       thus ?case using le finiteB 
  1034 	by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
  1035     qed
  1036   qed
  1037 
  1038 lemma setsum_mono:
  1039   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
  1040   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
  1041 proof (cases "finite K")
  1042   case True
  1043   thus ?thesis using le
  1044   proof (induct)
  1045     case empty
  1046     thus ?case by simp
  1047   next
  1048     case insert
  1049     thus ?case using add_mono 
  1050       by force
  1051   qed
  1052 next
  1053   case False
  1054   thus ?thesis
  1055     by (simp add: setsum_def)
  1056 qed
  1057 
  1058 lemma setsum_strict_mono:
  1059 fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
  1060 assumes fin_ne: "finite A"  "A \<noteq> {}"
  1061 shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
  1062 using fin_ne
  1063 proof (induct rule: finite_ne_induct)
  1064   case singleton thus ?case by simp
  1065 next
  1066   case insert thus ?case by (auto simp: add_strict_mono)
  1067 qed
  1068 
  1069 lemma setsum_negf:
  1070  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
  1071 proof (cases "finite A")
  1072   case True thus ?thesis by (induct set: Finites, auto)
  1073 next
  1074   case False thus ?thesis by (simp add: setsum_def)
  1075 qed
  1076 
  1077 lemma setsum_subtractf:
  1078  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
  1079   setsum f A - setsum g A"
  1080 proof (cases "finite A")
  1081   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
  1082 next
  1083   case False thus ?thesis by (simp add: setsum_def)
  1084 qed
  1085 
  1086 lemma setsum_nonneg:
  1087 assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
  1088 shows "0 \<le> setsum f A"
  1089 proof (cases "finite A")
  1090   case True thus ?thesis using nn
  1091   apply (induct set: Finites, auto)
  1092   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
  1093   apply (blast intro: add_mono)
  1094   done
  1095 next
  1096   case False thus ?thesis by (simp add: setsum_def)
  1097 qed
  1098 
  1099 lemma setsum_nonpos:
  1100 assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
  1101 shows "setsum f A \<le> 0"
  1102 proof (cases "finite A")
  1103   case True thus ?thesis using np
  1104   apply (induct set: Finites, auto)
  1105   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
  1106   apply (blast intro: add_mono)
  1107   done
  1108 next
  1109   case False thus ?thesis by (simp add: setsum_def)
  1110 qed
  1111 
  1112 lemma setsum_mono2:
  1113 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
  1114 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
  1115 shows "setsum f A \<le> setsum f B"
  1116 proof -
  1117   have "setsum f A \<le> setsum f A + setsum f (B-A)"
  1118     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
  1119   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
  1120     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
  1121   also have "A \<union> (B-A) = B" using sub by blast
  1122   finally show ?thesis .
  1123 qed
  1124 
  1125 lemma setsum_mono3: "finite B ==> A <= B ==> 
  1126     ALL x: B - A. 
  1127       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
  1128         setsum f A <= setsum f B"
  1129   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
  1130   apply (erule ssubst)
  1131   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
  1132   apply simp
  1133   apply (rule add_left_mono)
  1134   apply (erule setsum_nonneg)
  1135   apply (subst setsum_Un_disjoint [THEN sym])
  1136   apply (erule finite_subset, assumption)
  1137   apply (rule finite_subset)
  1138   prefer 2
  1139   apply assumption
  1140   apply auto
  1141   apply (rule setsum_cong)
  1142   apply auto
  1143 done
  1144 
  1145 (* FIXME: this is distributitivty, name as such! *)
  1146 (* suggested name: setsum_right_distrib (CB) *)
  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_left_distrib:
  1164   "setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)"
  1165 proof (cases "finite A")
  1166   case True
  1167   then show ?thesis
  1168   proof induct
  1169     case empty thus ?case by simp
  1170   next
  1171     case (insert x A) thus ?case by (simp add: left_distrib)
  1172   qed
  1173 next
  1174   case False thus ?thesis by (simp add: setsum_def)
  1175 qed
  1176 
  1177 lemma setsum_divide_distrib:
  1178   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
  1179 proof (cases "finite A")
  1180   case True
  1181   then show ?thesis
  1182   proof induct
  1183     case empty thus ?case by simp
  1184   next
  1185     case (insert x A) thus ?case by (simp add: add_divide_distrib)
  1186   qed
  1187 next
  1188   case False thus ?thesis by (simp add: setsum_def)
  1189 qed
  1190 
  1191 lemma setsum_abs[iff]: 
  1192   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1193   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1194 proof (cases "finite A")
  1195   case True
  1196   thus ?thesis
  1197   proof (induct)
  1198     case empty thus ?case by simp
  1199   next
  1200     case (insert x A)
  1201     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1202   qed
  1203 next
  1204   case False thus ?thesis by (simp add: setsum_def)
  1205 qed
  1206 
  1207 lemma setsum_abs_ge_zero[iff]: 
  1208   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1209   shows "0 \<le> setsum (%i. abs(f i)) A"
  1210 proof (cases "finite A")
  1211   case True
  1212   thus ?thesis
  1213   proof (induct)
  1214     case empty thus ?case by simp
  1215   next
  1216     case (insert x A) thus ?case by (auto intro: order_trans)
  1217   qed
  1218 next
  1219   case False thus ?thesis by (simp add: setsum_def)
  1220 qed
  1221 
  1222 lemma abs_setsum_abs[simp]: 
  1223   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1224   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1225 proof (cases "finite A")
  1226   case True
  1227   thus ?thesis
  1228   proof (induct)
  1229     case empty thus ?case by simp
  1230   next
  1231     case (insert a A)
  1232     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
  1233     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1234     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
  1235       by (simp del: abs_of_nonneg)
  1236     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1237     finally show ?case .
  1238   qed
  1239 next
  1240   case False thus ?thesis by (simp add: setsum_def)
  1241 qed
  1242 
  1243 
  1244 text {* Commuting outer and inner summation *}
  1245 
  1246 lemma swap_inj_on:
  1247   "inj_on (%(i, j). (j, i)) (A \<times> B)"
  1248   by (unfold inj_on_def) fast
  1249 
  1250 lemma swap_product:
  1251   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
  1252   by (simp add: split_def image_def) blast
  1253 
  1254 lemma setsum_commute:
  1255   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
  1256 proof (simp add: setsum_cartesian_product)
  1257   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
  1258     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
  1259     (is "?s = _")
  1260     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
  1261     apply (simp add: split_def)
  1262     done
  1263   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
  1264     (is "_ = ?t")
  1265     apply (simp add: swap_product)
  1266     done
  1267   finally show "?s = ?t" .
  1268 qed
  1269 
  1270 
  1271 subsection {* Generalized product over a set *}
  1272 
  1273 constdefs
  1274   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1275   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1276 
  1277 syntax
  1278   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1279 syntax (xsymbols)
  1280   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1281 syntax (HTML output)
  1282   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1283 
  1284 translations -- {* Beware of argument permutation! *}
  1285   "PROD i:A. b" == "setprod (%i. b) A" 
  1286   "\<Prod>i\<in>A. b" == "setprod (%i. b) A" 
  1287 
  1288 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1289  @{text"\<Prod>x|P. e"}. *}
  1290 
  1291 syntax
  1292   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1293 syntax (xsymbols)
  1294   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1295 syntax (HTML output)
  1296   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1297 
  1298 translations
  1299   "PROD x|P. t" => "setprod (%x. t) {x. P}"
  1300   "\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
  1301 
  1302 text{* Finally we abbreviate @{term"\<Prod>x\<in>A. x"} by @{text"\<Prod>A"}. *}
  1303 
  1304 syntax
  1305   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1306 
  1307 parse_translation {*
  1308   let
  1309     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1310   in [("_Setprod", Setprod_tr)] end;
  1311 *}
  1312 print_translation {*
  1313 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1314     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1315 in
  1316 [("setprod", setprod_tr')]
  1317 end
  1318 *}
  1319 
  1320 
  1321 lemma setprod_empty [simp]: "setprod f {} = 1"
  1322   by (auto simp add: setprod_def)
  1323 
  1324 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1325     setprod f (insert a A) = f a * setprod f A"
  1326 by (simp add: setprod_def)
  1327 
  1328 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1329   by (simp add: setprod_def)
  1330 
  1331 lemma setprod_reindex:
  1332      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1333 by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
  1334 
  1335 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1336 by (auto simp add: setprod_reindex)
  1337 
  1338 lemma setprod_cong:
  1339   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1340 by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
  1341 
  1342 lemma strong_setprod_cong:
  1343   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1344 by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
  1345 
  1346 lemma setprod_reindex_cong: "inj_on f A ==>
  1347     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1348   by (frule setprod_reindex, simp)
  1349 
  1350 
  1351 lemma setprod_1: "setprod (%i. 1) A = 1"
  1352   apply (case_tac "finite A")
  1353   apply (erule finite_induct, auto simp add: mult_ac)
  1354   done
  1355 
  1356 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1357   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1358   apply (erule ssubst, rule setprod_1)
  1359   apply (rule setprod_cong, auto)
  1360   done
  1361 
  1362 lemma setprod_Un_Int: "finite A ==> finite B
  1363     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1364 by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
  1365 
  1366 lemma setprod_Un_disjoint: "finite A ==> finite B
  1367   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1368 by (subst setprod_Un_Int [symmetric], auto)
  1369 
  1370 lemma setprod_UN_disjoint:
  1371     "finite I ==> (ALL i:I. finite (A i)) ==>
  1372         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1373       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1374 by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
  1375 
  1376 lemma setprod_Union_disjoint:
  1377   "[| (ALL A:C. finite A);
  1378       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1379    ==> setprod f (Union C) = setprod (setprod f) C"
  1380 apply (cases "finite C") 
  1381  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1382   apply (frule setprod_UN_disjoint [of C id f])
  1383  apply (unfold Union_def id_def, assumption+)
  1384 done
  1385 
  1386 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1387     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1388     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1389 by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
  1390 
  1391 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1392 lemma setprod_cartesian_product: 
  1393      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1394 apply (cases "finite A") 
  1395  apply (cases "finite B") 
  1396   apply (simp add: setprod_Sigma)
  1397  apply (cases "A={}", simp)
  1398  apply (simp add: setprod_1) 
  1399 apply (auto simp add: setprod_def
  1400             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1401 done
  1402 
  1403 lemma setprod_timesf:
  1404      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1405 by(simp add:setprod_def AC_mult.fold_distrib)
  1406 
  1407 
  1408 subsubsection {* Properties in more restricted classes of structures *}
  1409 
  1410 lemma setprod_eq_1_iff [simp]:
  1411     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1412   by (induct set: Finites) auto
  1413 
  1414 lemma setprod_zero:
  1415      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1416   apply (induct set: Finites, force, clarsimp)
  1417   apply (erule disjE, auto)
  1418   done
  1419 
  1420 lemma setprod_nonneg [rule_format]:
  1421      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1422   apply (case_tac "finite A")
  1423   apply (induct set: Finites, force, clarsimp)
  1424   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1425   apply (rule mult_mono, assumption+)
  1426   apply (auto simp add: setprod_def)
  1427   done
  1428 
  1429 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1430      --> 0 < setprod f A"
  1431   apply (case_tac "finite A")
  1432   apply (induct set: Finites, force, clarsimp)
  1433   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1434   apply (rule mult_strict_mono, assumption+)
  1435   apply (auto simp add: setprod_def)
  1436   done
  1437 
  1438 lemma setprod_nonzero [rule_format]:
  1439     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1440       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1441   apply (erule finite_induct, auto)
  1442   done
  1443 
  1444 lemma setprod_zero_eq:
  1445     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1446      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1447   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1448   done
  1449 
  1450 lemma setprod_nonzero_field:
  1451     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1452   apply (rule setprod_nonzero, auto)
  1453   done
  1454 
  1455 lemma setprod_zero_eq_field:
  1456     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1457   apply (rule setprod_zero_eq, auto)
  1458   done
  1459 
  1460 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1461     (setprod f (A Un B) :: 'a ::{field})
  1462       = setprod f A * setprod f B / setprod f (A Int B)"
  1463   apply (subst setprod_Un_Int [symmetric], auto)
  1464   apply (subgoal_tac "finite (A Int B)")
  1465   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1466   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1467   done
  1468 
  1469 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1470     (setprod f (A - {a}) :: 'a :: {field}) =
  1471       (if a:A then setprod f A / f a else setprod f A)"
  1472   apply (erule finite_induct)
  1473    apply (auto simp add: insert_Diff_if)
  1474   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1475   apply (erule ssubst)
  1476   apply (subst times_divide_eq_right [THEN sym])
  1477   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1478   done
  1479 
  1480 lemma setprod_inversef: "finite A ==>
  1481     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1482       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1483   apply (erule finite_induct)
  1484   apply (simp, simp)
  1485   done
  1486 
  1487 lemma setprod_dividef:
  1488      "[|finite A;
  1489         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1490       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1491   apply (subgoal_tac
  1492          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1493   apply (erule ssubst)
  1494   apply (subst divide_inverse)
  1495   apply (subst setprod_timesf)
  1496   apply (subst setprod_inversef, assumption+, rule refl)
  1497   apply (rule setprod_cong, rule refl)
  1498   apply (subst divide_inverse, auto)
  1499   done
  1500 
  1501 subsection {* Finite cardinality *}
  1502 
  1503 text {* This definition, although traditional, is ugly to work with:
  1504 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1505 But now that we have @{text setsum} things are easy:
  1506 *}
  1507 
  1508 constdefs
  1509   card :: "'a set => nat"
  1510   "card A == setsum (%x. 1::nat) A"
  1511 
  1512 lemma card_empty [simp]: "card {} = 0"
  1513   by (simp add: card_def)
  1514 
  1515 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1516   by (simp add: card_def)
  1517 
  1518 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1519 by (simp add: card_def)
  1520 
  1521 lemma card_insert_disjoint [simp]:
  1522   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1523 by(simp add: card_def)
  1524 
  1525 lemma card_insert_if:
  1526     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1527   by (simp add: insert_absorb)
  1528 
  1529 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1530   apply auto
  1531   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1532   done
  1533 
  1534 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1535 by auto
  1536 
  1537 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1538 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1539 apply(simp del:insert_Diff_single)
  1540 done
  1541 
  1542 lemma card_Diff_singleton:
  1543     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1544   by (simp add: card_Suc_Diff1 [symmetric])
  1545 
  1546 lemma card_Diff_singleton_if:
  1547     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1548   by (simp add: card_Diff_singleton)
  1549 
  1550 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1551   by (simp add: card_insert_if card_Suc_Diff1)
  1552 
  1553 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1554   by (simp add: card_insert_if)
  1555 
  1556 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1557 by (simp add: card_def setsum_mono2)
  1558 
  1559 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1560   apply (induct set: Finites, simp, clarify)
  1561   apply (subgoal_tac "finite A & A - {x} <= F")
  1562    prefer 2 apply (blast intro: finite_subset, atomize)
  1563   apply (drule_tac x = "A - {x}" in spec)
  1564   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1565   apply (case_tac "card A", auto)
  1566   done
  1567 
  1568 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1569   apply (simp add: psubset_def linorder_not_le [symmetric])
  1570   apply (blast dest: card_seteq)
  1571   done
  1572 
  1573 lemma card_Un_Int: "finite A ==> finite B
  1574     ==> card A + card B = card (A Un B) + card (A Int B)"
  1575 by(simp add:card_def setsum_Un_Int)
  1576 
  1577 lemma card_Un_disjoint: "finite A ==> finite B
  1578     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1579   by (simp add: card_Un_Int)
  1580 
  1581 lemma card_Diff_subset:
  1582   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1583 by(simp add:card_def setsum_diff_nat)
  1584 
  1585 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1586   apply (rule Suc_less_SucD)
  1587   apply (simp add: card_Suc_Diff1)
  1588   done
  1589 
  1590 lemma card_Diff2_less:
  1591     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1592   apply (case_tac "x = y")
  1593    apply (simp add: card_Diff1_less)
  1594   apply (rule less_trans)
  1595    prefer 2 apply (auto intro!: card_Diff1_less)
  1596   done
  1597 
  1598 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1599   apply (case_tac "x : A")
  1600    apply (simp_all add: card_Diff1_less less_imp_le)
  1601   done
  1602 
  1603 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1604 by (erule psubsetI, blast)
  1605 
  1606 lemma insert_partition:
  1607   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1608   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1609 by auto
  1610 
  1611 (* main cardinality theorem *)
  1612 lemma card_partition [rule_format]:
  1613      "finite C ==>  
  1614         finite (\<Union> C) -->  
  1615         (\<forall>c\<in>C. card c = k) -->   
  1616         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1617         k * card(C) = card (\<Union> C)"
  1618 apply (erule finite_induct, simp)
  1619 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1620        finite_subset [of _ "\<Union> (insert x F)"])
  1621 done
  1622 
  1623 
  1624 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  1625 apply (cases "finite A")
  1626 apply (erule finite_induct)
  1627 apply (auto simp add: ring_distrib add_ac)
  1628 done
  1629 
  1630 
  1631 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)"
  1632   apply (erule finite_induct)
  1633   apply (auto simp add: power_Suc)
  1634   done
  1635 
  1636 lemma setsum_bounded:
  1637   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
  1638   shows "setsum f A \<le> of_nat(card A) * K"
  1639 proof (cases "finite A")
  1640   case True
  1641   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1642 next
  1643   case False thus ?thesis by (simp add: setsum_def)
  1644 qed
  1645 
  1646 
  1647 subsubsection {* Cardinality of unions *}
  1648 
  1649 lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
  1650 by(induct n, auto)
  1651 
  1652 lemma card_UN_disjoint:
  1653     "finite I ==> (ALL i:I. finite (A i)) ==>
  1654         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1655       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1656   apply (simp add: card_def del: setsum_constant)
  1657   apply (subgoal_tac
  1658            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1659   apply (simp add: setsum_UN_disjoint del: setsum_constant)
  1660   apply (simp cong: setsum_cong)
  1661   done
  1662 
  1663 lemma card_Union_disjoint:
  1664   "finite C ==> (ALL A:C. finite A) ==>
  1665         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1666       card (Union C) = setsum card C"
  1667   apply (frule card_UN_disjoint [of C id])
  1668   apply (unfold Union_def id_def, assumption+)
  1669   done
  1670 
  1671 subsubsection {* Cardinality of image *}
  1672 
  1673 text{*The image of a finite set can be expressed using @{term fold}.*}
  1674 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1675   apply (erule finite_induct, simp)
  1676   apply (subst ACf.fold_insert) 
  1677   apply (auto simp add: ACf_def) 
  1678   done
  1679 
  1680 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1681   apply (induct set: Finites, simp)
  1682   apply (simp add: le_SucI finite_imageI card_insert_if)
  1683   done
  1684 
  1685 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1686 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  1687 
  1688 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1689   by (simp add: card_seteq card_image)
  1690 
  1691 lemma eq_card_imp_inj_on:
  1692   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1693 apply (induct rule:finite_induct, simp)
  1694 apply(frule card_image_le[where f = f])
  1695 apply(simp add:card_insert_if split:if_splits)
  1696 done
  1697 
  1698 lemma inj_on_iff_eq_card:
  1699   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1700 by(blast intro: card_image eq_card_imp_inj_on)
  1701 
  1702 
  1703 lemma card_inj_on_le:
  1704     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1705 apply (subgoal_tac "finite A") 
  1706  apply (force intro: card_mono simp add: card_image [symmetric])
  1707 apply (blast intro: finite_imageD dest: finite_subset) 
  1708 done
  1709 
  1710 lemma card_bij_eq:
  1711     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1712        finite A; finite B |] ==> card A = card B"
  1713   by (auto intro: le_anti_sym card_inj_on_le)
  1714 
  1715 
  1716 subsubsection {* Cardinality of products *}
  1717 
  1718 (*
  1719 lemma SigmaI_insert: "y \<notin> A ==>
  1720   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1721   by auto
  1722 *)
  1723 
  1724 lemma card_SigmaI [simp]:
  1725   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1726   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1727 by(simp add:card_def setsum_Sigma del:setsum_constant)
  1728 
  1729 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1730 apply (cases "finite A") 
  1731 apply (cases "finite B") 
  1732 apply (auto simp add: card_eq_0_iff
  1733             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1734 done
  1735 
  1736 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1737 by (simp add: card_cartesian_product)
  1738 
  1739 
  1740 
  1741 subsubsection {* Cardinality of the Powerset *}
  1742 
  1743 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1744   apply (induct set: Finites)
  1745    apply (simp_all add: Pow_insert)
  1746   apply (subst card_Un_disjoint, blast)
  1747     apply (blast intro: finite_imageI, blast)
  1748   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1749    apply (simp add: card_image Pow_insert)
  1750   apply (unfold inj_on_def)
  1751   apply (blast elim!: equalityE)
  1752   done
  1753 
  1754 text {* Relates to equivalence classes.  Based on a theorem of
  1755 F. Kammüller's.  *}
  1756 
  1757 lemma dvd_partition:
  1758   "finite (Union C) ==>
  1759     ALL c : C. k dvd card c ==>
  1760     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1761   k dvd card (Union C)"
  1762 apply(frule finite_UnionD)
  1763 apply(rotate_tac -1)
  1764   apply (induct set: Finites, simp_all, clarify)
  1765   apply (subst card_Un_disjoint)
  1766   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1767   done
  1768 
  1769 
  1770 subsection{* A fold functional for non-empty sets *}
  1771 
  1772 text{* Does not require start value. *}
  1773 
  1774 consts
  1775   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1776 
  1777 inductive "fold1Set f"
  1778 intros
  1779   fold1Set_insertI [intro]:
  1780    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1781 
  1782 constdefs
  1783   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1784   "fold1 f A == THE x. (A, x) : fold1Set f"
  1785 
  1786 lemma fold1Set_nonempty:
  1787  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1788 by(erule fold1Set.cases, simp_all) 
  1789 
  1790 
  1791 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1792 
  1793 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1794 
  1795 
  1796 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1797   by (blast intro: foldSet.intros elim: foldSet.cases)
  1798 
  1799 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1800   by (unfold fold1_def) blast
  1801 
  1802 lemma finite_nonempty_imp_fold1Set:
  1803   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1804 apply (induct A rule: finite_induct)
  1805 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1806 done
  1807 
  1808 text{*First, some lemmas about @{term foldSet}.*}
  1809 
  1810 lemma (in ACf) foldSet_insert_swap:
  1811 assumes fold: "(A,y) \<in> foldSet f id b"
  1812 shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1813 using fold
  1814 proof (induct rule: foldSet.induct)
  1815   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1816 next
  1817   case (insertI A x y)
  1818     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1819       using insertI by force  --{*how does @{term id} get unfolded?*}
  1820     thus ?case by (simp add: insert_commute AC)
  1821 qed
  1822 
  1823 lemma (in ACf) foldSet_permute_diff:
  1824 assumes fold: "(A,x) \<in> foldSet f id b"
  1825 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1826 using fold
  1827 proof (induct rule: foldSet.induct)
  1828   case emptyI thus ?case by simp
  1829 next
  1830   case (insertI A x y)
  1831   have "a = x \<or> a \<in> A" using insertI by simp
  1832   thus ?case
  1833   proof
  1834     assume "a = x"
  1835     with insertI show ?thesis
  1836       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
  1837   next
  1838     assume ainA: "a \<in> A"
  1839     hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1840       using insertI by (force simp: id_def)
  1841     moreover
  1842     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1843       using ainA insertI by blast
  1844     ultimately show ?thesis by (simp add: id_def)
  1845   qed
  1846 qed
  1847 
  1848 lemma (in ACf) fold1_eq_fold:
  1849      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1850 apply (simp add: fold1_def fold_def) 
  1851 apply (rule the_equality)
  1852 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1853 apply (rule sym, clarify)
  1854 apply (case_tac "Aa=A")
  1855  apply (best intro: the_equality foldSet_determ)  
  1856 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1857  apply (best intro: the_equality foldSet_determ)  
  1858 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1859  prefer 2 apply (blast elim: equalityE) 
  1860 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1861 done
  1862 
  1863 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  1864 apply safe
  1865 apply simp 
  1866 apply (drule_tac x=x in spec)
  1867 apply (drule_tac x="A-{x}" in spec, auto) 
  1868 done
  1869 
  1870 lemma (in ACf) fold1_insert:
  1871   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  1872   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1873 proof -
  1874   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
  1875     by (auto simp add: nonempty_iff)
  1876   with A show ?thesis
  1877     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
  1878 qed
  1879 
  1880 lemma (in ACIf) fold1_insert_idem [simp]:
  1881   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  1882   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1883 proof -
  1884   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
  1885     by (auto simp add: nonempty_iff)
  1886   show ?thesis
  1887   proof cases
  1888     assume "a = x"
  1889     thus ?thesis 
  1890     proof cases
  1891       assume "A' = {}"
  1892       with prems show ?thesis by (simp add: idem) 
  1893     next
  1894       assume "A' \<noteq> {}"
  1895       with prems show ?thesis
  1896 	by (simp add: fold1_insert assoc [symmetric] idem) 
  1897     qed
  1898   next
  1899     assume "a \<noteq> x"
  1900     with prems show ?thesis
  1901       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  1902   qed
  1903 qed
  1904 
  1905 
  1906 text{* Now the recursion rules for definitions: *}
  1907 
  1908 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1909 by(simp add:fold1_singleton)
  1910 
  1911 lemma (in ACf) fold1_insert_def:
  1912   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1913 by(simp add:fold1_insert)
  1914 
  1915 lemma (in ACIf) fold1_insert_idem_def:
  1916   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1917 by(simp add:fold1_insert_idem)
  1918 
  1919 subsubsection{* Determinacy for @{term fold1Set} *}
  1920 
  1921 text{*Not actually used!!*}
  1922 
  1923 lemma (in ACf) foldSet_permute:
  1924   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1925    ==> (insert b A, x) \<in> foldSet f id a"
  1926 apply (case_tac "a=b") 
  1927 apply (auto dest: foldSet_permute_diff) 
  1928 done
  1929 
  1930 lemma (in ACf) fold1Set_determ:
  1931   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1932 proof (clarify elim!: fold1Set.cases)
  1933   fix A x B y a b
  1934   assume Ax: "(A, x) \<in> foldSet f id a"
  1935   assume By: "(B, y) \<in> foldSet f id b"
  1936   assume anotA:  "a \<notin> A"
  1937   assume bnotB:  "b \<notin> B"
  1938   assume eq: "insert a A = insert b B"
  1939   show "y=x"
  1940   proof cases
  1941     assume same: "a=b"
  1942     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1943     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1944   next
  1945     assume diff: "a\<noteq>b"
  1946     let ?D = "B - {a}"
  1947     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1948      and aB: "a \<in> B" and bA: "b \<in> A"
  1949       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1950     with aB bnotB By
  1951     have "(insert b ?D, y) \<in> foldSet f id a" 
  1952       by (auto intro: foldSet_permute simp add: insert_absorb)
  1953     moreover
  1954     have "(insert b ?D, x) \<in> foldSet f id a"
  1955       by (simp add: A [symmetric] Ax) 
  1956     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1957   qed
  1958 qed
  1959 
  1960 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1961   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1962 
  1963 declare
  1964   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1965   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1966   -- {* No more proves involve these relations. *}
  1967 
  1968 subsubsection{* Semi-Lattices *}
  1969 
  1970 locale ACIfSL = ACIf +
  1971   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1972   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1973 
  1974 locale ACIfSLlin = ACIfSL +
  1975   assumes lin: "x\<cdot>y \<in> {x,y}"
  1976 
  1977 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1978 by(simp add: below_def idem)
  1979 
  1980 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1981 proof
  1982   assume "x \<sqsubseteq> y \<cdot> z"
  1983   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1984   have "x \<cdot> y = x"
  1985   proof -
  1986     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1987     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1988     also have "\<dots> = x" by(rule xyzx)
  1989     finally show ?thesis .
  1990   qed
  1991   moreover have "x \<cdot> z = x"
  1992   proof -
  1993     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  1994     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1995     also have "\<dots> = x" by(rule xyzx)
  1996     finally show ?thesis .
  1997   qed
  1998   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  1999 next
  2000   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  2001   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  2002   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  2003   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  2004   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  2005   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  2006 qed
  2007 
  2008 lemma (in ACIfSLlin) above_f_conv:
  2009  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  2010 proof
  2011   assume a: "x \<cdot> y \<sqsubseteq> z"
  2012   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  2013   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  2014   proof
  2015     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  2016   next
  2017     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  2018   qed
  2019 next
  2020   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  2021   thus "x \<cdot> y \<sqsubseteq> z"
  2022   proof
  2023     assume a: "x \<sqsubseteq> z"
  2024     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  2025     also have "x \<cdot> z = x" using a by(simp add:below_def)
  2026     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  2027   next
  2028     assume a: "y \<sqsubseteq> z"
  2029     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  2030     also have "y \<cdot> z = y" using a by(simp add:below_def)
  2031     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  2032   qed
  2033 qed
  2034 
  2035 
  2036 subsubsection{* Lemmas about @{text fold1} *}
  2037 
  2038 lemma (in ACf) fold1_Un:
  2039 assumes A: "finite A" "A \<noteq> {}"
  2040 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2041        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2042 using A
  2043 proof(induct rule:finite_ne_induct)
  2044   case singleton thus ?case by(simp add:fold1_insert)
  2045 next
  2046   case insert thus ?case by (simp add:fold1_insert assoc)
  2047 qed
  2048 
  2049 lemma (in ACIf) fold1_Un2:
  2050 assumes A: "finite A" "A \<noteq> {}"
  2051 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2052        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2053 using A
  2054 proof(induct rule:finite_ne_induct)
  2055   case singleton thus ?case by(simp add:fold1_insert_idem)
  2056 next
  2057   case insert thus ?case by (simp add:fold1_insert_idem assoc)
  2058 qed
  2059 
  2060 lemma (in ACf) fold1_in:
  2061   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  2062   shows "fold1 f A \<in> A"
  2063 using A
  2064 proof (induct rule:finite_ne_induct)
  2065   case singleton thus ?case by simp
  2066 next
  2067   case insert thus ?case using elem by (force simp add:fold1_insert)
  2068 qed
  2069 
  2070 lemma (in ACIfSL) below_fold1_iff:
  2071 assumes A: "finite A" "A \<noteq> {}"
  2072 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  2073 using A
  2074 by(induct rule:finite_ne_induct) simp_all
  2075 
  2076 lemma (in ACIfSL) fold1_belowI:
  2077 assumes A: "finite A" "A \<noteq> {}"
  2078 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  2079 using A
  2080 proof (induct rule:finite_ne_induct)
  2081   case singleton thus ?case by simp
  2082 next
  2083   case (insert x F)
  2084   from insert(5) have "a = x \<or> a \<in> F" by simp
  2085   thus ?case
  2086   proof
  2087     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  2088   next
  2089     assume "a \<in> F"
  2090     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  2091     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  2092       using insert by(simp add:below_def ACI)
  2093     also have "fold1 f F \<cdot> a = fold1 f F"
  2094       using bel  by(simp add:below_def ACI)
  2095     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  2096       using insert by(simp add:below_def ACI)
  2097     finally show ?thesis  by(simp add:below_def)
  2098   qed
  2099 qed
  2100 
  2101 lemma (in ACIfSLlin) fold1_below_iff:
  2102 assumes A: "finite A" "A \<noteq> {}"
  2103 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  2104 using A
  2105 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  2106 
  2107 
  2108 subsubsection{* Lattices *}
  2109 
  2110 locale Lattice = lattice +
  2111   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2112   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2113   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2114 
  2115 locale Distrib_Lattice = distrib_lattice + Lattice
  2116 
  2117 text{* Lattices are semilattices *}
  2118 
  2119 lemma (in Lattice) ACf_inf: "ACf inf"
  2120 by(blast intro: ACf.intro inf_commute inf_assoc)
  2121 
  2122 lemma (in Lattice) ACf_sup: "ACf sup"
  2123 by(blast intro: ACf.intro sup_commute sup_assoc)
  2124 
  2125 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2126 apply(rule ACIf.intro)
  2127 apply(rule ACf_inf)
  2128 apply(rule ACIf_axioms.intro)
  2129 apply(rule inf_idem)
  2130 done
  2131 
  2132 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2133 apply(rule ACIf.intro)
  2134 apply(rule ACf_sup)
  2135 apply(rule ACIf_axioms.intro)
  2136 apply(rule sup_idem)
  2137 done
  2138 
  2139 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2140 apply(rule ACIfSL.intro)
  2141 apply(rule ACf_inf)
  2142 apply(rule ACIf.axioms[OF ACIf_inf])
  2143 apply(rule ACIfSL_axioms.intro)
  2144 apply(rule iffI)
  2145  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2146 apply(erule subst)
  2147 apply(rule inf_le2)
  2148 done
  2149 
  2150 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2151 apply(rule ACIfSL.intro)
  2152 apply(rule ACf_sup)
  2153 apply(rule ACIf.axioms[OF ACIf_sup])
  2154 apply(rule ACIfSL_axioms.intro)
  2155 apply(rule iffI)
  2156  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2157 apply(erule subst)
  2158 apply(rule sup_ge2)
  2159 done
  2160 
  2161 
  2162 subsubsection{* Fold laws in lattices *}
  2163 
  2164 lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2165 apply(unfold Sup_def Inf_def)
  2166 apply(subgoal_tac "EX a. a:A")
  2167 prefer 2 apply blast
  2168 apply(erule exE)
  2169 apply(rule trans)
  2170 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2171 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2172 done
  2173 
  2174 lemma (in Lattice) sup_Inf_absorb[simp]:
  2175   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2176 apply(subst sup_commute)
  2177 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2178 done
  2179 
  2180 lemma (in Lattice) inf_Sup_absorb[simp]:
  2181   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2182 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2183 
  2184 
  2185 lemma (in Distrib_Lattice) sup_Inf1_distrib:
  2186 assumes A: "finite A" "A \<noteq> {}"
  2187 shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2188 using A
  2189 proof (induct rule: finite_ne_induct)
  2190   case singleton thus ?case by(simp add:Inf_def)
  2191 next
  2192   case (insert y A)
  2193   have fin: "finite {x \<squnion> a |a. a \<in> A}"
  2194     by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
  2195   have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
  2196     using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
  2197   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
  2198   also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
  2199   also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
  2200     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def fin])
  2201   also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
  2202     by blast
  2203   finally show ?case .
  2204 qed
  2205 
  2206 lemma (in Distrib_Lattice) sup_Inf2_distrib:
  2207 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2208 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2209 using A
  2210 proof (induct rule: finite_ne_induct)
  2211   case singleton thus ?case
  2212     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2213 next
  2214   case (insert x A)
  2215   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2216     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
  2217   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2218   proof -
  2219     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2220       by blast
  2221     thus ?thesis by(simp add: insert(1) B(1))
  2222   qed
  2223   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2224   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2225     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
  2226   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2227   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}"
  2228     using insert by(simp add:sup_Inf1_distrib[OF B])
  2229   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2230     (is "_ = \<Sqinter>?M")
  2231     using B insert
  2232     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2233   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2234     by blast
  2235   finally show ?case .
  2236 qed
  2237 
  2238 
  2239 subsection{*Min and Max*}
  2240 
  2241 text{* As an application of @{text fold1} we define the minimal and
  2242 maximal element of a (non-empty) set over a linear order. *}
  2243 
  2244 constdefs
  2245   Min :: "('a::linorder)set => 'a"
  2246   "Min  ==  fold1 min"
  2247 
  2248   Max :: "('a::linorder)set => 'a"
  2249   "Max  ==  fold1 max"
  2250 
  2251 
  2252 text{* Before we can do anything, we need to show that @{text min} and
  2253 @{text max} are ACI and the ordering is linear: *}
  2254 
  2255 interpretation min: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2256 apply(rule ACf.intro)
  2257 apply(auto simp:min_def)
  2258 done
  2259 
  2260 interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2261 apply(rule ACIf_axioms.intro)
  2262 apply(auto simp:min_def)
  2263 done
  2264 
  2265 interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2266 apply(rule ACf.intro)
  2267 apply(auto simp:max_def)
  2268 done
  2269 
  2270 interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2271 apply(rule ACIf_axioms.intro)
  2272 apply(auto simp:max_def)
  2273 done
  2274 
  2275 interpretation min:
  2276   ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
  2277 apply(rule ACIfSL_axioms.intro)
  2278 apply(auto simp:min_def)
  2279 done
  2280 
  2281 interpretation min:
  2282   ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
  2283 apply(rule ACIfSLlin_axioms.intro)
  2284 apply(auto simp:min_def)
  2285 done
  2286 
  2287 interpretation max:
  2288   ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
  2289 apply(rule ACIfSL_axioms.intro)
  2290 apply(auto simp:max_def)
  2291 done
  2292 
  2293 interpretation max:
  2294   ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
  2295 apply(rule ACIfSLlin_axioms.intro)
  2296 apply(auto simp:max_def)
  2297 done
  2298 
  2299 interpretation min_max:
  2300   Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2301 apply -
  2302 apply(rule Min_def)
  2303 apply(rule Max_def)
  2304 done
  2305 
  2306 
  2307 interpretation min_max:
  2308   Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2309 .
  2310 
  2311 text{* Now we instantiate the recursion equations and declare them
  2312 simplification rules: *}
  2313 
  2314 (* Making Min or Max a defined parameter of a locale, suitably
  2315   extending ACIf, could make the following interpretations more automatic. *)
  2316 
  2317 lemmas Min_singleton = fold1_singleton_def [OF Min_def]
  2318 lemmas Max_singleton = fold1_singleton_def [OF Max_def]
  2319 lemmas Min_insert = min.fold1_insert_idem_def [OF Min_def]
  2320 lemmas Max_insert = max.fold1_insert_idem_def [OF Max_def]
  2321 
  2322 declare Min_singleton [simp]  Max_singleton [simp]
  2323 declare Min_insert [simp]  Max_insert [simp]
  2324 
  2325 
  2326 text{* Now we instantiate some @{text fold1} properties: *}
  2327 
  2328 lemma Min_in [simp]:
  2329   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2330 using min.fold1_in
  2331 by(fastsimp simp: Min_def min_def)
  2332 
  2333 lemma Max_in [simp]:
  2334   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2335 using max.fold1_in
  2336 by(fastsimp simp: Max_def max_def)
  2337 
  2338 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2339 by(simp add: Min_def min.fold1_belowI)
  2340 
  2341 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2342 by(simp add: Max_def max.fold1_belowI)
  2343 
  2344 lemma Min_ge_iff[simp]:
  2345   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2346 by(simp add: Min_def min.below_fold1_iff)
  2347 
  2348 lemma Max_le_iff[simp]:
  2349   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2350 by(simp add: Max_def max.below_fold1_iff)
  2351 
  2352 lemma Min_le_iff:
  2353   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2354 by(simp add: Min_def min.fold1_below_iff)
  2355 
  2356 lemma Max_ge_iff:
  2357   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2358 by(simp add: Max_def max.fold1_below_iff)
  2359 
  2360 subsection {* Properties of axclass @{text finite} *}
  2361 
  2362 text{* Many of these are by Brian Huffman. *}
  2363 
  2364 lemma finite_set: "finite (A::'a::finite set)"
  2365 by (rule finite_subset [OF subset_UNIV finite])
  2366 
  2367 
  2368 instance unit :: finite
  2369 proof
  2370   have "finite {()}" by simp
  2371   also have "{()} = UNIV" by auto
  2372   finally show "finite (UNIV :: unit set)" .
  2373 qed
  2374 
  2375 instance bool :: finite
  2376 proof
  2377   have "finite {True, False}" by simp
  2378   also have "{True, False} = UNIV" by auto
  2379   finally show "finite (UNIV :: bool set)" .
  2380 qed
  2381 
  2382 
  2383 instance * :: (finite, finite) finite
  2384 proof
  2385   show "finite (UNIV :: ('a \<times> 'b) set)"
  2386   proof (rule finite_Prod_UNIV)
  2387     show "finite (UNIV :: 'a set)" by (rule finite)
  2388     show "finite (UNIV :: 'b set)" by (rule finite)
  2389   qed
  2390 qed
  2391 
  2392 instance "+" :: (finite, finite) finite
  2393 proof
  2394   have a: "finite (UNIV :: 'a set)" by (rule finite)
  2395   have b: "finite (UNIV :: 'b set)" by (rule finite)
  2396   from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
  2397     by (rule finite_Plus)
  2398   thus "finite (UNIV :: ('a + 'b) set)" by simp
  2399 qed
  2400 
  2401 
  2402 instance set :: (finite) finite
  2403 proof
  2404   have "finite (UNIV :: 'a set)" by (rule finite)
  2405   hence "finite (Pow (UNIV :: 'a set))"
  2406     by (rule finite_Pow_iff [THEN iffD2])
  2407   thus "finite (UNIV :: 'a set set)" by simp
  2408 qed
  2409 
  2410 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
  2411 by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
  2412 
  2413 instance fun :: (finite, finite) finite
  2414 proof
  2415   show "finite (UNIV :: ('a => 'b) set)"
  2416   proof (rule finite_imageD)
  2417     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
  2418     show "finite (range ?graph)" by (rule finite_set)
  2419     show "inj ?graph" by (rule inj_graph)
  2420   qed
  2421 qed
  2422 
  2423 end