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