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