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