src/HOL/Finite_Set.thy
author ballarin
Fri Mar 17 10:04:27 2006 +0100 (2006-03-17)
changeset 19279 48b527d0331b
parent 18493 343da052b961
child 19313 45c9fc22904b
permissions -rw-r--r--
Renamed setsum_mult to setsum_right_distrib.
     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 lemma setsum_right_distrib: 
  1149   fixes f :: "'a => ('b::semiring_0_cancel)"
  1150   shows "r * setsum f A = setsum (%n. r * f n) A"
  1151 proof (cases "finite A")
  1152   case True
  1153   thus ?thesis
  1154   proof (induct)
  1155     case empty thus ?case by simp
  1156   next
  1157     case (insert x A) thus ?case by (simp add: right_distrib)
  1158   qed
  1159 next
  1160   case False thus ?thesis by (simp add: setsum_def)
  1161 qed
  1162 
  1163 lemma setsum_left_distrib:
  1164   "setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)"
  1165 proof (cases "finite A")
  1166   case True
  1167   then show ?thesis
  1168   proof induct
  1169     case empty thus ?case by simp
  1170   next
  1171     case (insert x A) thus ?case by (simp add: left_distrib)
  1172   qed
  1173 next
  1174   case False thus ?thesis by (simp add: setsum_def)
  1175 qed
  1176 
  1177 lemma setsum_divide_distrib:
  1178   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
  1179 proof (cases "finite A")
  1180   case True
  1181   then show ?thesis
  1182   proof induct
  1183     case empty thus ?case by simp
  1184   next
  1185     case (insert x A) thus ?case by (simp add: add_divide_distrib)
  1186   qed
  1187 next
  1188   case False thus ?thesis by (simp add: setsum_def)
  1189 qed
  1190 
  1191 lemma setsum_abs[iff]: 
  1192   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1193   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
  1194 proof (cases "finite A")
  1195   case True
  1196   thus ?thesis
  1197   proof (induct)
  1198     case empty thus ?case by simp
  1199   next
  1200     case (insert x A)
  1201     thus ?case by (auto intro: abs_triangle_ineq order_trans)
  1202   qed
  1203 next
  1204   case False thus ?thesis by (simp add: setsum_def)
  1205 qed
  1206 
  1207 lemma setsum_abs_ge_zero[iff]: 
  1208   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1209   shows "0 \<le> setsum (%i. abs(f i)) A"
  1210 proof (cases "finite A")
  1211   case True
  1212   thus ?thesis
  1213   proof (induct)
  1214     case empty thus ?case by simp
  1215   next
  1216     case (insert x A) thus ?case by (auto intro: order_trans)
  1217   qed
  1218 next
  1219   case False thus ?thesis by (simp add: setsum_def)
  1220 qed
  1221 
  1222 lemma abs_setsum_abs[simp]: 
  1223   fixes f :: "'a => ('b::lordered_ab_group_abs)"
  1224   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
  1225 proof (cases "finite A")
  1226   case True
  1227   thus ?thesis
  1228   proof (induct)
  1229     case empty thus ?case by simp
  1230   next
  1231     case (insert a A)
  1232     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
  1233     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
  1234     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
  1235       by (simp del: abs_of_nonneg)
  1236     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
  1237     finally show ?case .
  1238   qed
  1239 next
  1240   case False thus ?thesis by (simp add: setsum_def)
  1241 qed
  1242 
  1243 
  1244 text {* Commuting outer and inner summation *}
  1245 
  1246 lemma swap_inj_on:
  1247   "inj_on (%(i, j). (j, i)) (A \<times> B)"
  1248   by (unfold inj_on_def) fast
  1249 
  1250 lemma swap_product:
  1251   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
  1252   by (simp add: split_def image_def) blast
  1253 
  1254 lemma setsum_commute:
  1255   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
  1256 proof (simp add: setsum_cartesian_product)
  1257   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
  1258     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
  1259     (is "?s = _")
  1260     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
  1261     apply (simp add: split_def)
  1262     done
  1263   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
  1264     (is "_ = ?t")
  1265     apply (simp add: swap_product)
  1266     done
  1267   finally show "?s = ?t" .
  1268 qed
  1269 
  1270 lemma setsum_product:
  1271   fixes f :: "nat => ('a::semiring_0_cancel)"
  1272   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
  1273   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
  1274 
  1275 
  1276 subsection {* Generalized product over a set *}
  1277 
  1278 constdefs
  1279   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
  1280   "setprod f A == if finite A then fold (op *) f 1 A else 1"
  1281 
  1282 syntax
  1283   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1284 syntax (xsymbols)
  1285   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1286 syntax (HTML output)
  1287   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1288 
  1289 translations -- {* Beware of argument permutation! *}
  1290   "PROD i:A. b" == "setprod (%i. b) A" 
  1291   "\<Prod>i\<in>A. b" == "setprod (%i. b) A" 
  1292 
  1293 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1294  @{text"\<Prod>x|P. e"}. *}
  1295 
  1296 syntax
  1297   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1298 syntax (xsymbols)
  1299   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1300 syntax (HTML output)
  1301   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1302 
  1303 translations
  1304   "PROD x|P. t" => "setprod (%x. t) {x. P}"
  1305   "\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
  1306 
  1307 text{* Finally we abbreviate @{term"\<Prod>x\<in>A. x"} by @{text"\<Prod>A"}. *}
  1308 
  1309 syntax
  1310   "_Setprod" :: "'a set => 'a::comm_monoid_mult"  ("\<Prod>_" [1000] 999)
  1311 
  1312 parse_translation {*
  1313   let
  1314     fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A
  1315   in [("_Setprod", Setprod_tr)] end;
  1316 *}
  1317 print_translation {*
  1318 let fun setprod_tr' [Abs(x,Tx,t), A] =
  1319     if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match
  1320 in
  1321 [("setprod", setprod_tr')]
  1322 end
  1323 *}
  1324 
  1325 
  1326 lemma setprod_empty [simp]: "setprod f {} = 1"
  1327   by (auto simp add: setprod_def)
  1328 
  1329 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
  1330     setprod f (insert a A) = f a * setprod f A"
  1331 by (simp add: setprod_def)
  1332 
  1333 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
  1334   by (simp add: setprod_def)
  1335 
  1336 lemma setprod_reindex:
  1337      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1338 by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
  1339 
  1340 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1341 by (auto simp add: setprod_reindex)
  1342 
  1343 lemma setprod_cong:
  1344   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1345 by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
  1346 
  1347 lemma strong_setprod_cong:
  1348   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1349 by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
  1350 
  1351 lemma setprod_reindex_cong: "inj_on f A ==>
  1352     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1353   by (frule setprod_reindex, simp)
  1354 
  1355 
  1356 lemma setprod_1: "setprod (%i. 1) A = 1"
  1357   apply (case_tac "finite A")
  1358   apply (erule finite_induct, auto simp add: mult_ac)
  1359   done
  1360 
  1361 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
  1362   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
  1363   apply (erule ssubst, rule setprod_1)
  1364   apply (rule setprod_cong, auto)
  1365   done
  1366 
  1367 lemma setprod_Un_Int: "finite A ==> finite B
  1368     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1369 by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
  1370 
  1371 lemma setprod_Un_disjoint: "finite A ==> finite B
  1372   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1373 by (subst setprod_Un_Int [symmetric], auto)
  1374 
  1375 lemma setprod_UN_disjoint:
  1376     "finite I ==> (ALL i:I. finite (A i)) ==>
  1377         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1378       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1379 by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
  1380 
  1381 lemma setprod_Union_disjoint:
  1382   "[| (ALL A:C. finite A);
  1383       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
  1384    ==> setprod f (Union C) = setprod (setprod f) C"
  1385 apply (cases "finite C") 
  1386  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
  1387   apply (frule setprod_UN_disjoint [of C id f])
  1388  apply (unfold Union_def id_def, assumption+)
  1389 done
  1390 
  1391 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1392     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1393     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1394 by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
  1395 
  1396 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1397 lemma setprod_cartesian_product: 
  1398      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1399 apply (cases "finite A") 
  1400  apply (cases "finite B") 
  1401   apply (simp add: setprod_Sigma)
  1402  apply (cases "A={}", simp)
  1403  apply (simp add: setprod_1) 
  1404 apply (auto simp add: setprod_def
  1405             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1406 done
  1407 
  1408 lemma setprod_timesf:
  1409      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1410 by(simp add:setprod_def AC_mult.fold_distrib)
  1411 
  1412 
  1413 subsubsection {* Properties in more restricted classes of structures *}
  1414 
  1415 lemma setprod_eq_1_iff [simp]:
  1416     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1417   by (induct set: Finites) auto
  1418 
  1419 lemma setprod_zero:
  1420      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
  1421   apply (induct set: Finites, force, clarsimp)
  1422   apply (erule disjE, auto)
  1423   done
  1424 
  1425 lemma setprod_nonneg [rule_format]:
  1426      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
  1427   apply (case_tac "finite A")
  1428   apply (induct set: Finites, force, clarsimp)
  1429   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
  1430   apply (rule mult_mono, assumption+)
  1431   apply (auto simp add: setprod_def)
  1432   done
  1433 
  1434 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
  1435      --> 0 < setprod f A"
  1436   apply (case_tac "finite A")
  1437   apply (induct set: Finites, force, clarsimp)
  1438   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
  1439   apply (rule mult_strict_mono, assumption+)
  1440   apply (auto simp add: setprod_def)
  1441   done
  1442 
  1443 lemma setprod_nonzero [rule_format]:
  1444     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1445       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
  1446   apply (erule finite_induct, auto)
  1447   done
  1448 
  1449 lemma setprod_zero_eq:
  1450     "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
  1451      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
  1452   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
  1453   done
  1454 
  1455 lemma setprod_nonzero_field:
  1456     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
  1457   apply (rule setprod_nonzero, auto)
  1458   done
  1459 
  1460 lemma setprod_zero_eq_field:
  1461     "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
  1462   apply (rule setprod_zero_eq, auto)
  1463   done
  1464 
  1465 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1466     (setprod f (A Un B) :: 'a ::{field})
  1467       = setprod f A * setprod f B / setprod f (A Int B)"
  1468   apply (subst setprod_Un_Int [symmetric], auto)
  1469   apply (subgoal_tac "finite (A Int B)")
  1470   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
  1471   apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
  1472   done
  1473 
  1474 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1475     (setprod f (A - {a}) :: 'a :: {field}) =
  1476       (if a:A then setprod f A / f a else setprod f A)"
  1477   apply (erule finite_induct)
  1478    apply (auto simp add: insert_Diff_if)
  1479   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
  1480   apply (erule ssubst)
  1481   apply (subst times_divide_eq_right [THEN sym])
  1482   apply (auto simp add: mult_ac times_divide_eq_right divide_self)
  1483   done
  1484 
  1485 lemma setprod_inversef: "finite A ==>
  1486     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
  1487       setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1488   apply (erule finite_induct)
  1489   apply (simp, simp)
  1490   done
  1491 
  1492 lemma setprod_dividef:
  1493      "[|finite A;
  1494         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
  1495       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1496   apply (subgoal_tac
  1497          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1498   apply (erule ssubst)
  1499   apply (subst divide_inverse)
  1500   apply (subst setprod_timesf)
  1501   apply (subst setprod_inversef, assumption+, rule refl)
  1502   apply (rule setprod_cong, rule refl)
  1503   apply (subst divide_inverse, auto)
  1504   done
  1505 
  1506 subsection {* Finite cardinality *}
  1507 
  1508 text {* This definition, although traditional, is ugly to work with:
  1509 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1510 But now that we have @{text setsum} things are easy:
  1511 *}
  1512 
  1513 constdefs
  1514   card :: "'a set => nat"
  1515   "card A == setsum (%x. 1::nat) A"
  1516 
  1517 lemma card_empty [simp]: "card {} = 0"
  1518   by (simp add: card_def)
  1519 
  1520 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1521   by (simp add: card_def)
  1522 
  1523 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
  1524 by (simp add: card_def)
  1525 
  1526 lemma card_insert_disjoint [simp]:
  1527   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1528 by(simp add: card_def)
  1529 
  1530 lemma card_insert_if:
  1531     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1532   by (simp add: insert_absorb)
  1533 
  1534 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
  1535   apply auto
  1536   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1537   done
  1538 
  1539 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1540 by auto
  1541 
  1542 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1543 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1544 apply(simp del:insert_Diff_single)
  1545 done
  1546 
  1547 lemma card_Diff_singleton:
  1548     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1549   by (simp add: card_Suc_Diff1 [symmetric])
  1550 
  1551 lemma card_Diff_singleton_if:
  1552     "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1553   by (simp add: card_Diff_singleton)
  1554 
  1555 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1556   by (simp add: card_insert_if card_Suc_Diff1)
  1557 
  1558 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1559   by (simp add: card_insert_if)
  1560 
  1561 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1562 by (simp add: card_def setsum_mono2)
  1563 
  1564 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1565   apply (induct set: Finites, simp, clarify)
  1566   apply (subgoal_tac "finite A & A - {x} <= F")
  1567    prefer 2 apply (blast intro: finite_subset, atomize)
  1568   apply (drule_tac x = "A - {x}" in spec)
  1569   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1570   apply (case_tac "card A", auto)
  1571   done
  1572 
  1573 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1574   apply (simp add: psubset_def linorder_not_le [symmetric])
  1575   apply (blast dest: card_seteq)
  1576   done
  1577 
  1578 lemma card_Un_Int: "finite A ==> finite B
  1579     ==> card A + card B = card (A Un B) + card (A Int B)"
  1580 by(simp add:card_def setsum_Un_Int)
  1581 
  1582 lemma card_Un_disjoint: "finite A ==> finite B
  1583     ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1584   by (simp add: card_Un_Int)
  1585 
  1586 lemma card_Diff_subset:
  1587   "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1588 by(simp add:card_def setsum_diff_nat)
  1589 
  1590 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1591   apply (rule Suc_less_SucD)
  1592   apply (simp add: card_Suc_Diff1)
  1593   done
  1594 
  1595 lemma card_Diff2_less:
  1596     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1597   apply (case_tac "x = y")
  1598    apply (simp add: card_Diff1_less)
  1599   apply (rule less_trans)
  1600    prefer 2 apply (auto intro!: card_Diff1_less)
  1601   done
  1602 
  1603 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1604   apply (case_tac "x : A")
  1605    apply (simp_all add: card_Diff1_less less_imp_le)
  1606   done
  1607 
  1608 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1609 by (erule psubsetI, blast)
  1610 
  1611 lemma insert_partition:
  1612   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
  1613   \<Longrightarrow> x \<inter> \<Union> F = {}"
  1614 by auto
  1615 
  1616 (* main cardinality theorem *)
  1617 lemma card_partition [rule_format]:
  1618      "finite C ==>  
  1619         finite (\<Union> C) -->  
  1620         (\<forall>c\<in>C. card c = k) -->   
  1621         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
  1622         k * card(C) = card (\<Union> C)"
  1623 apply (erule finite_induct, simp)
  1624 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
  1625        finite_subset [of _ "\<Union> (insert x F)"])
  1626 done
  1627 
  1628 
  1629 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  1630 apply (cases "finite A")
  1631 apply (erule finite_induct)
  1632 apply (auto simp add: ring_distrib add_ac)
  1633 done
  1634 
  1635 
  1636 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)"
  1637   apply (erule finite_induct)
  1638   apply (auto simp add: power_Suc)
  1639   done
  1640 
  1641 lemma setsum_bounded:
  1642   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
  1643   shows "setsum f A \<le> of_nat(card A) * K"
  1644 proof (cases "finite A")
  1645   case True
  1646   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1647 next
  1648   case False thus ?thesis by (simp add: setsum_def)
  1649 qed
  1650 
  1651 
  1652 subsubsection {* Cardinality of unions *}
  1653 
  1654 lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
  1655 by(induct n, auto)
  1656 
  1657 lemma card_UN_disjoint:
  1658     "finite I ==> (ALL i:I. finite (A i)) ==>
  1659         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1660       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1661   apply (simp add: card_def del: setsum_constant)
  1662   apply (subgoal_tac
  1663            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1664   apply (simp add: setsum_UN_disjoint del: setsum_constant)
  1665   apply (simp cong: setsum_cong)
  1666   done
  1667 
  1668 lemma card_Union_disjoint:
  1669   "finite C ==> (ALL A:C. finite A) ==>
  1670         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1671       card (Union C) = setsum card C"
  1672   apply (frule card_UN_disjoint [of C id])
  1673   apply (unfold Union_def id_def, assumption+)
  1674   done
  1675 
  1676 subsubsection {* Cardinality of image *}
  1677 
  1678 text{*The image of a finite set can be expressed using @{term fold}.*}
  1679 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
  1680   apply (erule finite_induct, simp)
  1681   apply (subst ACf.fold_insert) 
  1682   apply (auto simp add: ACf_def) 
  1683   done
  1684 
  1685 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1686   apply (induct set: Finites, simp)
  1687   apply (simp add: le_SucI finite_imageI card_insert_if)
  1688   done
  1689 
  1690 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1691 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  1692 
  1693 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1694   by (simp add: card_seteq card_image)
  1695 
  1696 lemma eq_card_imp_inj_on:
  1697   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1698 apply (induct rule:finite_induct, simp)
  1699 apply(frule card_image_le[where f = f])
  1700 apply(simp add:card_insert_if split:if_splits)
  1701 done
  1702 
  1703 lemma inj_on_iff_eq_card:
  1704   "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1705 by(blast intro: card_image eq_card_imp_inj_on)
  1706 
  1707 
  1708 lemma card_inj_on_le:
  1709     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1710 apply (subgoal_tac "finite A") 
  1711  apply (force intro: card_mono simp add: card_image [symmetric])
  1712 apply (blast intro: finite_imageD dest: finite_subset) 
  1713 done
  1714 
  1715 lemma card_bij_eq:
  1716     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1717        finite A; finite B |] ==> card A = card B"
  1718   by (auto intro: le_anti_sym card_inj_on_le)
  1719 
  1720 
  1721 subsubsection {* Cardinality of products *}
  1722 
  1723 (*
  1724 lemma SigmaI_insert: "y \<notin> A ==>
  1725   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1726   by auto
  1727 *)
  1728 
  1729 lemma card_SigmaI [simp]:
  1730   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1731   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1732 by(simp add:card_def setsum_Sigma del:setsum_constant)
  1733 
  1734 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1735 apply (cases "finite A") 
  1736 apply (cases "finite B") 
  1737 apply (auto simp add: card_eq_0_iff
  1738             dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1739 done
  1740 
  1741 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1742 by (simp add: card_cartesian_product)
  1743 
  1744 
  1745 
  1746 subsubsection {* Cardinality of the Powerset *}
  1747 
  1748 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1749   apply (induct set: Finites)
  1750    apply (simp_all add: Pow_insert)
  1751   apply (subst card_Un_disjoint, blast)
  1752     apply (blast intro: finite_imageI, blast)
  1753   apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1754    apply (simp add: card_image Pow_insert)
  1755   apply (unfold inj_on_def)
  1756   apply (blast elim!: equalityE)
  1757   done
  1758 
  1759 text {* Relates to equivalence classes.  Based on a theorem of
  1760 F. Kammüller's.  *}
  1761 
  1762 lemma dvd_partition:
  1763   "finite (Union C) ==>
  1764     ALL c : C. k dvd card c ==>
  1765     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1766   k dvd card (Union C)"
  1767 apply(frule finite_UnionD)
  1768 apply(rotate_tac -1)
  1769   apply (induct set: Finites, simp_all, clarify)
  1770   apply (subst card_Un_disjoint)
  1771   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
  1772   done
  1773 
  1774 
  1775 subsection{* A fold functional for non-empty sets *}
  1776 
  1777 text{* Does not require start value. *}
  1778 
  1779 consts
  1780   fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
  1781 
  1782 inductive "fold1Set f"
  1783 intros
  1784   fold1Set_insertI [intro]:
  1785    "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
  1786 
  1787 constdefs
  1788   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
  1789   "fold1 f A == THE x. (A, x) : fold1Set f"
  1790 
  1791 lemma fold1Set_nonempty:
  1792  "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
  1793 by(erule fold1Set.cases, simp_all) 
  1794 
  1795 
  1796 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
  1797 
  1798 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
  1799 
  1800 
  1801 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
  1802   by (blast intro: foldSet.intros elim: foldSet.cases)
  1803 
  1804 lemma fold1_singleton[simp]: "fold1 f {a} = a"
  1805   by (unfold fold1_def) blast
  1806 
  1807 lemma finite_nonempty_imp_fold1Set:
  1808   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
  1809 apply (induct A rule: finite_induct)
  1810 apply (auto dest: finite_imp_foldSet [of _ f id])  
  1811 done
  1812 
  1813 text{*First, some lemmas about @{term foldSet}.*}
  1814 
  1815 lemma (in ACf) foldSet_insert_swap:
  1816 assumes fold: "(A,y) \<in> foldSet f id b"
  1817 shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
  1818 using fold
  1819 proof (induct rule: foldSet.induct)
  1820   case emptyI thus ?case by (force simp add: fold_insert_aux commute)
  1821 next
  1822   case (insertI A x y)
  1823     have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
  1824       using insertI by force  --{*how does @{term id} get unfolded?*}
  1825     thus ?case by (simp add: insert_commute AC)
  1826 qed
  1827 
  1828 lemma (in ACf) foldSet_permute_diff:
  1829 assumes fold: "(A,x) \<in> foldSet f id b"
  1830 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
  1831 using fold
  1832 proof (induct rule: foldSet.induct)
  1833   case emptyI thus ?case by simp
  1834 next
  1835   case (insertI A x y)
  1836   have "a = x \<or> a \<in> A" using insertI by simp
  1837   thus ?case
  1838   proof
  1839     assume "a = x"
  1840     with insertI show ?thesis
  1841       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
  1842   next
  1843     assume ainA: "a \<in> A"
  1844     hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
  1845       using insertI by (force simp: id_def)
  1846     moreover
  1847     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
  1848       using ainA insertI by blast
  1849     ultimately show ?thesis by (simp add: id_def)
  1850   qed
  1851 qed
  1852 
  1853 lemma (in ACf) fold1_eq_fold:
  1854      "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
  1855 apply (simp add: fold1_def fold_def) 
  1856 apply (rule the_equality)
  1857 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
  1858 apply (rule sym, clarify)
  1859 apply (case_tac "Aa=A")
  1860  apply (best intro: the_equality foldSet_determ)  
  1861 apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
  1862  apply (best intro: the_equality foldSet_determ)  
  1863 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  1864  prefer 2 apply (blast elim: equalityE) 
  1865 apply (auto dest: foldSet_permute_diff [where a=a]) 
  1866 done
  1867 
  1868 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
  1869 apply safe
  1870 apply simp 
  1871 apply (drule_tac x=x in spec)
  1872 apply (drule_tac x="A-{x}" in spec, auto) 
  1873 done
  1874 
  1875 lemma (in ACf) fold1_insert:
  1876   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
  1877   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1878 proof -
  1879   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
  1880     by (auto simp add: nonempty_iff)
  1881   with A show ?thesis
  1882     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
  1883 qed
  1884 
  1885 lemma (in ACIf) fold1_insert_idem [simp]:
  1886   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
  1887   shows "fold1 f (insert x A) = f x (fold1 f A)"
  1888 proof -
  1889   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
  1890     by (auto simp add: nonempty_iff)
  1891   show ?thesis
  1892   proof cases
  1893     assume "a = x"
  1894     thus ?thesis 
  1895     proof cases
  1896       assume "A' = {}"
  1897       with prems show ?thesis by (simp add: idem) 
  1898     next
  1899       assume "A' \<noteq> {}"
  1900       with prems show ?thesis
  1901 	by (simp add: fold1_insert assoc [symmetric] idem) 
  1902     qed
  1903   next
  1904     assume "a \<noteq> x"
  1905     with prems show ?thesis
  1906       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
  1907   qed
  1908 qed
  1909 
  1910 
  1911 text{* Now the recursion rules for definitions: *}
  1912 
  1913 lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
  1914 by(simp add:fold1_singleton)
  1915 
  1916 lemma (in ACf) fold1_insert_def:
  1917   "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1918 by(simp add:fold1_insert)
  1919 
  1920 lemma (in ACIf) fold1_insert_idem_def:
  1921   "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
  1922 by(simp add:fold1_insert_idem)
  1923 
  1924 subsubsection{* Determinacy for @{term fold1Set} *}
  1925 
  1926 text{*Not actually used!!*}
  1927 
  1928 lemma (in ACf) foldSet_permute:
  1929   "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
  1930    ==> (insert b A, x) \<in> foldSet f id a"
  1931 apply (case_tac "a=b") 
  1932 apply (auto dest: foldSet_permute_diff) 
  1933 done
  1934 
  1935 lemma (in ACf) fold1Set_determ:
  1936   "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
  1937 proof (clarify elim!: fold1Set.cases)
  1938   fix A x B y a b
  1939   assume Ax: "(A, x) \<in> foldSet f id a"
  1940   assume By: "(B, y) \<in> foldSet f id b"
  1941   assume anotA:  "a \<notin> A"
  1942   assume bnotB:  "b \<notin> B"
  1943   assume eq: "insert a A = insert b B"
  1944   show "y=x"
  1945   proof cases
  1946     assume same: "a=b"
  1947     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
  1948     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
  1949   next
  1950     assume diff: "a\<noteq>b"
  1951     let ?D = "B - {a}"
  1952     have B: "B = insert a ?D" and A: "A = insert b ?D"
  1953      and aB: "a \<in> B" and bA: "b \<in> A"
  1954       using eq anotA bnotB diff by (blast elim!:equalityE)+
  1955     with aB bnotB By
  1956     have "(insert b ?D, y) \<in> foldSet f id a" 
  1957       by (auto intro: foldSet_permute simp add: insert_absorb)
  1958     moreover
  1959     have "(insert b ?D, x) \<in> foldSet f id a"
  1960       by (simp add: A [symmetric] Ax) 
  1961     ultimately show ?thesis by (blast intro: foldSet_determ) 
  1962   qed
  1963 qed
  1964 
  1965 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
  1966   by (unfold fold1_def) (blast intro: fold1Set_determ)
  1967 
  1968 declare
  1969   empty_foldSetE [rule del]   foldSet.intros [rule del]
  1970   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
  1971   -- {* No more proves involve these relations. *}
  1972 
  1973 subsubsection{* Semi-Lattices *}
  1974 
  1975 locale ACIfSL = ACIf +
  1976   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  1977   and strict_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
  1978   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
  1979   defines strict_below_def:  "(x \<sqsubset> y) \<equiv> (x \<sqsubseteq> y \<and> x \<noteq> y)"
  1980 
  1981 locale ACIfSLlin = ACIfSL +
  1982   assumes lin: "x\<cdot>y \<in> {x,y}"
  1983 
  1984 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"
  1985 by(simp add: below_def idem)
  1986 
  1987 lemma (in ACIfSL) below_f_conv[simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
  1988 proof
  1989   assume "x \<sqsubseteq> y \<cdot> z"
  1990   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
  1991   have "x \<cdot> y = x"
  1992   proof -
  1993     have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
  1994     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  1995     also have "\<dots> = x" by(rule xyzx)
  1996     finally show ?thesis .
  1997   qed
  1998   moreover have "x \<cdot> z = x"
  1999   proof -
  2000     have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
  2001     also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  2002     also have "\<dots> = x" by(rule xyzx)
  2003     finally show ?thesis .
  2004   qed
  2005   ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
  2006 next
  2007   assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
  2008   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  2009   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  2010   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  2011   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  2012   finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
  2013 qed
  2014 
  2015 lemma (in ACIfSLlin) above_f_conv:
  2016  "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
  2017 proof
  2018   assume a: "x \<cdot> y \<sqsubseteq> z"
  2019   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  2020   thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  2021   proof
  2022     assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  2023   next
  2024     assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
  2025   qed
  2026 next
  2027   assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
  2028   thus "x \<cdot> y \<sqsubseteq> z"
  2029   proof
  2030     assume a: "x \<sqsubseteq> z"
  2031     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  2032     also have "x \<cdot> z = x" using a by(simp add:below_def)
  2033     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  2034   next
  2035     assume a: "y \<sqsubseteq> z"
  2036     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  2037     also have "y \<cdot> z = y" using a by(simp add:below_def)
  2038     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
  2039   qed
  2040 qed
  2041 
  2042 
  2043 lemma (in ACIfSLlin) strict_below_f_conv[simp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
  2044 apply(simp add: strict_below_def)
  2045 using lin[of y z] by (auto simp:below_def ACI)
  2046 
  2047 
  2048 lemma (in ACIfSLlin) strict_above_f_conv:
  2049  "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
  2050 apply(simp add: strict_below_def above_f_conv)
  2051 using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
  2052 
  2053 
  2054 subsubsection{* Lemmas about @{text fold1} *}
  2055 
  2056 lemma (in ACf) fold1_Un:
  2057 assumes A: "finite A" "A \<noteq> {}"
  2058 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2059        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2060 using A
  2061 proof(induct rule:finite_ne_induct)
  2062   case singleton thus ?case by(simp add:fold1_insert)
  2063 next
  2064   case insert thus ?case by (simp add:fold1_insert assoc)
  2065 qed
  2066 
  2067 lemma (in ACIf) fold1_Un2:
  2068 assumes A: "finite A" "A \<noteq> {}"
  2069 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2070        fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2071 using A
  2072 proof(induct rule:finite_ne_induct)
  2073   case singleton thus ?case by(simp add:fold1_insert_idem)
  2074 next
  2075   case insert thus ?case by (simp add:fold1_insert_idem assoc)
  2076 qed
  2077 
  2078 lemma (in ACf) fold1_in:
  2079   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  2080   shows "fold1 f A \<in> A"
  2081 using A
  2082 proof (induct rule:finite_ne_induct)
  2083   case singleton thus ?case by simp
  2084 next
  2085   case insert thus ?case using elem by (force simp add:fold1_insert)
  2086 qed
  2087 
  2088 lemma (in ACIfSL) below_fold1_iff:
  2089 assumes A: "finite A" "A \<noteq> {}"
  2090 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
  2091 using A
  2092 by(induct rule:finite_ne_induct) simp_all
  2093 
  2094 lemma (in ACIfSLlin) strict_below_fold1_iff:
  2095   "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<sqsubset> fold1 f A = (\<forall>a\<in>A. x \<sqsubset> a)"
  2096 by(induct rule:finite_ne_induct) simp_all
  2097 
  2098 
  2099 lemma (in ACIfSL) fold1_belowI:
  2100 assumes A: "finite A" "A \<noteq> {}"
  2101 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
  2102 using A
  2103 proof (induct rule:finite_ne_induct)
  2104   case singleton thus ?case by simp
  2105 next
  2106   case (insert x F)
  2107   from insert(5) have "a = x \<or> a \<in> F" by simp
  2108   thus ?case
  2109   proof
  2110     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  2111   next
  2112     assume "a \<in> F"
  2113     hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
  2114     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  2115       using insert by(simp add:below_def ACI)
  2116     also have "fold1 f F \<cdot> a = fold1 f F"
  2117       using bel  by(simp add:below_def ACI)
  2118     also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  2119       using insert by(simp add:below_def ACI)
  2120     finally show ?thesis  by(simp add:below_def)
  2121   qed
  2122 qed
  2123 
  2124 
  2125 lemma (in ACIfSLlin) fold1_below_iff:
  2126 assumes A: "finite A" "A \<noteq> {}"
  2127 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
  2128 using A
  2129 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  2130 
  2131 lemma (in ACIfSLlin) fold1_strict_below_iff:
  2132 assumes A: "finite A" "A \<noteq> {}"
  2133 shows "fold1 f A \<sqsubset> x = (\<exists>a\<in>A. a \<sqsubset> x)"
  2134 using A
  2135 by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
  2136 
  2137 
  2138 lemma (in ACIfSLlin) fold1_antimono:
  2139 assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  2140 shows "fold1 f B \<sqsubseteq> fold1 f A"
  2141 proof(cases)
  2142   assume "A = B" thus ?thesis by simp
  2143 next
  2144   assume "A \<noteq> B"
  2145   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  2146   have "fold1 f B = fold1 f (A \<union> (B-A))" by(subst B)(rule refl)
  2147   also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
  2148   proof -
  2149     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  2150     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  2151     moreover have "(B-A) \<noteq> {}" using prems by blast
  2152     moreover have "A Int (B-A) = {}" using prems by blast
  2153     ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
  2154   qed
  2155   also have "\<dots> \<sqsubseteq> fold1 f A" by(simp add: above_f_conv)
  2156   finally show ?thesis .
  2157 qed
  2158 
  2159 
  2160 
  2161 subsubsection{* Lattices *}
  2162 
  2163 locale Lattice = lattice +
  2164   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
  2165   and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
  2166   defines "Inf == fold1 inf"  and "Sup == fold1 sup"
  2167 
  2168 locale Distrib_Lattice = distrib_lattice + Lattice
  2169 
  2170 text{* Lattices are semilattices *}
  2171 
  2172 lemma (in Lattice) ACf_inf: "ACf inf"
  2173 by(blast intro: ACf.intro inf_commute inf_assoc)
  2174 
  2175 lemma (in Lattice) ACf_sup: "ACf sup"
  2176 by(blast intro: ACf.intro sup_commute sup_assoc)
  2177 
  2178 lemma (in Lattice) ACIf_inf: "ACIf inf"
  2179 apply(rule ACIf.intro)
  2180 apply(rule ACf_inf)
  2181 apply(rule ACIf_axioms.intro)
  2182 apply(rule inf_idem)
  2183 done
  2184 
  2185 lemma (in Lattice) ACIf_sup: "ACIf sup"
  2186 apply(rule ACIf.intro)
  2187 apply(rule ACf_sup)
  2188 apply(rule ACIf_axioms.intro)
  2189 apply(rule sup_idem)
  2190 done
  2191 
  2192 lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \<sqsubseteq>)"
  2193 apply(rule ACIfSL.intro)
  2194 apply(rule ACf_inf)
  2195 apply(rule ACIf.axioms[OF ACIf_inf])
  2196 apply(rule ACIfSL_axioms.intro)
  2197 apply(rule iffI)
  2198  apply(blast intro: antisym inf_le1 inf_le2 inf_least refl)
  2199 apply(erule subst)
  2200 apply(rule inf_le2)
  2201 done
  2202 
  2203 lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \<sqsubseteq> x)"
  2204 apply(rule ACIfSL.intro)
  2205 apply(rule ACf_sup)
  2206 apply(rule ACIf.axioms[OF ACIf_sup])
  2207 apply(rule ACIfSL_axioms.intro)
  2208 apply(rule iffI)
  2209  apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
  2210 apply(erule subst)
  2211 apply(rule sup_ge2)
  2212 done
  2213 
  2214 
  2215 subsubsection{* Fold laws in lattices *}
  2216 
  2217 lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
  2218 apply(unfold Sup_def Inf_def)
  2219 apply(subgoal_tac "EX a. a:A")
  2220 prefer 2 apply blast
  2221 apply(erule exE)
  2222 apply(rule trans)
  2223 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2224 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2225 done
  2226 
  2227 lemma (in Lattice) sup_Inf_absorb[simp]:
  2228   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
  2229 apply(subst sup_commute)
  2230 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2231 done
  2232 
  2233 lemma (in Lattice) inf_Sup_absorb[simp]:
  2234   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
  2235 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2236 
  2237 
  2238 lemma (in ACIf) hom_fold1_commute:
  2239 assumes hom: "!!x y. h(f x y) = f (h x) (h y)"
  2240 and N: "finite N" "N \<noteq> {}" shows "h(fold1 f N) = fold1 f (h ` N)"
  2241 using N proof (induct rule: finite_ne_induct)
  2242   case singleton thus ?case by simp
  2243 next
  2244   case (insert n N)
  2245   have "h(fold1 f (insert n N)) = h(f n (fold1 f N))" using insert by(simp)
  2246   also have "\<dots> = f (h n) (h(fold1 f N))" by(rule hom)
  2247   also have "h(fold1 f N) = fold1 f (h ` N)" by(rule insert)
  2248   also have "f (h n) \<dots> = fold1 f (insert (h n) (h ` N))"
  2249     using insert by(simp)
  2250   also have "insert (h n) (h ` N) = h ` insert n N" by simp
  2251   finally show ?case .
  2252 qed
  2253 
  2254 lemma (in Distrib_Lattice) sup_Inf1_distrib:
  2255  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
  2256 apply(simp add:Inf_def image_def
  2257   ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
  2258 apply(rule arg_cong, blast)
  2259 done
  2260 
  2261 
  2262 lemma (in Distrib_Lattice) sup_Inf2_distrib:
  2263 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2264 shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
  2265 using A
  2266 proof (induct rule: finite_ne_induct)
  2267   case singleton thus ?case
  2268     by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
  2269 next
  2270   case (insert x A)
  2271   have finB: "finite {x \<squnion> b |b. b \<in> B}"
  2272     by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
  2273   have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
  2274   proof -
  2275     have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
  2276       by blast
  2277     thus ?thesis by(simp add: insert(1) B(1))
  2278   qed
  2279   have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2280   have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
  2281     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
  2282   also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
  2283   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}"
  2284     using insert by(simp add:sup_Inf1_distrib[OF B])
  2285   also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
  2286     (is "_ = \<Sqinter>?M")
  2287     using B insert
  2288     by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2289   also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2290     by blast
  2291   finally show ?case .
  2292 qed
  2293 
  2294 
  2295 lemma (in Distrib_Lattice) inf_Sup1_distrib:
  2296  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<sqinter> \<Squnion>A) = \<Squnion>{x \<sqinter> a|a. a \<in> A}"
  2297 apply(simp add:Sup_def image_def
  2298   ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
  2299 apply(rule arg_cong, blast)
  2300 done
  2301 
  2302 
  2303 lemma (in Distrib_Lattice) inf_Sup2_distrib:
  2304 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2305 shows "(\<Squnion>A \<sqinter> \<Squnion>B) = \<Squnion>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
  2306 using A
  2307 proof (induct rule: finite_ne_induct)
  2308   case singleton thus ?case
  2309     by(simp add: inf_Sup1_distrib[OF B] fold1_singleton_def[OF Sup_def])
  2310 next
  2311   case (insert x A)
  2312   have finB: "finite {x \<sqinter> b |b. b \<in> B}"
  2313     by(fast intro: finite_surj[where f = "%b. x \<sqinter> b", OF B(1)])
  2314   have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
  2315   proof -
  2316     have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"
  2317       by blast
  2318     thus ?thesis by(simp add: insert(1) B(1))
  2319   qed
  2320   have ne: "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2321   have "\<Squnion>(insert x A) \<sqinter> \<Squnion>B = (x \<squnion> \<Squnion>A) \<sqinter> \<Squnion>B"
  2322     using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_sup Sup_def])
  2323   also have "\<dots> = (x \<sqinter> \<Squnion>B) \<squnion> (\<Squnion>A \<sqinter> \<Squnion>B)" by(rule inf_sup_distrib2)
  2324   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}"
  2325     using insert by(simp add:inf_Sup1_distrib[OF B])
  2326   also have "\<dots> = \<Squnion>({x\<sqinter>b |b. b \<in> B} \<union> {a\<sqinter>b |a b. a \<in> A \<and> b \<in> B})"
  2327     (is "_ = \<Squnion>?M")
  2328     using B insert
  2329     by(simp add:Sup_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
  2330   also have "?M = {a \<sqinter> b |a b. a \<in> insert x A \<and> b \<in> B}"
  2331     by blast
  2332   finally show ?case .
  2333 qed
  2334 
  2335 
  2336 subsection{*Min and Max*}
  2337 
  2338 text{* As an application of @{text fold1} we define the minimal and
  2339 maximal element of a (non-empty) set over a linear order. *}
  2340 
  2341 constdefs
  2342   Min :: "('a::linorder)set => 'a"
  2343   "Min  ==  fold1 min"
  2344 
  2345   Max :: "('a::linorder)set => 'a"
  2346   "Max  ==  fold1 max"
  2347 
  2348 
  2349 text{* Before we can do anything, we need to show that @{text min} and
  2350 @{text max} are ACI and the ordering is linear: *}
  2351 
  2352 interpretation min: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2353 apply(rule ACf.intro)
  2354 apply(auto simp:min_def)
  2355 done
  2356 
  2357 interpretation min: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2358 apply(rule ACIf_axioms.intro)
  2359 apply(auto simp:min_def)
  2360 done
  2361 
  2362 interpretation max: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2363 apply(rule ACf.intro)
  2364 apply(auto simp:max_def)
  2365 done
  2366 
  2367 interpretation max: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
  2368 apply(rule ACIf_axioms.intro)
  2369 apply(auto simp:max_def)
  2370 done
  2371 
  2372 interpretation min:
  2373   ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
  2374 apply(simp add:order_less_le)
  2375 apply(rule ACIfSL_axioms.intro)
  2376 apply(auto simp:min_def)
  2377 done
  2378 
  2379 interpretation min:
  2380   ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
  2381 apply(rule ACIfSLlin_axioms.intro)
  2382 apply(auto simp:min_def)
  2383 done
  2384 
  2385 interpretation max:
  2386   ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
  2387 apply(simp add:order_less_le eq_sym_conv)
  2388 apply(rule ACIfSL_axioms.intro)
  2389 apply(auto simp:max_def)
  2390 done
  2391 
  2392 interpretation max:
  2393   ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
  2394 apply(rule ACIfSLlin_axioms.intro)
  2395 apply(auto simp:max_def)
  2396 done
  2397 
  2398 interpretation min_max:
  2399   Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2400 apply -
  2401 apply(rule Min_def)
  2402 apply(rule Max_def)
  2403 done
  2404 
  2405 
  2406 interpretation min_max:
  2407   Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
  2408 .
  2409 
  2410 text{* Now we instantiate the recursion equations and declare them
  2411 simplification rules: *}
  2412 
  2413 (* Making Min or Max a defined parameter of a locale, suitably
  2414   extending ACIf, could make the following interpretations more automatic. *)
  2415 
  2416 lemmas Min_singleton = fold1_singleton_def [OF Min_def]
  2417 lemmas Max_singleton = fold1_singleton_def [OF Max_def]
  2418 lemmas Min_insert = min.fold1_insert_idem_def [OF Min_def]
  2419 lemmas Max_insert = max.fold1_insert_idem_def [OF Max_def]
  2420 
  2421 declare Min_singleton [simp]  Max_singleton [simp]
  2422 declare Min_insert [simp]  Max_insert [simp]
  2423 
  2424 
  2425 text{* Now we instantiate some @{text fold1} properties: *}
  2426 
  2427 lemma Min_in [simp]:
  2428   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2429 using min.fold1_in
  2430 by(fastsimp simp: Min_def min_def)
  2431 
  2432 lemma Max_in [simp]:
  2433   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2434 using max.fold1_in
  2435 by(fastsimp simp: Max_def max_def)
  2436 
  2437 lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
  2438 by(simp add:Finite_Set.Min_def min.fold1_antimono)
  2439 
  2440 lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
  2441 by(simp add:Max_def max.fold1_antimono)
  2442 
  2443 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2444 by(simp add: Min_def min.fold1_belowI)
  2445 
  2446 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2447 by(simp add: Max_def max.fold1_belowI)
  2448 
  2449 lemma Min_ge_iff[simp]:
  2450   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
  2451 by(simp add: Min_def min.below_fold1_iff)
  2452 
  2453 lemma Max_le_iff[simp]:
  2454   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
  2455 by(simp add: Max_def max.below_fold1_iff)
  2456 
  2457 lemma Min_gr_iff[simp]:
  2458   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Min A) = (\<forall>a\<in>A. x < a)"
  2459 by(simp add: Min_def min.strict_below_fold1_iff)
  2460 
  2461 lemma Max_less_iff[simp]:
  2462   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A < x) = (\<forall>a\<in>A. a < x)"
  2463 by(simp add: Max_def max.strict_below_fold1_iff)
  2464 
  2465 lemma Min_le_iff:
  2466   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
  2467 by(simp add: Min_def min.fold1_below_iff)
  2468 
  2469 lemma Max_ge_iff:
  2470   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
  2471 by(simp add: Max_def max.fold1_below_iff)
  2472 
  2473 lemma Min_le_iff:
  2474   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A < x) = (\<exists>a\<in>A. a < x)"
  2475 by(simp add: Min_def min.fold1_strict_below_iff)
  2476 
  2477 lemma Max_ge_iff:
  2478   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Max A) = (\<exists>a\<in>A. x < a)"
  2479 by(simp add: Max_def max.fold1_strict_below_iff)
  2480 
  2481 lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
  2482   \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
  2483 by(simp add:Min_def min.f.fold1_Un2)
  2484 
  2485 lemma Max_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
  2486   \<Longrightarrow> Max (A \<union> B) = max (Max A) (Max B)"
  2487 by(simp add:Max_def max.f.fold1_Un2)
  2488 
  2489 
  2490 lemma hom_Min_commute:
  2491  "(!!x y::'a::linorder. h(min x y) = min (h x) (h y::'a))
  2492   \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h(Min N) = Min(h ` N)"
  2493 by(simp add:Finite_Set.Min_def min.hom_fold1_commute)
  2494 
  2495 lemma hom_Max_commute:
  2496  "(!!x y::'a::linorder. h(max x y) = max (h x) (h y::'a))
  2497   \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h(Max N) = Max(h ` N)"
  2498 by(simp add:Max_def max.hom_fold1_commute)
  2499 
  2500 
  2501 lemma add_Min_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
  2502  shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k + Min N = Min {k+m|m. m \<in> N}"
  2503 apply(subgoal_tac "!!x y. k + min x y = min (k + x) (k + y)")
  2504 using hom_Min_commute[of "op + k" N]
  2505 apply simp apply(rule arg_cong[where f = Min]) apply blast
  2506 apply(simp add:min_def linorder_not_le)
  2507 apply(blast intro:order.antisym order_less_imp_le add_left_mono)
  2508 done
  2509 
  2510 lemma add_Max_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
  2511  shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k + Max N = Max {k+m|m. m \<in> N}"
  2512 apply(subgoal_tac "!!x y. k + max x y = max (k + x) (k + y)")
  2513 using hom_Max_commute[of "op + k" N]
  2514 apply simp apply(rule arg_cong[where f = Max]) apply blast
  2515 apply(simp add:max_def linorder_not_le)
  2516 apply(blast intro:order.antisym order_less_imp_le add_left_mono)
  2517 done
  2518 
  2519 
  2520 
  2521 subsection {* Properties of axclass @{text finite} *}
  2522 
  2523 text{* Many of these are by Brian Huffman. *}
  2524 
  2525 lemma finite_set: "finite (A::'a::finite set)"
  2526 by (rule finite_subset [OF subset_UNIV finite])
  2527 
  2528 
  2529 instance unit :: finite
  2530 proof
  2531   have "finite {()}" by simp
  2532   also have "{()} = UNIV" by auto
  2533   finally show "finite (UNIV :: unit set)" .
  2534 qed
  2535 
  2536 instance bool :: finite
  2537 proof
  2538   have "finite {True, False}" by simp
  2539   also have "{True, False} = UNIV" by auto
  2540   finally show "finite (UNIV :: bool set)" .
  2541 qed
  2542 
  2543 
  2544 instance * :: (finite, finite) finite
  2545 proof
  2546   show "finite (UNIV :: ('a \<times> 'b) set)"
  2547   proof (rule finite_Prod_UNIV)
  2548     show "finite (UNIV :: 'a set)" by (rule finite)
  2549     show "finite (UNIV :: 'b set)" by (rule finite)
  2550   qed
  2551 qed
  2552 
  2553 instance "+" :: (finite, finite) finite
  2554 proof
  2555   have a: "finite (UNIV :: 'a set)" by (rule finite)
  2556   have b: "finite (UNIV :: 'b set)" by (rule finite)
  2557   from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
  2558     by (rule finite_Plus)
  2559   thus "finite (UNIV :: ('a + 'b) set)" by simp
  2560 qed
  2561 
  2562 
  2563 instance set :: (finite) finite
  2564 proof
  2565   have "finite (UNIV :: 'a set)" by (rule finite)
  2566   hence "finite (Pow (UNIV :: 'a set))"
  2567     by (rule finite_Pow_iff [THEN iffD2])
  2568   thus "finite (UNIV :: 'a set set)" by simp
  2569 qed
  2570 
  2571 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
  2572 by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
  2573 
  2574 instance fun :: (finite, finite) finite
  2575 proof
  2576   show "finite (UNIV :: ('a => 'b) set)"
  2577   proof (rule finite_imageD)
  2578     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
  2579     show "finite (range ?graph)" by (rule finite_set)
  2580     show "inj ?graph" by (rule inj_graph)
  2581   qed
  2582 qed
  2583 
  2584 end