# HG changeset patch
# User haftmann
# Date 1202283272 -3600
# Node ID c2e15e65165f2a446110f927e539869f50096884
# Parent  08d52e2dba07ad44046bf562de827688c66f0943
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder

diff -r 08d52e2dba07 -r c2e15e65165f NEWS
--- a/NEWS	Mon Feb 04 17:00:01 2008 +0100
+++ b/NEWS	Wed Feb 06 08:34:32 2008 +0100
@@ -35,6 +35,11 @@
 
 *** HOL ***
 
+* Theory Finite_Set: locales ACf, ACIf, ACIfSL and ACIfSLlin (whose purpose 
+mainly if for various fold_set functionals) have been abandoned in favour of
+the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult,
+lower_semilattice (resp. uper_semilattice) and linorder.  INCOMPATIBILITY.
+
 * Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
 form set-specific version is available as Inductive.lfp_ordinal_induct_set.
 
diff -r 08d52e2dba07 -r c2e15e65165f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -420,6 +420,157 @@
   done
 
 
+subsection {* Class @{text finite} and code generation *}
+
+lemma finite_code [code func]:
+  "finite {} \<longleftrightarrow> True"
+  "finite (insert a A) \<longleftrightarrow> finite A"
+  by auto
+
+setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
+class finite (attach UNIV) = type +
+  fixes itself :: "'a itself"
+  assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
+setup {* Sign.parent_path *}
+hide const finite
+
+lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
+  by (rule finite_subset [OF subset_UNIV finite_UNIV])
+
+lemma univ_unit [noatp]:
+  "UNIV = {()}" by auto
+
+instantiation unit :: finite
+begin
+
+definition
+  "itself = TYPE(unit)"
+
+instance proof
+  have "finite {()}" by simp
+  also note univ_unit [symmetric]
+  finally show "finite (UNIV :: unit set)" .
+qed
+
+end
+
+lemmas [code func] = univ_unit
+
+lemma univ_bool [noatp]:
+  "UNIV = {False, True}" by auto
+
+instantiation bool :: finite
+begin
+
+definition
+  "itself = TYPE(bool)"
+
+instance proof
+  have "finite {False, True}" by simp
+  also note univ_bool [symmetric]
+  finally show "finite (UNIV :: bool set)" .
+qed
+
+end
+
+lemmas [code func] = univ_bool
+
+instantiation * :: (finite, finite) finite
+begin
+
+definition
+  "itself = TYPE('a \<times> 'b)"
+
+instance proof
+  show "finite (UNIV :: ('a \<times> 'b) set)"
+  proof (rule finite_Prod_UNIV)
+    show "finite (UNIV :: 'a set)" by (rule finite)
+    show "finite (UNIV :: 'b set)" by (rule finite)
+  qed
+qed
+
+end
+
+lemma univ_prod [noatp, code func]:
+  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
+  unfolding UNIV_Times_UNIV ..
+
+instantiation "+" :: (finite, finite) finite
+begin
+
+definition
+  "itself = TYPE('a + 'b)"
+
+instance proof
+  have a: "finite (UNIV :: 'a set)" by (rule finite)
+  have b: "finite (UNIV :: 'b set)" by (rule finite)
+  from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
+    by (rule finite_Plus)
+  thus "finite (UNIV :: ('a + 'b) set)" by simp
+qed
+
+end
+
+lemma univ_sum [noatp, code func]:
+  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
+  unfolding UNIV_Plus_UNIV ..
+
+instantiation set :: (finite) finite
+begin
+
+definition
+  "itself = TYPE('a set)"
+
+instance proof
+  have "finite (UNIV :: 'a set)" by (rule finite)
+  hence "finite (Pow (UNIV :: 'a set))"
+    by (rule finite_Pow_iff [THEN iffD2])
+  thus "finite (UNIV :: 'a set set)" by simp
+qed
+
+end
+
+lemma univ_set [noatp, code func]:
+  "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
+
+lemma inj_graph: "inj (%f. {(x, y). y = f x})"
+  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
+
+instantiation "fun" :: (finite, finite) finite
+begin
+
+definition
+  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
+
+instance proof
+  show "finite (UNIV :: ('a => 'b) set)"
+  proof (rule finite_imageD)
+    let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
+    show "finite (range ?graph)" by (rule finite)
+    show "inj ?graph" by (rule inj_graph)
+  qed
+qed
+
+end
+
+hide (open) const itself
+
+subsection {* Equality and order on functions *}
+
+instance "fun" :: (finite, eq) eq ..
+
+lemma eq_fun [code func]:
+  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>eq"
+  shows "f = g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x = g x)"
+  unfolding expand_fun_eq by auto
+
+lemma order_fun [code func]:
+  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>order"
+  shows "f \<le> g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x \<le> g x)"
+    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<in>UNIV. f x \<noteq> g x)"
+  by (auto simp add: expand_fun_eq le_fun_def less_fun_def order_less_le)
+
+
 subsection {* A fold functional for finite sets *}
 
 text {* The intended behaviour is
@@ -463,56 +614,6 @@
   by (induct set: finite) auto
 
 
-subsubsection {* Commutative monoids *}
-
-(*FIXME integrate with Orderings.thy/OrderedGroup.thy*)
-locale ACf =
-  fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
-  assumes commute: "x \<cdot> y = y \<cdot> x"
-    and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
-begin
-
-lemma left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-proof -
-  have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
-  also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
-  also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
-  finally show ?thesis .
-qed
-
-lemmas AC = assoc commute left_commute
-
-end
-
-locale ACe = ACf +
-  fixes e :: 'a
-  assumes ident [simp]: "x \<cdot> e = x"
-begin
-
-lemma left_ident [simp]: "e \<cdot> x = x"
-proof -
-  have "x \<cdot> e = x" by (rule ident)
-  thus ?thesis by (subst commute)
-qed
-
-end
-
-locale ACIf = ACf +
-  assumes idem: "x \<cdot> x = x"
-begin
-
-lemma idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y"
-proof -
-  have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc)
-  also have "\<dots> = x \<cdot> y" by(simp add:idem)
-  finally show ?thesis .
-qed
-
-lemmas ACI = AC idem idem2
-
-end
-
-
 subsubsection{*From @{term foldSet} to @{term fold}*}
 
 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
@@ -557,16 +658,19 @@
   qed
 qed
 
-lemma (in ACf) foldSet_determ_aux:
+context ab_semigroup_mult
+begin
+
+lemma foldSet_determ_aux:
   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
-                foldSet f g z A x; foldSet f g z A x' \<rbrakk>
+                foldSet times g z A x; foldSet times g z A x' \<rbrakk>
    \<Longrightarrow> x' = x"
 proof (induct n rule: less_induct)
   case (less n)
     have IH: "!!m h A x x'. 
                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
-                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
-    have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'"
+                foldSet times g z A x; foldSet times g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
+    have Afoldx: "foldSet times g z A x" and Afoldx': "foldSet times g z A x'"
      and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
     show ?case
     proof (rule foldSet.cases [OF Afoldx])
@@ -574,16 +678,16 @@
       with Afoldx' show "x' = x" by blast
     next
       fix B b u
-      assume AbB: "A = insert b B" and x: "x = g b \<cdot> u"
-         and notinB: "b \<notin> B" and Bu: "foldSet f g z B u"
+      assume AbB: "A = insert b B" and x: "x = g b * u"
+         and notinB: "b \<notin> B" and Bu: "foldSet times g z B u"
       show "x'=x" 
       proof (rule foldSet.cases [OF Afoldx'])
         assume "A = {}" and "x' = z"
         with AbB show "x' = x" by blast
       next
 	fix C c v
-	assume AcC: "A = insert c C" and x': "x' = g c \<cdot> v"
-           and notinC: "c \<notin> C" and Cv: "foldSet f g z C v"
+	assume AcC: "A = insert c C" and x': "x' = g c * v"
+           and notinC: "c \<notin> C" and Cv: "foldSet times g z C v"
 	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
         from insert_inj_onE [OF Beq notinB injh]
         obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
@@ -607,51 +711,52 @@
 	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
 	  with AbB have "finite ?D" by simp
-	  then obtain d where Dfoldd: "foldSet f g z ?D d"
+	  then obtain d where Dfoldd: "foldSet times g z ?D d"
 	    using finite_imp_foldSet by iprover
 	  moreover have cinB: "c \<in> B" using B by auto
-	  ultimately have "foldSet f g z B (g c \<cdot> d)"
+	  ultimately have "foldSet times g z B (g c * d)"
 	    by(rule Diff1_foldSet)
-	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
-          moreover have "g b \<cdot> d = v"
-	  proof (rule IH[OF lessC Ceq inj_onC Cv])
-	    show "foldSet f g z C (g b \<cdot> d)" using C notinB Dfoldd
+	  then have "g c * d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
+          then have "u = g c * d" ..
+          moreover have "v = g b * d"
+	  proof (rule sym, rule IH [OF lessC Ceq inj_onC Cv])
+	    show "foldSet times g z C (g b * d)" using C notinB Dfoldd
 	      by fastsimp
 	  qed
-	  ultimately show ?thesis using x x' by (auto simp: AC)
+	  ultimately show ?thesis using x x'
+	    by (simp add: mult_left_commute)
 	qed
       qed
     qed
   qed
 
-
-lemma (in ACf) foldSet_determ:
-  "foldSet f g z A x ==> foldSet f g z A y ==> y = x"
+lemma foldSet_determ:
+  "foldSet times g z A x ==> foldSet times g z A y ==> y = x"
 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
 apply (blast intro: foldSet_determ_aux [rule_format])
 done
 
-lemma (in ACf) fold_equality: "foldSet f g z A y ==> fold f g z A = y"
+lemma fold_equality: "foldSet times g z A y ==> fold times g z A = y"
   by (unfold fold_def) (blast intro: foldSet_determ)
 
 text{* The base case for @{text fold}: *}
 
-lemma fold_empty [simp]: "fold f g z {} = z"
+lemma (in -) fold_empty [simp]: "fold f g z {} = z"
   by (unfold fold_def) blast
 
-lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
-    (foldSet f g z (insert x A) v) =
-    (EX y. foldSet f g z A y & v = f (g x) y)"
+lemma fold_insert_aux: "x \<notin> A ==>
+    (foldSet times g z (insert x A) v) =
+    (EX y. foldSet times g z A y & v = g x * y)"
   apply auto
-  apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
+  apply (rule_tac A1 = A and f1 = times in finite_imp_foldSet [THEN exE])
    apply (fastsimp dest: foldSet_imp_finite)
   apply (blast intro: foldSet_determ)
   done
 
 text{* The recursion equation for @{text fold}: *}
 
-lemma (in ACf) fold_insert[simp]:
-    "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
+lemma fold_insert [simp]:
+    "finite A ==> x \<notin> A ==> fold times g z (insert x A) = g x * fold times g z A"
   apply (unfold fold_def)
   apply (simp add: fold_insert_aux)
   apply (rule the_equality)
@@ -659,23 +764,27 @@
     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   done
 
-lemma (in ACf) fold_rec:
+lemma fold_rec:
 assumes fin: "finite A" and a: "a:A"
-shows "fold f g z A = f (g a) (fold f g z (A - {a}))"
+shows "fold times g z A = g a * fold times g z (A - {a})"
 proof-
   have A: "A = insert a (A - {a})" using a by blast
-  hence "fold f g z A = fold f g z (insert a (A - {a}))" by simp
-  also have "\<dots> = f (g a) (fold f g z (A - {a}))"
+  hence "fold times g z A = fold times g z (insert a (A - {a}))" by simp
+  also have "\<dots> = g a * fold times g z (A - {a})"
     by(rule fold_insert) (simp add:fin)+
   finally show ?thesis .
 qed
 
+end
 
 text{* A simplified version for idempotent functions: *}
 
-lemma (in ACIf) fold_insert_idem:
+context ab_semigroup_idem_mult
+begin
+
+lemma fold_insert_idem:
 assumes finA: "finite A"
-shows "fold f g z (insert a A) = g a \<cdot> fold f g z A"
+shows "fold times g z (insert a A) = g a * fold times g z A"
 proof cases
   assume "a \<in> A"
   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
@@ -683,11 +792,12 @@
   show ?thesis
   proof -
     from finA A have finB: "finite B" by(blast intro: finite_subset)
-    have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
-    also have "\<dots> = (g a) \<cdot> (fold f g z B)"
+    have "fold times g z (insert a A) = fold times g z (insert a B)" using A by simp
+    also have "\<dots> = g a * fold times g z B"
       using finB disj by simp
-    also have "\<dots> = g a \<cdot> fold f g z A"
-      using A finB disj by(simp add:idem assoc[symmetric])
+    also have "\<dots> = g a * fold times g z A"
+      using A finB disj
+	by (simp add: mult_idem mult_assoc [symmetric])
     finally show ?thesis .
   qed
 next
@@ -695,81 +805,61 @@
   with finA show ?thesis by simp
 qed
 
-lemma (in ACIf) foldI_conv_id:
-  "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
+lemma foldI_conv_id:
+  "finite A \<Longrightarrow> fold times g z A = fold times id z (g ` A)"
 by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
 
+end
+
 subsubsection{*Lemmas about @{text fold}*}
 
-lemma (in ACf) fold_commute:
-  "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
+context ab_semigroup_mult
+begin
+
+lemma fold_commute:
+  "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
   apply (induct set: finite)
    apply simp
-  apply (simp add: left_commute [of x])
+  apply (simp add: mult_left_commute [of x])
   done
 
-lemma (in ACf) fold_nest_Un_Int:
+lemma fold_nest_Un_Int:
   "finite A ==> finite B
-    ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
+    ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
   apply (induct set: finite)
    apply simp
   apply (simp add: fold_commute Int_insert_left insert_absorb)
   done
 
-lemma (in ACf) fold_nest_Un_disjoint:
+lemma fold_nest_Un_disjoint:
   "finite A ==> finite B ==> A Int B = {}
-    ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
+    ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
   by (simp add: fold_nest_Un_Int)
 
-lemma (in ACf) fold_reindex:
+lemma fold_reindex:
 assumes fin: "finite A"
-shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
+shows "inj_on h A \<Longrightarrow> fold times g z (h ` A) = fold times (g \<circ> h) z A"
 using fin apply induct
  apply simp
 apply simp
 done
 
-lemma (in ACe) fold_Un_Int:
-  "finite A ==> finite B ==>
-    fold f g e A \<cdot> fold f g e B =
-    fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
-  apply (induct set: finite, simp)
-  apply (simp add: AC insert_absorb Int_insert_left)
-  done
-
-corollary (in ACe) fold_Un_disjoint:
-  "finite A ==> finite B ==> A Int B = {} ==>
-    fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
-  by (simp add: fold_Un_Int)
-
-lemma (in ACe) fold_UN_disjoint:
-  "\<lbrakk> finite I; ALL i:I. finite (A i);
-     ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
-   \<Longrightarrow> fold f g e (UNION I A) =
-       fold f (%i. fold f g e (A i)) e I"
-  apply (induct set: finite, 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: fold_Un_disjoint)
-  done
-
-text{*Fusion theorem, as described in
-Graham Hutton's paper,
-A Tutorial on the Universality and Expressiveness of Fold,
-JFP 9:4 (355-372), 1999.*}
-lemma (in ACf) fold_fusion:
-      includes ACf g
-      shows
-	"finite A ==> 
-	 (!!x y. h (g x y) = f x (h y)) ==>
-         h (fold g j w A) = fold f j (h w) A"
-  by (induct set: finite) simp_all
-
-lemma (in ACf) fold_cong:
-  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
-  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
+text{*
+  Fusion theorem, as described in Graham Hutton's paper,
+  A Tutorial on the Universality and Expressiveness of Fold,
+  JFP 9:4 (355-372), 1999.
+*}
+
+lemma fold_fusion:
+  includes ab_semigroup_mult g
+  assumes fin: "finite A"
+    and hyp: "\<And>x y. h (g x y) = times x (h y)"
+  shows "h (fold g j w A) = fold times j (h w) A"
+  using fin hyp by (induct set: finite) simp_all
+
+lemma fold_cong:
+  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
+  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold times g z C = fold times h z C")
    apply simp
   apply (erule finite_induct, simp)
   apply (simp add: subset_insert_iff, clarify)
@@ -783,9 +873,39 @@
   apply (simp add: Ball_def del: insert_Diff_single)
   done
 
-lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
-  fold f (%x. fold f (g x) e (B x)) e A =
-  fold f (split g) e (SIGMA x:A. B x)"
+end
+
+context comm_monoid_mult
+begin
+
+lemma fold_Un_Int:
+  "finite A ==> finite B ==>
+    fold times g 1 A * fold times g 1 B =
+    fold times g 1 (A Un B) * fold times g 1 (A Int B)"
+  by (induct set: finite) 
+    (auto simp add: mult_ac insert_absorb Int_insert_left)
+
+corollary fold_Un_disjoint:
+  "finite A ==> finite B ==> A Int B = {} ==>
+    fold times g 1 (A Un B) = fold times g 1 A * fold times g 1 B"
+  by (simp add: fold_Un_Int)
+
+lemma fold_UN_disjoint:
+  "\<lbrakk> finite I; ALL i:I. finite (A i);
+     ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
+   \<Longrightarrow> fold times g 1 (UNION I A) =
+       fold times (%i. fold times g 1 (A i)) 1 I"
+  apply (induct set: finite, 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: fold_Un_disjoint)
+  done
+
+lemma fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
+  fold times (%x. fold times (g x) 1 (B x)) 1 A =
+  fold times (split g) 1 (SIGMA x:A. B x)"
 apply (subst Sigma_def)
 apply (subst fold_UN_disjoint, assumption, simp)
  apply blast
@@ -795,24 +915,18 @@
 apply simp
 done
 
-lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
-   fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
-apply (erule finite_induct, simp)
-apply (simp add:AC)
-done
-
-
-text{* Interpretation of locales -- see OrderedGroup.thy *}
-
-interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
-  by unfold_locales (auto intro: add_assoc add_commute)
-
-interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
-  by unfold_locales (auto intro: mult_assoc mult_commute)
+lemma fold_distrib: "finite A \<Longrightarrow>
+   fold times (%x. g x * h x) 1 A = fold times g 1 A *  fold times h 1 A"
+  by (erule finite_induct) (simp_all add: mult_ac)
+
+end
 
 
 subsection {* Generalized summation over a set *}
 
+interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
+  by unfold_locales (auto intro: add_assoc add_commute)
+
 constdefs
   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   "setsum f A == if finite A then fold (op +) f 0 A else 0"
@@ -873,7 +987,7 @@
 
 lemma setsum_reindex:
      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
-by(auto simp add: setsum_def AC_add.fold_reindex dest!:finite_imageD)
+by(auto simp add: setsum_def comm_monoid_add.fold_reindex dest!:finite_imageD)
 
 lemma setsum_reindex_id:
      "inj_on f B ==> setsum f B = setsum id (f ` B)"
@@ -881,12 +995,12 @@
 
 lemma setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
-by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
+by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_cong)
 
 lemma strong_setsum_cong[cong]:
   "A = B ==> (!!x. x:B =simp=> f x = g x)
    ==> setsum (%x. f x) A = setsum (%x. g x) B"
-by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
+by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_cong)
 
 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
   by (rule setsum_cong[OF refl], auto);
@@ -907,7 +1021,7 @@
 lemma setsum_Un_Int: "finite A ==> finite B ==>
   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-by(simp add: setsum_def AC_add.fold_Un_Int [symmetric])
+by(simp add: setsum_def comm_monoid_add.fold_Un_Int [symmetric])
 
 lemma setsum_Un_disjoint: "finite A ==> finite B
   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
@@ -919,7 +1033,7 @@
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
-by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong)
+by(simp add: setsum_def comm_monoid_add.fold_UN_disjoint cong: setsum_cong)
 
 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
@@ -937,7 +1051,7 @@
   the rhs need not be, since SIGMA A B could still be finite.*)
 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
-by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
+by(simp add:setsum_def comm_monoid_add.fold_Sigma split_def cong:setsum_cong)
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setsum_cartesian_product: 
@@ -952,7 +1066,7 @@
 done
 
 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
-by(simp add:setsum_def AC_add.fold_distrib)
+by(simp add:setsum_def comm_monoid_add.fold_distrib)
 
 
 subsubsection {* Properties in more restricted classes of structures *}
@@ -1331,18 +1445,18 @@
 
 lemma setprod_reindex:
      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
-by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
+by(auto simp: setprod_def fold_reindex dest!:finite_imageD)
 
 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
 by (auto simp add: setprod_reindex)
 
 lemma setprod_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
+by(fastsimp simp: setprod_def intro: fold_cong)
 
 lemma strong_setprod_cong:
   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
+by(fastsimp simp: simp_implies_def setprod_def intro: fold_cong)
 
 lemma setprod_reindex_cong: "inj_on f A ==>
     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
@@ -1362,7 +1476,7 @@
 
 lemma setprod_Un_Int: "finite A ==> finite B
     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
-by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
+by(simp add: setprod_def fold_Un_Int[symmetric])
 
 lemma setprod_Un_disjoint: "finite A ==> finite B
   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
@@ -1372,7 +1486,7 @@
     "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 (%i. setprod f (A i)) I"
-by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
+by(simp add: setprod_def fold_UN_disjoint cong: setprod_cong)
 
 lemma setprod_Union_disjoint:
   "[| (ALL A:C. finite A);
@@ -1387,7 +1501,7 @@
 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
-by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
+by(simp add:setprod_def fold_Sigma split_def cong:setprod_cong)
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setprod_cartesian_product: 
@@ -1403,7 +1517,7 @@
 
 lemma setprod_timesf:
      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
-by(simp add:setprod_def AC_mult.fold_distrib)
+by(simp add:setprod_def fold_distrib)
 
 
 subsubsection {* Properties in more restricted classes of structures *}
@@ -1555,6 +1669,12 @@
 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
 
+lemma card_code [code func]:
+  "card {} = 0"
+  "card (insert a A) =
+    (if finite A then Suc (card (A - {a})) else card (insert a A))"
+  by (auto simp add: card_insert)
+
 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
 by (simp add: card_insert_if)
 
@@ -1701,10 +1821,14 @@
 
 text{*The image of a finite set can be expressed using @{term fold}.*}
 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
-  apply (erule finite_induct, simp)
-  apply (subst ACf.fold_insert) 
-  apply (auto simp add: ACf_def) 
-  done
+proof (induct rule: finite_induct)
+  case empty then show ?case by simp
+next
+  invoke ab_semigroup_mult ["op Un"]
+    by unfold_locales auto
+  case insert 
+  then show ?case by simp
+qed
 
 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   apply (induct set: finite)
@@ -1861,22 +1985,25 @@
 
 text{*First, some lemmas about @{term foldSet}.*}
 
-lemma (in ACf) foldSet_insert_swap:
-assumes fold: "foldSet f id b A y"
-shows "b \<notin> A \<Longrightarrow> foldSet f id z (insert b A) (z \<cdot> y)"
+context ab_semigroup_mult
+begin
+
+lemma foldSet_insert_swap:
+assumes fold: "foldSet times id b A y"
+shows "b \<notin> A \<Longrightarrow> foldSet times id z (insert b A) (z * y)"
 using fold
 proof (induct rule: foldSet.induct)
-  case emptyI thus ?case by (force simp add: fold_insert_aux commute)
+  case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
 next
   case (insertI x A y)
-    have "foldSet f (\<lambda>u. u) z (insert x (insert b A)) (x \<cdot> (z \<cdot> y))"
+    have "foldSet times (\<lambda>u. u) z (insert x (insert b A)) (x * (z * y))"
       using insertI by force  --{*how does @{term id} get unfolded?*}
-    thus ?case by (simp add: insert_commute AC)
+    thus ?case by (simp add: insert_commute mult_ac)
 qed
 
-lemma (in ACf) foldSet_permute_diff:
-assumes fold: "foldSet f id b A x"
-shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet f id a (insert b (A-{a})) x"
+lemma foldSet_permute_diff:
+assumes fold: "foldSet times id b A x"
+shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet times id a (insert b (A-{a})) x"
 using fold
 proof (induct rule: foldSet.induct)
   case emptyI thus ?case by simp
@@ -1890,7 +2017,7 @@
       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
   next
     assume ainA: "a \<in> A"
-    hence "foldSet f id a (insert x (insert b (A - {a}))) (x \<cdot> y)"
+    hence "foldSet times id a (insert x (insert b (A - {a}))) (x * y)"
       using insertI by (force simp: id_def)
     moreover
     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
@@ -1899,15 +2026,15 @@
   qed
 qed
 
-lemma (in ACf) fold1_eq_fold:
-     "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
+lemma fold1_eq_fold:
+     "[|finite A; a \<notin> A|] ==> fold1 times (insert a A) = fold times id a A"
 apply (simp add: fold1_def fold_def) 
 apply (rule the_equality)
-apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
+apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ times id]) 
 apply (rule sym, clarify)
 apply (case_tac "Aa=A")
  apply (best intro: the_equality foldSet_determ)  
-apply (subgoal_tac "foldSet f id a A x")
+apply (subgoal_tac "foldSet times id a A x")
  apply (best intro: the_equality foldSet_determ)  
 apply (subgoal_tac "insert aa (Aa - {a}) = A") 
  prefer 2 apply (blast elim: equalityE) 
@@ -1921,9 +2048,9 @@
 apply (drule_tac x="A-{x}" in spec, auto) 
 done
 
-lemma (in ACf) fold1_insert:
+lemma fold1_insert:
   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
-  shows "fold1 f (insert x A) = f x (fold1 f A)"
+  shows "fold1 times (insert x A) = x * fold1 times A"
 proof -
   from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
     by (auto simp add: nonempty_iff)
@@ -1931,9 +2058,14 @@
     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
 qed
 
-lemma (in ACIf) fold1_insert_idem [simp]:
+end
+
+context ab_semigroup_idem_mult
+begin
+
+lemma fold1_insert_idem [simp]:
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
-  shows "fold1 f (insert x A) = f x (fold1 f A)"
+  shows "fold1 times (insert x A) = x * fold1 times A"
 proof -
   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
     by (auto simp add: nonempty_iff)
@@ -1943,11 +2075,11 @@
     thus ?thesis 
     proof cases
       assume "A' = {}"
-      with prems show ?thesis by (simp add: idem) 
+      with prems show ?thesis by (simp add: mult_idem) 
     next
       assume "A' \<noteq> {}"
       with prems show ?thesis
-	by (simp add: fold1_insert assoc [symmetric] idem) 
+	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem) 
     qed
   next
     assume "a \<noteq> x"
@@ -1956,53 +2088,58 @@
   qed
 qed
 
-lemma (in ACIf) hom_fold1_commute:
-assumes hom: "!!x y. h(f x y) = f (h x) (h y)"
-and N: "finite N" "N \<noteq> {}" shows "h(fold1 f N) = fold1 f (h ` N)"
+lemma hom_fold1_commute:
+assumes hom: "!!x y. h (x * y) = h x * h y"
+and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
 using N proof (induct rule: finite_ne_induct)
   case singleton thus ?case by simp
 next
   case (insert n N)
-  then have "h(fold1 f (insert n N)) = h(f n (fold1 f N))" by simp
-  also have "\<dots> = f (h n) (h(fold1 f N))" by(rule hom)
-  also have "h(fold1 f N) = fold1 f (h ` N)" by(rule insert)
-  also have "f (h n) \<dots> = fold1 f (insert (h n) (h ` N))"
+  then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
+  also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
+  also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
+  also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
     using insert by(simp)
   also have "insert (h n) (h ` N) = h ` insert n N" by simp
   finally show ?case .
 qed
 
+end
+
 
 text{* Now the recursion rules for definitions: *}
 
 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
 by(simp add:fold1_singleton)
 
-lemma (in ACf) fold1_insert_def:
-  "\<lbrakk> g = fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x \<cdot> (g A)"
-by(simp add:fold1_insert)
-
-lemma (in ACIf) fold1_insert_idem_def:
-  "\<lbrakk> g = fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x \<cdot> (g A)"
-by(simp add:fold1_insert_idem)
+lemma (in ab_semigroup_mult) fold1_insert_def:
+  "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
+by (simp add:fold1_insert)
+
+lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
+  "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
+by simp
 
 subsubsection{* Determinacy for @{term fold1Set} *}
 
 text{*Not actually used!!*}
 
-lemma (in ACf) foldSet_permute:
-  "[|foldSet f id b (insert a A) x; a \<notin> A; b \<notin> A|]
-   ==> foldSet f id a (insert b A) x"
-apply (case_tac "a=b") 
+context ab_semigroup_mult
+begin
+
+lemma foldSet_permute:
+  "[|foldSet times id b (insert a A) x; a \<notin> A; b \<notin> A|]
+   ==> foldSet times id a (insert b A) x"
+apply (cases "a=b") 
 apply (auto dest: foldSet_permute_diff) 
 done
 
-lemma (in ACf) fold1Set_determ:
-  "fold1Set f A x ==> fold1Set f A y ==> y = x"
+lemma fold1Set_determ:
+  "fold1Set times A x ==> fold1Set times A y ==> y = x"
 proof (clarify elim!: fold1Set.cases)
   fix A x B y a b
-  assume Ax: "foldSet f id a A x"
-  assume By: "foldSet f id b B y"
+  assume Ax: "foldSet times id a A x"
+  assume By: "foldSet times id b B y"
   assume anotA:  "a \<notin> A"
   assume bnotB:  "b \<notin> B"
   assume eq: "insert a A = insert b B"
@@ -2018,171 +2155,40 @@
      and aB: "a \<in> B" and bA: "b \<in> A"
       using eq anotA bnotB diff by (blast elim!:equalityE)+
     with aB bnotB By
-    have "foldSet f id a (insert b ?D) y" 
+    have "foldSet times id a (insert b ?D) y" 
       by (auto intro: foldSet_permute simp add: insert_absorb)
     moreover
-    have "foldSet f id a (insert b ?D) x"
+    have "foldSet times id a (insert b ?D) x"
       by (simp add: A [symmetric] Ax) 
     ultimately show ?thesis by (blast intro: foldSet_determ) 
   qed
 qed
 
-lemma (in ACf) fold1Set_equality: "fold1Set f A y ==> fold1 f A = y"
+lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
   by (unfold fold1_def) (blast intro: fold1Set_determ)
 
+end
+
 declare
   empty_foldSetE [rule del]   foldSet.intros [rule del]
   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
   -- {* No more proofs involve these relations. *}
 
-
-subsubsection{* Semi-Lattices *}
-
-locale ACIfSL = ord + ACIf +
-  assumes below_def: "less_eq x y \<longleftrightarrow> x \<cdot> y = x"
-  and strict_below_def: "less x y \<longleftrightarrow> less_eq x y \<and> x \<noteq> y"
+subsubsection {* Lemmas about @{text fold1} *}
+
+context ab_semigroup_mult
 begin
 
-notation
-  less     ("(_/ \<prec> _)"  [51, 51] 50)
-
-notation (xsymbols)
-  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
-
-notation (HTML output)
-  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
-
-lemma below_refl [simp]: "x \<preceq> x"
-  by (simp add: below_def idem)
-
-lemma below_antisym:
-  assumes xy: "x \<preceq> y" and yx: "y \<preceq> x"
-  shows "x = y"
-  using xy [unfolded below_def, symmetric]
-    yx [unfolded below_def commute]
-  by (rule trans)
-
-lemma below_trans:
-  assumes xy: "x \<preceq> y" and yz: "y \<preceq> z"
-  shows "x \<preceq> z"
-proof -
-  from xy have x_xy: "x \<cdot> y = x" by (simp add: below_def)
-  from yz have y_yz: "y \<cdot> z = y" by (simp add: below_def)
-  from y_yz have "x \<cdot> y \<cdot> z = x \<cdot> y" by (simp add: assoc)
-  with x_xy have "x \<cdot> y \<cdot> z = x"  by simp
-  moreover from x_xy have "x \<cdot> z = x \<cdot> y \<cdot> z" by simp
-  ultimately have "x \<cdot> z = x" by simp
-  then show ?thesis by (simp add: below_def)
-qed
-
-lemma below_f_conv [simp,noatp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)"
-proof
-  assume "x \<preceq> y \<cdot> z"
-  hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
-  have "x \<cdot> y = x"
-  proof -
-    have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
-    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
-    also have "\<dots> = x" by(rule xyzx)
-    finally show ?thesis .
-  qed
-  moreover have "x \<cdot> z = x"
-  proof -
-    have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
-    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
-    also have "\<dots> = x" by(rule xyzx)
-    finally show ?thesis .
-  qed
-  ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def)
-next
-  assume a: "x \<preceq> y \<and> x \<preceq> z"
-  hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
-  have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
-  also have "x \<cdot> y = x" using a by(simp_all add: below_def)
-  also have "x \<cdot> z = x" using a by(simp_all add: below_def)
-  finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def)
-qed
-
-end
-
-interpretation ACIfSL < order
-by unfold_locales
-  (simp add: strict_below_def, auto intro: below_refl below_trans below_antisym)
-
-locale ACIfSLlin = ACIfSL +
-  assumes lin: "x\<cdot>y \<in> {x,y}"
-begin
-
-lemma above_f_conv:
- "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)"
-proof
-  assume a: "x \<cdot> y \<preceq> z"
-  have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
-  thus "x \<preceq> z \<or> y \<preceq> z"
-  proof
-    assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
-  next
-    assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
-  qed
-next
-  assume "x \<preceq> z \<or> y \<preceq> z"
-  thus "x \<cdot> y \<preceq> z"
-  proof
-    assume a: "x \<preceq> z"
-    have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
-    also have "x \<cdot> z = x" using a by(simp add:below_def)
-    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
-  next
-    assume a: "y \<preceq> z"
-    have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
-    also have "y \<cdot> z = y" using a by(simp add:below_def)
-    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
-  qed
-qed
-
-lemma strict_below_f_conv[simp,noatp]: "x \<prec> y \<cdot> z = (x \<prec> y \<and> x \<prec> z)"
-apply(simp add: strict_below_def)
-using lin[of y z] by (auto simp:below_def ACI)
-
-lemma strict_above_f_conv:
-  "x \<cdot> y \<prec> z = (x \<prec> z \<or> y \<prec> z)"
-apply(simp add: strict_below_def above_f_conv)
-using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
-
-end
-
-interpretation ACIfSLlin < linorder
-  by unfold_locales
-    (insert lin [simplified insert_iff], simp add: below_def commute)
-
-
-subsubsection{* Lemmas about @{text fold1} *}
-
-lemma (in ACf) fold1_Un:
+lemma fold1_Un:
 assumes A: "finite A" "A \<noteq> {}"
 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
-       fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
-using A
-proof(induct rule:finite_ne_induct)
-  case singleton thus ?case by(simp add:fold1_insert)
-next
-  case insert thus ?case by (simp add:fold1_insert assoc)
-qed
-
-lemma (in ACIf) fold1_Un2:
-assumes A: "finite A" "A \<noteq> {}"
-shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
-       fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
-using A
-proof(induct rule:finite_ne_induct)
-  case singleton thus ?case by(simp add:fold1_insert_idem)
-next
-  case insert thus ?case by (simp add:fold1_insert_idem assoc)
-qed
-
-lemma (in ACf) fold1_in:
-  assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
-  shows "fold1 f A \<in> A"
+       fold1 times (A Un B) = fold1 times A * fold1 times B"
+using A by (induct rule: finite_ne_induct)
+  (simp_all add: fold1_insert mult_assoc)
+
+lemma fold1_in:
+  assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
+  shows "fold1 times A \<in> A"
 using A
 proof (induct rule:finite_ne_induct)
   case singleton thus ?case by simp
@@ -2190,73 +2196,17 @@
   case insert thus ?case using elem by (force simp add:fold1_insert)
 qed
 
-lemma (in ACIfSL) below_fold1_iff:
+end
+
+lemma (in ab_semigroup_idem_mult) fold1_Un2:
 assumes A: "finite A" "A \<noteq> {}"
-shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)"
+shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
+       fold1 times (A Un B) = fold1 times A * fold1 times B"
 using A
-by(induct rule:finite_ne_induct) simp_all
-
-lemma (in ACIfSLlin) strict_below_fold1_iff:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<prec> fold1 f A = (\<forall>a\<in>A. x \<prec> a)"
-by(induct rule:finite_ne_induct) simp_all
-
-
-lemma (in ACIfSL) fold1_belowI:
-assumes A: "finite A" "A \<noteq> {}"
-shows "a \<in> A \<Longrightarrow> fold1 f A \<preceq> a"
-using A
-proof (induct rule:finite_ne_induct)
+proof(induct rule:finite_ne_induct)
   case singleton thus ?case by simp
 next
-  case (insert x F)
-  from insert(5) have "a = x \<or> a \<in> F" by simp
-  thus ?case
-  proof
-    assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
-  next
-    assume "a \<in> F"
-    hence bel: "fold1 f F \<preceq> a" by(rule insert)
-    have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
-      using insert by(simp add:below_def ACI)
-    also have "fold1 f F \<cdot> a = fold1 f F"
-      using bel  by(simp add:below_def ACI)
-    also have "x \<cdot> \<dots> = fold1 f (insert x F)"
-      using insert by(simp add:below_def ACI)
-    finally show ?thesis  by(simp add:below_def)
-  qed
-qed
-
-lemma (in ACIfSLlin) fold1_below_iff:
-assumes A: "finite A" "A \<noteq> {}"
-shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)"
-using A
-by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
-
-lemma (in ACIfSLlin) fold1_strict_below_iff:
-assumes A: "finite A" "A \<noteq> {}"
-shows "fold1 f A \<prec> x = (\<exists>a\<in>A. a \<prec> x)"
-using A
-by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
-
-lemma (in ACIfSLlin) fold1_antimono:
-assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
-shows "fold1 f B \<preceq> fold1 f A"
-proof(cases)
-  assume "A = B" thus ?thesis by simp
-next
-  assume "A \<noteq> B"
-  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
-  have "fold1 f B = fold1 f (A \<union> (B-A))" by(subst B)(rule refl)
-  also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
-  proof -
-    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
-    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
-    moreover have "(B-A) \<noteq> {}" using prems by blast
-    moreover have "A Int (B-A) = {}" using prems by blast
-    ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
-  qed
-  also have "\<dots> \<preceq> fold1 f A" by(simp add: above_f_conv)
-  finally show ?thesis .
+  case insert thus ?case by (simp add: mult_assoc)
 qed
 
 
@@ -2268,51 +2218,62 @@
   over (non-empty) sets by means of @{text fold1}.
 *}
 
-lemma (in lower_semilattice) ACf_inf: "ACf inf"
-  by (blast intro: ACf.intro inf_commute inf_assoc)
-
-lemma (in upper_semilattice) ACf_sup: "ACf sup"
-  by (blast intro: ACf.intro sup_commute sup_assoc)
-
-lemma (in lower_semilattice) ACIf_inf: "ACIf inf"
-apply(rule ACIf.intro)
-apply(rule ACf_inf)
-apply(rule ACIf_axioms.intro)
-apply(rule inf_idem)
-done
-
-lemma (in upper_semilattice) ACIf_sup: "ACIf sup"
-apply(rule ACIf.intro)
-apply(rule ACf_sup)
-apply(rule ACIf_axioms.intro)
-apply(rule sup_idem)
-done
-
-lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<le>) (op <) inf"
-apply(rule ACIfSL.intro)
-apply(rule ACIf.intro)
-apply(rule ACf_inf)
-apply(rule ACIf.axioms[OF ACIf_inf])
-apply(rule ACIfSL_axioms.intro)
-apply(rule iffI)
- apply(blast intro: antisym inf_le1 inf_le2 inf_greatest refl)
-apply(erule subst)
-apply(rule inf_le2)
-apply(rule less_le)
-done
-
-lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<le> x) (%x y. y < x) sup"
-apply(rule ACIfSL.intro)
-apply(rule ACIf.intro)
-apply(rule ACf_sup)
-apply(rule ACIf.axioms[OF ACIf_sup])
-apply(rule ACIfSL_axioms.intro)
-apply(rule iffI)
- apply(blast intro: antisym sup_ge1 sup_ge2 sup_least refl)
-apply(erule subst)
-apply(rule sup_ge2)
-apply(simp add: neq_commute less_le)
-done
+context lower_semilattice
+begin
+
+lemma ab_semigroup_idem_mult_inf:
+  "ab_semigroup_idem_mult inf"
+  apply unfold_locales
+  apply (rule inf_assoc)
+  apply (rule inf_commute)
+  apply (rule inf_idem)
+  done
+
+lemma below_fold1_iff:
+  assumes "finite A" "A \<noteq> {}"
+  shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
+proof -
+  invoke ab_semigroup_idem_mult [inf]
+    by (rule ab_semigroup_idem_mult_inf)
+  show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
+qed
+
+lemma fold1_belowI:
+  assumes "finite A" "A \<noteq> {}"
+    and "a \<in> A"
+  shows "fold1 inf A \<le> a"
+using assms proof (induct rule: finite_ne_induct)
+  case singleton thus ?case by simp
+next
+  invoke ab_semigroup_idem_mult [inf]
+    by (rule ab_semigroup_idem_mult_inf)
+  case (insert x F)
+  from insert(5) have "a = x \<or> a \<in> F" by simp
+  thus ?case
+  proof
+    assume "a = x" thus ?thesis using insert
+      by (simp add: mult_ac_idem)
+  next
+    assume "a \<in> F"
+    hence bel: "fold1 inf F \<le> a" by (rule insert)
+    have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
+      using insert by (simp add: mult_ac_idem)
+    also have "inf (fold1 inf F) a = fold1 inf F"
+      using bel by (auto intro: antisym)
+    also have "inf x \<dots> = fold1 inf (insert x F)"
+      using insert by (simp add: mult_ac_idem)
+    finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
+    moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
+    ultimately show ?thesis by simp
+  qed
+qed
+
+end
+
+lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
+  "ab_semigroup_idem_mult sup"
+  by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
+    (rule dual_lattice)
 
 context lattice
 begin
@@ -2333,19 +2294,20 @@
 prefer 2 apply blast
 apply(erule exE)
 apply(rule order_trans)
-apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
-apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
+apply(erule (2) fold1_belowI)
+apply(erule (2) lower_semilattice.fold1_belowI [OF dual_lattice])
 done
 
 lemma sup_Inf_absorb [simp]:
   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (sup a (\<Sqinter>\<^bsub>fin\<^esub>A)) = a"
 apply(subst sup_commute)
-apply(simp add: Inf_fin_def sup_absorb2 ACIfSL.fold1_belowI [OF ACIfSL_inf])
+apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
 done
 
 lemma inf_Sup_absorb [simp]:
   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (inf a (\<Squnion>\<^bsub>fin\<^esub>A)) = a"
-by(simp add: Sup_fin_def inf_absorb1 ACIfSL.fold1_belowI [OF ACIfSL_sup])
+by (simp add: Sup_fin_def inf_absorb1
+  lower_semilattice.fold1_belowI [OF dual_lattice])
 
 end
 
@@ -2353,11 +2315,17 @@
 begin
 
 lemma sup_Inf1_distrib:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
-apply(simp add: Inf_fin_def image_def
-  ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
-apply(rule arg_cong, blast)
-done
+  assumes "finite A"
+    and "A \<noteq> {}"
+  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
+proof -
+  invoke ab_semigroup_idem_mult [inf]
+    by (rule ab_semigroup_idem_mult_inf)
+  from assms show ?thesis
+    by (simp add: Inf_fin_def image_def
+      hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
+        (rule arg_cong, blast)
+qed
 
 lemma sup_Inf2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
@@ -2366,6 +2334,8 @@
   case singleton thus ?case
     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
 next
+  invoke ab_semigroup_idem_mult [inf]
+    by (rule ab_semigroup_idem_mult_inf)
   case (insert x A)
   have finB: "finite {sup x b |b. b \<in> B}"
     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
@@ -2377,26 +2347,29 @@
   qed
   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
-    using insert
- by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_fin_def])
+    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
   also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
   also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:sup_Inf1_distrib[OF B])
   also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
     using B insert
-    by (simp add: Inf_fin_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
+    by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
     by blast
   finally show ?case .
 qed
 
 lemma inf_Sup1_distrib:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
-apply (simp add: Sup_fin_def image_def
-  ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
-apply (rule arg_cong, blast)
-done
+  assumes "finite A" and "A \<noteq> {}"
+  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
+proof -
+  invoke ab_semigroup_idem_mult [sup]
+    by (rule ab_semigroup_idem_mult_sup)
+  from assms show ?thesis
+    by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
+      (rule arg_cong, blast)
+qed
 
 lemma inf_Sup2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
@@ -2415,15 +2388,17 @@
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
+  invoke ab_semigroup_idem_mult [sup]
+    by (rule ab_semigroup_idem_mult_sup)
   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
-    using insert by (simp add: ACIf.fold1_insert_idem_def [OF ACIf_sup Sup_fin_def])
+    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
   also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
   also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:inf_Sup1_distrib[OF B])
   also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
     using B insert
-    by (simp add: Sup_fin_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
+    by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
     by blast
   finally show ?case .
@@ -2439,14 +2414,26 @@
 *}
 
 lemma Inf_fin_Inf:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
-unfolding Inf_fin_def by (induct A set: finite)
-   (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
+proof -
+  invoke ab_semigroup_idem_mult [inf]
+    by (rule ab_semigroup_idem_mult_inf)
+  from assms show ?thesis
+  unfolding Inf_fin_def by (induct A set: finite)
+    (simp_all add: Inf_insert_simp)
+qed
 
 lemma Sup_fin_Sup:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = Sup A"
-unfolding Sup_fin_def by (induct A set: finite)
-   (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
+proof -
+  invoke ab_semigroup_idem_mult [sup]
+    by (rule ab_semigroup_idem_mult_sup)
+  from assms show ?thesis
+  unfolding Sup_fin_def by (induct A set: finite)
+    (simp_all add: Sup_insert_simp)
+qed
 
 end
 
@@ -2462,6 +2449,86 @@
 context linorder
 begin
 
+lemma ab_semigroup_idem_mult_min:
+  "ab_semigroup_idem_mult min"
+  by unfold_locales (auto simp add: min_def)
+
+lemma ab_semigroup_idem_mult_max:
+  "ab_semigroup_idem_mult max"
+  by unfold_locales (auto simp add: max_def)
+
+lemma min_lattice:
+  "lower_semilattice (op \<le>) (op <) min"
+  by unfold_locales (auto simp add: min_def)
+
+lemma max_lattice:
+  "lower_semilattice (op \<ge>) (op >) max"
+  by unfold_locales (auto simp add: max_def)
+
+lemma dual_max:
+  "ord.max (op \<ge>) = min"
+  by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
+
+lemma dual_min:
+  "ord.min (op \<ge>) = max"
+  by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
+
+lemma strict_below_fold1_iff:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms show ?thesis
+  by (induct rule: finite_ne_induct)
+    (simp_all add: fold1_insert)
+qed
+
+lemma fold1_below_iff:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms show ?thesis
+  by (induct rule: finite_ne_induct)
+    (simp_all add: fold1_insert min_le_iff_disj)
+qed
+
+lemma fold1_strict_below_iff:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms show ?thesis
+  by (induct rule: finite_ne_induct)
+    (simp_all add: fold1_insert min_less_iff_disj)
+qed
+
+lemma fold1_antimono:
+  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
+  shows "fold1 min B \<le> fold1 min A"
+proof cases
+  assume "A = B" thus ?thesis by simp
+next
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  assume "A \<noteq> B"
+  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
+  have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
+  also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
+  proof -
+    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
+    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
+    moreover have "(B-A) \<noteq> {}" using prems by blast
+    moreover have "A Int (B-A) = {}" using prems by blast
+    ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
+  qed
+  also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
+  finally show ?thesis .
+qed
+
 definition
   Min :: "'a set \<Rightarrow> 'a"
 where
@@ -2472,138 +2539,204 @@
 where
   "Max = fold1 max"
 
-end context linorder begin
-
-text {* recall: @{term min} and @{term max} behave like @{const inf} and @{const sup} *}
-
-lemma ACIf_min: "ACIf min"
-  by (rule lower_semilattice.ACIf_inf,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-
-lemma ACf_min: "ACf min"
-  by (rule lower_semilattice.ACf_inf,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-
-lemma ACIfSL_min: "ACIfSL (op \<le>) (op <) min"
-  by (rule lower_semilattice.ACIfSL_inf,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-
-lemma ACIfSLlin_min: "ACIfSLlin (op \<le>) (op <) min"
-  by (rule ACIfSLlin.intro,
-    rule lower_semilattice.ACIfSL_inf,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-    (unfold_locales, simp add: min_def)
-
-lemma ACIf_max: "ACIf max"
-  by (rule upper_semilattice.ACIf_sup,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-
-lemma ACf_max: "ACf max"
-  by (rule upper_semilattice.ACf_sup,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-
-lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
-  by (rule upper_semilattice.ACIfSL_sup,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-
-lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
-  by (rule ACIfSLlin.intro,
-    rule upper_semilattice.ACIfSL_sup,
-    rule lattice.axioms,
-    rule distrib_lattice.axioms,
-    rule distrib_lattice_min_max)
-    (unfold_locales, simp add: max_def)
-
 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
-lemmas Min_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_min Min_def]
-lemmas Max_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_max Max_def]
+
+lemma Min_insert [simp]:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Min (insert x A) = min x (Min A)"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
+qed
+
+lemma Max_insert [simp]:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Max (insert x A) = max x (Max A)"
+proof -
+  invoke ab_semigroup_idem_mult [max]
+    by (rule ab_semigroup_idem_mult_max)
+  from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
+qed
 
 lemma Min_in [simp]:
-  shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
-  using ACf.fold1_in [OF ACf_min]
-  by (fastsimp simp: Min_def min_def)
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Min A \<in> A"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
+qed
 
 lemma Max_in [simp]:
-  shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
-  using ACf.fold1_in [OF ACf_max]
-  by (fastsimp simp: Max_def max_def)
-
-lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
-  by (simp add: Min_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_min])
-
-lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
-  by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
-
-lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
-  by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
-
-lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
-  by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
-
-lemma Min_ge_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
-  by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min])
-
-lemma Max_le_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
-  by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max])
-
-lemma Min_gr_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
-  by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min])
-
-lemma Max_less_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
-  by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Max A \<in> A"
+proof -
+  invoke ab_semigroup_idem_mult [max]
+    by (rule ab_semigroup_idem_mult_max)
+  from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
+qed
+
+lemma Min_Un:
+  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
+  shows "Min (A \<union> B) = min (Min A) (Min B)"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms show ?thesis
+    by (simp add: Min_def fold1_Un2)
+qed
+
+lemma Max_Un:
+  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
+  shows "Max (A \<union> B) = max (Max A) (Max B)"
+proof -
+  invoke ab_semigroup_idem_mult [max]
+    by (rule ab_semigroup_idem_mult_max)
+  from assms show ?thesis
+    by (simp add: Max_def fold1_Un2)
+qed
+
+lemma hom_Min_commute:
+  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
+    and "finite N" and "N \<noteq> {}"
+  shows "h (Min N) = Min (h ` N)"
+proof -
+  invoke ab_semigroup_idem_mult [min]
+    by (rule ab_semigroup_idem_mult_min)
+  from assms show ?thesis
+    by (simp add: Min_def hom_fold1_commute)
+qed
+
+lemma hom_Max_commute:
+  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
+    and "finite N" and "N \<noteq> {}"
+  shows "h (Max N) = Max (h ` N)"
+proof -
+  invoke ab_semigroup_idem_mult [max]
+    by (rule ab_semigroup_idem_mult_max)
+  from assms show ?thesis
+    by (simp add: Max_def hom_fold1_commute [of h])
+qed
+
+lemma Min_le [simp]:
+  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
+  shows "Min A \<le> x"
+proof -
+  invoke lower_semilattice [_ _ min]
+    by (rule min_lattice)
+  from assms show ?thesis by (simp add: Min_def fold1_belowI)
+qed
+
+lemma Max_ge [simp]:
+  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
+  shows "x \<le> Max A"
+proof -
+  invoke lower_semilattice [_ _ max]
+    by (rule max_lattice)
+  from assms show ?thesis by (simp add: Max_def fold1_belowI)
+qed
+
+lemma Min_ge_iff [simp, noatp]:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
+proof -
+  invoke lower_semilattice [_ _ min]
+    by (rule min_lattice)
+  from assms show ?thesis by (simp add: Min_def below_fold1_iff)
+qed
+
+lemma Max_le_iff [simp, noatp]:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
+proof -
+  invoke lower_semilattice [_ _ max]
+    by (rule max_lattice)
+  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
+qed
+
+lemma Min_gr_iff [simp, noatp]:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
+proof -
+  invoke lower_semilattice [_ _ min]
+    by (rule min_lattice)
+  from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
+qed
+
+lemma Max_less_iff [simp, noatp]:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
+proof -
+  note Max = Max_def
+  invoke linorder ["op \<ge>" "op >"]
+    by (rule dual_linorder)
+  from assms show ?thesis
+    by (simp add: Max strict_below_fold1_iff [folded dual_max])
+qed
 
 lemma Min_le_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
-  by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
+proof -
+  invoke lower_semilattice [_ _ min]
+    by (rule min_lattice)
+  from assms show ?thesis
+    by (simp add: Min_def fold1_below_iff)
+qed
 
 lemma Max_ge_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
-  by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
+proof -
+  note Max = Max_def
+  invoke linorder ["op \<ge>" "op >"]
+    by (rule dual_linorder)
+  from assms show ?thesis
+    by (simp add: Max fold1_below_iff [folded dual_max])
+qed
 
 lemma Min_less_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
-  by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
+proof -
+  invoke lower_semilattice [_ _ min]
+    by (rule min_lattice)
+  from assms show ?thesis
+    by (simp add: Min_def fold1_strict_below_iff)
+qed
 
 lemma Max_gr_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
-  by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])
-
-lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
-  \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
-  by (simp add: Min_def ACIf.fold1_Un2 [OF ACIf_min])
-
-lemma Max_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
-  \<Longrightarrow> Max (A \<union> B) = max (Max A) (Max B)"
-  by (simp add: Max_def ACIf.fold1_Un2 [OF ACIf_max])
-
-lemma hom_Min_commute:
- "(\<And>x y. h (min x y) = min (h x) (h y))
-  \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h (Min N) = Min (h ` N)"
-  by (simp add: Min_def ACIf.hom_fold1_commute [OF ACIf_min])
-
-lemma hom_Max_commute:
- "(\<And>x y. h (max x y) = max (h x) (h y))
-  \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h (Max N) = Max (h ` N)"
-  by (simp add: Max_def ACIf.hom_fold1_commute [OF ACIf_max])
+  assumes "finite A" and "A \<noteq> {}"
+  shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
+proof -
+  note Max = Max_def
+  invoke linorder ["op \<ge>" "op >"]
+    by (rule dual_linorder)
+  from assms show ?thesis
+    by (simp add: Max fold1_strict_below_iff [folded dual_max])
+qed
+
+lemma Min_antimono:
+  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
+  shows "Min N \<le> Min M"
+proof -
+  invoke distrib_lattice ["op \<le>" "op <" min max]
+    by (rule distrib_lattice_min_max)
+  from assms show ?thesis by (simp add: Min_def fold1_antimono)
+qed
+
+lemma Max_mono:
+  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
+  shows "Max M \<le> Max N"
+proof -
+  note Max = Max_def
+  invoke linorder ["op \<ge>" "op >"]
+    by (rule dual_linorder)
+  from assms show ?thesis
+    by (simp add: Max fold1_antimono [folded dual_max])
+qed
 
 end
 
@@ -2638,161 +2771,4 @@
 
 end
 
-
-subsection {* Class @{text finite} and code generation *}
-
-lemma finite_code [code func]:
-  "finite {} \<longleftrightarrow> True"
-  "finite (insert a A) \<longleftrightarrow> finite A"
-  by auto
-
-lemma card_code [code func]:
-  "card {} = 0"
-  "card (insert a A) =
-    (if finite A then Suc (card (A - {a})) else card (insert a A))"
-  by (auto simp add: card_insert)
-
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
-class finite (attach UNIV) = type +
-  fixes itself :: "'a itself"
-  assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide const finite
-
-lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
-  by (rule finite_subset [OF subset_UNIV finite_UNIV])
-
-lemma univ_unit [noatp]:
-  "UNIV = {()}" by auto
-
-instantiation unit :: finite
-begin
-
-definition
-  "itself = TYPE(unit)"
-
-instance proof
-  have "finite {()}" by simp
-  also note univ_unit [symmetric]
-  finally show "finite (UNIV :: unit set)" .
-qed
-
 end
-
-lemmas [code func] = univ_unit
-
-lemma univ_bool [noatp]:
-  "UNIV = {False, True}" by auto
-
-instantiation bool :: finite
-begin
-
-definition
-  "itself = TYPE(bool)"
-
-instance proof
-  have "finite {False, True}" by simp
-  also note univ_bool [symmetric]
-  finally show "finite (UNIV :: bool set)" .
-qed
-
-end
-
-lemmas [code func] = univ_bool
-
-instantiation * :: (finite, finite) finite
-begin
-
-definition
-  "itself = TYPE('a \<times> 'b)"
-
-instance proof
-  show "finite (UNIV :: ('a \<times> 'b) set)"
-  proof (rule finite_Prod_UNIV)
-    show "finite (UNIV :: 'a set)" by (rule finite)
-    show "finite (UNIV :: 'b set)" by (rule finite)
-  qed
-qed
-
-end
-
-lemma univ_prod [noatp, code func]:
-  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
-  unfolding UNIV_Times_UNIV ..
-
-instantiation "+" :: (finite, finite) finite
-begin
-
-definition
-  "itself = TYPE('a + 'b)"
-
-instance proof
-  have a: "finite (UNIV :: 'a set)" by (rule finite)
-  have b: "finite (UNIV :: 'b set)" by (rule finite)
-  from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
-    by (rule finite_Plus)
-  thus "finite (UNIV :: ('a + 'b) set)" by simp
-qed
-
-end
-
-lemma univ_sum [noatp, code func]:
-  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
-  unfolding UNIV_Plus_UNIV ..
-
-instantiation set :: (finite) finite
-begin
-
-definition
-  "itself = TYPE('a set)"
-
-instance proof
-  have "finite (UNIV :: 'a set)" by (rule finite)
-  hence "finite (Pow (UNIV :: 'a set))"
-    by (rule finite_Pow_iff [THEN iffD2])
-  thus "finite (UNIV :: 'a set set)" by simp
-qed
-
-end
-
-lemma univ_set [noatp, code func]:
-  "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
-
-lemma inj_graph: "inj (%f. {(x, y). y = f x})"
-  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
-
-instantiation "fun" :: (finite, finite) finite
-begin
-
-definition
-  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
-
-instance proof
-  show "finite (UNIV :: ('a => 'b) set)"
-  proof (rule finite_imageD)
-    let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
-    show "finite (range ?graph)" by (rule finite)
-    show "inj ?graph" by (rule inj_graph)
-  qed
-qed
-
-end
-
-hide (open) const itself
-
-subsection {* Equality and order on functions *}
-
-instance "fun" :: (finite, eq) eq ..
-
-lemma eq_fun [code func]:
-  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>eq"
-  shows "f = g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x = g x)"
-  unfolding expand_fun_eq by auto
-
-lemma order_fun [code func]:
-  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>order"
-  shows "f \<le> g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x \<le> g x)"
-    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<in>UNIV. f x \<noteq> g x)"
-  by (auto simp add: expand_fun_eq le_fun_def less_fun_def order_less_le)
-
-end
diff -r 08d52e2dba07 -r c2e15e65165f src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -389,11 +389,11 @@
 have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
   by (metis linorder_linear abs_le_D1)
 have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
-  by (metis abs_mult_self AC_mult.f.commute)
+  by (metis abs_mult_self)
 have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
-  by (metis not_square_less_zero AC_mult.f.commute)
+  by (metis not_square_less_zero)
 have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
-  by (metis abs_mult AC_mult.f.commute)
+  by (metis abs_mult mult_commute)
 have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
   by (metis abs_mult 5)
 have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
@@ -403,7 +403,7 @@
 have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
   by (metis abs_idempotent abs_mult 8)
 have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
-  by (metis AC_mult.f.commute 7 11)
+  by (metis mult_commute 7 11)
 have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
   by (metis 8 7 12)
 have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
@@ -597,8 +597,10 @@
       (c * abs(f x)) * (ca * abs(g x))")
 ML{*ResAtp.problem_name := "BigO__bigo_mult_simpler"*}
 prefer 2 
-apply (metis  Finite_Set.AC_mult.f.assoc  Finite_Set.AC_mult.f.left_commute  OrderedGroup.abs_of_pos  OrderedGroup.mult_left_commute  Ring_and_Field.abs_mult  Ring_and_Field.mult_pos_pos)
-  apply(erule ssubst) 
+apply (metis mult_assoc mult_left_commute
+  OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
+  Ring_and_Field.abs_mult Ring_and_Field.mult_pos_pos)
+  apply (erule ssubst) 
   apply (subst abs_mult)
 (*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
   just been done*)
@@ -627,7 +629,7 @@
 have 9: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar>"
   by (metis OrderedGroup.abs_ge_zero 5)
 have 10: "\<And>X1\<Colon>'b\<Colon>ordered_idom. X1 * (1\<Colon>'b\<Colon>ordered_idom) = X1"
-  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
+  by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
 have 11: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
   by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
 have 12: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
@@ -901,10 +903,10 @@
   apply safe
   apply (rule_tac [2] ext) 
    prefer 2 
-   apply (metis AC_mult.f_e.left_ident mult_assoc right_inverse)
+   apply simp
   apply (simp add: mult_assoc [symmetric] abs_mult)
   (*couldn't get this proof without the step above; SLOW*)
-  apply (metis AC_mult.f.assoc abs_ge_zero mult_left_mono)
+  apply (metis mult_assoc abs_ge_zero mult_left_mono)
 done
 
 
diff -r 08d52e2dba07 -r c2e15e65165f src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -610,12 +610,12 @@
     "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
 
-lemma (in ACIf) fold_pd_PDUnit:
-  "fold_pd g f (PDUnit x) = g x"
+lemma (in ab_semigroup_idem_mult) fold_pd_PDUnit:
+  "fold_pd g (op *) (PDUnit x) = g x"
 unfolding fold_pd_def Rep_PDUnit by simp
 
-lemma (in ACIf) fold_pd_PDPlus:
-  "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
+lemma (in ab_semigroup_idem_mult) fold_pd_PDPlus:
+  "fold_pd g (op *) (PDPlus t u) = fold_pd g (op *) t * fold_pd g (op *) u"
 unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 
 text {* approx-pd *}
diff -r 08d52e2dba07 -r c2e15e65165f src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -443,10 +443,10 @@
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 
-lemma ACI_convex_bind: "ACIf (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_convex_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 apply unfold_locales
+apply (simp add: convex_plus_assoc)
 apply (simp add: convex_plus_commute)
-apply (simp add: convex_plus_assoc)
 apply (simp add: convex_plus_absorb eta_cfun)
 done
 
@@ -457,8 +457,8 @@
     (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
 unfolding convex_bind_basis_def
 apply -
-apply (rule ACIf.fold_pd_PDUnit [OF ACI_convex_bind])
-apply (rule ACIf.fold_pd_PDPlus [OF ACI_convex_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_convex_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_convex_bind])
 done
 
 lemma monofun_LAM:
diff -r 08d52e2dba07 -r c2e15e65165f src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -433,10 +433,10 @@
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 
-lemma ACI_lower_bind: "ACIf (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 apply unfold_locales
+apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
-apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_absorb eta_cfun)
 done
 
@@ -447,8 +447,8 @@
     (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
 unfolding lower_bind_basis_def
 apply -
-apply (rule ACIf.fold_pd_PDUnit [OF ACI_lower_bind])
-apply (rule ACIf.fold_pd_PDPlus [OF ACI_lower_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
 done
 
 lemma lower_bind_basis_mono:
diff -r 08d52e2dba07 -r c2e15e65165f src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -403,10 +403,10 @@
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 
-lemma ACI_upper_bind: "ACIf (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 apply unfold_locales
+apply (simp add: upper_plus_assoc)
 apply (simp add: upper_plus_commute)
-apply (simp add: upper_plus_assoc)
 apply (simp add: upper_plus_absorb eta_cfun)
 done
 
@@ -417,8 +417,8 @@
     (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
 unfolding upper_bind_basis_def
 apply -
-apply (rule ACIf.fold_pd_PDUnit [OF ACI_upper_bind])
-apply (rule ACIf.fold_pd_PDPlus [OF ACI_upper_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
 done
 
 lemma upper_bind_basis_mono: