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