src/HOL/Finite_Set.thy
author paulson
Wed Feb 09 10:17:09 2005 +0100 (2005-02-09)
changeset 15508 c09defa4c956
parent 15507 2f3186b3e455
child 15509 c54970704285
permissions -rw-r--r--
revised fold1 proofs
     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 f 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 consts
  1746   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1747 
  1748 inductive "fold1Set f"
  1749 intros
  1750   fold1Set_insertI [intro]:
  1751    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1752 
  1753 constdefs
  1754   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1755   "fold1 f A == THE x. (A, x) : fold1Set f"
  1756 
  1757 lemma fold1Set_nonempty:
  1758  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1759 by(erule fold1Set.cases, simp_all) 
  1760 
  1761 
  1762 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1763 
  1764 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1765 
  1766 
  1767 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1768   by (blast intro: foldSet.intros elim: foldSet.cases)
  1769 
  1770 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1771   by (unfold fold1_def) blast
  1772 
  1773 lemma finite_nonempty_imp_fold1Set:
  1774   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1775 apply (induct A rule: finite_induct)
  1776 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1777 done
  1778 
  1779 text{*First, some lemmas about @{term foldSet}.*}
  1780 
  1781 
  1782 lemma (in ACf) foldSet_insert_swap:
  1783 assumes fold: "(A,y) \<in> foldSet f id b"
  1784 shows "\<lbrakk> z \<notin> A; b \<notin> A; z \<noteq> b \<rbrakk> \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1785 using fold
  1786 proof (induct rule: foldSet.induct)
  1787   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1788 next
  1789   case (insertI A x y)
  1790     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1791       using insertI by force
  1792     thus ?case by (simp add: insert_commute AC)
  1793 qed
  1794 
  1795 lemma (in ACf) foldSet_permute_diff:
  1796 assumes fold: "(A,x) \<in> foldSet f id b"
  1797 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1798 using fold
  1799 proof (induct rule: foldSet.induct)
  1800   case emptyI thus ?case by simp
  1801 next
  1802   case (insertI A x y)
  1803   show ?case
  1804   proof -
  1805     have a: "a \<in> insert x A" and b: "b \<notin> insert x A" .
  1806     from a have "a = x \<or> a \<in> A" by simp
  1807     thus "(insert b (insert x A - {a}), id x \<cdot> y) \<in> foldSet f id a"
  1808     proof
  1809       assume "a = x"
  1810       with insertI b show ?thesis by simp (blast intro: foldSet_insert_swap)
  1811     next
  1812       assume ainA: "a \<in> A"
  1813       hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1814 	using insertI b by (force simp:id_def)
  1815       moreover
  1816       have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1817 	using ainA insertI by blast
  1818       ultimately show ?thesis by simp
  1819     qed
  1820   qed
  1821 qed
  1822 
  1823 lemma (in ACf) fold1_eq_fold:
  1824      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1825 apply (simp add: fold1_def fold_def) 
  1826 apply (rule the_equality)
  1827 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1828 apply (rule sym, clarify)
  1829 apply (case_tac "Aa=A")
  1830  apply (best intro: the_equality foldSet_determ)  
  1831 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1832  apply (best intro: the_equality foldSet_determ)  
  1833 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1834  prefer 2 apply (blast elim: equalityE) 
  1835 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1836 done
  1837 
  1838 lemma (in ACf) fold1_insert:
  1839   "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  1840 apply (induct A rule: finite_induct, force)
  1841 apply (simp only: insert_commute, simp) 
  1842 apply (erule conjE) 
  1843 apply (simp add: fold1_eq_fold) 
  1844 apply (subst fold1_eq_fold, auto) 
  1845 done
  1846 
  1847 lemma (in ACIf) fold1_insert2 [simp]:
  1848   "finite A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
  1849 apply (induct A rule: finite_induct, force)
  1850 apply (case_tac "xa=x") 
  1851  prefer 2 apply (simp add: insert_commute fold1_eq_fold fold_insert2) 
  1852 apply (case_tac "F={}") 
  1853 apply (simp add: idem) 
  1854 apply (simp add: fold1_insert assoc [symmetric] idem) 
  1855 done
  1856 
  1857 
  1858 text{* Now the recursion rules for definitions: *}
  1859 
  1860 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1861 by(simp add:fold1_singleton)
  1862 
  1863 lemma (in ACf) fold1_insert_def:
  1864   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1865 by(simp add:fold1_insert)
  1866 
  1867 lemma (in ACIf) fold1_insert2_def:
  1868   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1869 by(simp add:fold1_insert2)
  1870 
  1871 subsubsection{* Determinacy for @{term fold1Set} *}
  1872 
  1873 text{*Not actually used!!*}
  1874 
  1875 lemma (in ACf) foldSet_permute:
  1876   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1877    ==> (insert b A, x) \<in> foldSet f id a"
  1878 apply (case_tac "a=b") 
  1879 apply (auto dest: foldSet_permute_diff) 
  1880 done
  1881 
  1882 lemma (in ACf) fold1Set_determ:
  1883   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1884 proof (clarify elim!: fold1Set.cases)
  1885   fix A x B y a b
  1886   assume Ax: "(A, x) \<in> foldSet f id a"
  1887   assume By: "(B, y) \<in> foldSet f id b"
  1888   assume anotA:  "a \<notin> A"
  1889   assume bnotB:  "b \<notin> B"
  1890   assume eq: "insert a A = insert b B"
  1891   show "y=x"
  1892   proof cases
  1893     assume same: "a=b"
  1894     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1895     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1896   next
  1897     assume diff: "a\<noteq>b"
  1898     let ?D = "B - {a}"
  1899     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1900      and aB: "a \<in> B" and bA: "b \<in> A"
  1901       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1902     with aB bnotB By
  1903     have "(insert b ?D, y) \<in> foldSet f id a" 
  1904       by (auto intro: foldSet_permute simp add: insert_absorb)
  1905     moreover
  1906     have "(insert b ?D, x) \<in> foldSet f id a"
  1907       by (simp add: A [symmetric] Ax) 
  1908     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1909   qed
  1910 qed
  1911 
  1912 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1913   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1914 
  1915 declare
  1916   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1917   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1918   -- {* No more proves involve these relations. *}
  1919 
  1920 subsubsection{* Semi-Lattices *}
  1921 
  1922 locale ACIfSL = ACIf +
  1923   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1924   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1925 
  1926 locale ACIfSLlin = ACIfSL +
  1927   assumes lin: "x\<cdot>y \<in> {x,y}"
  1928 
  1929 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1930 by(simp add: below_def idem)
  1931 
  1932 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1933 proof
  1934   assume "x \<sqsubseteq> y \<cdot> z"
  1935   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1936   have "x \<cdot> y = x"
  1937   proof -
  1938     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1939     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1940     also have "\<dots> = x" by(rule xyzx)
  1941     finally show ?thesis .
  1942   qed
  1943   moreover have "x \<cdot> z = x"
  1944   proof -
  1945     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  1946     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1947     also have "\<dots> = x" by(rule xyzx)
  1948     finally show ?thesis .
  1949   qed
  1950   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  1951 next
  1952   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  1953   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  1954   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  1955   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  1956   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  1957   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  1958 qed
  1959 
  1960 lemma (in ACIfSLlin) above_f_conv:
  1961  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  1962 proof
  1963   assume a: "x \<cdot> y \<sqsubseteq> z"
  1964   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  1965   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1966   proof
  1967     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1968   next
  1969     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  1970   qed
  1971 next
  1972   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  1973   thus "x \<cdot> y \<sqsubseteq> z"
  1974   proof
  1975     assume a: "x \<sqsubseteq> z"
  1976     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  1977     also have "x \<cdot> z = x" using a by(simp add:below_def)
  1978     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1979   next
  1980     assume a: "y \<sqsubseteq> z"
  1981     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1982     also have "y \<cdot> z = y" using a by(simp add:below_def)
  1983     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  1984   qed
  1985 qed
  1986 
  1987 
  1988 subsubsection{* Lemmas about @{text fold1} *}
  1989 
  1990 lemma (in ACf) fold1_Un:
  1991 assumes A: "finite A" "A \<noteq> {}"
  1992 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  1993        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  1994 using A
  1995 proof(induct rule:finite_ne_induct)
  1996   case singleton thus ?case by(simp add:fold1_insert)
  1997 next
  1998   case insert thus ?case by (simp add:fold1_insert assoc)
  1999 qed
  2000 
  2001 lemma (in ACIf) fold1_Un2:
  2002 assumes A: "finite A" "A \<noteq> {}"
  2003 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2004        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2005 using A
  2006 proof(induct rule:finite_ne_induct)
  2007   case singleton thus ?case by(simp add:fold1_insert2)
  2008 next
  2009   case insert thus ?case by (simp add:fold1_insert2 assoc)
  2010 qed
  2011 
  2012 lemma (in ACf) fold1_in:
  2013   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  2014   shows "fold1 f A \<in> A"
  2015 using A
  2016 proof (induct rule:finite_ne_induct)
  2017   case singleton thus ?case by simp
  2018 next
  2019   case insert thus ?case using elem by (force simp add:fold1_insert)
  2020 qed
  2021 
  2022 lemma (in ACIfSL) below_fold1_iff:
  2023 assumes A: "finite A" "A \<noteq> {}"
  2024 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  2025 using A
  2026 by(induct rule:finite_ne_induct) simp_all
  2027 
  2028 lemma (in ACIfSL) fold1_belowI:
  2029 assumes A: "finite A" "A \<noteq> {}"
  2030 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  2031 using A
  2032 proof (induct rule:finite_ne_induct)
  2033   case singleton thus ?case by simp
  2034 next
  2035   case (insert x F)
  2036   from insert(4) have "a = x \<or> a \<in> F" by simp
  2037   thus ?case
  2038   proof
  2039     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  2040   next
  2041     assume "a \<in> F"
  2042     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  2043     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  2044       using insert by(simp add:below_def ACI)
  2045     also have "fold1 f F \<cdot> a = fold1 f F"
  2046       using bel  by(simp add:below_def ACI)
  2047     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  2048       using insert by(simp add:below_def ACI)
  2049     finally show ?thesis  by(simp add:below_def)
  2050   qed
  2051 qed
  2052 
  2053 lemma (in ACIfSLlin) fold1_below_iff:
  2054 assumes A: "finite A" "A \<noteq> {}"
  2055 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  2056 using A
  2057 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  2058 
  2059 subsubsection{* Lattices *}
  2060 
  2061 locale Lattice =
  2062   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  2063   and inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
  2064   and sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
  2065   and Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2066   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2067   assumes refl: "x \<sqsubseteq> x"
  2068   and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
  2069   and antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
  2070   and inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
  2071   and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
  2072   and sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
  2073   and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
  2074   and inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
  2075   and sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
  2076   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2077 
  2078 
  2079 lemma (in Lattice) inf_comm: "(x \<sqinter> y) = (y \<sqinter> x)"
  2080 by(blast intro: antisym inf_le1 inf_le2 inf_least)
  2081 
  2082 lemma (in Lattice) sup_comm: "(x \<squnion> y) = (y \<squnion> x)"
  2083 by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest)
  2084 
  2085 lemma (in Lattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
  2086 by(blast intro: antisym inf_le1 inf_le2 inf_least trans)
  2087 
  2088 lemma (in Lattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
  2089 by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans)
  2090 
  2091 lemma (in Lattice) inf_idem[simp]: "x \<sqinter> x = x"
  2092 by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2093 
  2094 lemma (in Lattice) sup_idem[simp]: "x \<squnion> x = x"
  2095 by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2096 
  2097 lemma (in Lattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
  2098 by(blast intro: antisym sup_ge2 sup_greatest refl)
  2099 
  2100 lemma (in Lattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
  2101 by(blast intro: antisym inf_le1 inf_least refl)
  2102 
  2103 text{* Towards distributivity: if you have one of them, you have them all. *}
  2104 
  2105 lemma (in Lattice) distrib_imp1:
  2106 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
  2107 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
  2108 proof-
  2109   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
  2110   also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_comm sup_assoc)
  2111   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
  2112     by(simp add:inf_sup_absorb inf_comm)
  2113   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
  2114   finally show ?thesis .
  2115 qed
  2116 
  2117 lemma (in Lattice) distrib_imp2:
  2118 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
  2119 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
  2120 proof-
  2121   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
  2122   also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_comm inf_assoc)
  2123   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
  2124     by(simp add:sup_inf_absorb sup_comm)
  2125   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
  2126   finally show ?thesis .
  2127 qed
  2128 
  2129 text{* Lattices are semilattices *}
  2130 
  2131 lemma (in Lattice) ACf_inf: "ACf inf"
  2132 by(blast intro: ACf.intro inf_comm inf_assoc)
  2133 
  2134 lemma (in Lattice) ACf_sup: "ACf sup"
  2135 by(blast intro: ACf.intro sup_comm sup_assoc)
  2136 
  2137 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2138 apply(rule ACIf.intro)
  2139 apply(rule ACf_inf)
  2140 apply(rule ACIf_axioms.intro)
  2141 apply(rule inf_idem)
  2142 done
  2143 
  2144 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2145 apply(rule ACIf.intro)
  2146 apply(rule ACf_sup)
  2147 apply(rule ACIf_axioms.intro)
  2148 apply(rule sup_idem)
  2149 done
  2150 
  2151 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2152 apply(rule ACIfSL.intro)
  2153 apply(rule ACf_inf)
  2154 apply(rule ACIf.axioms[OF ACIf_inf])
  2155 apply(rule ACIfSL_axioms.intro)
  2156 apply(rule iffI)
  2157  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2158 apply(erule subst)
  2159 apply(rule inf_le2)
  2160 done
  2161 
  2162 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2163 apply(rule ACIfSL.intro)
  2164 apply(rule ACf_sup)
  2165 apply(rule ACIf.axioms[OF ACIf_sup])
  2166 apply(rule ACIfSL_axioms.intro)
  2167 apply(rule iffI)
  2168  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2169 apply(erule subst)
  2170 apply(rule sup_ge2)
  2171 done
  2172 
  2173 text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
  2174 
  2175 lemmas (in Lattice) ACI = ACIf.ACI[OF ACIf_inf] ACIf.ACI[OF ACIf_sup]
  2176 
  2177 subsubsection{* Distributive lattices *}
  2178 
  2179 locale DistribLattice = Lattice +
  2180   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
  2181 
  2182 lemma (in DistribLattice) sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
  2183 by(simp add:ACI sup_inf_distrib1)
  2184 
  2185 lemma (in DistribLattice) inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
  2186 by(rule distrib_imp2[OF sup_inf_distrib1])
  2187 
  2188 lemma (in DistribLattice) inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
  2189 by(simp add:ACI inf_sup_distrib1)
  2190 
  2191 lemmas (in DistribLattice) distrib =
  2192   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
  2193 
  2194 
  2195 subsubsection{* Fold laws in lattices *}
  2196 
  2197 lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2198 apply(unfold Sup_def Inf_def)
  2199 apply(subgoal_tac "EX a. a:A")
  2200 prefer 2 apply blast
  2201 apply(erule exE)
  2202 apply(rule trans)
  2203 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2204 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2205 done
  2206 
  2207 lemma (in Lattice) sup_Inf_absorb:
  2208   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2209 apply(subst sup_comm)
  2210 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2211 done
  2212 
  2213 lemma (in Lattice) inf_Sup_absorb:
  2214   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2215 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2216 
  2217 
  2218 lemma (in DistribLattice) sup_Inf1_distrib:
  2219 assumes A: "finite A" "A \<noteq> {}"
  2220 shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2221 using A
  2222 proof (induct rule: finite_ne_induct)
  2223   case singleton thus ?case by(simp add:Inf_def)
  2224 next
  2225   case (insert y A)
  2226   have fin: "finite {x \<squnion> a |a. a \<in> A}"
  2227     by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(0)])
  2228   have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
  2229     using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
  2230   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
  2231   also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
  2232   also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
  2233     using insert by(simp add:ACIf.fold1_insert2_def[OF ACIf_inf Inf_def fin])
  2234   also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
  2235     by blast
  2236   finally show ?case .
  2237 qed
  2238 
  2239 lemma (in DistribLattice) sup_Inf2_distrib:
  2240 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2241 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2242 using A
  2243 proof (induct rule: finite_ne_induct)
  2244   case singleton thus ?case
  2245     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2246 next
  2247   case (insert x A)
  2248   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2249     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(0)])
  2250   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2251   proof -
  2252     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2253       by blast
  2254     thus ?thesis by(simp add: insert(0) B(0))
  2255   qed
  2256   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2257   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2258     using insert by(simp add:ACIf.fold1_insert2_def[OF ACIf_inf Inf_def])
  2259   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2260   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}"
  2261     using insert by(simp add:sup_Inf1_distrib[OF B])
  2262   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2263     (is "_ = \<Sqinter>?M")
  2264     using B insert
  2265     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2266   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2267     by blast
  2268   finally show ?case .
  2269 qed
  2270 
  2271 
  2272 subsection{*Min and Max*}
  2273 
  2274 text{* As an application of @{text fold1} we define the minimal and
  2275 maximal element of a (non-empty) set over a linear order. *}
  2276 
  2277 constdefs
  2278   Min :: "('a::linorder)set => 'a"
  2279   "Min  ==  fold1 min"
  2280 
  2281   Max :: "('a::linorder)set => 'a"
  2282   "Max  ==  fold1 max"
  2283 
  2284 
  2285 text{* Before we can do anything, we need to show that @{text min} and
  2286 @{text max} are ACI and the ordering is linear: *}
  2287 
  2288 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2289 apply(rule ACf.intro)
  2290 apply(auto simp:min_def)
  2291 done
  2292 
  2293 lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2294 apply(rule ACIf.intro[OF ACf_min])
  2295 apply(rule ACIf_axioms.intro)
  2296 apply(auto simp:min_def)
  2297 done
  2298 
  2299 lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2300 apply(rule ACf.intro)
  2301 apply(auto simp:max_def)
  2302 done
  2303 
  2304 lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
  2305 apply(rule ACIf.intro[OF ACf_max])
  2306 apply(rule ACIf_axioms.intro)
  2307 apply(auto simp:max_def)
  2308 done
  2309 
  2310 lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
  2311 apply(rule ACIfSL.intro)
  2312 apply(rule ACf_min)
  2313 apply(rule ACIf.axioms[OF ACIf_min])
  2314 apply(rule ACIfSL_axioms.intro)
  2315 apply(auto simp:min_def)
  2316 done
  2317 
  2318 lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
  2319 apply(rule ACIfSLlin.intro)
  2320 apply(rule ACf_min)
  2321 apply(rule ACIf.axioms[OF ACIf_min])
  2322 apply(rule ACIfSL.axioms[OF ACIfSL_min])
  2323 apply(rule ACIfSLlin_axioms.intro)
  2324 apply(auto simp:min_def)
  2325 done
  2326 
  2327 lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
  2328 apply(rule ACIfSL.intro)
  2329 apply(rule ACf_max)
  2330 apply(rule ACIf.axioms[OF ACIf_max])
  2331 apply(rule ACIfSL_axioms.intro)
  2332 apply(auto simp:max_def)
  2333 done
  2334 
  2335 lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
  2336 apply(rule ACIfSLlin.intro)
  2337 apply(rule ACf_max)
  2338 apply(rule ACIf.axioms[OF ACIf_max])
  2339 apply(rule ACIfSL.axioms[OF ACIfSL_max])
  2340 apply(rule ACIfSLlin_axioms.intro)
  2341 apply(auto simp:max_def)
  2342 done
  2343 
  2344 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
  2345 apply(rule Lattice.intro)
  2346 apply simp
  2347 apply(erule (1) order_trans)
  2348 apply(erule (1) order_antisym)
  2349 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
  2350 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
  2351 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
  2352 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
  2353 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
  2354 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
  2355 apply(rule_tac x=x and y=y in linorder_le_cases)
  2356 apply(simp add:min_def max_def)
  2357 apply(simp add:min_def max_def)
  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 done
  2362 
  2363 lemma DistribLattice_min_max: "DistribLattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
  2364 apply(rule DistribLattice.intro)
  2365 apply(rule Lattice_min_max)
  2366 apply(rule DistribLattice_axioms.intro)
  2367 apply(rule_tac x=x and y=y in linorder_le_cases)
  2368 apply(rule_tac x=x and y=z in linorder_le_cases)
  2369 apply(rule_tac x=y and y=z in linorder_le_cases)
  2370 apply(simp add:min_def max_def)
  2371 apply(simp add:min_def max_def)
  2372 apply(rule_tac x=y and y=z in linorder_le_cases)
  2373 apply(simp add:min_def max_def)
  2374 apply(simp add:min_def max_def)
  2375 apply(rule_tac x=x and y=z in linorder_le_cases)
  2376 apply(rule_tac x=y and y=z in linorder_le_cases)
  2377 apply(simp add:min_def max_def)
  2378 apply(simp add:min_def max_def)
  2379 apply(rule_tac x=y and y=z in linorder_le_cases)
  2380 apply(simp add:min_def max_def)
  2381 apply(simp add:min_def max_def)
  2382 done
  2383 
  2384 text{* Now we instantiate the recursion equations and declare them
  2385 simplification rules: *}
  2386 
  2387 declare
  2388   fold1_singleton_def[OF Min_def, simp]
  2389   ACIf.fold1_insert2_def[OF ACIf_min Min_def, simp]
  2390   fold1_singleton_def[OF Max_def, simp]
  2391   ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
  2392 
  2393 text{* Now we instantiate some @{text fold1} properties: *}
  2394 
  2395 lemma Min_in [simp]:
  2396   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2397 using ACf.fold1_in[OF ACf_min]
  2398 by(fastsimp simp: Min_def min_def)
  2399 
  2400 lemma Max_in [simp]:
  2401   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2402 using ACf.fold1_in[OF ACf_max]
  2403 by(fastsimp simp: Max_def max_def)
  2404 
  2405 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2406 by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
  2407 
  2408 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2409 by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
  2410 
  2411 lemma Min_ge_iff[simp]:
  2412   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2413 by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min])
  2414 
  2415 lemma Max_le_iff[simp]:
  2416   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2417 by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max])
  2418 
  2419 lemma Min_le_iff:
  2420   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2421 by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
  2422 
  2423 lemma Max_ge_iff:
  2424   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2425 by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
  2426 
  2427 lemma Min_le_Max:
  2428   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
  2429 by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
  2430 
  2431 lemma max_Min2_distrib:
  2432   "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
  2433   max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
  2434 by(simp add: Min_def DistribLattice.sup_Inf2_distrib[OF DistribLattice_min_max])
  2435 
  2436 end