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