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