diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Finite_Set.thy
     ID:         $Id$
     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
+                Additions by Jeremy Avigad in Feb 2004
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
@@ -8,6 +9,65 @@
 
 theory Finite_Set = Divides + Power + Inductive + SetInterval:
 
+subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
+
+axclass plus_ac0 < plus, zero
+  commute:     "x + y = y + x"
+  assoc:       "(x + y) + z = x + (y + z)"
+  zero [simp]: "0 + x = x"
+
+lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.assoc [THEN trans])
+apply (rule plus_ac0.commute [THEN arg_cong])
+done
+
+lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.zero)
+done
+
+lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
+                  plus_ac0.zero plus_ac0_zero_right
+
+instance semiring < plus_ac0
+proof qed (rule add_commute add_assoc almost_semiring.add_0)+
+
+axclass times_ac1 < times, one
+  commute: "x * y = y * x"
+  assoc:   "(x * y) * z = x * (y * z)"
+  one:    "1 * x = x"
+
+theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
+  y * (x * z)"
+proof -
+  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
+    by (rule times_ac1.assoc [THEN sym])
+  also have "x * y = y * x"
+    by (rule times_ac1.commute)
+  also have "(y * x) * z = y * (x * z)"
+    by (rule times_ac1.assoc)
+  finally show ?thesis .
+qed
+
+theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
+proof -
+  have "x * 1 = 1 * x"
+    by (rule times_ac1.commute)
+  also have "... = x"
+    by (rule times_ac1.one)
+  finally show ?thesis .
+qed
+
+instance semiring < times_ac1
+  apply intro_classes
+  apply (rule mult_commute)
+  apply (rule mult_assoc, simp)
+  done
+
+theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute
+  times_ac1.one times_ac1_one_right
+
 subsection {* Collection of finite sets *}
 
 consts Finites :: "'a set set"
@@ -25,8 +85,8 @@
   finite: "finite UNIV"
 
 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
- "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
-by(subgoal_tac "A ~= UNIV", blast, blast)
+ "[| ~finite(UNIV::'a set); finite A  |] ==> \<exists>a::'a. a \<notin> A"
+by(subgoal_tac "A \<noteq> UNIV", blast, blast)
 
 
 lemma finite_induct [case_names empty insert, induct set: Finites]:
@@ -167,6 +227,11 @@
   -- {* The image of a finite set is finite. *}
   by (induct set: Finites) simp_all
 
+lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
+  apply (frule finite_imageI)
+  apply (erule finite_subset, assumption)
+  done
+
 lemma finite_range_imageI:
     "finite (range g) ==> finite (range (%x. f (g x)))"
   apply (drule finite_imageI, simp)
@@ -195,16 +260,16 @@
 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   -- {* The inverse image of a singleton under an injective function
          is included in a singleton. *}
-  apply (auto simp add: inj_on_def) 
-  apply (blast intro: the_equality [symmetric]) 
+  apply (auto simp add: inj_on_def)
+  apply (blast intro: the_equality [symmetric])
   done
 
 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   -- {* The inverse image of a finite set under an injective function
          is finite. *}
-  apply (induct set: Finites, simp_all) 
-  apply (subst vimage_insert) 
-  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
+  apply (induct set: Finites, simp_all)
+  apply (subst vimage_insert)
+  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   done
 
 
@@ -215,10 +280,10 @@
 
 text {*
   Strengthen RHS to
-  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}?
+  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
 
   We'd need to prove
-  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}"}
+  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   by induction. *}
 
 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
@@ -281,6 +346,9 @@
   apply simp
   done
 
+
+subsubsection {* Intervals of nats *}
+
 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
   by (induct k) (simp_all add: lessThan_Suc)
 
@@ -337,6 +405,10 @@
    apply (auto simp add: finite_Field)
   done
 
+lemma finite_cartesian_product: "[| finite A; finite B |] ==>
+    finite (A <*> B)"
+  by (rule finite_SigmaI)
+
 
 subsection {* Finite cardinality *}
 
@@ -521,8 +593,7 @@
   done
 
 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
-  apply (induct set: Finites, simp_all, atomize)
-  apply safe
+  apply (induct set: Finites, simp_all, atomize, safe)
    apply (unfold inj_on_def, blast)
   apply (subst card_insert_disjoint)
     apply (erule finite_imageI, blast, blast)
@@ -553,7 +624,7 @@
 lemma dvd_partition:
   "finite C ==> finite (Union C) ==>
     ALL c : C. k dvd card c ==>
-    (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
+    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
   k dvd card (Union C)"
   apply (induct set: Finites, simp_all, clarify)
   apply (subst card_Un_disjoint)
@@ -784,10 +855,6 @@
   apply (erule finite_induct, auto)
   done
 
-lemma setsum_eq_0_iff [simp]:
-    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
-  by (induct set: Finites) auto
-
 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
@@ -825,6 +892,14 @@
   apply (simp add: setsum_Un_disjoint)
   done
 
+lemma setsum_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      setsum f (Union C) = setsum (setsum f) C"
+  apply (frule setsum_UN_disjoint [of C id f])
+  apply (unfold Union_def id_def, assumption+)
+  done
+
 lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
@@ -832,21 +907,6 @@
   apply (simp add: plus_ac0)
   done
 
-lemma setsum_Un: "finite A ==> finite B ==>
-    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
-  -- {* For the natural numbers, we have subtraction. *}
-  apply (subst setsum_Un_Int [symmetric], auto)
-  done
-
-lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
-    (if a:A then setsum f A - f a else setsum f A)"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: setsum_def)
-  apply (erule finite_induct)
-   apply (auto simp add: insert_Diff_if)
-  apply (drule_tac a = a in mk_disjoint_insert, auto)
-  done
-
 lemma setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   apply (case_tac "finite B")
@@ -865,12 +925,356 @@
   apply (simp add: Ball_def del:insert_Diff_single)
   done
 
-subsubsection{* Min and Max of finite linearly ordered sets *}
+lemma card_UN_disjoint:
+  fixes f :: "'a => 'b::plus_ac0"
+  shows
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
+  apply (subst card_eq_setsum)
+  apply (subst finite_UN, assumption+)
+  apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
+      setsum (%i. (setsum (%x. 1) (A i))) I")
+  apply (erule ssubst)
+  apply (erule setsum_UN_disjoint, assumption+)
+  apply (rule setsum_cong)
+  apply (simp, simp add: card_eq_setsum)
+  done
+
+lemma card_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      card (Union C) = setsum card C"
+  apply (frule card_UN_disjoint [of C id])
+  apply (unfold Union_def id_def, assumption+)
+  done
+
+lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
+  apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
+  apply (erule ssubst, rule setsum_0)
+  apply (rule setsum_cong, auto)
+  done
+
+
+subsubsection {* Reindexing sums *}
+
+lemma setsum_reindex [rule_format]: "finite B ==>
+                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setsum_insert)
+apply (simp add: inj_on_def)
+  done
+
+lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
+    setsum f B = setsum id (f ` B)"
+by (auto simp add: setsum_reindex id_o)
+
+
+subsubsection {* Properties in more restricted classes of structures *}
+
+lemma setsum_eq_0_iff [simp]:
+    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
+  by (induct set: Finites) auto
+
+lemma setsum_constant_nat:
+    "finite A ==> (\<Sum>x: A. y) = (card A) * y"
+  -- {* Later generalized to any semiring. *}
+  by (erule finite_induct, auto)
+
+lemma setsum_Un: "finite A ==> finite B ==>
+    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
+  -- {* For the natural numbers, we have subtraction. *}
+  by (subst setsum_Un_Int [symmetric], auto)
+
+lemma setsum_Un_ring: "finite A ==> finite B ==>
+    (setsum f (A Un B) :: 'a :: ring) =
+      setsum f A + setsum f B - setsum f (A Int B)"
+  apply (subst setsum_Un_Int [symmetric], auto)
+  apply (simp add: compare_rls)
+  done
+
+lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
+    (if a:A then setsum f A - f a else setsum f A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setsum_def)
+  apply (erule finite_induct)
+   apply (auto simp add: insert_Diff_if)
+  apply (drule_tac a = a in mk_disjoint_insert, auto)
+  done
+
+lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
+  - setsum f A"
+  by (induct set: Finites, auto)
+
+lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
+  setsum f A - setsum g A"
+  by (simp add: diff_minus setsum_addf setsum_negf)
+
+lemma setsum_nonneg: "[| finite A;
+    \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
+    0 \<le>  setsum f A";
+  apply (induct set: Finites, auto)
+  apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
+  apply (blast intro: add_mono)
+  done
+
+subsubsection {* Cardinality of Sigma and Cartesian product *}
+
+lemma SigmaI_insert: "y \<notin> A ==>
+  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
+  by auto
+
+lemma card_cartesian_product_singleton [simp]: "finite A ==>
+    card({x} <*> A) = card(A)"
+  apply (subgoal_tac "inj_on (%y .(x,y)) A")
+  apply (frule card_image, assumption)
+  apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
+  apply (auto simp add: inj_on_def)
+  done
+
+lemma card_SigmaI [rule_format,simp]: "finite A ==>
+  (ALL a:A. finite (B a)) -->
+  card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
+  apply (erule finite_induct, auto)
+  apply (subst SigmaI_insert, assumption)
+  apply (subst card_Un_disjoint)
+  apply (auto intro: finite_SigmaI)
+  done
+
+lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
+  card (A <*> B) = card(A) * card(B)"
+  apply (subst card_SigmaI, assumption+)
+  apply (simp add: setsum_constant_nat)
+  done
+
+
+subsection {* Generalized product over a set *}
+
+constdefs
+  setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
+  "setprod f A == if finite A then fold (op * o f) 1 A else 1"
+
+syntax
+  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+                ("\<Prod>_:_. _" [0, 51, 10] 10)
+
+syntax (xsymbols)
+  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+translations
+  "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
+
+
+lemma setprod_empty [simp]: "setprod f {} = 1"
+  by (auto simp add: setprod_def)
+
+lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
+    setprod f (insert a A) = f a * setprod f A"
+  by (auto simp add: setprod_def LC_def LC.fold_insert
+      times_ac1_left_commute)
+
+lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto simp add: times_ac1)
+  apply (simp add: setprod_def)
+  done
+
+lemma setprod_Un_Int: "finite A ==> finite B
+    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
+  apply (induct set: Finites, simp)
+  apply (simp add: times_ac1 insert_absorb)
+  apply (simp add: times_ac1 Int_insert_left insert_absorb)
+  done
+
+lemma setprod_Un_disjoint: "finite A ==> finite B
+  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
+  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+  done
+
+lemma setprod_UN_disjoint:
+  fixes f :: "'a => 'b::times_ac1"
+  shows
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
+  apply (induct set: Finites, simp, atomize)
+  apply (subgoal_tac "ALL i:F. x \<noteq> i")
+   prefer 2 apply blast
+  apply (subgoal_tac "A x Int UNION F A = {}")
+   prefer 2 apply blast
+  apply (simp add: setprod_Un_disjoint)
+  done
+
+lemma setprod_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      setprod f (Union C) = setprod (setprod f) C"
+  apply (frule setprod_UN_disjoint [of C id f])
+  apply (unfold Union_def id_def, assumption+)
+  done
+
+lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
+    (setprod f A * setprod g A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setprod_def times_ac1)
+  apply (erule finite_induct, auto)
+  apply (simp add: times_ac1)
+  apply (simp add: times_ac1)
+  done
+
+lemma setprod_cong:
+  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
+  apply (case_tac "finite B")
+   prefer 2 apply (simp add: setprod_def, simp)
+  apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
+   apply simp
+  apply (erule finite_induct, simp)
+  apply (simp add: subset_insert_iff, clarify)
+  apply (subgoal_tac "finite C")
+   prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+  apply (subgoal_tac "C = insert x (C - {x})")
+   prefer 2 apply blast
+  apply (erule ssubst)
+  apply (drule spec)
+  apply (erule (1) notE impE)
+  apply (simp add: Ball_def del:insert_Diff_single)
+  done
+
+lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
+  apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
+  apply (erule ssubst, rule setprod_1)
+  apply (rule setprod_cong, auto)
+  done
+
+
+subsubsection {* Reindexing products *}
+
+lemma setprod_reindex [rule_format]: "finite B ==>
+                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setprod_insert)
+apply (simp add: inj_on_def)
+  done
+
+lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
+    setprod f B = setprod id (f ` B)"
+by (auto simp add: setprod_reindex id_o)
+
+
+subsubsection {* Properties in more restricted classes of structures *}
+
+lemma setprod_eq_1_iff [simp]:
+    "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
+  by (induct set: Finites) auto
+
+lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
+    y^(card A)"
+  apply (erule finite_induct)
+  apply (auto simp add: power_Suc)
+  done
+
+lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
+    setprod f A = 0"
+  apply (induct set: Finites, force, clarsimp)
+  apply (erule disjE, auto)
+  done
+
+lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
+     --> 0 \<le> setprod f A"
+  apply (case_tac "finite A")
+  apply (induct set: Finites, force, clarsimp)
+  apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
+  apply (rule mult_mono, assumption+)
+  apply (auto simp add: setprod_def)
+  done
+
+lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
+     --> 0 < setprod f A"
+  apply (case_tac "finite A")
+  apply (induct set: Finites, force, clarsimp)
+  apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
+  apply (rule mult_strict_mono, assumption+)
+  apply (auto simp add: setprod_def)
+  done
+
+lemma setprod_nonzero [rule_format]:
+    "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
+      finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
+  apply (erule finite_induct, auto)
+  done
+
+lemma setprod_zero_eq:
+    "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
+     finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
+  apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
+  done
+
+lemma setprod_nonzero_field:
+    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
+  apply (rule setprod_nonzero, auto)
+  done
+
+lemma setprod_zero_eq_field:
+    "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
+  apply (rule setprod_zero_eq, auto)
+  done
+
+lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
+    (setprod f (A Un B) :: 'a ::{field})
+      = setprod f A * setprod f B / setprod f (A Int B)"
+  apply (subst setprod_Un_Int [symmetric], auto)
+  apply (subgoal_tac "finite (A Int B)")
+  apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
+  apply (subst times_divide_eq_right [THEN sym], auto)
+  done
+
+lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
+    (setprod f (A - {a}) :: 'a :: {field}) =
+      (if a:A then setprod f A / f a else setprod f A)"
+  apply (erule finite_induct)
+   apply (auto simp add: insert_Diff_if)
+  apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
+  apply (erule ssubst)
+  apply (subst times_divide_eq_right [THEN sym])
+  apply (auto simp add: mult_ac)
+  done
+
+lemma setprod_inversef: "finite A ==>
+    ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
+      setprod (inverse \<circ> f) A = inverse (setprod f A)"
+  apply (erule finite_induct)
+  apply (simp, simp)
+  done
+
+lemma setprod_dividef:
+     "[|finite A;
+        \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
+      ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
+  apply (subgoal_tac
+         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
+  apply (erule ssubst)
+  apply (subst divide_inverse)
+  apply (subst setprod_timesf)
+  apply (subst setprod_inversef, assumption+, rule refl)
+  apply (rule setprod_cong, rule refl)
+  apply (subst divide_inverse, auto)
+  done
+
+
+subsection{* Min and Max of finite linearly ordered sets *}
 
 text{* Seemed easier to define directly than via fold. *}
 
 lemma ex_Max: fixes S :: "('a::linorder)set"
-  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
+  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
 using fin
 proof (induct)
   case empty thus ?case by simp
@@ -886,14 +1290,14 @@
     proof (cases)
       assume "x \<le> m" thus ?thesis using m by blast
     next
-      assume "\<not> x \<le> m" thus ?thesis using m
+      assume "~ x \<le> m" thus ?thesis using m
 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
     qed
   qed
 qed
 
 lemma ex_Min: fixes S :: "('a::linorder)set"
-  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
+  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
 using fin
 proof (induct)
   case empty thus ?case by simp
@@ -909,18 +1313,18 @@
     proof (cases)
       assume "m \<le> x" thus ?thesis using m by blast
     next
-      assume "\<not> m \<le> x" thus ?thesis using m
+      assume "~ m \<le> x" thus ?thesis using m
 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
     qed
   qed
 qed
 
 constdefs
- Min :: "('a::linorder)set \<Rightarrow> 'a"
-"Min S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
+ Min :: "('a::linorder)set => 'a"
+"Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
 
- Max :: "('a::linorder)set \<Rightarrow> 'a"
-"Max S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
+ Max :: "('a::linorder)set => 'a"
+"Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
 
 lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
                  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
@@ -946,6 +1350,7 @@
   qed
 qed
 
+subsection {* Theorems about @{text "choose"} *}
 
 text {*
   \medskip Basic theorem about @{text "choose"}.  By Florian
@@ -965,7 +1370,7 @@
   apply safe
    apply (auto intro: finite_subset [THEN card_insert_disjoint])
   apply (drule_tac x = "xa - {x}" in spec)
-  apply (subgoal_tac "x ~: xa", auto)
+  apply (subgoal_tac "x \<notin> xa", auto)
   apply (erule rev_mp, subst card_Diff_singleton)
   apply (auto intro: finite_subset)
   done
@@ -974,8 +1379,8 @@
     "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
   by (auto intro: card_mono simp add: card_image [symmetric])
 
-lemma card_bij_eq: 
-    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 
+lemma card_bij_eq:
+    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
        finite A; finite B |] ==> card A = card B"
   by (auto intro: le_anti_sym card_inj_on_le)