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