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
authorhaftmann
Wed Feb 06 08:34:32 2008 +0100 (2008-02-06)
changeset 26041c2e15e65165f
parent 26040 08d52e2dba07
child 26042 e7a421d1f5c1
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
NEWS
src/HOL/Finite_Set.thy
src/HOL/MetisExamples/BigO.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/NEWS	Mon Feb 04 17:00:01 2008 +0100
     1.2 +++ b/NEWS	Wed Feb 06 08:34:32 2008 +0100
     1.3 @@ -35,6 +35,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Finite_Set: locales ACf, ACIf, ACIfSL and ACIfSLlin (whose purpose 
     1.8 +mainly if for various fold_set functionals) have been abandoned in favour of
     1.9 +the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult,
    1.10 +lower_semilattice (resp. uper_semilattice) and linorder.  INCOMPATIBILITY.
    1.11 +
    1.12  * Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
    1.13  form set-specific version is available as Inductive.lfp_ordinal_induct_set.
    1.14  
     2.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 04 17:00:01 2008 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 06 08:34:32 2008 +0100
     2.3 @@ -420,6 +420,157 @@
     2.4    done
     2.5  
     2.6  
     2.7 +subsection {* Class @{text finite} and code generation *}
     2.8 +
     2.9 +lemma finite_code [code func]:
    2.10 +  "finite {} \<longleftrightarrow> True"
    2.11 +  "finite (insert a A) \<longleftrightarrow> finite A"
    2.12 +  by auto
    2.13 +
    2.14 +setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
    2.15 +class finite (attach UNIV) = type +
    2.16 +  fixes itself :: "'a itself"
    2.17 +  assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
    2.18 +setup {* Sign.parent_path *}
    2.19 +hide const finite
    2.20 +
    2.21 +lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
    2.22 +  by (rule finite_subset [OF subset_UNIV finite_UNIV])
    2.23 +
    2.24 +lemma univ_unit [noatp]:
    2.25 +  "UNIV = {()}" by auto
    2.26 +
    2.27 +instantiation unit :: finite
    2.28 +begin
    2.29 +
    2.30 +definition
    2.31 +  "itself = TYPE(unit)"
    2.32 +
    2.33 +instance proof
    2.34 +  have "finite {()}" by simp
    2.35 +  also note univ_unit [symmetric]
    2.36 +  finally show "finite (UNIV :: unit set)" .
    2.37 +qed
    2.38 +
    2.39 +end
    2.40 +
    2.41 +lemmas [code func] = univ_unit
    2.42 +
    2.43 +lemma univ_bool [noatp]:
    2.44 +  "UNIV = {False, True}" by auto
    2.45 +
    2.46 +instantiation bool :: finite
    2.47 +begin
    2.48 +
    2.49 +definition
    2.50 +  "itself = TYPE(bool)"
    2.51 +
    2.52 +instance proof
    2.53 +  have "finite {False, True}" by simp
    2.54 +  also note univ_bool [symmetric]
    2.55 +  finally show "finite (UNIV :: bool set)" .
    2.56 +qed
    2.57 +
    2.58 +end
    2.59 +
    2.60 +lemmas [code func] = univ_bool
    2.61 +
    2.62 +instantiation * :: (finite, finite) finite
    2.63 +begin
    2.64 +
    2.65 +definition
    2.66 +  "itself = TYPE('a \<times> 'b)"
    2.67 +
    2.68 +instance proof
    2.69 +  show "finite (UNIV :: ('a \<times> 'b) set)"
    2.70 +  proof (rule finite_Prod_UNIV)
    2.71 +    show "finite (UNIV :: 'a set)" by (rule finite)
    2.72 +    show "finite (UNIV :: 'b set)" by (rule finite)
    2.73 +  qed
    2.74 +qed
    2.75 +
    2.76 +end
    2.77 +
    2.78 +lemma univ_prod [noatp, code func]:
    2.79 +  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
    2.80 +  unfolding UNIV_Times_UNIV ..
    2.81 +
    2.82 +instantiation "+" :: (finite, finite) finite
    2.83 +begin
    2.84 +
    2.85 +definition
    2.86 +  "itself = TYPE('a + 'b)"
    2.87 +
    2.88 +instance proof
    2.89 +  have a: "finite (UNIV :: 'a set)" by (rule finite)
    2.90 +  have b: "finite (UNIV :: 'b set)" by (rule finite)
    2.91 +  from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
    2.92 +    by (rule finite_Plus)
    2.93 +  thus "finite (UNIV :: ('a + 'b) set)" by simp
    2.94 +qed
    2.95 +
    2.96 +end
    2.97 +
    2.98 +lemma univ_sum [noatp, code func]:
    2.99 +  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
   2.100 +  unfolding UNIV_Plus_UNIV ..
   2.101 +
   2.102 +instantiation set :: (finite) finite
   2.103 +begin
   2.104 +
   2.105 +definition
   2.106 +  "itself = TYPE('a set)"
   2.107 +
   2.108 +instance proof
   2.109 +  have "finite (UNIV :: 'a set)" by (rule finite)
   2.110 +  hence "finite (Pow (UNIV :: 'a set))"
   2.111 +    by (rule finite_Pow_iff [THEN iffD2])
   2.112 +  thus "finite (UNIV :: 'a set set)" by simp
   2.113 +qed
   2.114 +
   2.115 +end
   2.116 +
   2.117 +lemma univ_set [noatp, code func]:
   2.118 +  "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
   2.119 +
   2.120 +lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   2.121 +  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   2.122 +
   2.123 +instantiation "fun" :: (finite, finite) finite
   2.124 +begin
   2.125 +
   2.126 +definition
   2.127 +  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
   2.128 +
   2.129 +instance proof
   2.130 +  show "finite (UNIV :: ('a => 'b) set)"
   2.131 +  proof (rule finite_imageD)
   2.132 +    let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
   2.133 +    show "finite (range ?graph)" by (rule finite)
   2.134 +    show "inj ?graph" by (rule inj_graph)
   2.135 +  qed
   2.136 +qed
   2.137 +
   2.138 +end
   2.139 +
   2.140 +hide (open) const itself
   2.141 +
   2.142 +subsection {* Equality and order on functions *}
   2.143 +
   2.144 +instance "fun" :: (finite, eq) eq ..
   2.145 +
   2.146 +lemma eq_fun [code func]:
   2.147 +  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>eq"
   2.148 +  shows "f = g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x = g x)"
   2.149 +  unfolding expand_fun_eq by auto
   2.150 +
   2.151 +lemma order_fun [code func]:
   2.152 +  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>order"
   2.153 +  shows "f \<le> g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x \<le> g x)"
   2.154 +    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<in>UNIV. f x \<noteq> g x)"
   2.155 +  by (auto simp add: expand_fun_eq le_fun_def less_fun_def order_less_le)
   2.156 +
   2.157 +
   2.158  subsection {* A fold functional for finite sets *}
   2.159  
   2.160  text {* The intended behaviour is
   2.161 @@ -463,56 +614,6 @@
   2.162    by (induct set: finite) auto
   2.163  
   2.164  
   2.165 -subsubsection {* Commutative monoids *}
   2.166 -
   2.167 -(*FIXME integrate with Orderings.thy/OrderedGroup.thy*)
   2.168 -locale ACf =
   2.169 -  fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   2.170 -  assumes commute: "x \<cdot> y = y \<cdot> x"
   2.171 -    and assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   2.172 -begin
   2.173 -
   2.174 -lemma left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   2.175 -proof -
   2.176 -  have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
   2.177 -  also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)
   2.178 -  also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)
   2.179 -  finally show ?thesis .
   2.180 -qed
   2.181 -
   2.182 -lemmas AC = assoc commute left_commute
   2.183 -
   2.184 -end
   2.185 -
   2.186 -locale ACe = ACf +
   2.187 -  fixes e :: 'a
   2.188 -  assumes ident [simp]: "x \<cdot> e = x"
   2.189 -begin
   2.190 -
   2.191 -lemma left_ident [simp]: "e \<cdot> x = x"
   2.192 -proof -
   2.193 -  have "x \<cdot> e = x" by (rule ident)
   2.194 -  thus ?thesis by (subst commute)
   2.195 -qed
   2.196 -
   2.197 -end
   2.198 -
   2.199 -locale ACIf = ACf +
   2.200 -  assumes idem: "x \<cdot> x = x"
   2.201 -begin
   2.202 -
   2.203 -lemma idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y"
   2.204 -proof -
   2.205 -  have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc)
   2.206 -  also have "\<dots> = x \<cdot> y" by(simp add:idem)
   2.207 -  finally show ?thesis .
   2.208 -qed
   2.209 -
   2.210 -lemmas ACI = AC idem idem2
   2.211 -
   2.212 -end
   2.213 -
   2.214 -
   2.215  subsubsection{*From @{term foldSet} to @{term fold}*}
   2.216  
   2.217  lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
   2.218 @@ -557,16 +658,19 @@
   2.219    qed
   2.220  qed
   2.221  
   2.222 -lemma (in ACf) foldSet_determ_aux:
   2.223 +context ab_semigroup_mult
   2.224 +begin
   2.225 +
   2.226 +lemma foldSet_determ_aux:
   2.227    "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   2.228 -                foldSet f g z A x; foldSet f g z A x' \<rbrakk>
   2.229 +                foldSet times g z A x; foldSet times g z A x' \<rbrakk>
   2.230     \<Longrightarrow> x' = x"
   2.231  proof (induct n rule: less_induct)
   2.232    case (less n)
   2.233      have IH: "!!m h A x x'. 
   2.234                 \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   2.235 -                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
   2.236 -    have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'"
   2.237 +                foldSet times g z A x; foldSet times g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
   2.238 +    have Afoldx: "foldSet times g z A x" and Afoldx': "foldSet times g z A x'"
   2.239       and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
   2.240      show ?case
   2.241      proof (rule foldSet.cases [OF Afoldx])
   2.242 @@ -574,16 +678,16 @@
   2.243        with Afoldx' show "x' = x" by blast
   2.244      next
   2.245        fix B b u
   2.246 -      assume AbB: "A = insert b B" and x: "x = g b \<cdot> u"
   2.247 -         and notinB: "b \<notin> B" and Bu: "foldSet f g z B u"
   2.248 +      assume AbB: "A = insert b B" and x: "x = g b * u"
   2.249 +         and notinB: "b \<notin> B" and Bu: "foldSet times g z B u"
   2.250        show "x'=x" 
   2.251        proof (rule foldSet.cases [OF Afoldx'])
   2.252          assume "A = {}" and "x' = z"
   2.253          with AbB show "x' = x" by blast
   2.254        next
   2.255  	fix C c v
   2.256 -	assume AcC: "A = insert c C" and x': "x' = g c \<cdot> v"
   2.257 -           and notinC: "c \<notin> C" and Cv: "foldSet f g z C v"
   2.258 +	assume AcC: "A = insert c C" and x': "x' = g c * v"
   2.259 +           and notinC: "c \<notin> C" and Cv: "foldSet times g z C v"
   2.260  	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   2.261          from insert_inj_onE [OF Beq notinB injh]
   2.262          obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   2.263 @@ -607,51 +711,52 @@
   2.264  	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   2.265  	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   2.266  	  with AbB have "finite ?D" by simp
   2.267 -	  then obtain d where Dfoldd: "foldSet f g z ?D d"
   2.268 +	  then obtain d where Dfoldd: "foldSet times g z ?D d"
   2.269  	    using finite_imp_foldSet by iprover
   2.270  	  moreover have cinB: "c \<in> B" using B by auto
   2.271 -	  ultimately have "foldSet f g z B (g c \<cdot> d)"
   2.272 +	  ultimately have "foldSet times g z B (g c * d)"
   2.273  	    by(rule Diff1_foldSet)
   2.274 -	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   2.275 -          moreover have "g b \<cdot> d = v"
   2.276 -	  proof (rule IH[OF lessC Ceq inj_onC Cv])
   2.277 -	    show "foldSet f g z C (g b \<cdot> d)" using C notinB Dfoldd
   2.278 +	  then have "g c * d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   2.279 +          then have "u = g c * d" ..
   2.280 +          moreover have "v = g b * d"
   2.281 +	  proof (rule sym, rule IH [OF lessC Ceq inj_onC Cv])
   2.282 +	    show "foldSet times g z C (g b * d)" using C notinB Dfoldd
   2.283  	      by fastsimp
   2.284  	  qed
   2.285 -	  ultimately show ?thesis using x x' by (auto simp: AC)
   2.286 +	  ultimately show ?thesis using x x'
   2.287 +	    by (simp add: mult_left_commute)
   2.288  	qed
   2.289        qed
   2.290      qed
   2.291    qed
   2.292  
   2.293 -
   2.294 -lemma (in ACf) foldSet_determ:
   2.295 -  "foldSet f g z A x ==> foldSet f g z A y ==> y = x"
   2.296 +lemma foldSet_determ:
   2.297 +  "foldSet times g z A x ==> foldSet times g z A y ==> y = x"
   2.298  apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   2.299  apply (blast intro: foldSet_determ_aux [rule_format])
   2.300  done
   2.301  
   2.302 -lemma (in ACf) fold_equality: "foldSet f g z A y ==> fold f g z A = y"
   2.303 +lemma fold_equality: "foldSet times g z A y ==> fold times g z A = y"
   2.304    by (unfold fold_def) (blast intro: foldSet_determ)
   2.305  
   2.306  text{* The base case for @{text fold}: *}
   2.307  
   2.308 -lemma fold_empty [simp]: "fold f g z {} = z"
   2.309 +lemma (in -) fold_empty [simp]: "fold f g z {} = z"
   2.310    by (unfold fold_def) blast
   2.311  
   2.312 -lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   2.313 -    (foldSet f g z (insert x A) v) =
   2.314 -    (EX y. foldSet f g z A y & v = f (g x) y)"
   2.315 +lemma fold_insert_aux: "x \<notin> A ==>
   2.316 +    (foldSet times g z (insert x A) v) =
   2.317 +    (EX y. foldSet times g z A y & v = g x * y)"
   2.318    apply auto
   2.319 -  apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   2.320 +  apply (rule_tac A1 = A and f1 = times in finite_imp_foldSet [THEN exE])
   2.321     apply (fastsimp dest: foldSet_imp_finite)
   2.322    apply (blast intro: foldSet_determ)
   2.323    done
   2.324  
   2.325  text{* The recursion equation for @{text fold}: *}
   2.326  
   2.327 -lemma (in ACf) fold_insert[simp]:
   2.328 -    "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
   2.329 +lemma fold_insert [simp]:
   2.330 +    "finite A ==> x \<notin> A ==> fold times g z (insert x A) = g x * fold times g z A"
   2.331    apply (unfold fold_def)
   2.332    apply (simp add: fold_insert_aux)
   2.333    apply (rule the_equality)
   2.334 @@ -659,23 +764,27 @@
   2.335      cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
   2.336    done
   2.337  
   2.338 -lemma (in ACf) fold_rec:
   2.339 +lemma fold_rec:
   2.340  assumes fin: "finite A" and a: "a:A"
   2.341 -shows "fold f g z A = f (g a) (fold f g z (A - {a}))"
   2.342 +shows "fold times g z A = g a * fold times g z (A - {a})"
   2.343  proof-
   2.344    have A: "A = insert a (A - {a})" using a by blast
   2.345 -  hence "fold f g z A = fold f g z (insert a (A - {a}))" by simp
   2.346 -  also have "\<dots> = f (g a) (fold f g z (A - {a}))"
   2.347 +  hence "fold times g z A = fold times g z (insert a (A - {a}))" by simp
   2.348 +  also have "\<dots> = g a * fold times g z (A - {a})"
   2.349      by(rule fold_insert) (simp add:fin)+
   2.350    finally show ?thesis .
   2.351  qed
   2.352  
   2.353 +end
   2.354  
   2.355  text{* A simplified version for idempotent functions: *}
   2.356  
   2.357 -lemma (in ACIf) fold_insert_idem:
   2.358 +context ab_semigroup_idem_mult
   2.359 +begin
   2.360 +
   2.361 +lemma fold_insert_idem:
   2.362  assumes finA: "finite A"
   2.363 -shows "fold f g z (insert a A) = g a \<cdot> fold f g z A"
   2.364 +shows "fold times g z (insert a A) = g a * fold times g z A"
   2.365  proof cases
   2.366    assume "a \<in> A"
   2.367    then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
   2.368 @@ -683,11 +792,12 @@
   2.369    show ?thesis
   2.370    proof -
   2.371      from finA A have finB: "finite B" by(blast intro: finite_subset)
   2.372 -    have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
   2.373 -    also have "\<dots> = (g a) \<cdot> (fold f g z B)"
   2.374 +    have "fold times g z (insert a A) = fold times g z (insert a B)" using A by simp
   2.375 +    also have "\<dots> = g a * fold times g z B"
   2.376        using finB disj by simp
   2.377 -    also have "\<dots> = g a \<cdot> fold f g z A"
   2.378 -      using A finB disj by(simp add:idem assoc[symmetric])
   2.379 +    also have "\<dots> = g a * fold times g z A"
   2.380 +      using A finB disj
   2.381 +	by (simp add: mult_idem mult_assoc [symmetric])
   2.382      finally show ?thesis .
   2.383    qed
   2.384  next
   2.385 @@ -695,81 +805,61 @@
   2.386    with finA show ?thesis by simp
   2.387  qed
   2.388  
   2.389 -lemma (in ACIf) foldI_conv_id:
   2.390 -  "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
   2.391 +lemma foldI_conv_id:
   2.392 +  "finite A \<Longrightarrow> fold times g z A = fold times id z (g ` A)"
   2.393  by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
   2.394  
   2.395 +end
   2.396 +
   2.397  subsubsection{*Lemmas about @{text fold}*}
   2.398  
   2.399 -lemma (in ACf) fold_commute:
   2.400 -  "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
   2.401 +context ab_semigroup_mult
   2.402 +begin
   2.403 +
   2.404 +lemma fold_commute:
   2.405 +  "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
   2.406    apply (induct set: finite)
   2.407     apply simp
   2.408 -  apply (simp add: left_commute [of x])
   2.409 +  apply (simp add: mult_left_commute [of x])
   2.410    done
   2.411  
   2.412 -lemma (in ACf) fold_nest_Un_Int:
   2.413 +lemma fold_nest_Un_Int:
   2.414    "finite A ==> finite B
   2.415 -    ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   2.416 +    ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
   2.417    apply (induct set: finite)
   2.418     apply simp
   2.419    apply (simp add: fold_commute Int_insert_left insert_absorb)
   2.420    done
   2.421  
   2.422 -lemma (in ACf) fold_nest_Un_disjoint:
   2.423 +lemma fold_nest_Un_disjoint:
   2.424    "finite A ==> finite B ==> A Int B = {}
   2.425 -    ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
   2.426 +    ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
   2.427    by (simp add: fold_nest_Un_Int)
   2.428  
   2.429 -lemma (in ACf) fold_reindex:
   2.430 +lemma fold_reindex:
   2.431  assumes fin: "finite A"
   2.432 -shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
   2.433 +shows "inj_on h A \<Longrightarrow> fold times g z (h ` A) = fold times (g \<circ> h) z A"
   2.434  using fin apply induct
   2.435   apply simp
   2.436  apply simp
   2.437  done
   2.438  
   2.439 -lemma (in ACe) fold_Un_Int:
   2.440 -  "finite A ==> finite B ==>
   2.441 -    fold f g e A \<cdot> fold f g e B =
   2.442 -    fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   2.443 -  apply (induct set: finite, simp)
   2.444 -  apply (simp add: AC insert_absorb Int_insert_left)
   2.445 -  done
   2.446 -
   2.447 -corollary (in ACe) fold_Un_disjoint:
   2.448 -  "finite A ==> finite B ==> A Int B = {} ==>
   2.449 -    fold f g e (A Un B) = fold f g e A \<cdot> fold f g e B"
   2.450 -  by (simp add: fold_Un_Int)
   2.451 -
   2.452 -lemma (in ACe) fold_UN_disjoint:
   2.453 -  "\<lbrakk> finite I; ALL i:I. finite (A i);
   2.454 -     ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   2.455 -   \<Longrightarrow> fold f g e (UNION I A) =
   2.456 -       fold f (%i. fold f g e (A i)) e I"
   2.457 -  apply (induct set: finite, simp, atomize)
   2.458 -  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.459 -   prefer 2 apply blast
   2.460 -  apply (subgoal_tac "A x Int UNION F A = {}")
   2.461 -   prefer 2 apply blast
   2.462 -  apply (simp add: fold_Un_disjoint)
   2.463 -  done
   2.464 -
   2.465 -text{*Fusion theorem, as described in
   2.466 -Graham Hutton's paper,
   2.467 -A Tutorial on the Universality and Expressiveness of Fold,
   2.468 -JFP 9:4 (355-372), 1999.*}
   2.469 -lemma (in ACf) fold_fusion:
   2.470 -      includes ACf g
   2.471 -      shows
   2.472 -	"finite A ==> 
   2.473 -	 (!!x y. h (g x y) = f x (h y)) ==>
   2.474 -         h (fold g j w A) = fold f j (h w) A"
   2.475 -  by (induct set: finite) simp_all
   2.476 -
   2.477 -lemma (in ACf) fold_cong:
   2.478 -  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   2.479 -  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
   2.480 +text{*
   2.481 +  Fusion theorem, as described in Graham Hutton's paper,
   2.482 +  A Tutorial on the Universality and Expressiveness of Fold,
   2.483 +  JFP 9:4 (355-372), 1999.
   2.484 +*}
   2.485 +
   2.486 +lemma fold_fusion:
   2.487 +  includes ab_semigroup_mult g
   2.488 +  assumes fin: "finite A"
   2.489 +    and hyp: "\<And>x y. h (g x y) = times x (h y)"
   2.490 +  shows "h (fold g j w A) = fold times j (h w) A"
   2.491 +  using fin hyp by (induct set: finite) simp_all
   2.492 +
   2.493 +lemma fold_cong:
   2.494 +  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
   2.495 +  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold times g z C = fold times h z C")
   2.496     apply simp
   2.497    apply (erule finite_induct, simp)
   2.498    apply (simp add: subset_insert_iff, clarify)
   2.499 @@ -783,9 +873,39 @@
   2.500    apply (simp add: Ball_def del: insert_Diff_single)
   2.501    done
   2.502  
   2.503 -lemma (in ACe) fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   2.504 -  fold f (%x. fold f (g x) e (B x)) e A =
   2.505 -  fold f (split g) e (SIGMA x:A. B x)"
   2.506 +end
   2.507 +
   2.508 +context comm_monoid_mult
   2.509 +begin
   2.510 +
   2.511 +lemma fold_Un_Int:
   2.512 +  "finite A ==> finite B ==>
   2.513 +    fold times g 1 A * fold times g 1 B =
   2.514 +    fold times g 1 (A Un B) * fold times g 1 (A Int B)"
   2.515 +  by (induct set: finite) 
   2.516 +    (auto simp add: mult_ac insert_absorb Int_insert_left)
   2.517 +
   2.518 +corollary fold_Un_disjoint:
   2.519 +  "finite A ==> finite B ==> A Int B = {} ==>
   2.520 +    fold times g 1 (A Un B) = fold times g 1 A * fold times g 1 B"
   2.521 +  by (simp add: fold_Un_Int)
   2.522 +
   2.523 +lemma fold_UN_disjoint:
   2.524 +  "\<lbrakk> finite I; ALL i:I. finite (A i);
   2.525 +     ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   2.526 +   \<Longrightarrow> fold times g 1 (UNION I A) =
   2.527 +       fold times (%i. fold times g 1 (A i)) 1 I"
   2.528 +  apply (induct set: finite, simp, atomize)
   2.529 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.530 +   prefer 2 apply blast
   2.531 +  apply (subgoal_tac "A x Int UNION F A = {}")
   2.532 +   prefer 2 apply blast
   2.533 +  apply (simp add: fold_Un_disjoint)
   2.534 +  done
   2.535 +
   2.536 +lemma fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   2.537 +  fold times (%x. fold times (g x) 1 (B x)) 1 A =
   2.538 +  fold times (split g) 1 (SIGMA x:A. B x)"
   2.539  apply (subst Sigma_def)
   2.540  apply (subst fold_UN_disjoint, assumption, simp)
   2.541   apply blast
   2.542 @@ -795,24 +915,18 @@
   2.543  apply simp
   2.544  done
   2.545  
   2.546 -lemma (in ACe) fold_distrib: "finite A \<Longrightarrow>
   2.547 -   fold f (%x. f (g x) (h x)) e A = f (fold f g e A) (fold f h e A)"
   2.548 -apply (erule finite_induct, simp)
   2.549 -apply (simp add:AC)
   2.550 -done
   2.551 -
   2.552 -
   2.553 -text{* Interpretation of locales -- see OrderedGroup.thy *}
   2.554 -
   2.555 -interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
   2.556 -  by unfold_locales (auto intro: add_assoc add_commute)
   2.557 -
   2.558 -interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
   2.559 -  by unfold_locales (auto intro: mult_assoc mult_commute)
   2.560 +lemma fold_distrib: "finite A \<Longrightarrow>
   2.561 +   fold times (%x. g x * h x) 1 A = fold times g 1 A *  fold times h 1 A"
   2.562 +  by (erule finite_induct) (simp_all add: mult_ac)
   2.563 +
   2.564 +end
   2.565  
   2.566  
   2.567  subsection {* Generalized summation over a set *}
   2.568  
   2.569 +interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
   2.570 +  by unfold_locales (auto intro: add_assoc add_commute)
   2.571 +
   2.572  constdefs
   2.573    setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   2.574    "setsum f A == if finite A then fold (op +) f 0 A else 0"
   2.575 @@ -873,7 +987,7 @@
   2.576  
   2.577  lemma setsum_reindex:
   2.578       "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   2.579 -by(auto simp add: setsum_def AC_add.fold_reindex dest!:finite_imageD)
   2.580 +by(auto simp add: setsum_def comm_monoid_add.fold_reindex dest!:finite_imageD)
   2.581  
   2.582  lemma setsum_reindex_id:
   2.583       "inj_on f B ==> setsum f B = setsum id (f ` B)"
   2.584 @@ -881,12 +995,12 @@
   2.585  
   2.586  lemma setsum_cong:
   2.587    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   2.588 -by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
   2.589 +by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_cong)
   2.590  
   2.591  lemma strong_setsum_cong[cong]:
   2.592    "A = B ==> (!!x. x:B =simp=> f x = g x)
   2.593     ==> setsum (%x. f x) A = setsum (%x. g x) B"
   2.594 -by(fastsimp simp: simp_implies_def setsum_def intro: AC_add.fold_cong)
   2.595 +by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_cong)
   2.596  
   2.597  lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
   2.598    by (rule setsum_cong[OF refl], auto);
   2.599 @@ -907,7 +1021,7 @@
   2.600  lemma setsum_Un_Int: "finite A ==> finite B ==>
   2.601    setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   2.602    -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   2.603 -by(simp add: setsum_def AC_add.fold_Un_Int [symmetric])
   2.604 +by(simp add: setsum_def comm_monoid_add.fold_Un_Int [symmetric])
   2.605  
   2.606  lemma setsum_Un_disjoint: "finite A ==> finite B
   2.607    ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   2.608 @@ -919,7 +1033,7 @@
   2.609      "finite I ==> (ALL i:I. finite (A i)) ==>
   2.610          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.611        setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   2.612 -by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong)
   2.613 +by(simp add: setsum_def comm_monoid_add.fold_UN_disjoint cong: setsum_cong)
   2.614  
   2.615  text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   2.616  directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   2.617 @@ -937,7 +1051,7 @@
   2.618    the rhs need not be, since SIGMA A B could still be finite.*)
   2.619  lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   2.620      (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   2.621 -by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
   2.622 +by(simp add:setsum_def comm_monoid_add.fold_Sigma split_def cong:setsum_cong)
   2.623  
   2.624  text{*Here we can eliminate the finiteness assumptions, by cases.*}
   2.625  lemma setsum_cartesian_product: 
   2.626 @@ -952,7 +1066,7 @@
   2.627  done
   2.628  
   2.629  lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   2.630 -by(simp add:setsum_def AC_add.fold_distrib)
   2.631 +by(simp add:setsum_def comm_monoid_add.fold_distrib)
   2.632  
   2.633  
   2.634  subsubsection {* Properties in more restricted classes of structures *}
   2.635 @@ -1331,18 +1445,18 @@
   2.636  
   2.637  lemma setprod_reindex:
   2.638       "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
   2.639 -by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
   2.640 +by(auto simp: setprod_def fold_reindex dest!:finite_imageD)
   2.641  
   2.642  lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
   2.643  by (auto simp add: setprod_reindex)
   2.644  
   2.645  lemma setprod_cong:
   2.646    "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
   2.647 -by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
   2.648 +by(fastsimp simp: setprod_def intro: fold_cong)
   2.649  
   2.650  lemma strong_setprod_cong:
   2.651    "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
   2.652 -by(fastsimp simp: simp_implies_def setprod_def intro: AC_mult.fold_cong)
   2.653 +by(fastsimp simp: simp_implies_def setprod_def intro: fold_cong)
   2.654  
   2.655  lemma setprod_reindex_cong: "inj_on f A ==>
   2.656      B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
   2.657 @@ -1362,7 +1476,7 @@
   2.658  
   2.659  lemma setprod_Un_Int: "finite A ==> finite B
   2.660      ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   2.661 -by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
   2.662 +by(simp add: setprod_def fold_Un_Int[symmetric])
   2.663  
   2.664  lemma setprod_Un_disjoint: "finite A ==> finite B
   2.665    ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   2.666 @@ -1372,7 +1486,7 @@
   2.667      "finite I ==> (ALL i:I. finite (A i)) ==>
   2.668          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   2.669        setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
   2.670 -by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
   2.671 +by(simp add: setprod_def fold_UN_disjoint cong: setprod_cong)
   2.672  
   2.673  lemma setprod_Union_disjoint:
   2.674    "[| (ALL A:C. finite A);
   2.675 @@ -1387,7 +1501,7 @@
   2.676  lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   2.677      (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
   2.678      (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   2.679 -by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
   2.680 +by(simp add:setprod_def fold_Sigma split_def cong:setprod_cong)
   2.681  
   2.682  text{*Here we can eliminate the finiteness assumptions, by cases.*}
   2.683  lemma setprod_cartesian_product: 
   2.684 @@ -1403,7 +1517,7 @@
   2.685  
   2.686  lemma setprod_timesf:
   2.687       "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
   2.688 -by(simp add:setprod_def AC_mult.fold_distrib)
   2.689 +by(simp add:setprod_def fold_distrib)
   2.690  
   2.691  
   2.692  subsubsection {* Properties in more restricted classes of structures *}
   2.693 @@ -1555,6 +1669,12 @@
   2.694  lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
   2.695  by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
   2.696  
   2.697 +lemma card_code [code func]:
   2.698 +  "card {} = 0"
   2.699 +  "card (insert a A) =
   2.700 +    (if finite A then Suc (card (A - {a})) else card (insert a A))"
   2.701 +  by (auto simp add: card_insert)
   2.702 +
   2.703  lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
   2.704  by (simp add: card_insert_if)
   2.705  
   2.706 @@ -1701,10 +1821,14 @@
   2.707  
   2.708  text{*The image of a finite set can be expressed using @{term fold}.*}
   2.709  lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
   2.710 -  apply (erule finite_induct, simp)
   2.711 -  apply (subst ACf.fold_insert) 
   2.712 -  apply (auto simp add: ACf_def) 
   2.713 -  done
   2.714 +proof (induct rule: finite_induct)
   2.715 +  case empty then show ?case by simp
   2.716 +next
   2.717 +  invoke ab_semigroup_mult ["op Un"]
   2.718 +    by unfold_locales auto
   2.719 +  case insert 
   2.720 +  then show ?case by simp
   2.721 +qed
   2.722  
   2.723  lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   2.724    apply (induct set: finite)
   2.725 @@ -1861,22 +1985,25 @@
   2.726  
   2.727  text{*First, some lemmas about @{term foldSet}.*}
   2.728  
   2.729 -lemma (in ACf) foldSet_insert_swap:
   2.730 -assumes fold: "foldSet f id b A y"
   2.731 -shows "b \<notin> A \<Longrightarrow> foldSet f id z (insert b A) (z \<cdot> y)"
   2.732 +context ab_semigroup_mult
   2.733 +begin
   2.734 +
   2.735 +lemma foldSet_insert_swap:
   2.736 +assumes fold: "foldSet times id b A y"
   2.737 +shows "b \<notin> A \<Longrightarrow> foldSet times id z (insert b A) (z * y)"
   2.738  using fold
   2.739  proof (induct rule: foldSet.induct)
   2.740 -  case emptyI thus ?case by (force simp add: fold_insert_aux commute)
   2.741 +  case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
   2.742  next
   2.743    case (insertI x A y)
   2.744 -    have "foldSet f (\<lambda>u. u) z (insert x (insert b A)) (x \<cdot> (z \<cdot> y))"
   2.745 +    have "foldSet times (\<lambda>u. u) z (insert x (insert b A)) (x * (z * y))"
   2.746        using insertI by force  --{*how does @{term id} get unfolded?*}
   2.747 -    thus ?case by (simp add: insert_commute AC)
   2.748 +    thus ?case by (simp add: insert_commute mult_ac)
   2.749  qed
   2.750  
   2.751 -lemma (in ACf) foldSet_permute_diff:
   2.752 -assumes fold: "foldSet f id b A x"
   2.753 -shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet f id a (insert b (A-{a})) x"
   2.754 +lemma foldSet_permute_diff:
   2.755 +assumes fold: "foldSet times id b A x"
   2.756 +shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet times id a (insert b (A-{a})) x"
   2.757  using fold
   2.758  proof (induct rule: foldSet.induct)
   2.759    case emptyI thus ?case by simp
   2.760 @@ -1890,7 +2017,7 @@
   2.761        by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
   2.762    next
   2.763      assume ainA: "a \<in> A"
   2.764 -    hence "foldSet f id a (insert x (insert b (A - {a}))) (x \<cdot> y)"
   2.765 +    hence "foldSet times id a (insert x (insert b (A - {a}))) (x * y)"
   2.766        using insertI by (force simp: id_def)
   2.767      moreover
   2.768      have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
   2.769 @@ -1899,15 +2026,15 @@
   2.770    qed
   2.771  qed
   2.772  
   2.773 -lemma (in ACf) fold1_eq_fold:
   2.774 -     "[|finite A; a \<notin> A|] ==> fold1 f (insert a A) = fold f id a A"
   2.775 +lemma fold1_eq_fold:
   2.776 +     "[|finite A; a \<notin> A|] ==> fold1 times (insert a A) = fold times id a A"
   2.777  apply (simp add: fold1_def fold_def) 
   2.778  apply (rule the_equality)
   2.779 -apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) 
   2.780 +apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ times id]) 
   2.781  apply (rule sym, clarify)
   2.782  apply (case_tac "Aa=A")
   2.783   apply (best intro: the_equality foldSet_determ)  
   2.784 -apply (subgoal_tac "foldSet f id a A x")
   2.785 +apply (subgoal_tac "foldSet times id a A x")
   2.786   apply (best intro: the_equality foldSet_determ)  
   2.787  apply (subgoal_tac "insert aa (Aa - {a}) = A") 
   2.788   prefer 2 apply (blast elim: equalityE) 
   2.789 @@ -1921,9 +2048,9 @@
   2.790  apply (drule_tac x="A-{x}" in spec, auto) 
   2.791  done
   2.792  
   2.793 -lemma (in ACf) fold1_insert:
   2.794 +lemma fold1_insert:
   2.795    assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
   2.796 -  shows "fold1 f (insert x A) = f x (fold1 f A)"
   2.797 +  shows "fold1 times (insert x A) = x * fold1 times A"
   2.798  proof -
   2.799    from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
   2.800      by (auto simp add: nonempty_iff)
   2.801 @@ -1931,9 +2058,14 @@
   2.802      by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
   2.803  qed
   2.804  
   2.805 -lemma (in ACIf) fold1_insert_idem [simp]:
   2.806 +end
   2.807 +
   2.808 +context ab_semigroup_idem_mult
   2.809 +begin
   2.810 +
   2.811 +lemma fold1_insert_idem [simp]:
   2.812    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   2.813 -  shows "fold1 f (insert x A) = f x (fold1 f A)"
   2.814 +  shows "fold1 times (insert x A) = x * fold1 times A"
   2.815  proof -
   2.816    from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
   2.817      by (auto simp add: nonempty_iff)
   2.818 @@ -1943,11 +2075,11 @@
   2.819      thus ?thesis 
   2.820      proof cases
   2.821        assume "A' = {}"
   2.822 -      with prems show ?thesis by (simp add: idem) 
   2.823 +      with prems show ?thesis by (simp add: mult_idem) 
   2.824      next
   2.825        assume "A' \<noteq> {}"
   2.826        with prems show ?thesis
   2.827 -	by (simp add: fold1_insert assoc [symmetric] idem) 
   2.828 +	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem) 
   2.829      qed
   2.830    next
   2.831      assume "a \<noteq> x"
   2.832 @@ -1956,53 +2088,58 @@
   2.833    qed
   2.834  qed
   2.835  
   2.836 -lemma (in ACIf) hom_fold1_commute:
   2.837 -assumes hom: "!!x y. h(f x y) = f (h x) (h y)"
   2.838 -and N: "finite N" "N \<noteq> {}" shows "h(fold1 f N) = fold1 f (h ` N)"
   2.839 +lemma hom_fold1_commute:
   2.840 +assumes hom: "!!x y. h (x * y) = h x * h y"
   2.841 +and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
   2.842  using N proof (induct rule: finite_ne_induct)
   2.843    case singleton thus ?case by simp
   2.844  next
   2.845    case (insert n N)
   2.846 -  then have "h(fold1 f (insert n N)) = h(f n (fold1 f N))" by simp
   2.847 -  also have "\<dots> = f (h n) (h(fold1 f N))" by(rule hom)
   2.848 -  also have "h(fold1 f N) = fold1 f (h ` N)" by(rule insert)
   2.849 -  also have "f (h n) \<dots> = fold1 f (insert (h n) (h ` N))"
   2.850 +  then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
   2.851 +  also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
   2.852 +  also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
   2.853 +  also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
   2.854      using insert by(simp)
   2.855    also have "insert (h n) (h ` N) = h ` insert n N" by simp
   2.856    finally show ?case .
   2.857  qed
   2.858  
   2.859 +end
   2.860 +
   2.861  
   2.862  text{* Now the recursion rules for definitions: *}
   2.863  
   2.864  lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
   2.865  by(simp add:fold1_singleton)
   2.866  
   2.867 -lemma (in ACf) fold1_insert_def:
   2.868 -  "\<lbrakk> g = fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x \<cdot> (g A)"
   2.869 -by(simp add:fold1_insert)
   2.870 -
   2.871 -lemma (in ACIf) fold1_insert_idem_def:
   2.872 -  "\<lbrakk> g = fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x \<cdot> (g A)"
   2.873 -by(simp add:fold1_insert_idem)
   2.874 +lemma (in ab_semigroup_mult) fold1_insert_def:
   2.875 +  "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
   2.876 +by (simp add:fold1_insert)
   2.877 +
   2.878 +lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
   2.879 +  "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
   2.880 +by simp
   2.881  
   2.882  subsubsection{* Determinacy for @{term fold1Set} *}
   2.883  
   2.884  text{*Not actually used!!*}
   2.885  
   2.886 -lemma (in ACf) foldSet_permute:
   2.887 -  "[|foldSet f id b (insert a A) x; a \<notin> A; b \<notin> A|]
   2.888 -   ==> foldSet f id a (insert b A) x"
   2.889 -apply (case_tac "a=b") 
   2.890 +context ab_semigroup_mult
   2.891 +begin
   2.892 +
   2.893 +lemma foldSet_permute:
   2.894 +  "[|foldSet times id b (insert a A) x; a \<notin> A; b \<notin> A|]
   2.895 +   ==> foldSet times id a (insert b A) x"
   2.896 +apply (cases "a=b") 
   2.897  apply (auto dest: foldSet_permute_diff) 
   2.898  done
   2.899  
   2.900 -lemma (in ACf) fold1Set_determ:
   2.901 -  "fold1Set f A x ==> fold1Set f A y ==> y = x"
   2.902 +lemma fold1Set_determ:
   2.903 +  "fold1Set times A x ==> fold1Set times A y ==> y = x"
   2.904  proof (clarify elim!: fold1Set.cases)
   2.905    fix A x B y a b
   2.906 -  assume Ax: "foldSet f id a A x"
   2.907 -  assume By: "foldSet f id b B y"
   2.908 +  assume Ax: "foldSet times id a A x"
   2.909 +  assume By: "foldSet times id b B y"
   2.910    assume anotA:  "a \<notin> A"
   2.911    assume bnotB:  "b \<notin> B"
   2.912    assume eq: "insert a A = insert b B"
   2.913 @@ -2018,171 +2155,40 @@
   2.914       and aB: "a \<in> B" and bA: "b \<in> A"
   2.915        using eq anotA bnotB diff by (blast elim!:equalityE)+
   2.916      with aB bnotB By
   2.917 -    have "foldSet f id a (insert b ?D) y" 
   2.918 +    have "foldSet times id a (insert b ?D) y" 
   2.919        by (auto intro: foldSet_permute simp add: insert_absorb)
   2.920      moreover
   2.921 -    have "foldSet f id a (insert b ?D) x"
   2.922 +    have "foldSet times id a (insert b ?D) x"
   2.923        by (simp add: A [symmetric] Ax) 
   2.924      ultimately show ?thesis by (blast intro: foldSet_determ) 
   2.925    qed
   2.926  qed
   2.927  
   2.928 -lemma (in ACf) fold1Set_equality: "fold1Set f A y ==> fold1 f A = y"
   2.929 +lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
   2.930    by (unfold fold1_def) (blast intro: fold1Set_determ)
   2.931  
   2.932 +end
   2.933 +
   2.934  declare
   2.935    empty_foldSetE [rule del]   foldSet.intros [rule del]
   2.936    empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
   2.937    -- {* No more proofs involve these relations. *}
   2.938  
   2.939 -
   2.940 -subsubsection{* Semi-Lattices *}
   2.941 -
   2.942 -locale ACIfSL = ord + ACIf +
   2.943 -  assumes below_def: "less_eq x y \<longleftrightarrow> x \<cdot> y = x"
   2.944 -  and strict_below_def: "less x y \<longleftrightarrow> less_eq x y \<and> x \<noteq> y"
   2.945 +subsubsection {* Lemmas about @{text fold1} *}
   2.946 +
   2.947 +context ab_semigroup_mult
   2.948  begin
   2.949  
   2.950 -notation
   2.951 -  less     ("(_/ \<prec> _)"  [51, 51] 50)
   2.952 -
   2.953 -notation (xsymbols)
   2.954 -  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
   2.955 -
   2.956 -notation (HTML output)
   2.957 -  less_eq  ("(_/ \<preceq> _)"  [51, 51] 50)
   2.958 -
   2.959 -lemma below_refl [simp]: "x \<preceq> x"
   2.960 -  by (simp add: below_def idem)
   2.961 -
   2.962 -lemma below_antisym:
   2.963 -  assumes xy: "x \<preceq> y" and yx: "y \<preceq> x"
   2.964 -  shows "x = y"
   2.965 -  using xy [unfolded below_def, symmetric]
   2.966 -    yx [unfolded below_def commute]
   2.967 -  by (rule trans)
   2.968 -
   2.969 -lemma below_trans:
   2.970 -  assumes xy: "x \<preceq> y" and yz: "y \<preceq> z"
   2.971 -  shows "x \<preceq> z"
   2.972 -proof -
   2.973 -  from xy have x_xy: "x \<cdot> y = x" by (simp add: below_def)
   2.974 -  from yz have y_yz: "y \<cdot> z = y" by (simp add: below_def)
   2.975 -  from y_yz have "x \<cdot> y \<cdot> z = x \<cdot> y" by (simp add: assoc)
   2.976 -  with x_xy have "x \<cdot> y \<cdot> z = x"  by simp
   2.977 -  moreover from x_xy have "x \<cdot> z = x \<cdot> y \<cdot> z" by simp
   2.978 -  ultimately have "x \<cdot> z = x" by simp
   2.979 -  then show ?thesis by (simp add: below_def)
   2.980 -qed
   2.981 -
   2.982 -lemma below_f_conv [simp,noatp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)"
   2.983 -proof
   2.984 -  assume "x \<preceq> y \<cdot> z"
   2.985 -  hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
   2.986 -  have "x \<cdot> y = x"
   2.987 -  proof -
   2.988 -    have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
   2.989 -    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
   2.990 -    also have "\<dots> = x" by(rule xyzx)
   2.991 -    finally show ?thesis .
   2.992 -  qed
   2.993 -  moreover have "x \<cdot> z = x"
   2.994 -  proof -
   2.995 -    have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
   2.996 -    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
   2.997 -    also have "\<dots> = x" by(rule xyzx)
   2.998 -    finally show ?thesis .
   2.999 -  qed
  2.1000 -  ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def)
  2.1001 -next
  2.1002 -  assume a: "x \<preceq> y \<and> x \<preceq> z"
  2.1003 -  hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
  2.1004 -  have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
  2.1005 -  also have "x \<cdot> y = x" using a by(simp_all add: below_def)
  2.1006 -  also have "x \<cdot> z = x" using a by(simp_all add: below_def)
  2.1007 -  finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def)
  2.1008 -qed
  2.1009 -
  2.1010 -end
  2.1011 -
  2.1012 -interpretation ACIfSL < order
  2.1013 -by unfold_locales
  2.1014 -  (simp add: strict_below_def, auto intro: below_refl below_trans below_antisym)
  2.1015 -
  2.1016 -locale ACIfSLlin = ACIfSL +
  2.1017 -  assumes lin: "x\<cdot>y \<in> {x,y}"
  2.1018 -begin
  2.1019 -
  2.1020 -lemma above_f_conv:
  2.1021 - "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)"
  2.1022 -proof
  2.1023 -  assume a: "x \<cdot> y \<preceq> z"
  2.1024 -  have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
  2.1025 -  thus "x \<preceq> z \<or> y \<preceq> z"
  2.1026 -  proof
  2.1027 -    assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
  2.1028 -  next
  2.1029 -    assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
  2.1030 -  qed
  2.1031 -next
  2.1032 -  assume "x \<preceq> z \<or> y \<preceq> z"
  2.1033 -  thus "x \<cdot> y \<preceq> z"
  2.1034 -  proof
  2.1035 -    assume a: "x \<preceq> z"
  2.1036 -    have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
  2.1037 -    also have "x \<cdot> z = x" using a by(simp add:below_def)
  2.1038 -    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
  2.1039 -  next
  2.1040 -    assume a: "y \<preceq> z"
  2.1041 -    have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
  2.1042 -    also have "y \<cdot> z = y" using a by(simp add:below_def)
  2.1043 -    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
  2.1044 -  qed
  2.1045 -qed
  2.1046 -
  2.1047 -lemma strict_below_f_conv[simp,noatp]: "x \<prec> y \<cdot> z = (x \<prec> y \<and> x \<prec> z)"
  2.1048 -apply(simp add: strict_below_def)
  2.1049 -using lin[of y z] by (auto simp:below_def ACI)
  2.1050 -
  2.1051 -lemma strict_above_f_conv:
  2.1052 -  "x \<cdot> y \<prec> z = (x \<prec> z \<or> y \<prec> z)"
  2.1053 -apply(simp add: strict_below_def above_f_conv)
  2.1054 -using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
  2.1055 -
  2.1056 -end
  2.1057 -
  2.1058 -interpretation ACIfSLlin < linorder
  2.1059 -  by unfold_locales
  2.1060 -    (insert lin [simplified insert_iff], simp add: below_def commute)
  2.1061 -
  2.1062 -
  2.1063 -subsubsection{* Lemmas about @{text fold1} *}
  2.1064 -
  2.1065 -lemma (in ACf) fold1_Un:
  2.1066 +lemma fold1_Un:
  2.1067  assumes A: "finite A" "A \<noteq> {}"
  2.1068  shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
  2.1069 -       fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2.1070 -using A
  2.1071 -proof(induct rule:finite_ne_induct)
  2.1072 -  case singleton thus ?case by(simp add:fold1_insert)
  2.1073 -next
  2.1074 -  case insert thus ?case by (simp add:fold1_insert assoc)
  2.1075 -qed
  2.1076 -
  2.1077 -lemma (in ACIf) fold1_Un2:
  2.1078 -assumes A: "finite A" "A \<noteq> {}"
  2.1079 -shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2.1080 -       fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
  2.1081 -using A
  2.1082 -proof(induct rule:finite_ne_induct)
  2.1083 -  case singleton thus ?case by(simp add:fold1_insert_idem)
  2.1084 -next
  2.1085 -  case insert thus ?case by (simp add:fold1_insert_idem assoc)
  2.1086 -qed
  2.1087 -
  2.1088 -lemma (in ACf) fold1_in:
  2.1089 -  assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
  2.1090 -  shows "fold1 f A \<in> A"
  2.1091 +       fold1 times (A Un B) = fold1 times A * fold1 times B"
  2.1092 +using A by (induct rule: finite_ne_induct)
  2.1093 +  (simp_all add: fold1_insert mult_assoc)
  2.1094 +
  2.1095 +lemma fold1_in:
  2.1096 +  assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
  2.1097 +  shows "fold1 times A \<in> A"
  2.1098  using A
  2.1099  proof (induct rule:finite_ne_induct)
  2.1100    case singleton thus ?case by simp
  2.1101 @@ -2190,73 +2196,17 @@
  2.1102    case insert thus ?case using elem by (force simp add:fold1_insert)
  2.1103  qed
  2.1104  
  2.1105 -lemma (in ACIfSL) below_fold1_iff:
  2.1106 +end
  2.1107 +
  2.1108 +lemma (in ab_semigroup_idem_mult) fold1_Un2:
  2.1109  assumes A: "finite A" "A \<noteq> {}"
  2.1110 -shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)"
  2.1111 +shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
  2.1112 +       fold1 times (A Un B) = fold1 times A * fold1 times B"
  2.1113  using A
  2.1114 -by(induct rule:finite_ne_induct) simp_all
  2.1115 -
  2.1116 -lemma (in ACIfSLlin) strict_below_fold1_iff:
  2.1117 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<prec> fold1 f A = (\<forall>a\<in>A. x \<prec> a)"
  2.1118 -by(induct rule:finite_ne_induct) simp_all
  2.1119 -
  2.1120 -
  2.1121 -lemma (in ACIfSL) fold1_belowI:
  2.1122 -assumes A: "finite A" "A \<noteq> {}"
  2.1123 -shows "a \<in> A \<Longrightarrow> fold1 f A \<preceq> a"
  2.1124 -using A
  2.1125 -proof (induct rule:finite_ne_induct)
  2.1126 +proof(induct rule:finite_ne_induct)
  2.1127    case singleton thus ?case by simp
  2.1128  next
  2.1129 -  case (insert x F)
  2.1130 -  from insert(5) have "a = x \<or> a \<in> F" by simp
  2.1131 -  thus ?case
  2.1132 -  proof
  2.1133 -    assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
  2.1134 -  next
  2.1135 -    assume "a \<in> F"
  2.1136 -    hence bel: "fold1 f F \<preceq> a" by(rule insert)
  2.1137 -    have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
  2.1138 -      using insert by(simp add:below_def ACI)
  2.1139 -    also have "fold1 f F \<cdot> a = fold1 f F"
  2.1140 -      using bel  by(simp add:below_def ACI)
  2.1141 -    also have "x \<cdot> \<dots> = fold1 f (insert x F)"
  2.1142 -      using insert by(simp add:below_def ACI)
  2.1143 -    finally show ?thesis  by(simp add:below_def)
  2.1144 -  qed
  2.1145 -qed
  2.1146 -
  2.1147 -lemma (in ACIfSLlin) fold1_below_iff:
  2.1148 -assumes A: "finite A" "A \<noteq> {}"
  2.1149 -shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)"
  2.1150 -using A
  2.1151 -by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
  2.1152 -
  2.1153 -lemma (in ACIfSLlin) fold1_strict_below_iff:
  2.1154 -assumes A: "finite A" "A \<noteq> {}"
  2.1155 -shows "fold1 f A \<prec> x = (\<exists>a\<in>A. a \<prec> x)"
  2.1156 -using A
  2.1157 -by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
  2.1158 -
  2.1159 -lemma (in ACIfSLlin) fold1_antimono:
  2.1160 -assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  2.1161 -shows "fold1 f B \<preceq> fold1 f A"
  2.1162 -proof(cases)
  2.1163 -  assume "A = B" thus ?thesis by simp
  2.1164 -next
  2.1165 -  assume "A \<noteq> B"
  2.1166 -  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  2.1167 -  have "fold1 f B = fold1 f (A \<union> (B-A))" by(subst B)(rule refl)
  2.1168 -  also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
  2.1169 -  proof -
  2.1170 -    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  2.1171 -    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  2.1172 -    moreover have "(B-A) \<noteq> {}" using prems by blast
  2.1173 -    moreover have "A Int (B-A) = {}" using prems by blast
  2.1174 -    ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
  2.1175 -  qed
  2.1176 -  also have "\<dots> \<preceq> fold1 f A" by(simp add: above_f_conv)
  2.1177 -  finally show ?thesis .
  2.1178 +  case insert thus ?case by (simp add: mult_assoc)
  2.1179  qed
  2.1180  
  2.1181  
  2.1182 @@ -2268,51 +2218,62 @@
  2.1183    over (non-empty) sets by means of @{text fold1}.
  2.1184  *}
  2.1185  
  2.1186 -lemma (in lower_semilattice) ACf_inf: "ACf inf"
  2.1187 -  by (blast intro: ACf.intro inf_commute inf_assoc)
  2.1188 -
  2.1189 -lemma (in upper_semilattice) ACf_sup: "ACf sup"
  2.1190 -  by (blast intro: ACf.intro sup_commute sup_assoc)
  2.1191 -
  2.1192 -lemma (in lower_semilattice) ACIf_inf: "ACIf inf"
  2.1193 -apply(rule ACIf.intro)
  2.1194 -apply(rule ACf_inf)
  2.1195 -apply(rule ACIf_axioms.intro)
  2.1196 -apply(rule inf_idem)
  2.1197 -done
  2.1198 -
  2.1199 -lemma (in upper_semilattice) ACIf_sup: "ACIf sup"
  2.1200 -apply(rule ACIf.intro)
  2.1201 -apply(rule ACf_sup)
  2.1202 -apply(rule ACIf_axioms.intro)
  2.1203 -apply(rule sup_idem)
  2.1204 -done
  2.1205 -
  2.1206 -lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<le>) (op <) inf"
  2.1207 -apply(rule ACIfSL.intro)
  2.1208 -apply(rule ACIf.intro)
  2.1209 -apply(rule ACf_inf)
  2.1210 -apply(rule ACIf.axioms[OF ACIf_inf])
  2.1211 -apply(rule ACIfSL_axioms.intro)
  2.1212 -apply(rule iffI)
  2.1213 - apply(blast intro: antisym inf_le1 inf_le2 inf_greatest refl)
  2.1214 -apply(erule subst)
  2.1215 -apply(rule inf_le2)
  2.1216 -apply(rule less_le)
  2.1217 -done
  2.1218 -
  2.1219 -lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<le> x) (%x y. y < x) sup"
  2.1220 -apply(rule ACIfSL.intro)
  2.1221 -apply(rule ACIf.intro)
  2.1222 -apply(rule ACf_sup)
  2.1223 -apply(rule ACIf.axioms[OF ACIf_sup])
  2.1224 -apply(rule ACIfSL_axioms.intro)
  2.1225 -apply(rule iffI)
  2.1226 - apply(blast intro: antisym sup_ge1 sup_ge2 sup_least refl)
  2.1227 -apply(erule subst)
  2.1228 -apply(rule sup_ge2)
  2.1229 -apply(simp add: neq_commute less_le)
  2.1230 -done
  2.1231 +context lower_semilattice
  2.1232 +begin
  2.1233 +
  2.1234 +lemma ab_semigroup_idem_mult_inf:
  2.1235 +  "ab_semigroup_idem_mult inf"
  2.1236 +  apply unfold_locales
  2.1237 +  apply (rule inf_assoc)
  2.1238 +  apply (rule inf_commute)
  2.1239 +  apply (rule inf_idem)
  2.1240 +  done
  2.1241 +
  2.1242 +lemma below_fold1_iff:
  2.1243 +  assumes "finite A" "A \<noteq> {}"
  2.1244 +  shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2.1245 +proof -
  2.1246 +  invoke ab_semigroup_idem_mult [inf]
  2.1247 +    by (rule ab_semigroup_idem_mult_inf)
  2.1248 +  show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  2.1249 +qed
  2.1250 +
  2.1251 +lemma fold1_belowI:
  2.1252 +  assumes "finite A" "A \<noteq> {}"
  2.1253 +    and "a \<in> A"
  2.1254 +  shows "fold1 inf A \<le> a"
  2.1255 +using assms proof (induct rule: finite_ne_induct)
  2.1256 +  case singleton thus ?case by simp
  2.1257 +next
  2.1258 +  invoke ab_semigroup_idem_mult [inf]
  2.1259 +    by (rule ab_semigroup_idem_mult_inf)
  2.1260 +  case (insert x F)
  2.1261 +  from insert(5) have "a = x \<or> a \<in> F" by simp
  2.1262 +  thus ?case
  2.1263 +  proof
  2.1264 +    assume "a = x" thus ?thesis using insert
  2.1265 +      by (simp add: mult_ac_idem)
  2.1266 +  next
  2.1267 +    assume "a \<in> F"
  2.1268 +    hence bel: "fold1 inf F \<le> a" by (rule insert)
  2.1269 +    have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  2.1270 +      using insert by (simp add: mult_ac_idem)
  2.1271 +    also have "inf (fold1 inf F) a = fold1 inf F"
  2.1272 +      using bel by (auto intro: antisym)
  2.1273 +    also have "inf x \<dots> = fold1 inf (insert x F)"
  2.1274 +      using insert by (simp add: mult_ac_idem)
  2.1275 +    finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  2.1276 +    moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  2.1277 +    ultimately show ?thesis by simp
  2.1278 +  qed
  2.1279 +qed
  2.1280 +
  2.1281 +end
  2.1282 +
  2.1283 +lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
  2.1284 +  "ab_semigroup_idem_mult sup"
  2.1285 +  by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
  2.1286 +    (rule dual_lattice)
  2.1287  
  2.1288  context lattice
  2.1289  begin
  2.1290 @@ -2333,19 +2294,20 @@
  2.1291  prefer 2 apply blast
  2.1292  apply(erule exE)
  2.1293  apply(rule order_trans)
  2.1294 -apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
  2.1295 -apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
  2.1296 +apply(erule (2) fold1_belowI)
  2.1297 +apply(erule (2) lower_semilattice.fold1_belowI [OF dual_lattice])
  2.1298  done
  2.1299  
  2.1300  lemma sup_Inf_absorb [simp]:
  2.1301    "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (sup a (\<Sqinter>\<^bsub>fin\<^esub>A)) = a"
  2.1302  apply(subst sup_commute)
  2.1303 -apply(simp add: Inf_fin_def sup_absorb2 ACIfSL.fold1_belowI [OF ACIfSL_inf])
  2.1304 +apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  2.1305  done
  2.1306  
  2.1307  lemma inf_Sup_absorb [simp]:
  2.1308    "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (inf a (\<Squnion>\<^bsub>fin\<^esub>A)) = a"
  2.1309 -by(simp add: Sup_fin_def inf_absorb1 ACIfSL.fold1_belowI [OF ACIfSL_sup])
  2.1310 +by (simp add: Sup_fin_def inf_absorb1
  2.1311 +  lower_semilattice.fold1_belowI [OF dual_lattice])
  2.1312  
  2.1313  end
  2.1314  
  2.1315 @@ -2353,11 +2315,17 @@
  2.1316  begin
  2.1317  
  2.1318  lemma sup_Inf1_distrib:
  2.1319 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  2.1320 -apply(simp add: Inf_fin_def image_def
  2.1321 -  ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
  2.1322 -apply(rule arg_cong, blast)
  2.1323 -done
  2.1324 +  assumes "finite A"
  2.1325 +    and "A \<noteq> {}"
  2.1326 +  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  2.1327 +proof -
  2.1328 +  invoke ab_semigroup_idem_mult [inf]
  2.1329 +    by (rule ab_semigroup_idem_mult_inf)
  2.1330 +  from assms show ?thesis
  2.1331 +    by (simp add: Inf_fin_def image_def
  2.1332 +      hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  2.1333 +        (rule arg_cong, blast)
  2.1334 +qed
  2.1335  
  2.1336  lemma sup_Inf2_distrib:
  2.1337    assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2.1338 @@ -2366,6 +2334,8 @@
  2.1339    case singleton thus ?case
  2.1340      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
  2.1341  next
  2.1342 +  invoke ab_semigroup_idem_mult [inf]
  2.1343 +    by (rule ab_semigroup_idem_mult_inf)
  2.1344    case (insert x A)
  2.1345    have finB: "finite {sup x b |b. b \<in> B}"
  2.1346      by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  2.1347 @@ -2377,26 +2347,29 @@
  2.1348    qed
  2.1349    have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2.1350    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)"
  2.1351 -    using insert
  2.1352 - by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_fin_def])
  2.1353 +    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
  2.1354    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)
  2.1355    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})"
  2.1356      using insert by(simp add:sup_Inf1_distrib[OF B])
  2.1357    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})"
  2.1358      (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  2.1359      using B insert
  2.1360 -    by (simp add: Inf_fin_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
  2.1361 +    by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  2.1362    also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2.1363      by blast
  2.1364    finally show ?case .
  2.1365  qed
  2.1366  
  2.1367  lemma inf_Sup1_distrib:
  2.1368 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  2.1369 -apply (simp add: Sup_fin_def image_def
  2.1370 -  ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
  2.1371 -apply (rule arg_cong, blast)
  2.1372 -done
  2.1373 +  assumes "finite A" and "A \<noteq> {}"
  2.1374 +  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  2.1375 +proof -
  2.1376 +  invoke ab_semigroup_idem_mult [sup]
  2.1377 +    by (rule ab_semigroup_idem_mult_sup)
  2.1378 +  from assms show ?thesis
  2.1379 +    by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  2.1380 +      (rule arg_cong, blast)
  2.1381 +qed
  2.1382  
  2.1383  lemma inf_Sup2_distrib:
  2.1384    assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2.1385 @@ -2415,15 +2388,17 @@
  2.1386      thus ?thesis by(simp add: insert(1) B(1))
  2.1387    qed
  2.1388    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2.1389 +  invoke ab_semigroup_idem_mult [sup]
  2.1390 +    by (rule ab_semigroup_idem_mult_sup)
  2.1391    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)"
  2.1392 -    using insert by (simp add: ACIf.fold1_insert_idem_def [OF ACIf_sup Sup_fin_def])
  2.1393 +    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
  2.1394    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)
  2.1395    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})"
  2.1396      using insert by(simp add:inf_Sup1_distrib[OF B])
  2.1397    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})"
  2.1398      (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  2.1399      using B insert
  2.1400 -    by (simp add: Sup_fin_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
  2.1401 +    by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  2.1402    also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2.1403      by blast
  2.1404    finally show ?case .
  2.1405 @@ -2439,14 +2414,26 @@
  2.1406  *}
  2.1407  
  2.1408  lemma Inf_fin_Inf:
  2.1409 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  2.1410 -unfolding Inf_fin_def by (induct A set: finite)
  2.1411 -   (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
  2.1412 +  assumes "finite A" and "A \<noteq> {}"
  2.1413 +  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  2.1414 +proof -
  2.1415 +  invoke ab_semigroup_idem_mult [inf]
  2.1416 +    by (rule ab_semigroup_idem_mult_inf)
  2.1417 +  from assms show ?thesis
  2.1418 +  unfolding Inf_fin_def by (induct A set: finite)
  2.1419 +    (simp_all add: Inf_insert_simp)
  2.1420 +qed
  2.1421  
  2.1422  lemma Sup_fin_Sup:
  2.1423 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  2.1424 -unfolding Sup_fin_def by (induct A set: finite)
  2.1425 -   (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
  2.1426 +  assumes "finite A" and "A \<noteq> {}"
  2.1427 +  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  2.1428 +proof -
  2.1429 +  invoke ab_semigroup_idem_mult [sup]
  2.1430 +    by (rule ab_semigroup_idem_mult_sup)
  2.1431 +  from assms show ?thesis
  2.1432 +  unfolding Sup_fin_def by (induct A set: finite)
  2.1433 +    (simp_all add: Sup_insert_simp)
  2.1434 +qed
  2.1435  
  2.1436  end
  2.1437  
  2.1438 @@ -2462,6 +2449,86 @@
  2.1439  context linorder
  2.1440  begin
  2.1441  
  2.1442 +lemma ab_semigroup_idem_mult_min:
  2.1443 +  "ab_semigroup_idem_mult min"
  2.1444 +  by unfold_locales (auto simp add: min_def)
  2.1445 +
  2.1446 +lemma ab_semigroup_idem_mult_max:
  2.1447 +  "ab_semigroup_idem_mult max"
  2.1448 +  by unfold_locales (auto simp add: max_def)
  2.1449 +
  2.1450 +lemma min_lattice:
  2.1451 +  "lower_semilattice (op \<le>) (op <) min"
  2.1452 +  by unfold_locales (auto simp add: min_def)
  2.1453 +
  2.1454 +lemma max_lattice:
  2.1455 +  "lower_semilattice (op \<ge>) (op >) max"
  2.1456 +  by unfold_locales (auto simp add: max_def)
  2.1457 +
  2.1458 +lemma dual_max:
  2.1459 +  "ord.max (op \<ge>) = min"
  2.1460 +  by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
  2.1461 +
  2.1462 +lemma dual_min:
  2.1463 +  "ord.min (op \<ge>) = max"
  2.1464 +  by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
  2.1465 +
  2.1466 +lemma strict_below_fold1_iff:
  2.1467 +  assumes "finite A" and "A \<noteq> {}"
  2.1468 +  shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2.1469 +proof -
  2.1470 +  invoke ab_semigroup_idem_mult [min]
  2.1471 +    by (rule ab_semigroup_idem_mult_min)
  2.1472 +  from assms show ?thesis
  2.1473 +  by (induct rule: finite_ne_induct)
  2.1474 +    (simp_all add: fold1_insert)
  2.1475 +qed
  2.1476 +
  2.1477 +lemma fold1_below_iff:
  2.1478 +  assumes "finite A" and "A \<noteq> {}"
  2.1479 +  shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2.1480 +proof -
  2.1481 +  invoke ab_semigroup_idem_mult [min]
  2.1482 +    by (rule ab_semigroup_idem_mult_min)
  2.1483 +  from assms show ?thesis
  2.1484 +  by (induct rule: finite_ne_induct)
  2.1485 +    (simp_all add: fold1_insert min_le_iff_disj)
  2.1486 +qed
  2.1487 +
  2.1488 +lemma fold1_strict_below_iff:
  2.1489 +  assumes "finite A" and "A \<noteq> {}"
  2.1490 +  shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2.1491 +proof -
  2.1492 +  invoke ab_semigroup_idem_mult [min]
  2.1493 +    by (rule ab_semigroup_idem_mult_min)
  2.1494 +  from assms show ?thesis
  2.1495 +  by (induct rule: finite_ne_induct)
  2.1496 +    (simp_all add: fold1_insert min_less_iff_disj)
  2.1497 +qed
  2.1498 +
  2.1499 +lemma fold1_antimono:
  2.1500 +  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  2.1501 +  shows "fold1 min B \<le> fold1 min A"
  2.1502 +proof cases
  2.1503 +  assume "A = B" thus ?thesis by simp
  2.1504 +next
  2.1505 +  invoke ab_semigroup_idem_mult [min]
  2.1506 +    by (rule ab_semigroup_idem_mult_min)
  2.1507 +  assume "A \<noteq> B"
  2.1508 +  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  2.1509 +  have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  2.1510 +  also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  2.1511 +  proof -
  2.1512 +    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  2.1513 +    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  2.1514 +    moreover have "(B-A) \<noteq> {}" using prems by blast
  2.1515 +    moreover have "A Int (B-A) = {}" using prems by blast
  2.1516 +    ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  2.1517 +  qed
  2.1518 +  also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  2.1519 +  finally show ?thesis .
  2.1520 +qed
  2.1521 +
  2.1522  definition
  2.1523    Min :: "'a set \<Rightarrow> 'a"
  2.1524  where
  2.1525 @@ -2472,138 +2539,204 @@
  2.1526  where
  2.1527    "Max = fold1 max"
  2.1528  
  2.1529 -end context linorder begin
  2.1530 -
  2.1531 -text {* recall: @{term min} and @{term max} behave like @{const inf} and @{const sup} *}
  2.1532 -
  2.1533 -lemma ACIf_min: "ACIf min"
  2.1534 -  by (rule lower_semilattice.ACIf_inf,
  2.1535 -    rule lattice.axioms,
  2.1536 -    rule distrib_lattice.axioms,
  2.1537 -    rule distrib_lattice_min_max)
  2.1538 -
  2.1539 -lemma ACf_min: "ACf min"
  2.1540 -  by (rule lower_semilattice.ACf_inf,
  2.1541 -    rule lattice.axioms,
  2.1542 -    rule distrib_lattice.axioms,
  2.1543 -    rule distrib_lattice_min_max)
  2.1544 -
  2.1545 -lemma ACIfSL_min: "ACIfSL (op \<le>) (op <) min"
  2.1546 -  by (rule lower_semilattice.ACIfSL_inf,
  2.1547 -    rule lattice.axioms,
  2.1548 -    rule distrib_lattice.axioms,
  2.1549 -    rule distrib_lattice_min_max)
  2.1550 -
  2.1551 -lemma ACIfSLlin_min: "ACIfSLlin (op \<le>) (op <) min"
  2.1552 -  by (rule ACIfSLlin.intro,
  2.1553 -    rule lower_semilattice.ACIfSL_inf,
  2.1554 -    rule lattice.axioms,
  2.1555 -    rule distrib_lattice.axioms,
  2.1556 -    rule distrib_lattice_min_max)
  2.1557 -    (unfold_locales, simp add: min_def)
  2.1558 -
  2.1559 -lemma ACIf_max: "ACIf max"
  2.1560 -  by (rule upper_semilattice.ACIf_sup,
  2.1561 -    rule lattice.axioms,
  2.1562 -    rule distrib_lattice.axioms,
  2.1563 -    rule distrib_lattice_min_max)
  2.1564 -
  2.1565 -lemma ACf_max: "ACf max"
  2.1566 -  by (rule upper_semilattice.ACf_sup,
  2.1567 -    rule lattice.axioms,
  2.1568 -    rule distrib_lattice.axioms,
  2.1569 -    rule distrib_lattice_min_max)
  2.1570 -
  2.1571 -lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
  2.1572 -  by (rule upper_semilattice.ACIfSL_sup,
  2.1573 -    rule lattice.axioms,
  2.1574 -    rule distrib_lattice.axioms,
  2.1575 -    rule distrib_lattice_min_max)
  2.1576 -
  2.1577 -lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
  2.1578 -  by (rule ACIfSLlin.intro,
  2.1579 -    rule upper_semilattice.ACIfSL_sup,
  2.1580 -    rule lattice.axioms,
  2.1581 -    rule distrib_lattice.axioms,
  2.1582 -    rule distrib_lattice_min_max)
  2.1583 -    (unfold_locales, simp add: max_def)
  2.1584 -
  2.1585  lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
  2.1586  lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
  2.1587 -lemmas Min_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_min Min_def]
  2.1588 -lemmas Max_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_max Max_def]
  2.1589 +
  2.1590 +lemma Min_insert [simp]:
  2.1591 +  assumes "finite A" and "A \<noteq> {}"
  2.1592 +  shows "Min (insert x A) = min x (Min A)"
  2.1593 +proof -
  2.1594 +  invoke ab_semigroup_idem_mult [min]
  2.1595 +    by (rule ab_semigroup_idem_mult_min)
  2.1596 +  from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
  2.1597 +qed
  2.1598 +
  2.1599 +lemma Max_insert [simp]:
  2.1600 +  assumes "finite A" and "A \<noteq> {}"
  2.1601 +  shows "Max (insert x A) = max x (Max A)"
  2.1602 +proof -
  2.1603 +  invoke ab_semigroup_idem_mult [max]
  2.1604 +    by (rule ab_semigroup_idem_mult_max)
  2.1605 +  from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
  2.1606 +qed
  2.1607  
  2.1608  lemma Min_in [simp]:
  2.1609 -  shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
  2.1610 -  using ACf.fold1_in [OF ACf_min]
  2.1611 -  by (fastsimp simp: Min_def min_def)
  2.1612 +  assumes "finite A" and "A \<noteq> {}"
  2.1613 +  shows "Min A \<in> A"
  2.1614 +proof -
  2.1615 +  invoke ab_semigroup_idem_mult [min]
  2.1616 +    by (rule ab_semigroup_idem_mult_min)
  2.1617 +  from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
  2.1618 +qed
  2.1619  
  2.1620  lemma Max_in [simp]:
  2.1621 -  shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
  2.1622 -  using ACf.fold1_in [OF ACf_max]
  2.1623 -  by (fastsimp simp: Max_def max_def)
  2.1624 -
  2.1625 -lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
  2.1626 -  by (simp add: Min_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_min])
  2.1627 -
  2.1628 -lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
  2.1629 -  by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
  2.1630 -
  2.1631 -lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
  2.1632 -  by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
  2.1633 -
  2.1634 -lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
  2.1635 -  by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
  2.1636 -
  2.1637 -lemma Min_ge_iff [simp,noatp]:
  2.1638 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2.1639 -  by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min])
  2.1640 -
  2.1641 -lemma Max_le_iff [simp,noatp]:
  2.1642 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2.1643 -  by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max])
  2.1644 -
  2.1645 -lemma Min_gr_iff [simp,noatp]:
  2.1646 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2.1647 -  by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min])
  2.1648 -
  2.1649 -lemma Max_less_iff [simp,noatp]:
  2.1650 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  2.1651 -  by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max])
  2.1652 +  assumes "finite A" and "A \<noteq> {}"
  2.1653 +  shows "Max A \<in> A"
  2.1654 +proof -
  2.1655 +  invoke ab_semigroup_idem_mult [max]
  2.1656 +    by (rule ab_semigroup_idem_mult_max)
  2.1657 +  from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
  2.1658 +qed
  2.1659 +
  2.1660 +lemma Min_Un:
  2.1661 +  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2.1662 +  shows "Min (A \<union> B) = min (Min A) (Min B)"
  2.1663 +proof -
  2.1664 +  invoke ab_semigroup_idem_mult [min]
  2.1665 +    by (rule ab_semigroup_idem_mult_min)
  2.1666 +  from assms show ?thesis
  2.1667 +    by (simp add: Min_def fold1_Un2)
  2.1668 +qed
  2.1669 +
  2.1670 +lemma Max_Un:
  2.1671 +  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  2.1672 +  shows "Max (A \<union> B) = max (Max A) (Max B)"
  2.1673 +proof -
  2.1674 +  invoke ab_semigroup_idem_mult [max]
  2.1675 +    by (rule ab_semigroup_idem_mult_max)
  2.1676 +  from assms show ?thesis
  2.1677 +    by (simp add: Max_def fold1_Un2)
  2.1678 +qed
  2.1679 +
  2.1680 +lemma hom_Min_commute:
  2.1681 +  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  2.1682 +    and "finite N" and "N \<noteq> {}"
  2.1683 +  shows "h (Min N) = Min (h ` N)"
  2.1684 +proof -
  2.1685 +  invoke ab_semigroup_idem_mult [min]
  2.1686 +    by (rule ab_semigroup_idem_mult_min)
  2.1687 +  from assms show ?thesis
  2.1688 +    by (simp add: Min_def hom_fold1_commute)
  2.1689 +qed
  2.1690 +
  2.1691 +lemma hom_Max_commute:
  2.1692 +  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  2.1693 +    and "finite N" and "N \<noteq> {}"
  2.1694 +  shows "h (Max N) = Max (h ` N)"
  2.1695 +proof -
  2.1696 +  invoke ab_semigroup_idem_mult [max]
  2.1697 +    by (rule ab_semigroup_idem_mult_max)
  2.1698 +  from assms show ?thesis
  2.1699 +    by (simp add: Max_def hom_fold1_commute [of h])
  2.1700 +qed
  2.1701 +
  2.1702 +lemma Min_le [simp]:
  2.1703 +  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
  2.1704 +  shows "Min A \<le> x"
  2.1705 +proof -
  2.1706 +  invoke lower_semilattice [_ _ min]
  2.1707 +    by (rule min_lattice)
  2.1708 +  from assms show ?thesis by (simp add: Min_def fold1_belowI)
  2.1709 +qed
  2.1710 +
  2.1711 +lemma Max_ge [simp]:
  2.1712 +  assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
  2.1713 +  shows "x \<le> Max A"
  2.1714 +proof -
  2.1715 +  invoke lower_semilattice [_ _ max]
  2.1716 +    by (rule max_lattice)
  2.1717 +  from assms show ?thesis by (simp add: Max_def fold1_belowI)
  2.1718 +qed
  2.1719 +
  2.1720 +lemma Min_ge_iff [simp, noatp]:
  2.1721 +  assumes "finite A" and "A \<noteq> {}"
  2.1722 +  shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2.1723 +proof -
  2.1724 +  invoke lower_semilattice [_ _ min]
  2.1725 +    by (rule min_lattice)
  2.1726 +  from assms show ?thesis by (simp add: Min_def below_fold1_iff)
  2.1727 +qed
  2.1728 +
  2.1729 +lemma Max_le_iff [simp, noatp]:
  2.1730 +  assumes "finite A" and "A \<noteq> {}"
  2.1731 +  shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2.1732 +proof -
  2.1733 +  invoke lower_semilattice [_ _ max]
  2.1734 +    by (rule max_lattice)
  2.1735 +  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
  2.1736 +qed
  2.1737 +
  2.1738 +lemma Min_gr_iff [simp, noatp]:
  2.1739 +  assumes "finite A" and "A \<noteq> {}"
  2.1740 +  shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2.1741 +proof -
  2.1742 +  invoke lower_semilattice [_ _ min]
  2.1743 +    by (rule min_lattice)
  2.1744 +  from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
  2.1745 +qed
  2.1746 +
  2.1747 +lemma Max_less_iff [simp, noatp]:
  2.1748 +  assumes "finite A" and "A \<noteq> {}"
  2.1749 +  shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  2.1750 +proof -
  2.1751 +  note Max = Max_def
  2.1752 +  invoke linorder ["op \<ge>" "op >"]
  2.1753 +    by (rule dual_linorder)
  2.1754 +  from assms show ?thesis
  2.1755 +    by (simp add: Max strict_below_fold1_iff [folded dual_max])
  2.1756 +qed
  2.1757  
  2.1758  lemma Min_le_iff [noatp]:
  2.1759 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2.1760 -  by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min])
  2.1761 +  assumes "finite A" and "A \<noteq> {}"
  2.1762 +  shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2.1763 +proof -
  2.1764 +  invoke lower_semilattice [_ _ min]
  2.1765 +    by (rule min_lattice)
  2.1766 +  from assms show ?thesis
  2.1767 +    by (simp add: Min_def fold1_below_iff)
  2.1768 +qed
  2.1769  
  2.1770  lemma Max_ge_iff [noatp]:
  2.1771 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  2.1772 -  by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max])
  2.1773 +  assumes "finite A" and "A \<noteq> {}"
  2.1774 +  shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  2.1775 +proof -
  2.1776 +  note Max = Max_def
  2.1777 +  invoke linorder ["op \<ge>" "op >"]
  2.1778 +    by (rule dual_linorder)
  2.1779 +  from assms show ?thesis
  2.1780 +    by (simp add: Max fold1_below_iff [folded dual_max])
  2.1781 +qed
  2.1782  
  2.1783  lemma Min_less_iff [noatp]:
  2.1784 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2.1785 -  by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min])
  2.1786 +  assumes "finite A" and "A \<noteq> {}"
  2.1787 +  shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2.1788 +proof -
  2.1789 +  invoke lower_semilattice [_ _ min]
  2.1790 +    by (rule min_lattice)
  2.1791 +  from assms show ?thesis
  2.1792 +    by (simp add: Min_def fold1_strict_below_iff)
  2.1793 +qed
  2.1794  
  2.1795  lemma Max_gr_iff [noatp]:
  2.1796 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  2.1797 -  by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])
  2.1798 -
  2.1799 -lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
  2.1800 -  \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
  2.1801 -  by (simp add: Min_def ACIf.fold1_Un2 [OF ACIf_min])
  2.1802 -
  2.1803 -lemma Max_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
  2.1804 -  \<Longrightarrow> Max (A \<union> B) = max (Max A) (Max B)"
  2.1805 -  by (simp add: Max_def ACIf.fold1_Un2 [OF ACIf_max])
  2.1806 -
  2.1807 -lemma hom_Min_commute:
  2.1808 - "(\<And>x y. h (min x y) = min (h x) (h y))
  2.1809 -  \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h (Min N) = Min (h ` N)"
  2.1810 -  by (simp add: Min_def ACIf.hom_fold1_commute [OF ACIf_min])
  2.1811 -
  2.1812 -lemma hom_Max_commute:
  2.1813 - "(\<And>x y. h (max x y) = max (h x) (h y))
  2.1814 -  \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h (Max N) = Max (h ` N)"
  2.1815 -  by (simp add: Max_def ACIf.hom_fold1_commute [OF ACIf_max])
  2.1816 +  assumes "finite A" and "A \<noteq> {}"
  2.1817 +  shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  2.1818 +proof -
  2.1819 +  note Max = Max_def
  2.1820 +  invoke linorder ["op \<ge>" "op >"]
  2.1821 +    by (rule dual_linorder)
  2.1822 +  from assms show ?thesis
  2.1823 +    by (simp add: Max fold1_strict_below_iff [folded dual_max])
  2.1824 +qed
  2.1825 +
  2.1826 +lemma Min_antimono:
  2.1827 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2.1828 +  shows "Min N \<le> Min M"
  2.1829 +proof -
  2.1830 +  invoke distrib_lattice ["op \<le>" "op <" min max]
  2.1831 +    by (rule distrib_lattice_min_max)
  2.1832 +  from assms show ?thesis by (simp add: Min_def fold1_antimono)
  2.1833 +qed
  2.1834 +
  2.1835 +lemma Max_mono:
  2.1836 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2.1837 +  shows "Max M \<le> Max N"
  2.1838 +proof -
  2.1839 +  note Max = Max_def
  2.1840 +  invoke linorder ["op \<ge>" "op >"]
  2.1841 +    by (rule dual_linorder)
  2.1842 +  from assms show ?thesis
  2.1843 +    by (simp add: Max fold1_antimono [folded dual_max])
  2.1844 +qed
  2.1845  
  2.1846  end
  2.1847  
  2.1848 @@ -2638,161 +2771,4 @@
  2.1849  
  2.1850  end
  2.1851  
  2.1852 -
  2.1853 -subsection {* Class @{text finite} and code generation *}
  2.1854 -
  2.1855 -lemma finite_code [code func]:
  2.1856 -  "finite {} \<longleftrightarrow> True"
  2.1857 -  "finite (insert a A) \<longleftrightarrow> finite A"
  2.1858 -  by auto
  2.1859 -
  2.1860 -lemma card_code [code func]:
  2.1861 -  "card {} = 0"
  2.1862 -  "card (insert a A) =
  2.1863 -    (if finite A then Suc (card (A - {a})) else card (insert a A))"
  2.1864 -  by (auto simp add: card_insert)
  2.1865 -
  2.1866 -setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
  2.1867 -class finite (attach UNIV) = type +
  2.1868 -  fixes itself :: "'a itself"
  2.1869 -  assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
  2.1870 -setup {* Sign.parent_path *}
  2.1871 -hide const finite
  2.1872 -
  2.1873 -lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
  2.1874 -  by (rule finite_subset [OF subset_UNIV finite_UNIV])
  2.1875 -
  2.1876 -lemma univ_unit [noatp]:
  2.1877 -  "UNIV = {()}" by auto
  2.1878 -
  2.1879 -instantiation unit :: finite
  2.1880 -begin
  2.1881 -
  2.1882 -definition
  2.1883 -  "itself = TYPE(unit)"
  2.1884 -
  2.1885 -instance proof
  2.1886 -  have "finite {()}" by simp
  2.1887 -  also note univ_unit [symmetric]
  2.1888 -  finally show "finite (UNIV :: unit set)" .
  2.1889 -qed
  2.1890 -
  2.1891  end
  2.1892 -
  2.1893 -lemmas [code func] = univ_unit
  2.1894 -
  2.1895 -lemma univ_bool [noatp]:
  2.1896 -  "UNIV = {False, True}" by auto
  2.1897 -
  2.1898 -instantiation bool :: finite
  2.1899 -begin
  2.1900 -
  2.1901 -definition
  2.1902 -  "itself = TYPE(bool)"
  2.1903 -
  2.1904 -instance proof
  2.1905 -  have "finite {False, True}" by simp
  2.1906 -  also note univ_bool [symmetric]
  2.1907 -  finally show "finite (UNIV :: bool set)" .
  2.1908 -qed
  2.1909 -
  2.1910 -end
  2.1911 -
  2.1912 -lemmas [code func] = univ_bool
  2.1913 -
  2.1914 -instantiation * :: (finite, finite) finite
  2.1915 -begin
  2.1916 -
  2.1917 -definition
  2.1918 -  "itself = TYPE('a \<times> 'b)"
  2.1919 -
  2.1920 -instance proof
  2.1921 -  show "finite (UNIV :: ('a \<times> 'b) set)"
  2.1922 -  proof (rule finite_Prod_UNIV)
  2.1923 -    show "finite (UNIV :: 'a set)" by (rule finite)
  2.1924 -    show "finite (UNIV :: 'b set)" by (rule finite)
  2.1925 -  qed
  2.1926 -qed
  2.1927 -
  2.1928 -end
  2.1929 -
  2.1930 -lemma univ_prod [noatp, code func]:
  2.1931 -  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
  2.1932 -  unfolding UNIV_Times_UNIV ..
  2.1933 -
  2.1934 -instantiation "+" :: (finite, finite) finite
  2.1935 -begin
  2.1936 -
  2.1937 -definition
  2.1938 -  "itself = TYPE('a + 'b)"
  2.1939 -
  2.1940 -instance proof
  2.1941 -  have a: "finite (UNIV :: 'a set)" by (rule finite)
  2.1942 -  have b: "finite (UNIV :: 'b set)" by (rule finite)
  2.1943 -  from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
  2.1944 -    by (rule finite_Plus)
  2.1945 -  thus "finite (UNIV :: ('a + 'b) set)" by simp
  2.1946 -qed
  2.1947 -
  2.1948 -end
  2.1949 -
  2.1950 -lemma univ_sum [noatp, code func]:
  2.1951 -  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
  2.1952 -  unfolding UNIV_Plus_UNIV ..
  2.1953 -
  2.1954 -instantiation set :: (finite) finite
  2.1955 -begin
  2.1956 -
  2.1957 -definition
  2.1958 -  "itself = TYPE('a set)"
  2.1959 -
  2.1960 -instance proof
  2.1961 -  have "finite (UNIV :: 'a set)" by (rule finite)
  2.1962 -  hence "finite (Pow (UNIV :: 'a set))"
  2.1963 -    by (rule finite_Pow_iff [THEN iffD2])
  2.1964 -  thus "finite (UNIV :: 'a set set)" by simp
  2.1965 -qed
  2.1966 -
  2.1967 -end
  2.1968 -
  2.1969 -lemma univ_set [noatp, code func]:
  2.1970 -  "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
  2.1971 -
  2.1972 -lemma inj_graph: "inj (%f. {(x, y). y = f x})"
  2.1973 -  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
  2.1974 -
  2.1975 -instantiation "fun" :: (finite, finite) finite
  2.1976 -begin
  2.1977 -
  2.1978 -definition
  2.1979 -  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
  2.1980 -
  2.1981 -instance proof
  2.1982 -  show "finite (UNIV :: ('a => 'b) set)"
  2.1983 -  proof (rule finite_imageD)
  2.1984 -    let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
  2.1985 -    show "finite (range ?graph)" by (rule finite)
  2.1986 -    show "inj ?graph" by (rule inj_graph)
  2.1987 -  qed
  2.1988 -qed
  2.1989 -
  2.1990 -end
  2.1991 -
  2.1992 -hide (open) const itself
  2.1993 -
  2.1994 -subsection {* Equality and order on functions *}
  2.1995 -
  2.1996 -instance "fun" :: (finite, eq) eq ..
  2.1997 -
  2.1998 -lemma eq_fun [code func]:
  2.1999 -  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>eq"
  2.2000 -  shows "f = g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x = g x)"
  2.2001 -  unfolding expand_fun_eq by auto
  2.2002 -
  2.2003 -lemma order_fun [code func]:
  2.2004 -  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>order"
  2.2005 -  shows "f \<le> g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x \<le> g x)"
  2.2006 -    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<in>UNIV. f x \<noteq> g x)"
  2.2007 -  by (auto simp add: expand_fun_eq le_fun_def less_fun_def order_less_le)
  2.2008 -
  2.2009 -end
     3.1 --- a/src/HOL/MetisExamples/BigO.thy	Mon Feb 04 17:00:01 2008 +0100
     3.2 +++ b/src/HOL/MetisExamples/BigO.thy	Wed Feb 06 08:34:32 2008 +0100
     3.3 @@ -389,11 +389,11 @@
     3.4  have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
     3.5    by (metis linorder_linear abs_le_D1)
     3.6  have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
     3.7 -  by (metis abs_mult_self AC_mult.f.commute)
     3.8 +  by (metis abs_mult_self)
     3.9  have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
    3.10 -  by (metis not_square_less_zero AC_mult.f.commute)
    3.11 +  by (metis not_square_less_zero)
    3.12  have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
    3.13 -  by (metis abs_mult AC_mult.f.commute)
    3.14 +  by (metis abs_mult mult_commute)
    3.15  have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
    3.16    by (metis abs_mult 5)
    3.17  have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
    3.18 @@ -403,7 +403,7 @@
    3.19  have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
    3.20    by (metis abs_idempotent abs_mult 8)
    3.21  have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
    3.22 -  by (metis AC_mult.f.commute 7 11)
    3.23 +  by (metis mult_commute 7 11)
    3.24  have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
    3.25    by (metis 8 7 12)
    3.26  have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
    3.27 @@ -597,8 +597,10 @@
    3.28        (c * abs(f x)) * (ca * abs(g x))")
    3.29  ML{*ResAtp.problem_name := "BigO__bigo_mult_simpler"*}
    3.30  prefer 2 
    3.31 -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)
    3.32 -  apply(erule ssubst) 
    3.33 +apply (metis mult_assoc mult_left_commute
    3.34 +  OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
    3.35 +  Ring_and_Field.abs_mult Ring_and_Field.mult_pos_pos)
    3.36 +  apply (erule ssubst) 
    3.37    apply (subst abs_mult)
    3.38  (*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
    3.39    just been done*)
    3.40 @@ -627,7 +629,7 @@
    3.41  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>"
    3.42    by (metis OrderedGroup.abs_ge_zero 5)
    3.43  have 10: "\<And>X1\<Colon>'b\<Colon>ordered_idom. X1 * (1\<Colon>'b\<Colon>ordered_idom) = X1"
    3.44 -  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
    3.45 +  by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
    3.46  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>"
    3.47    by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
    3.48  have 12: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
    3.49 @@ -901,10 +903,10 @@
    3.50    apply safe
    3.51    apply (rule_tac [2] ext) 
    3.52     prefer 2 
    3.53 -   apply (metis AC_mult.f_e.left_ident mult_assoc right_inverse)
    3.54 +   apply simp
    3.55    apply (simp add: mult_assoc [symmetric] abs_mult)
    3.56    (*couldn't get this proof without the step above; SLOW*)
    3.57 -  apply (metis AC_mult.f.assoc abs_ge_zero mult_left_mono)
    3.58 +  apply (metis mult_assoc abs_ge_zero mult_left_mono)
    3.59  done
    3.60  
    3.61  
     4.1 --- a/src/HOLCF/CompactBasis.thy	Mon Feb 04 17:00:01 2008 +0100
     4.2 +++ b/src/HOLCF/CompactBasis.thy	Wed Feb 06 08:34:32 2008 +0100
     4.3 @@ -610,12 +610,12 @@
     4.4      "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
     4.5    where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
     4.6  
     4.7 -lemma (in ACIf) fold_pd_PDUnit:
     4.8 -  "fold_pd g f (PDUnit x) = g x"
     4.9 +lemma (in ab_semigroup_idem_mult) fold_pd_PDUnit:
    4.10 +  "fold_pd g (op *) (PDUnit x) = g x"
    4.11  unfolding fold_pd_def Rep_PDUnit by simp
    4.12  
    4.13 -lemma (in ACIf) fold_pd_PDPlus:
    4.14 -  "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
    4.15 +lemma (in ab_semigroup_idem_mult) fold_pd_PDPlus:
    4.16 +  "fold_pd g (op *) (PDPlus t u) = fold_pd g (op *) t * fold_pd g (op *) u"
    4.17  unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
    4.18  
    4.19  text {* approx-pd *}
     5.1 --- a/src/HOLCF/ConvexPD.thy	Mon Feb 04 17:00:01 2008 +0100
     5.2 +++ b/src/HOLCF/ConvexPD.thy	Wed Feb 06 08:34:32 2008 +0100
     5.3 @@ -443,10 +443,10 @@
     5.4      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     5.5      (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     5.6  
     5.7 -lemma ACI_convex_bind: "ACIf (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     5.8 +lemma ACI_convex_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     5.9  apply unfold_locales
    5.10 +apply (simp add: convex_plus_assoc)
    5.11  apply (simp add: convex_plus_commute)
    5.12 -apply (simp add: convex_plus_assoc)
    5.13  apply (simp add: convex_plus_absorb eta_cfun)
    5.14  done
    5.15  
    5.16 @@ -457,8 +457,8 @@
    5.17      (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
    5.18  unfolding convex_bind_basis_def
    5.19  apply -
    5.20 -apply (rule ACIf.fold_pd_PDUnit [OF ACI_convex_bind])
    5.21 -apply (rule ACIf.fold_pd_PDPlus [OF ACI_convex_bind])
    5.22 +apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_convex_bind])
    5.23 +apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_convex_bind])
    5.24  done
    5.25  
    5.26  lemma monofun_LAM:
     6.1 --- a/src/HOLCF/LowerPD.thy	Mon Feb 04 17:00:01 2008 +0100
     6.2 +++ b/src/HOLCF/LowerPD.thy	Wed Feb 06 08:34:32 2008 +0100
     6.3 @@ -433,10 +433,10 @@
     6.4      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     6.5      (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     6.6  
     6.7 -lemma ACI_lower_bind: "ACIf (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     6.8 +lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     6.9  apply unfold_locales
    6.10 +apply (simp add: lower_plus_assoc)
    6.11  apply (simp add: lower_plus_commute)
    6.12 -apply (simp add: lower_plus_assoc)
    6.13  apply (simp add: lower_plus_absorb eta_cfun)
    6.14  done
    6.15  
    6.16 @@ -447,8 +447,8 @@
    6.17      (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
    6.18  unfolding lower_bind_basis_def
    6.19  apply -
    6.20 -apply (rule ACIf.fold_pd_PDUnit [OF ACI_lower_bind])
    6.21 -apply (rule ACIf.fold_pd_PDPlus [OF ACI_lower_bind])
    6.22 +apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
    6.23 +apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
    6.24  done
    6.25  
    6.26  lemma lower_bind_basis_mono:
     7.1 --- a/src/HOLCF/UpperPD.thy	Mon Feb 04 17:00:01 2008 +0100
     7.2 +++ b/src/HOLCF/UpperPD.thy	Wed Feb 06 08:34:32 2008 +0100
     7.3 @@ -403,10 +403,10 @@
     7.4      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     7.5      (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     7.6  
     7.7 -lemma ACI_upper_bind: "ACIf (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     7.8 +lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     7.9  apply unfold_locales
    7.10 +apply (simp add: upper_plus_assoc)
    7.11  apply (simp add: upper_plus_commute)
    7.12 -apply (simp add: upper_plus_assoc)
    7.13  apply (simp add: upper_plus_absorb eta_cfun)
    7.14  done
    7.15  
    7.16 @@ -417,8 +417,8 @@
    7.17      (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
    7.18  unfolding upper_bind_basis_def
    7.19  apply -
    7.20 -apply (rule ACIf.fold_pd_PDUnit [OF ACI_upper_bind])
    7.21 -apply (rule ACIf.fold_pd_PDPlus [OF ACI_upper_bind])
    7.22 +apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
    7.23 +apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
    7.24  done
    7.25  
    7.26  lemma upper_bind_basis_mono: