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