# HG changeset patch
# User ballarin
# Date 1217341189 -7200
# Node ID ed7a2e0fab59ec4ae4d2c4608f58b24c86b82b80
# Parent  ef4b26efa8b6dfbd13a37bf8f09622b983159788
New theory on divisibility.

diff -r ef4b26efa8b6 -r ed7a2e0fab59 src/HOL/Algebra/Congruence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Congruence.thy	Tue Jul 29 16:19:49 2008 +0200
@@ -0,0 +1,407 @@
+(*
+  Title:  Algebra/Congruence.thy
+  Id:     $Id$
+  Author: Clemens Ballarin, started 3 January 2008
+  Copyright: Clemens Ballarin
+*)
+
+theory Congruence imports Main begin
+
+section {* Objects *}
+
+text {* Structure with a carrier set. *}
+
+record 'a partial_object =
+  carrier :: "'a set"
+
+text {* Dito with equivalence relation *}
+
+record 'a eq_object = "'a partial_object" +
+  eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
+
+constdefs (structure S)
+  elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
+  "x .\<in> A \<equiv> (\<exists>y \<in> A. x .= y)"
+
+  set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
+  "A {.=} B == ((\<forall>x \<in> A. x .\<in> B) \<and> (\<forall>x \<in> B. x .\<in> A))"
+
+  eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
+  "class_of x == {y \<in> carrier S. x .= y}"
+
+  eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
+  "closure_of A == {y \<in> carrier S. y .\<in> A}"
+
+  eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
+  "is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
+
+syntax
+  not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
+  not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
+  set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+
+translations
+  "x .\<noteq>\<index> y" == "~(x .=\<index> y)"
+  "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
+  "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
+
+
+section {* Equivalence Relations *}
+
+locale equivalence =
+  fixes S (structure)
+  assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
+    and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
+    and trans [trans]: "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
+
+lemma elemI:
+  fixes R (structure)
+  assumes "a' \<in> A" and "a .= a'"
+  shows "a .\<in> A"
+unfolding elem_def
+using assms
+by fast
+
+lemma (in equivalence) elem_exact:
+  assumes "a \<in> carrier S" and "a \<in> A"
+  shows "a .\<in> A"
+using assms
+by (fast intro: elemI)
+
+lemma elemE:
+  fixes S (structure)
+  assumes "a .\<in> A"
+    and "\<And>a'. \<lbrakk>a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using assms
+unfolding elem_def
+by fast
+
+lemma (in equivalence) elem_cong_l [trans]:
+  assumes cong: "a' .= a"
+    and a: "a .\<in> A"
+    and carr: "a \<in> carrier S"  "a' \<in> carrier S"
+    and Acarr: "A \<subseteq> carrier S"
+  shows "a' .\<in> A"
+using a
+apply (elim elemE, intro elemI)
+proof assumption
+  fix b
+  assume bA: "b \<in> A"
+  note [simp] = carr bA[THEN subsetD[OF Acarr]]
+  note cong
+  also assume "a .= b"
+  finally show "a' .= b" by simp
+qed
+
+lemma (in equivalence) elem_subsetD:
+  assumes "A \<subseteq> B"
+    and aA: "a .\<in> A"
+  shows "a .\<in> B"
+using assms
+by (fast intro: elemI elim: elemE dest: subsetD)
+
+lemma (in equivalence) mem_imp_elem [simp, intro]:
+  "[| x \<in> A; x \<in> carrier S |] ==> x .\<in> A"
+  unfolding elem_def by blast
+
+lemma set_eqI:
+  fixes R (structure)
+  assumes ltr: "\<And>a. a \<in> A \<Longrightarrow> a .\<in> B"
+    and rtl: "\<And>b. b \<in> B \<Longrightarrow> b .\<in> A"
+  shows "A {.=} B"
+unfolding set_eq_def
+by (fast intro: ltr rtl)
+
+lemma set_eqI2:
+  fixes R (structure)
+  assumes ltr: "\<And>a b. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a .= b"
+    and rtl: "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. b .= a"
+  shows "A {.=} B"
+  by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+
+
+lemma set_eqD1:
+  fixes R (structure)
+  assumes AA': "A {.=} A'"
+    and "a \<in> A"
+  shows "\<exists>a'\<in>A'. a .= a'"
+using assms
+unfolding set_eq_def elem_def
+by fast
+
+lemma set_eqD2:
+  fixes R (structure)
+  assumes AA': "A {.=} A'"
+    and "a' \<in> A'"
+  shows "\<exists>a\<in>A. a' .= a"
+using assms
+unfolding set_eq_def elem_def
+by fast
+
+lemma set_eqE:
+  fixes R (structure)
+  assumes AB: "A {.=} B"
+    and r: "\<lbrakk>\<forall>a\<in>A. a .\<in> B; \<forall>b\<in>B. b .\<in> A\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using AB
+unfolding set_eq_def
+by (blast dest: r)
+
+lemma set_eqE2:
+  fixes R (structure)
+  assumes AB: "A {.=} B"
+    and r: "\<lbrakk>\<forall>a\<in>A. (\<exists>b\<in>B. a .= b); \<forall>b\<in>B. (\<exists>a\<in>A. b .= a)\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using AB
+unfolding set_eq_def elem_def
+by (blast dest: r)
+
+lemma set_eqE':
+  fixes R (structure)
+  assumes AB: "A {.=} B"
+    and aA: "a \<in> A" and bB: "b \<in> B"
+    and r: "\<And>a' b'. \<lbrakk>a' \<in> A; b .= a'; b' \<in> B; a .= b'\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+proof -
+  from AB aA
+      have "\<exists>b'\<in>B. a .= b'" by (rule set_eqD1)
+  from this obtain b'
+      where b': "b' \<in> B" "a .= b'" by auto
+
+  from AB bB
+      have "\<exists>a'\<in>A. b .= a'" by (rule set_eqD2)
+  from this obtain a'
+      where a': "a' \<in> A" "b .= a'" by auto
+
+  from a' b'
+      show "P" by (rule r)
+qed
+
+lemma (in equivalence) eq_elem_cong_r [trans]:
+  assumes a: "a .\<in> A"
+    and cong: "A {.=} A'"
+    and carr: "a \<in> carrier S"
+    and Carr: "A \<subseteq> carrier S" "A' \<subseteq> carrier S"
+  shows "a .\<in> A'"
+using a cong
+proof (elim elemE set_eqE)
+  fix b
+  assume bA: "b \<in> A"
+     and inA': "\<forall>b\<in>A. b .\<in> A'"
+  note [simp] = carr Carr Carr[THEN subsetD] bA
+  assume "a .= b"
+  also from bA inA'
+       have "b .\<in> A'" by fast
+  finally
+       show "a .\<in> A'" by simp
+qed
+
+lemma (in equivalence) set_eq_sym [sym]:
+  assumes "A {.=} B"
+    and "A \<subseteq> carrier S" "B \<subseteq> carrier S"
+  shows "B {.=} A"
+using assms
+unfolding set_eq_def elem_def
+by fast
+
+(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
+
+lemma (in equivalence) equal_set_eq_trans [trans]:
+  assumes AB: "A = B" and BC: "B {.=} C"
+  shows "A {.=} C"
+  using AB BC by simp
+
+lemma (in equivalence) set_eq_equal_trans [trans]:
+  assumes AB: "A {.=} B" and BC: "B = C"
+  shows "A {.=} C"
+  using AB BC by simp
+
+lemma (in equivalence) set_eq_trans [trans]:
+  assumes AB: "A {.=} B" and BC: "B {.=} C"
+    and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"
+  shows "A {.=} C"
+proof (intro set_eqI)
+  fix a
+  assume aA: "a \<in> A"
+  with carr have "a \<in> carrier S" by fast
+  note [simp] = carr this
+
+  from aA
+       have "a .\<in> A" by (simp add: elem_exact)
+  also note AB
+  also note BC
+  finally
+       show "a .\<in> C" by simp
+next
+  fix c
+  assume cC: "c \<in> C"
+  with carr have "c \<in> carrier S" by fast
+  note [simp] = carr this
+
+  from cC
+       have "c .\<in> C" by (simp add: elem_exact)
+  also note BC[symmetric]
+  also note AB[symmetric]
+  finally
+       show "c .\<in> A" by simp
+qed
+
+(* FIXME: generalise for insert *)
+
+(*
+lemma (in equivalence) set_eq_insert:
+  assumes x: "x .= x'"
+    and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
+  shows "insert x A {.=} insert x' A"
+  unfolding set_eq_def elem_def
+apply rule
+apply rule
+apply (case_tac "xa = x")
+using x apply fast
+apply (subgoal_tac "xa \<in> A") prefer 2 apply fast
+apply (rule_tac x=xa in bexI)
+using carr apply (rule_tac refl) apply auto [1]
+apply safe
+*)
+
+lemma (in equivalence) set_eq_pairI:
+  assumes xx': "x .= x'"
+    and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
+  shows "{x, y} {.=} {x', y}"
+unfolding set_eq_def elem_def
+proof safe
+  have "x' \<in> {x', y}" by fast
+  with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast
+next
+  have "y \<in> {x', y}" by fast
+  with carr show "\<exists>b\<in>{x', y}. y .= b" by fast
+next
+  have "x \<in> {x, y}" by fast
+  with xx'[symmetric] carr
+  show "\<exists>a\<in>{x, y}. x' .= a" by fast
+next
+  have "y \<in> {x, y}" by fast
+  with carr show "\<exists>a\<in>{x, y}. y .= a" by fast
+qed
+
+lemma (in equivalence) is_closedI:
+  assumes closed: "!!x y. [| x .= y; x \<in> A; y \<in> carrier S |] ==> y \<in> A"
+    and S: "A \<subseteq> carrier S"
+  shows "is_closed A"
+  unfolding eq_is_closed_def eq_closure_of_def elem_def
+  using S
+  by (blast dest: closed sym)
+
+lemma (in equivalence) closure_of_eq:
+  "[| x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> closure_of A"
+  unfolding eq_closure_of_def elem_def
+  by (blast intro: trans sym)
+
+lemma (in equivalence) is_closed_eq [dest]:
+  "[| x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> A"
+  unfolding eq_is_closed_def
+  using closure_of_eq [where A = A]
+  by simp
+
+lemma (in equivalence) is_closed_eq_rev [dest]:
+  "[| x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x \<in> A"
+  by (drule sym) (simp_all add: is_closed_eq)
+
+lemma closure_of_closed [simp, intro]:
+  fixes S (structure)
+  shows "closure_of A \<subseteq> carrier S"
+unfolding eq_closure_of_def
+by fast
+
+lemma closure_of_memI:
+  fixes S (structure)
+  assumes "a .\<in> A"
+    and "a \<in> carrier S"
+  shows "a \<in> closure_of A"
+unfolding eq_closure_of_def
+using assms
+by fast
+
+lemma closure_ofI2:
+  fixes S (structure)
+  assumes "a .= a'"
+    and "a' \<in> A"
+    and "a \<in> carrier S"
+  shows "a \<in> closure_of A"
+unfolding eq_closure_of_def elem_def
+using assms
+by fast
+
+lemma closure_of_memE:
+  fixes S (structure)
+  assumes p: "a \<in> closure_of A"
+    and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+proof -
+  from p
+      have acarr: "a \<in> carrier S"
+      and "a .\<in> A"
+      by (simp add: eq_closure_of_def)+
+  thus "P" by (rule r)
+qed
+
+lemma closure_ofE2:
+  fixes S (structure)
+  assumes p: "a \<in> closure_of A"
+    and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+proof -
+  from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def)
+
+  from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def)
+  from this obtain a'
+      where "a' \<in> A" and "a .= a'" by auto
+
+  from acarr and this
+      show "P" by (rule r)
+qed
+
+(*
+lemma (in equivalence) classes_consistent:
+  assumes Acarr: "A \<subseteq> carrier S"
+  shows "is_closed (closure_of A)"
+apply (blast intro: elemI elim elemE)
+using assms
+apply (intro is_closedI closure_of_memI, simp)
+ apply (elim elemE closure_of_memE)
+proof -
+  fix x a' a''
+  assume carr: "x \<in> carrier S" "a' \<in> carrier S"
+  assume a''A: "a'' \<in> A"
+  with Acarr have "a'' \<in> carrier S" by fast
+  note [simp] = carr this Acarr
+
+  assume "x .= a'"
+  also assume "a' .= a''"
+  also from a''A
+       have "a'' .\<in> A" by (simp add: elem_exact)
+  finally show "x .\<in> A" by simp
+qed
+*)
+(*
+lemma (in equivalence) classes_small:
+  assumes "is_closed B"
+    and "A \<subseteq> B"
+  shows "closure_of A \<subseteq> B"
+using assms
+by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)
+
+lemma (in equivalence) classes_eq:
+  assumes "A \<subseteq> carrier S"
+  shows "A {.=} closure_of A"
+using assms
+by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE)
+
+lemma (in equivalence) complete_classes:
+  assumes c: "is_closed A"
+  shows "A = closure_of A"
+using assms
+by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
+*)
+
+end
diff -r ef4b26efa8b6 -r ed7a2e0fab59 src/HOL/Algebra/Divisibility.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Divisibility.thy	Tue Jul 29 16:19:49 2008 +0200
@@ -0,0 +1,3931 @@
+(*
+  Title:     Divisibility in monoids and rings
+  Id:        $Id$
+  Author:    Clemens Ballarin, started 18 July 2008
+  Copyright: Clemens Ballarin
+*)
+
+theory Divisibility
+imports Permutation Coset Group GLattice
+begin
+
+subsection {* Monoid with cancelation law *}
+
+locale monoid_cancel = monoid +
+  assumes l_cancel: 
+          "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+      and r_cancel: 
+          "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+
+lemma (in monoid) monoid_cancelI:
+  assumes l_cancel: 
+          "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+      and r_cancel: 
+          "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+  shows "monoid_cancel G"
+by unfold_locales fact+
+
+lemma (in monoid_cancel) is_monoid_cancel:
+  "monoid_cancel G"
+by intro_locales
+
+interpretation group \<subseteq> monoid_cancel
+by unfold_locales simp+
+
+
+locale comm_monoid_cancel = monoid_cancel + comm_monoid
+
+lemma comm_monoid_cancelI:
+  includes comm_monoid
+  assumes cancel: 
+          "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
+  shows "comm_monoid_cancel G"
+apply unfold_locales
+ apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
+  apply (iprover intro: cancel)
+ apply (simp add: m_comm)
+apply (iprover intro: cancel)
+done
+
+lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
+  "comm_monoid_cancel G"
+by intro_locales
+
+interpretation comm_group \<subseteq> comm_monoid_cancel
+by unfold_locales
+
+
+subsection {* Products of units in monoids *}
+
+lemma (in monoid) Units_m_closed[simp, intro]:
+  assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
+  shows "h1 \<otimes> h2 \<in> Units G"
+unfolding Units_def
+using assms
+apply safe
+apply fast
+apply (intro bexI[of _ "inv h2 \<otimes> inv h1"], safe)
+  apply (simp add: m_assoc Units_closed)
+  apply (simp add: m_assoc[symmetric] Units_closed Units_l_inv)
+ apply (simp add: m_assoc Units_closed)
+ apply (simp add: m_assoc[symmetric] Units_closed Units_r_inv)
+apply fast
+done
+
+lemma (in monoid) prod_unit_l:
+  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "b \<in> Units G"
+proof -
+  have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
+
+  have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
+  also have "\<dots> = \<one>" by (simp add: Units_l_inv)
+  finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
+
+  have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
+  also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp
+  also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a"
+       by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
+  also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
+    by (simp add: m_assoc del: Units_l_inv)
+  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
+  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
+  finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
+
+  from c li ri
+      show "b \<in> Units G" by (simp add: Units_def, fast)
+qed
+
+lemma (in monoid) prod_unit_r:
+  assumes abunit[simp]: "a \<otimes> b \<in> Units G" and bunit[simp]: "b \<in> Units G"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "a \<in> Units G"
+proof -
+  have c: "b \<otimes> inv (a \<otimes> b) \<in> carrier G" by simp
+
+  have "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = (a \<otimes> b) \<otimes> inv (a \<otimes> b)"
+    by (simp add: m_assoc del: Units_r_inv)
+  also have "\<dots> = \<one>" by simp
+  finally have li: "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = \<one>" .
+
+  have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric])
+  also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp
+  also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" 
+       by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
+  also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)"
+    by (simp add: m_assoc del: Units_l_inv)
+  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
+  finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp
+
+  from c li ri
+      show "a \<in> Units G" by (simp add: Units_def, fast)
+qed
+
+lemma (in comm_monoid) unit_factor:
+  assumes abunit: "a \<otimes> b \<in> Units G"
+    and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "a \<in> Units G"
+using abunit[simplified Units_def]
+proof clarsimp
+  fix i
+  assume [simp]: "i \<in> carrier G"
+    and li: "i \<otimes> (a \<otimes> b) = \<one>"
+    and ri: "a \<otimes> b \<otimes> i = \<one>"
+
+  have carr': "b \<otimes> i \<in> carrier G" by simp
+
+  have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm)
+  also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc)
+  also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm)
+  also note li
+  finally have li': "(b \<otimes> i) \<otimes> a = \<one>" .
+
+  have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc)
+  also note ri
+  finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" .
+
+  from carr' li' ri'
+      show "a \<in> Units G" by (simp add: Units_def, fast)
+qed
+
+subsection {* Divisibility and association *}
+
+subsubsection {* Function definitions *}
+
+constdefs (structure G)
+  factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
+  "a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c"
+
+constdefs (structure G)
+  associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
+  "a \<sim> b == a divides b \<and> b divides a"
+
+abbreviation
+  "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
+
+constdefs (structure G)
+  properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
+  "properfactor G a b == a divides b \<and> \<not>(b divides a)"
+
+constdefs (structure G)
+  irreducible :: "[_, 'a] \<Rightarrow> bool"
+  "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
+
+constdefs (structure G)
+  prime :: "[_, 'a] \<Rightarrow> bool"
+  "prime G p == p \<notin> Units G \<and> 
+                (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)"
+
+
+
+subsubsection {* Divisibility *}
+
+lemma dividesI:
+  fixes G (structure)
+  assumes carr: "c \<in> carrier G"
+    and p: "b = a \<otimes> c"
+  shows "a divides b"
+unfolding factor_def
+using assms by fast
+
+lemma dividesI' [intro]:
+   fixes G (structure)
+  assumes p: "b = a \<otimes> c"
+    and carr: "c \<in> carrier G"
+  shows "a divides b"
+using assms
+by (fast intro: dividesI)
+
+lemma dividesD:
+  fixes G (structure)
+  assumes "a divides b"
+  shows "\<exists>c\<in>carrier G. b = a \<otimes> c"
+using assms
+unfolding factor_def
+by fast
+
+lemma dividesE [elim]:
+  fixes G (structure)
+  assumes d: "a divides b"
+    and elim: "\<And>c. \<lbrakk>b = a \<otimes> c; c \<in> carrier G\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+proof -
+  from dividesD[OF d]
+      obtain c
+      where "c\<in>carrier G"
+      and "b = a \<otimes> c"
+      by auto
+  thus "P" by (elim elim)
+qed
+
+lemma (in monoid) divides_refl[simp, intro!]:
+  assumes carr: "a \<in> carrier G"
+  shows "a divides a"
+apply (intro dividesI[of "\<one>"])
+apply (simp, simp add: carr)
+done
+
+lemma (in monoid) divides_trans [trans]:
+  assumes dvds: "a divides b"  "b divides c"
+    and acarr: "a \<in> carrier G"
+  shows "a divides c"
+using dvds[THEN dividesD]
+by (blast intro: dividesI m_assoc acarr)
+
+lemma (in monoid) divides_mult_lI [intro]:
+  assumes ab: "a divides b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "(c \<otimes> a) divides (c \<otimes> b)"
+using ab
+apply (elim dividesE, simp add: m_assoc[symmetric] carr)
+apply (fast intro: dividesI)
+done
+
+lemma (in monoid_cancel) divides_mult_l [simp]:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b"
+apply safe
+ apply (elim dividesE, intro dividesI, assumption)
+ apply (rule l_cancel[of c])
+    apply (simp add: m_assoc carr)+
+apply (fast intro: divides_mult_lI carr)
+done
+
+lemma (in comm_monoid) divides_mult_rI [intro]:
+  assumes ab: "a divides b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "(a \<otimes> c) divides (b \<otimes> c)"
+using carr ab
+apply (simp add: m_comm[of a c] m_comm[of b c])
+apply (rule divides_mult_lI, assumption+)
+done
+
+lemma (in comm_monoid_cancel) divides_mult_r [simp]:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b"
+using carr
+by (simp add: m_comm[of a c] m_comm[of b c])
+
+lemma (in monoid) divides_prod_r:
+  assumes ab: "a divides b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "a divides (b \<otimes> c)"
+using ab carr
+by (fast intro: m_assoc)
+
+lemma (in comm_monoid) divides_prod_l:
+  assumes carr[intro]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+    and ab: "a divides b"
+  shows "a divides (c \<otimes> b)"
+using ab carr
+apply (simp add: m_comm[of c b])
+apply (fast intro: divides_prod_r)
+done
+
+lemma (in monoid) unit_divides:
+  assumes uunit: "u \<in> Units G"
+      and acarr: "a \<in> carrier G"
+  shows "u divides a"
+proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr)
+  from uunit acarr
+      have xcarr: "inv u \<otimes> a \<in> carrier G" by fast
+
+  from uunit acarr
+       have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" by (fast intro: m_assoc[symmetric])
+  also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit])
+  also from acarr 
+       have "\<dots> = a" by simp
+  finally
+       show "a = u \<otimes> (inv u \<otimes> a)" ..
+qed
+
+lemma (in comm_monoid) divides_unit:
+  assumes udvd: "a divides u"
+      and  carr: "a \<in> carrier G"  "u \<in> Units G"
+  shows "a \<in> Units G"
+using udvd carr
+by (blast intro: unit_factor)
+
+lemma (in comm_monoid) Unit_eq_dividesone:
+  assumes ucarr: "u \<in> carrier G"
+  shows "u \<in> Units G = u divides \<one>"
+using ucarr
+by (fast dest: divides_unit intro: unit_divides)
+
+
+subsubsection {* Association *}
+
+lemma associatedI:
+  fixes G (structure)
+  assumes "a divides b"  "b divides a"
+  shows "a \<sim> b"
+using assms
+by (simp add: associated_def)
+
+lemma (in monoid) associatedI2:
+  assumes uunit[simp]: "u \<in> Units G"
+    and a: "a = b \<otimes> u"
+    and bcarr[simp]: "b \<in> carrier G"
+  shows "a \<sim> b"
+using uunit bcarr
+unfolding a
+apply (intro associatedI)
+ apply (rule dividesI[of "inv u"], simp)
+ apply (simp add: m_assoc Units_closed Units_r_inv)
+apply fast
+done
+
+lemma (in monoid) associatedI2':
+  assumes a: "a = b \<otimes> u"
+    and uunit: "u \<in> Units G"
+    and bcarr: "b \<in> carrier G"
+  shows "a \<sim> b"
+using assms by (intro associatedI2)
+
+lemma associatedD:
+  fixes G (structure)
+  assumes "a \<sim> b"
+  shows "a divides b"
+using assms by (simp add: associated_def)
+
+lemma (in monoid_cancel) associatedD2:
+  assumes assoc: "a \<sim> b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "\<exists>u\<in>Units G. a = b \<otimes> u"
+using assoc
+unfolding associated_def
+proof clarify
+  assume "b divides a"
+  hence "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD)
+  from this obtain u
+      where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"
+      by auto
+
+  assume "a divides b"
+  hence "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD)
+  from this obtain u'
+      where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"
+      by auto
+  note carr = carr ucarr u'carr
+
+  from carr
+       have "a \<otimes> \<one> = a" by simp
+  also have "\<dots> = b \<otimes> u" by (simp add: a)
+  also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b)
+  also from carr
+       have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)
+  finally
+       have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" .
+  with carr
+      have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel)
+
+  from carr
+       have "b \<otimes> \<one> = b" by simp
+  also have "\<dots> = a \<otimes> u'" by (simp add: b)
+  also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a)
+  also from carr
+       have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)
+  finally
+       have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" .
+  with carr
+      have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel)
+
+  from u'carr u1[symmetric] u2[symmetric]
+      have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" by fast
+  hence "u \<in> Units G" by (simp add: Units_def ucarr)
+
+  from ucarr this a
+      show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast
+qed
+
+lemma associatedE:
+  fixes G (structure)
+  assumes assoc: "a \<sim> b"
+    and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+proof -
+  from assoc
+      have "a divides b"  "b divides a"
+      by (simp add: associated_def)+
+  thus "P" by (elim e)
+qed
+
+lemma (in monoid_cancel) associatedE2:
+  assumes assoc: "a \<sim> b"
+    and e: "\<And>u. \<lbrakk>a = b \<otimes> u; u \<in> Units G\<rbrakk> \<Longrightarrow> P"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "P"
+proof -
+  from assoc and carr
+      have "\<exists>u\<in>Units G. a = b \<otimes> u" by (rule associatedD2)
+  from this obtain u
+      where "u \<in> Units G"  "a = b \<otimes> u"
+      by auto
+  thus "P" by (elim e)
+qed
+
+lemma (in monoid) associated_refl [simp, intro!]:
+  assumes "a \<in> carrier G"
+  shows "a \<sim> a"
+using assms
+by (fast intro: associatedI)
+
+lemma (in monoid) associated_sym [sym]:
+  assumes "a \<sim> b"
+    and "a \<in> carrier G"  "b \<in> carrier G"
+  shows "b \<sim> a"
+using assms
+by (iprover intro: associatedI elim: associatedE)
+
+lemma (in monoid) associated_trans [trans]:
+  assumes "a \<sim> b"  "b \<sim> c"
+    and "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "a \<sim> c"
+using assms
+by (iprover intro: associatedI divides_trans elim: associatedE)
+
+lemma (in monoid) division_equiv [intro, simp]:
+  "equivalence (division_rel G)"
+  apply unfold_locales
+  apply simp_all
+  apply (rule associated_sym, assumption+)
+  apply (iprover intro: associated_trans)
+  done
+
+
+subsubsection {* Division and associativity *}
+
+lemma divides_antisym:
+  fixes G (structure)
+  assumes "a divides b"  "b divides a"
+    and "a \<in> carrier G"  "b \<in> carrier G"
+  shows "a \<sim> b"
+using assms
+by (fast intro: associatedI)
+
+lemma (in monoid) divides_cong_l [trans]:
+  assumes xx': "x \<sim> x'"
+    and xdvdy: "x' divides y"
+    and carr [simp]: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  shows "x divides y"
+proof -
+  from xx'
+       have "x divides x'" by (simp add: associatedD)
+  also note xdvdy
+  finally
+       show "x divides y" by simp
+qed
+
+lemma (in monoid) divides_cong_r [trans]:
+  assumes xdvdy: "x divides y"
+    and yy': "y \<sim> y'"
+    and carr[simp]: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
+  shows "x divides y'"
+proof -
+  note xdvdy
+  also from yy'
+       have "y divides y'" by (simp add: associatedD)
+  finally
+       show "x divides y'" by simp
+qed
+
+lemma (in monoid) division_gpartial_order [simp, intro!]:
+  "gpartial_order (division_rel G)"
+  apply unfold_locales
+  apply simp_all
+  apply (simp add: associated_sym)
+  apply (blast intro: associated_trans)
+  apply (simp add: divides_antisym)
+  apply (blast intro: divides_trans)
+  apply (blast intro: divides_cong_l divides_cong_r associated_sym)
+  done
+
+    
+subsubsection {* Multiplication and associativity *}
+
+lemma (in monoid_cancel) mult_cong_r:
+  assumes "b \<sim> b'"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
+  shows "a \<otimes> b \<sim> a \<otimes> b'"
+using assms
+apply (elim associatedE2, intro associatedI2)
+apply (auto intro: m_assoc[symmetric])
+done
+
+lemma (in comm_monoid_cancel) mult_cong_l:
+  assumes "a \<sim> a'"
+    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
+  shows "a \<otimes> b \<sim> a' \<otimes> b"
+using assms
+apply (elim associatedE2, intro associatedI2)
+    apply assumption
+   apply (simp add: m_assoc Units_closed)
+   apply (simp add: m_comm Units_closed)
+  apply simp+
+done
+
+lemma (in monoid_cancel) assoc_l_cancel:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
+    and "a \<otimes> b \<sim> a \<otimes> b'"
+  shows "b \<sim> b'"
+using assms
+apply (elim associatedE2, intro associatedI2)
+    apply assumption
+   apply (rule l_cancel[of a])
+      apply (simp add: m_assoc Units_closed)
+     apply fast+
+done
+
+lemma (in comm_monoid_cancel) assoc_r_cancel:
+  assumes "a \<otimes> b \<sim> a' \<otimes> b"
+    and carr: "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
+  shows "a \<sim> a'"
+using assms
+apply (elim associatedE2, intro associatedI2)
+    apply assumption
+   apply (rule r_cancel[of a b])
+      apply (simp add: m_assoc Units_closed)
+      apply (simp add: m_comm Units_closed)
+     apply fast+
+done
+
+
+subsubsection {* Units *}
+
+lemma (in monoid_cancel) assoc_unit_l [trans]:
+  assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"
+    and carr: "a \<in> carrier G" 
+  shows "a \<in> Units G"
+using assms
+by (fast elim: associatedE2)
+
+lemma (in monoid_cancel) assoc_unit_r [trans]:
+  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
+    and bcarr: "b \<in> carrier G"
+  shows "b \<in> Units G"
+using aunit bcarr associated_sym[OF asc]
+by (blast intro: assoc_unit_l)
+
+lemma (in comm_monoid) Units_cong:
+  assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
+    and bcarr: "b \<in> carrier G"
+  shows "b \<in> Units G"
+using assms
+by (blast intro: divides_unit elim: associatedE)
+
+lemma (in monoid) Units_assoc:
+  assumes units: "a \<in> Units G"  "b \<in> Units G"
+  shows "a \<sim> b"
+using units
+by (fast intro: associatedI unit_divides)
+
+lemma (in monoid) Units_are_ones:
+  "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"
+apply (simp add: set_eq_def elem_def, rule, simp_all)
+proof clarsimp
+  fix a
+  assume aunit: "a \<in> Units G"
+  show "a \<sim> \<one>"
+  apply (rule associatedI)
+   apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])
+  apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])
+  done
+next
+  have "\<one> \<in> Units G" by simp
+  moreover have "\<one> \<sim> \<one>" by simp
+  ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast
+qed
+
+lemma (in comm_monoid) Units_Lower:
+  "Units G = Lower (division_rel G) (carrier G)"
+apply (simp add: Units_def Lower_def)
+apply (rule, rule)
+ apply clarsimp
+  apply (rule unit_divides)
+   apply (unfold Units_def, fast)
+  apply assumption
+apply clarsimp
+proof -
+  fix x
+  assume xcarr: "x \<in> carrier G"
+  assume r[rule_format]: "\<forall>y. y \<in> carrier G \<longrightarrow> x divides y"
+  have "\<one> \<in> carrier G" by simp
+  hence "x divides \<one>" by (rule r)
+  hence "\<exists>x'\<in>carrier G. \<one> = x \<otimes> x'" by (rule dividesE, fast)
+  from this obtain x'
+      where x'carr: "x' \<in> carrier G"
+      and xx': "\<one> = x \<otimes> x'"
+      by auto
+
+  note xx'
+  also with xcarr x'carr
+       have "\<dots> = x' \<otimes> x" by (simp add: m_comm)
+  finally
+       have "\<one> = x' \<otimes> x" .
+
+  from x'carr xx'[symmetric] this[symmetric]
+      show "\<exists>y\<in>carrier G. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
+qed
+
+
+subsubsection {* Proper factors *}
+
+lemma properfactorI:
+  fixes G (structure)
+  assumes "a divides b"
+    and "\<not>(b divides a)"
+  shows "properfactor G a b"
+using assms
+unfolding properfactor_def
+by simp
+
+lemma properfactorI2:
+  fixes G (structure)
+  assumes advdb: "a divides b"
+    and neq: "\<not>(a \<sim> b)"
+  shows "properfactor G a b"
+apply (rule properfactorI, rule advdb)
+proof (rule ccontr, simp)
+  assume "b divides a"
+  with advdb have "a \<sim> b" by (rule associatedI)
+  with neq show "False" by fast
+qed
+
+lemma (in comm_monoid_cancel) properfactorI3:
+  assumes p: "p = a \<otimes> b"
+    and nunit: "b \<notin> Units G"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "p \<in> carrier G"
+  shows "properfactor G a p"
+unfolding p
+using carr
+apply (intro properfactorI, fast)
+proof (clarsimp, elim dividesE)
+  fix c
+  assume ccarr: "c \<in> carrier G"
+  note [simp] = carr ccarr
+
+  have "a \<otimes> \<one> = a" by simp
+  also assume "a = a \<otimes> b \<otimes> c"
+  also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc)
+  finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" .
+
+  hence rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+)
+  also have "\<dots> = c \<otimes> b" by (simp add: m_comm)
+  finally have linv: "\<one> = c \<otimes> b" .
+
+  from ccarr linv[symmetric] rinv[symmetric]
+  have "b \<in> Units G" unfolding Units_def by fastsimp
+  with nunit
+      show "False" ..
+qed
+
+lemma properfactorE:
+  fixes G (structure)
+  assumes pf: "properfactor G a b"
+    and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using pf
+unfolding properfactor_def
+by (fast intro: r)
+
+lemma properfactorE2:
+  fixes G (structure)
+  assumes pf: "properfactor G a b"
+    and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using pf
+unfolding properfactor_def
+by (fast elim: elim associatedE)
+
+lemma (in monoid) properfactor_unitE:
+  assumes uunit: "u \<in> Units G"
+    and pf: "properfactor G a u"
+    and acarr: "a \<in> carrier G"
+  shows "P"
+using pf unit_divides[OF uunit acarr]
+by (fast elim: properfactorE)
+
+
+lemma (in monoid) properfactor_divides:
+  assumes pf: "properfactor G a b"
+  shows "a divides b"
+using pf
+by (elim properfactorE)
+
+lemma (in monoid) properfactor_trans1 [trans]:
+  assumes dvds: "a divides b"  "properfactor G b c"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G a c"
+using dvds carr
+apply (elim properfactorE, intro properfactorI)
+ apply (iprover intro: divides_trans)+
+done
+
+lemma (in monoid) properfactor_trans2 [trans]:
+  assumes dvds: "properfactor G a b"  "b divides c"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G a c"
+using dvds carr
+apply (elim properfactorE, intro properfactorI)
+ apply (iprover intro: divides_trans)+
+done
+
+lemma properfactor_glless:
+  fixes G (structure)
+  shows "properfactor G = glless (division_rel G)"
+apply (rule ext) apply (rule ext) apply rule
+ apply (fastsimp elim: properfactorE2 intro: gllessI)
+apply (fastsimp elim: gllessE intro: properfactorI2)
+done
+
+lemma (in monoid) properfactor_cong_l [trans]:
+  assumes x'x: "x' \<sim> x"
+    and pf: "properfactor G x y"
+    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  shows "properfactor G x' y"
+using pf
+unfolding properfactor_glless
+proof -
+  interpret gpartial_order ["division_rel G"] ..
+  from x'x
+       have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
+  also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
+  finally
+       show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)
+qed
+
+lemma (in monoid) properfactor_cong_r [trans]:
+  assumes pf: "properfactor G x y"
+    and yy': "y \<sim> y'"
+    and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
+  shows "properfactor G x y'"
+using pf
+unfolding properfactor_glless
+proof -
+  interpret gpartial_order ["division_rel G"] ..
+  assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
+  also from yy'
+       have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
+  finally
+       show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)
+qed
+
+lemma (in monoid_cancel) properfactor_mult_lI [intro]:
+  assumes ab: "properfactor G a b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
+using ab carr
+by (fastsimp elim: properfactorE intro: properfactorI)
+
+lemma (in monoid_cancel) properfactor_mult_l [simp]:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"
+using carr
+by (fastsimp elim: properfactorE intro: properfactorI)
+
+lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
+  assumes ab: "properfactor G a b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
+using ab carr
+by (fastsimp elim: properfactorE intro: properfactorI)
+
+lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"
+using carr
+by (fastsimp elim: properfactorE intro: properfactorI)
+
+lemma (in monoid) properfactor_prod_r:
+  assumes ab: "properfactor G a b"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G a (b \<otimes> c)"
+by (intro properfactor_trans2[OF ab] divides_prod_r, simp+)
+
+lemma (in comm_monoid) properfactor_prod_l:
+  assumes ab: "properfactor G a b"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "properfactor G a (c \<otimes> b)"
+by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
+
+
+subsection {* Irreducible elements and primes *}
+
+subsubsection {* Irreducible elements *}
+
+lemma irreducibleI:
+  fixes G (structure)
+  assumes "a \<notin> Units G"
+    and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G"
+  shows "irreducible G a"
+using assms 
+unfolding irreducible_def
+by blast
+
+lemma irreducibleE:
+  fixes G (structure)
+  assumes irr: "irreducible G a"
+     and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using assms
+unfolding irreducible_def
+by blast
+
+lemma irreducibleD:
+  fixes G (structure)
+  assumes irr: "irreducible G a"
+     and pf: "properfactor G b a"
+     and bcarr: "b \<in> carrier G"
+  shows "b \<in> Units G"
+using assms
+by (fast elim: irreducibleE)
+
+lemma (in monoid_cancel) irreducible_cong [trans]:
+  assumes irred: "irreducible G a"
+    and aa': "a \<sim> a'"
+    and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"
+  shows "irreducible G a'"
+using assms
+apply (elim irreducibleE, intro irreducibleI)
+apply simp_all
+proof clarify
+  assume "a' \<in> Units G"
+  also note aa'[symmetric]
+  finally have aunit: "a \<in> Units G" by simp
+
+  assume "a \<notin> Units G"
+  with aunit
+      show "False" by fast
+next
+  fix b
+  assume r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G"
+    and bcarr[simp]: "b \<in> carrier G"
+  assume "properfactor G b a'"
+  also note aa'[symmetric]
+  finally
+       have "properfactor G b a" by simp
+
+  with bcarr
+     show "b \<in> Units G" by (fast intro: r)
+qed
+
+
+lemma (in monoid) irreducible_prod_rI:
+  assumes airr: "irreducible G a"
+    and bunit: "b \<in> Units G"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "irreducible G (a \<otimes> b)"
+using airr carr bunit
+apply (elim irreducibleE, intro irreducibleI, clarify)
+ apply (subgoal_tac "a \<in> Units G", simp)
+ apply (intro prod_unit_r[of a b] carr bunit, assumption)
+proof -
+  fix c
+  assume [simp]: "c \<in> carrier G"
+    and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G"
+  assume "properfactor G c (a \<otimes> b)"
+  also have "a \<otimes> b \<sim> a" by (intro associatedI2[OF bunit], simp+)
+  finally
+       have pfa: "properfactor G c a" by simp
+  show "c \<in> Units G" by (rule r, simp add: pfa)
+qed
+
+lemma (in comm_monoid) irreducible_prod_lI:
+  assumes birr: "irreducible G b"
+    and aunit: "a \<in> Units G"
+    and carr [simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "irreducible G (a \<otimes> b)"
+apply (subst m_comm, simp+)
+apply (intro irreducible_prod_rI assms)
+done
+
+lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
+  assumes irr: "irreducible G (a \<otimes> b)"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+    and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P"
+    and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using irr
+proof (elim irreducibleE)
+  assume abnunit: "a \<otimes> b \<notin> Units G"
+    and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G"
+
+  show "P"
+  proof (cases "a \<in> Units G")
+    assume aunit: "a \<in>  Units G"
+
+    have "irreducible G b"
+    apply (rule irreducibleI)
+    proof (rule ccontr, simp)
+      assume "b \<in> Units G"
+      with aunit have "(a \<otimes> b) \<in> Units G" by fast
+      with abnunit show "False" ..
+    next
+      fix c
+      assume ccarr: "c \<in> carrier G"
+        and "properfactor G c b"
+      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a])
+      from ccarr this show "c \<in> Units G" by (fast intro: isunit)
+    qed
+
+    from aunit this show "P" by (rule e2)
+  next
+    assume anunit: "a \<notin> Units G"
+    with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3)
+    hence bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)
+    hence bunit: "b \<in> Units G" by (intro isunit, simp)
+
+    have "irreducible G a"
+    apply (rule irreducibleI)
+    proof (rule ccontr, simp)
+      assume "a \<in> Units G"
+      with bunit have "(a \<otimes> b) \<in> Units G" by fast
+      with abnunit show "False" ..
+    next
+      fix c
+      assume ccarr: "c \<in> carrier G"
+        and "properfactor G c a"
+      hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_r[of c a b])
+      from ccarr this show "c \<in> Units G" by (fast intro: isunit)
+    qed
+
+    from this bunit show "P" by (rule e1)
+  qed
+qed
+
+
+subsubsection {* Prime elements *}
+
+lemma primeI:
+  fixes G (structure)
+  assumes "p \<notin> Units G"
+    and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b"
+  shows "prime G p"
+using assms
+unfolding prime_def
+by blast
+
+lemma primeE:
+  fixes G (structure)
+  assumes pprime: "prime G p"
+    and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G.
+                          p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using pprime
+unfolding prime_def
+by (blast dest: e)
+
+lemma (in comm_monoid_cancel) prime_divides:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+    and pprime: "prime G p"
+    and pdvd: "p divides a \<otimes> b"
+  shows "p divides a \<or> p divides b"
+using assms
+by (blast elim: primeE)
+
+lemma (in monoid_cancel) prime_cong [trans]:
+  assumes pprime: "prime G p"
+    and pp': "p \<sim> p'"
+    and carr[simp]: "p \<in> carrier G"  "p' \<in> carrier G"
+  shows "prime G p'"
+using pprime
+apply (elim primeE, intro primeI)
+proof clarify
+  assume pnunit: "p \<notin> Units G"
+  assume "p' \<in> Units G"
+  also note pp'[symmetric]
+  finally
+       have "p \<in> Units G" by simp
+  with pnunit
+       show False ..
+next
+  fix a b
+  assume r[rule_format]:
+         "\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b"
+  assume p'dvd: "p' divides a \<otimes> b"
+    and carr'[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+
+  note pp'
+  also note p'dvd
+  finally
+       have "p divides a \<otimes> b" by simp
+  hence "p divides a \<or> p divides b" by (intro r, simp+)
+  moreover {
+    note pp'[symmetric]
+    also assume "p divides a"
+    finally
+         have "p' divides a" by simp
+    hence "p' divides a \<or> p' divides b" by simp
+  }
+  moreover {
+    note pp'[symmetric]
+    also assume "p divides b"
+    finally
+         have "p' divides b" by simp
+    hence "p' divides a \<or> p' divides b" by simp
+  }
+  ultimately
+    show "p' divides a \<or> p' divides b" by fast
+qed
+
+
+subsection {* Factorization and factorial monoids *}
+
+(*
+hide (open) const mult     (* Multiset.mult, conflicting with monoid.mult *)
+*)
+
+subsubsection {* Function definitions *}
+
+constdefs (structure G)
+  factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
+  "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a"
+
+  wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
+  "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a"
+
+abbreviation
+  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where
+  "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
+
+constdefs (structure G)
+  essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
+  "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)"
+
+
+locale factorial_monoid = comm_monoid_cancel +
+  assumes factors_exist: 
+          "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
+      and factors_unique: 
+          "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; 
+            set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
+
+
+subsubsection {* Comparing lists of elements *}
+
+text {* Association on lists *}
+
+lemma (in monoid) listassoc_refl [simp, intro]:
+  assumes "set as \<subseteq> carrier G"
+  shows "as [\<sim>] as"
+using assms
+by (induct as) simp+
+
+lemma (in monoid) listassoc_sym [sym]:
+  assumes "as [\<sim>] bs"
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "bs [\<sim>] as"
+using assms
+proof (induct as arbitrary: bs, simp)
+  case Cons
+  thus ?case
+    apply (induct bs, simp)
+    apply clarsimp
+    apply (iprover intro: associated_sym)
+  done
+qed
+
+lemma (in monoid) listassoc_trans [trans]:
+  assumes "as [\<sim>] bs" and "bs [\<sim>] cs"
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" and "set cs \<subseteq> carrier G"
+  shows "as [\<sim>] cs"
+using assms
+apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
+apply (rule associated_trans)
+    apply (subgoal_tac "as ! i \<sim> bs ! i", assumption)
+    apply (simp, simp)
+  apply blast+
+done
+
+lemma (in monoid_cancel) irrlist_listassoc_cong:
+  assumes "\<forall>a\<in>set as. irreducible G a"
+    and "as [\<sim>] bs"
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "\<forall>a\<in>set bs. irreducible G a"
+using assms
+apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
+apply (blast intro: irreducible_cong)
+done
+
+
+text {* Permutations *}
+
+lemma perm_map [intro]:
+  assumes p: "a <~~> b"
+  shows "map f a <~~> map f b"
+using p
+by induct auto
+
+lemma perm_map_switch:
+  assumes m: "map f a = map f b" and p: "b <~~> c"
+  shows "\<exists>d. a <~~> d \<and> map f d = map f c"
+using p m
+by (induct arbitrary: a) (simp, force, force, blast)
+
+lemma (in monoid) perm_assoc_switch:
+   assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
+   shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
+using p a
+apply (induct bs cs arbitrary: as, simp)
+  apply (clarsimp simp add: list_all2_Cons2, blast)
+ apply (clarsimp simp add: list_all2_Cons2)
+ apply blast
+apply blast
+done
+
+lemma (in monoid) perm_assoc_switch_r:
+   assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
+   shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
+using p a
+apply (induct as bs arbitrary: cs, simp)
+  apply (clarsimp simp add: list_all2_Cons1, blast)
+ apply (clarsimp simp add: list_all2_Cons1)
+ apply blast
+apply blast
+done
+
+declare perm_sym [sym]
+
+lemma perm_setP:
+  assumes perm: "as <~~> bs"
+    and as: "P (set as)"
+  shows "P (set bs)"
+proof -
+  from perm
+      have "multiset_of as = multiset_of bs"
+      by (simp add: multiset_of_eq_perm)
+  hence "set as = set bs" by (rule multiset_of_eq_setD)
+  with as
+      show "P (set bs)" by simp
+qed
+
+lemmas (in monoid) perm_closed =
+    perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
+
+lemmas (in monoid) irrlist_perm_cong =
+    perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
+
+
+text {* Essentially equal factorizations *}
+
+lemma (in monoid) essentially_equalI:
+  assumes ex: "fs1 <~~> fs1'"  "fs1' [\<sim>] fs2"
+  shows "essentially_equal G fs1 fs2"
+using ex
+unfolding essentially_equal_def
+by fast
+
+lemma (in monoid) essentially_equalE:
+  assumes ee: "essentially_equal G fs1 fs2"
+    and e: "\<And>fs1'. \<lbrakk>fs1 <~~> fs1'; fs1' [\<sim>] fs2\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using ee
+unfolding essentially_equal_def
+by (fast intro: e)
+
+lemma (in monoid) ee_refl [simp,intro]:
+  assumes carr: "set as \<subseteq> carrier G"
+  shows "essentially_equal G as as"
+using carr
+by (fast intro: essentially_equalI)
+
+lemma (in monoid) ee_sym [sym]:
+  assumes ee: "essentially_equal G as bs"
+    and carr: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
+  shows "essentially_equal G bs as"
+using ee
+proof (elim essentially_equalE)
+  fix fs
+  assume "as <~~> fs"  "fs [\<sim>] bs"
+  hence "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs" by (rule perm_assoc_switch_r)
+  from this obtain fs'
+      where a: "as [\<sim>] fs'" and p: "fs' <~~> bs"
+      by auto
+  from p have "bs <~~> fs'" by (rule perm_sym)
+  with a[symmetric] carr
+      show ?thesis
+      by (iprover intro: essentially_equalI perm_closed)
+qed
+
+lemma (in monoid) ee_trans [trans]:
+  assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs"
+    and ascarr: "set as \<subseteq> carrier G" 
+    and bscarr: "set bs \<subseteq> carrier G"
+    and cscarr: "set cs \<subseteq> carrier G"
+  shows "essentially_equal G as cs"
+using ab bc
+proof (elim essentially_equalE)
+  fix abs bcs
+  assume  "abs [\<sim>] bs" and pb: "bs <~~> bcs"
+  hence "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs" by (rule perm_assoc_switch)
+  from this obtain bs'
+      where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
+      by auto
+
+  assume "as <~~> abs"
+  with p
+      have pp: "as <~~> bs'" by fast
+
+  from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
+  from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
+  note a
+  also assume "bcs [\<sim>] cs"
+  finally (listassoc_trans) have"bs' [\<sim>] cs" by (simp add: c1 c2 cscarr)
+
+  with pp
+      show ?thesis
+      by (rule essentially_equalI)
+qed
+
+
+subsubsection {* Properties of lists of elements *}
+
+text {* Multiplication of factors in a list *}
+
+lemma (in monoid) multlist_closed [simp, intro]:
+  assumes ascarr: "set fs \<subseteq> carrier G"
+  shows "foldr (op \<otimes>) fs \<one> \<in> carrier G"
+by (insert ascarr, induct fs, simp+)
+
+lemma  (in comm_monoid) multlist_dividesI (*[intro]*):
+  assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G"
+  shows "f divides (foldr (op \<otimes>) fs \<one>)"
+using assms
+apply (induct fs)
+ apply simp
+apply (case_tac "f = a", simp)
+ apply (fast intro: dividesI)
+apply clarsimp
+apply (elim dividesE, intro dividesI)
+ defer 1
+ apply (simp add: m_comm)
+ apply (simp add: m_assoc[symmetric])
+ apply (simp add: m_comm)
+apply simp
+done
+
+lemma (in comm_monoid_cancel) multlist_listassoc_cong:
+  assumes "fs [\<sim>] fs'"
+    and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
+  shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
+using assms
+proof (induct fs arbitrary: fs', simp)
+  case (Cons a as fs')
+  thus ?case
+  apply (induct fs', simp)
+  proof clarsimp
+    fix b bs
+    assume "a \<sim> b" 
+      and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+      and ascarr: "set as \<subseteq> carrier G"
+    hence p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>"
+        by (fast intro: mult_cong_l)
+    also
+      assume "as [\<sim>] bs"
+         and bscarr: "set bs \<subseteq> carrier G"
+         and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>"
+      hence "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp
+      with ascarr bscarr bcarr
+          have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
+          by (fast intro: mult_cong_r)
+   finally
+       show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
+       by (simp add: ascarr bscarr acarr bcarr)
+  qed
+qed
+
+lemma (in comm_monoid) multlist_perm_cong:
+  assumes prm: "as <~~> bs"
+    and ascarr: "set as \<subseteq> carrier G"
+  shows "foldr (op \<otimes>) as \<one> = foldr (op \<otimes>) bs \<one>"
+using prm ascarr
+apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
+proof clarsimp
+  fix xs ys zs
+  assume "xs <~~> ys"  "set xs \<subseteq> carrier G"
+  hence "set ys \<subseteq> carrier G" by (rule perm_closed)
+  moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>"
+  ultimately show "foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" by simp
+qed
+
+lemma (in comm_monoid_cancel) multlist_ee_cong:
+  assumes "essentially_equal G fs fs'"
+    and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
+  shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
+using assms
+apply (elim essentially_equalE)
+apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
+done
+
+
+subsubsection {* Factorization in irreducible elements *}
+
+lemma wfactorsI:
+  includes (struct G)
+  assumes "\<forall>f\<in>set fs. irreducible G f"
+    and "foldr (op \<otimes>) fs \<one> \<sim> a"
+  shows "wfactors G fs a"
+using assms
+unfolding wfactors_def
+by simp
+
+lemma wfactorsE:
+  includes (struct G)
+  assumes wf: "wfactors G fs a"
+    and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using wf
+unfolding wfactors_def
+by (fast dest: e)
+
+lemma (in monoid) factorsI:
+  includes (struct G)
+  assumes "\<forall>f\<in>set fs. irreducible G f"
+    and "foldr (op \<otimes>) fs \<one> = a"
+  shows "factors G fs a"
+using assms
+unfolding factors_def
+by simp
+
+lemma factorsE:
+  includes (struct G)
+  assumes f: "factors G fs a"
+    and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+using f
+unfolding factors_def
+by (simp add: e)
+
+lemma (in monoid) factors_wfactors:
+  assumes "factors G as a" and "set as \<subseteq> carrier G"
+  shows "wfactors G as a"
+using assms
+by (blast elim: factorsE intro: wfactorsI)
+
+lemma (in monoid) wfactors_factors:
+  assumes "wfactors G as a" and "set as \<subseteq> carrier G"
+  shows "\<exists>a'. factors G as a' \<and> a' \<sim> a"
+using assms
+by (blast elim: wfactorsE intro: factorsI)
+
+lemma (in monoid) factors_closed [dest]:
+  assumes "factors G fs a" and "set fs \<subseteq> carrier G"
+  shows "a \<in> carrier G"
+using assms
+by (elim factorsE, clarsimp)
+
+lemma (in monoid) nunit_factors:
+  assumes anunit: "a \<notin> Units G"
+    and fs: "factors G as a"
+  shows "length as > 0"
+apply (insert fs, elim factorsE)
+proof (cases "length as = 0")
+  assume "length as = 0"
+  hence fold: "foldr op \<otimes> as \<one> = \<one>" by force
+
+  assume "foldr op \<otimes> as \<one> = a"
+  with fold
+       have "a = \<one>" by simp
+  then have "a \<in> Units G" by fast
+  with anunit
+       have "False" by simp
+  thus ?thesis ..
+qed simp
+
+lemma (in monoid) unit_wfactors [simp]:
+  assumes aunit: "a \<in> Units G"
+  shows "wfactors G [] a"
+using aunit
+by (intro wfactorsI) (simp, simp add: Units_assoc)
+
+lemma (in comm_monoid_cancel) unit_wfactors_empty:
+  assumes aunit: "a \<in> Units G"
+    and wf: "wfactors G fs a"
+    and carr[simp]: "set fs \<subseteq> carrier G"
+  shows "fs = []"
+proof (rule ccontr, cases fs, simp)
+  fix f fs'
+  assume fs: "fs = f # fs'"
+
+  from carr
+      have fcarr[simp]: "f \<in> carrier G"
+      and carr'[simp]: "set fs' \<subseteq> carrier G"
+      by (simp add: fs)+
+
+  from fs wf
+      have "irreducible G f" by (simp add: wfactors_def)
+  hence fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)
+
+  from fs wf
+      have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
+
+  note aunit
+  also from fs wf
+       have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
+       have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>" 
+       by (simp add: Units_closed[OF aunit] a[symmetric])
+  finally
+       have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp
+  hence "f \<in> Units G" by (intro unit_factor[of f], simp+)
+
+  with fnunit show "False" by simp
+qed
+
+
+text {* Comparing wfactors *}
+
+lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
+  assumes fact: "wfactors G fs a"
+    and asc: "fs [\<sim>] fs'"
+    and carr: "a \<in> carrier G"  "set fs \<subseteq> carrier G"  "set fs' \<subseteq> carrier G"
+  shows "wfactors G fs' a"
+using fact
+apply (elim wfactorsE, intro wfactorsI)
+proof -
+  assume "\<forall>f\<in>set fs. irreducible G f"
+  also note asc
+  finally (irrlist_listassoc_cong)
+       show "\<forall>f\<in>set fs'. irreducible G f" by (simp add: carr)
+next
+  from asc[symmetric]
+       have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" 
+       by (simp add: multlist_listassoc_cong carr)
+  also assume "foldr op \<otimes> fs \<one> \<sim> a"
+  finally
+       show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr)
+qed
+
+lemma (in comm_monoid) wfactors_perm_cong_l:
+  assumes "wfactors G fs a"
+    and "fs <~~> fs'"
+    and "set fs \<subseteq> carrier G"
+  shows "wfactors G fs' a"
+using assms
+apply (elim wfactorsE, intro wfactorsI)
+ apply (rule irrlist_perm_cong, assumption+)
+apply (simp add: multlist_perm_cong[symmetric])
+done
+
+lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
+  assumes ee: "essentially_equal G as bs"
+    and bfs: "wfactors G bs b"
+    and carr: "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
+  shows "wfactors G as b"
+using ee
+proof (elim essentially_equalE)
+  fix fs
+  assume prm: "as <~~> fs"
+  with carr
+       have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
+
+  note bfs
+  also assume [symmetric]: "fs [\<sim>] bs"
+  also (wfactors_listassoc_cong_l)
+       note prm[symmetric]
+  finally (wfactors_perm_cong_l)
+       show "wfactors G as b" by (simp add: carr fscarr)
+qed
+
+lemma (in monoid) wfactors_cong_r [trans]:
+  assumes fac: "wfactors G fs a" and aa': "a \<sim> a'"
+    and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"  "set fs \<subseteq> carrier G"
+  shows "wfactors G fs a'"
+using fac
+proof (elim wfactorsE, intro wfactorsI)
+  assume "foldr op \<otimes> fs \<one> \<sim> a" also note aa'
+  finally show "foldr op \<otimes> fs \<one> \<sim> a'" by simp
+qed
+
+
+subsubsection {* Essentially equal factorizations *}
+
+lemma (in comm_monoid_cancel) unitfactor_ee:
+  assumes uunit: "u \<in> Units G"
+    and carr: "set as \<subseteq> carrier G"
+  shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as" (is "essentially_equal G ?as' as")
+using assms
+apply (intro essentially_equalI[of _ ?as'], simp)
+apply (cases as, simp)
+apply (clarsimp, fast intro: associatedI2[of u])
+done
+
+lemma (in comm_monoid_cancel) factors_cong_unit:
+  assumes uunit: "u \<in> Units G" and anunit: "a \<notin> Units G"
+    and afs: "factors G as a"
+    and ascarr: "set as \<subseteq> carrier G"
+  shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)" (is "factors G ?as' ?a'")
+using assms
+apply (elim factorsE, clarify)
+apply (cases as)
+ apply (simp add: nunit_factors)
+apply clarsimp
+apply (elim factorsE, intro factorsI)
+ apply (clarsimp, fast intro: irreducible_prod_rI)
+apply (simp add: m_ac Units_closed)
+done
+
+lemma (in comm_monoid) perm_wfactorsD:
+  assumes prm: "as <~~> bs"
+    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
+    and ascarr[simp]: "set as \<subseteq> carrier G"
+  shows "a \<sim> b"
+using afs bfs
+proof (elim wfactorsE)
+  from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)
+  assume "foldr op \<otimes> as \<one> \<sim> a"
+  hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
+  also from prm
+       have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp)
+  also assume "foldr op \<otimes> bs \<one> \<sim> b"
+  finally
+       show "a \<sim> b" by simp
+qed
+
+lemma (in comm_monoid_cancel) listassoc_wfactorsD:
+  assumes assoc: "as [\<sim>] bs"
+    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
+    and [simp]: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
+  shows "a \<sim> b"
+using afs bfs
+proof (elim wfactorsE)
+  assume "foldr op \<otimes> as \<one> \<sim> a"
+  hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
+  also from assoc
+       have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+)
+  also assume "foldr op \<otimes> bs \<one> \<sim> b"
+  finally
+       show "a \<sim> b" by simp
+qed
+
+lemma (in comm_monoid_cancel) ee_wfactorsD:
+  assumes ee: "essentially_equal G as bs"
+    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
+    and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"
+  shows "a \<sim> b"
+using ee
+proof (elim essentially_equalE)
+  fix fs
+  assume prm: "as <~~> fs"
+  hence as'carr[simp]: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
+  from afs prm
+      have afs': "wfactors G fs a" by (rule wfactors_perm_cong_l, simp)
+  assume "fs [\<sim>] bs"
+  from this afs' bfs
+      show "a \<sim> b" by (rule listassoc_wfactorsD, simp+)
+qed
+
+lemma (in comm_monoid_cancel) ee_factorsD:
+  assumes ee: "essentially_equal G as bs"
+    and afs: "factors G as a" and bfs:"factors G bs b"
+    and "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
+  shows "a \<sim> b"
+using assms
+by (blast intro: factors_wfactors dest: ee_wfactorsD)
+
+lemma (in factorial_monoid) ee_factorsI:
+  assumes ab: "a \<sim> b"
+    and afs: "factors G as a" and anunit: "a \<notin> Units G"
+    and bfs: "factors G bs b" and bnunit: "b \<notin> Units G"
+    and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
+  shows "essentially_equal G as bs"
+proof -
+  note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD]
+                    factors_closed[OF bfs bscarr] bscarr[THEN subsetD]
+
+  from ab carr
+      have "\<exists>u\<in>Units G. a = b \<otimes> u" by (fast elim: associatedE2)
+  from this obtain u
+      where uunit: "u \<in> Units G"
+      and a: "a = b \<otimes> u" by auto
+
+  from uunit bscarr
+      have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs" 
+                (is "essentially_equal G ?bs' bs")
+      by (rule unitfactor_ee)
+
+  from bscarr uunit
+      have bs'carr: "set ?bs' \<subseteq> carrier G"
+      by (cases bs) (simp add: Units_closed)+
+
+  from uunit bnunit bfs bscarr
+      have fac: "factors G ?bs' (b \<otimes> u)"
+      by (rule factors_cong_unit)
+
+  from afs fac[simplified a[symmetric]] ascarr bs'carr anunit
+       have "essentially_equal G as ?bs'"
+       by (blast intro: factors_unique)
+  also note ee
+  finally
+      show "essentially_equal G as bs" by (simp add: ascarr bscarr bs'carr)
+qed
+
+lemma (in factorial_monoid) ee_wfactorsI:
+  assumes asc: "a \<sim> b"
+    and asf: "wfactors G as a" and bsf: "wfactors G bs b"
+    and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"
+    and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"
+  shows "essentially_equal G as bs"
+using assms
+proof (cases "a \<in> Units G")
+  assume aunit: "a \<in> Units G"
+  also note asc
+  finally have bunit: "b \<in> Units G" by simp
+
+  from aunit asf ascarr
+      have e: "as = []" by (rule unit_wfactors_empty)
+  from bunit bsf bscarr
+      have e': "bs = []" by (rule unit_wfactors_empty)
+
+  have "essentially_equal G [] []"
+      by (fast intro: essentially_equalI)
+  thus ?thesis by (simp add: e e')
+next
+  assume anunit: "a \<notin> Units G"
+  have bnunit: "b \<notin> Units G"
+  proof clarify
+    assume "b \<in> Units G"
+    also note asc[symmetric]
+    finally have "a \<in> Units G" by simp
+    with anunit
+         show "False" ..
+  qed
+
+  have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors[OF asf ascarr])
+  from this obtain a'
+      where fa': "factors G as a'"
+      and a': "a' \<sim> a"
+      by auto
+  from fa' ascarr
+      have a'carr[simp]: "a' \<in> carrier G" by fast
+
+  have a'nunit: "a' \<notin> Units G"
+  proof (clarify)
+    assume "a' \<in> Units G"
+    also note a'
+    finally have "a \<in> Units G" by simp
+    with anunit
+         show "False" ..
+  qed
+
+  have "\<exists>b'. factors G bs b' \<and> b' \<sim> b" by (rule wfactors_factors[OF bsf bscarr])
+  from this obtain b'
+      where fb': "factors G bs b'"
+      and b': "b' \<sim> b"
+      by auto
+  from fb' bscarr
+      have b'carr[simp]: "b' \<in> carrier G" by fast
+
+  have b'nunit: "b' \<notin> Units G"
+  proof (clarify)
+    assume "b' \<in> Units G"
+    also note b'
+    finally have "b \<in> Units G" by simp
+    with bnunit
+        show "False" ..
+  qed
+
+  note a'
+  also note asc
+  also note b'[symmetric]
+  finally
+       have "a' \<sim> b'" by simp
+
+  from this fa' a'nunit fb' b'nunit ascarr bscarr
+  show "essentially_equal G as bs"
+      by (rule ee_factorsI)
+qed
+
+lemma (in factorial_monoid) ee_wfactors:
+  assumes asf: "wfactors G as a"
+    and bsf: "wfactors G bs b"
+    and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+    and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
+  shows asc: "a \<sim> b = essentially_equal G as bs"
+using assms
+by (fast intro: ee_wfactorsI ee_wfactorsD)
+
+lemma (in factorial_monoid) wfactors_exist [intro, simp]:
+  assumes acarr[simp]: "a \<in> carrier G"
+  shows "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
+proof (cases "a \<in> Units G")
+  assume "a \<in> Units G"
+  hence "wfactors G [] a" by (rule unit_wfactors)
+  thus ?thesis by (intro exI) force
+next
+  assume "a \<notin> Units G"
+  hence "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (intro factors_exist acarr)
+  from this obtain fs
+      where fscarr: "set fs \<subseteq> carrier G"
+      and f: "factors G fs a"
+      by auto
+  from f have "wfactors G fs a" by (rule factors_wfactors) fact
+  from fscarr this
+      show ?thesis by fast
+qed
+
+lemma (in monoid) wfactors_prod_exists [intro, simp]:
+  assumes "\<forall>a \<in> set as. irreducible G a" and "set as \<subseteq> carrier G"
+  shows "\<exists>a. a \<in> carrier G \<and> wfactors G as a"
+unfolding wfactors_def
+using assms
+by blast
+
+lemma (in factorial_monoid) wfactors_unique:
+  assumes "wfactors G fs a" and "wfactors G fs' a"
+    and "a \<in> carrier G"
+    and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
+  shows "essentially_equal G fs fs'"
+using assms
+by (fast intro: ee_wfactorsI[of a a])
+
+lemma (in monoid) factors_mult_single:
+  assumes "irreducible G a" and "factors G fb b" and "a \<in> carrier G"
+  shows "factors G (a # fb) (a \<otimes> b)"
+using assms
+unfolding factors_def
+by simp
+
+lemma (in monoid_cancel) wfactors_mult_single:
+  assumes f: "irreducible G a"  "wfactors G fb b"
+        "a \<in> carrier G"  "b \<in> carrier G"  "set fb \<subseteq> carrier G"
+  shows "wfactors G (a # fb) (a \<otimes> b)"
+using assms
+unfolding wfactors_def
+by (simp add: mult_cong_r)
+
+lemma (in monoid) factors_mult:
+  assumes factors: "factors G fa a"  "factors G fb b"
+    and ascarr: "set fa \<subseteq> carrier G" and bscarr:"set fb \<subseteq> carrier G"
+  shows "factors G (fa @ fb) (a \<otimes> b)"
+using assms
+unfolding factors_def
+apply (safe, force)
+apply (induct fa)
+ apply simp
+apply (simp add: m_assoc)
+done
+
+lemma (in comm_monoid_cancel) wfactors_mult [intro]:
+  assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
+    and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+    and ascarr: "set as \<subseteq> carrier G" and bscarr:"set bs \<subseteq> carrier G"
+  shows "wfactors G (as @ bs) (a \<otimes> b)"
+apply (insert wfactors_factors[OF asf ascarr])
+apply (insert wfactors_factors[OF bsf bscarr])
+proof (clarsimp)
+  fix a' b'
+  assume asf': "factors G as a'" and a'a: "a' \<sim> a"
+     and bsf': "factors G bs b'" and b'b: "b' \<sim> b"
+  from asf' have a'carr: "a' \<in> carrier G" by (rule factors_closed) fact
+  from bsf' have b'carr: "b' \<in> carrier G" by (rule factors_closed) fact
+
+  note carr = acarr bcarr a'carr b'carr ascarr bscarr
+
+  from asf' bsf'
+      have "factors G (as @ bs) (a' \<otimes> b')" by (rule factors_mult) fact+
+
+  with carr
+       have abf': "wfactors G (as @ bs) (a' \<otimes> b')" by (intro factors_wfactors) simp+
+  also from b'b carr
+       have trb: "a' \<otimes> b' \<sim> a' \<otimes> b" by (intro mult_cong_r)
+  also from a'a carr
+       have tra: "a' \<otimes> b \<sim> a \<otimes> b" by (intro mult_cong_l)
+  finally
+       show "wfactors G (as @ bs) (a \<otimes> b)"
+       by (simp add: carr)
+qed
+
+lemma (in comm_monoid) factors_dividesI:
+  assumes "factors G fs a" and "f \<in> set fs"
+    and "set fs \<subseteq> carrier G"
+  shows "f divides a"
+using assms
+by (fast elim: factorsE intro: multlist_dividesI)
+
+lemma (in comm_monoid) wfactors_dividesI:
+  assumes p: "wfactors G fs a"
+    and fscarr: "set fs \<subseteq> carrier G" and acarr: "a \<in> carrier G"
+    and f: "f \<in> set fs"
+  shows "f divides a"
+apply (insert wfactors_factors[OF p fscarr], clarsimp)
+proof -
+  fix a'
+  assume fsa': "factors G fs a'"
+    and a'a: "a' \<sim> a"
+  with fscarr
+      have a'carr: "a' \<in> carrier G" by (simp add: factors_closed)
+
+  from fsa' fscarr f
+       have "f divides a'" by (fast intro: factors_dividesI)
+  also note a'a
+  finally
+       show "f divides a" by (simp add: f fscarr[THEN subsetD] acarr a'carr)
+qed
+
+
+subsubsection {* Factorial monoids and wfactors *}
+
+lemma (in comm_monoid_cancel) factorial_monoidI:
+  assumes wfactors_exists: 
+          "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
+      and wfactors_unique: 
+          "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G; 
+                       wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
+  shows "factorial_monoid G"
+proof (unfold_locales)
+  fix a
+  assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"
+
+  from wfactors_exists[OF acarr]
+  obtain as
+      where ascarr: "set as \<subseteq> carrier G"
+      and afs: "wfactors G as a"
+      by auto
+  from afs ascarr
+      have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors)
+  from this obtain a'
+      where afs': "factors G as a'"
+      and a'a: "a' \<sim> a"
+      by auto
+  from afs' ascarr
+      have a'carr: "a' \<in> carrier G" by fast
+  have a'nunit: "a' \<notin> Units G"
+  proof clarify
+    assume "a' \<in> Units G"
+    also note a'a
+    finally have "a \<in> Units G" by (simp add: acarr)
+    with anunit
+        show "False" ..
+  qed
+
+  from a'carr acarr a'a
+      have "\<exists>u. u \<in> Units G \<and> a' = a \<otimes> u" by (blast elim: associatedE2)
+  from this obtain  u
+      where uunit: "u \<in> Units G"
+      and a': "a' = a \<otimes> u"
+      by auto
+
+  note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
+
+  have "a = a \<otimes> \<one>" by simp
+  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)
+  also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
+  finally
+       have a: "a = a' \<otimes> inv u" .
+
+  from ascarr uunit
+      have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G"
+      by (cases as, clarsimp+)
+
+  from afs' uunit a'nunit acarr ascarr
+      have "factors G (as[0:=(as!0 \<otimes> inv u)]) a"
+      by (simp add: a factors_cong_unit)
+
+  with cr
+      show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by fast
+qed (blast intro: factors_wfactors wfactors_unique)
+
+
+subsection {* Factorizations as multisets *}
+
+text {* Gives useful operations like intersection *}
+
+(* FIXME: use class_of x instead of closure_of {x} *)
+
+abbreviation
+  "assocs G x == eq_closure_of (division_rel G) {x}"
+
+constdefs (structure G)
+  "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
+
+
+text {* Helper lemmas *}
+
+lemma (in monoid) assocs_repr_independence:
+  assumes "y \<in> assocs G x"
+    and "x \<in> carrier G"
+  shows "assocs G x = assocs G y"
+using assms
+apply safe
+ apply (elim closure_ofE2, intro closure_ofI2[of _ _ y])
+   apply (clarsimp, iprover intro: associated_trans associated_sym, simp+)
+apply (elim closure_ofE2, intro closure_ofI2[of _ _ x])
+  apply (clarsimp, iprover intro: associated_trans, simp+)
+done
+
+lemma (in monoid) assocs_self:
+  assumes "x \<in> carrier G"
+  shows "x \<in> assocs G x"
+using assms
+by (fastsimp intro: closure_ofI2)
+
+lemma (in monoid) assocs_repr_independenceD:
+  assumes repr: "assocs G x = assocs G y"
+    and ycarr: "y \<in> carrier G"
+  shows "y \<in> assocs G x"
+unfolding repr
+using ycarr
+by (intro assocs_self)
+
+lemma (in comm_monoid) assocs_assoc:
+  assumes "a \<in> assocs G b"
+    and "b \<in> carrier G"
+  shows "a \<sim> b"
+using assms
+by (elim closure_ofE2, simp)
+
+lemmas (in comm_monoid) assocs_eqD =
+    assocs_repr_independenceD[THEN assocs_assoc]
+
+
+subsubsection {* Comparing multisets *}
+
+lemma (in monoid) fmset_perm_cong:
+  assumes prm: "as <~~> bs"
+  shows "fmset G as = fmset G bs"
+using perm_map[OF prm]
+by (simp add: multiset_of_eq_perm fmset_def)
+
+lemma (in comm_monoid_cancel) eqc_listassoc_cong:
+  assumes "as [\<sim>] bs"
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "map (assocs G) as = map (assocs G) bs"
+using assms
+apply (induct as arbitrary: bs, simp)
+apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)
+ apply (clarsimp elim!: closure_ofE2) defer 1
+ apply (clarsimp elim!: closure_ofE2) defer 1
+proof -
+  fix a x z
+  assume carr[simp]: "a \<in> carrier G"  "x \<in> carrier G"  "z \<in> carrier G"
+  assume "x \<sim> a"
+  also assume "a \<sim> z"
+  finally have "x \<sim> z" by simp
+  with carr
+      show "x \<in> assocs G z"
+      by (intro closure_ofI2) simp+
+next
+  fix a x z
+  assume carr[simp]: "a \<in> carrier G"  "x \<in> carrier G"  "z \<in> carrier G"
+  assume "x \<sim> z"
+  also assume [symmetric]: "a \<sim> z"
+  finally have "x \<sim> a" by simp
+  with carr
+      show "x \<in> assocs G a"
+      by (intro closure_ofI2) simp+
+qed
+
+lemma (in comm_monoid_cancel) fmset_listassoc_cong:
+  assumes "as [\<sim>] bs" 
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "fmset G as = fmset G bs"
+using assms
+unfolding fmset_def
+by (simp add: eqc_listassoc_cong)
+
+lemma (in comm_monoid_cancel) ee_fmset:
+  assumes ee: "essentially_equal G as bs" 
+    and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
+  shows "fmset G as = fmset G bs"
+using ee
+proof (elim essentially_equalE)
+  fix as'
+  assume prm: "as <~~> as'"
+  from prm ascarr
+      have as'carr: "set as' \<subseteq> carrier G" by (rule perm_closed)
+
+  from prm
+       have "fmset G as = fmset G as'" by (rule fmset_perm_cong)
+  also assume "as' [\<sim>] bs"
+       with as'carr bscarr
+       have "fmset G as' = fmset G bs" by (simp add: fmset_listassoc_cong)
+  finally
+       show "fmset G as = fmset G bs" .
+qed
+
+lemma (in monoid_cancel) fmset_ee__hlp_induct:
+  assumes prm: "cas <~~> cbs"
+    and cdef: "cas = map (assocs G) as"  "cbs = map (assocs G) bs"
+  shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> 
+                 cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
+apply (rule perm.induct[of cas cbs], rule prm)
+apply safe apply simp_all
+  apply (simp add: map_eq_Cons_conv, blast)
+ apply force
+proof -
+  fix ys as bs
+  assume p1: "map (assocs G) as <~~> ys"
+    and r1[rule_format]:
+        "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and>
+                  ys = map (assocs G) bs
+                  \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)"
+    and p2: "ys <~~> map (assocs G) bs"
+    and r2[rule_format]:
+        "\<forall>as bsa. ys = map (assocs G) as \<and>
+                  map (assocs G) bs = map (assocs G) bsa
+                  \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)"
+    and p3: "map (assocs G) as <~~> map (assocs G) bs"
+
+  from p1
+      have "multiset_of (map (assocs G) as) = multiset_of ys"
+      by (simp add: multiset_of_eq_perm)
+  hence setys: "set (map (assocs G) as) = set ys" by (rule multiset_of_eq_setD)
+
+  have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast
+  with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp
+  hence "\<exists>yy. ys = map (assocs G) yy"
+    apply (induct ys, simp, clarsimp)
+  proof -
+    fix yy x
+    show "\<exists>yya. (assocs G x) # map (assocs G) yy =
+                map (assocs G) yya"
+    by (rule exI[of _ "x#yy"], simp)
+  qed
+  from this obtain yy
+      where ys: "ys = map (assocs G) yy"
+      by auto
+
+  from p1 ys
+      have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy"
+      by (intro r1, simp)
+  from this obtain as'
+      where asas': "as <~~> as'"
+      and as'yy: "map (assocs G) as' = map (assocs G) yy"
+      by auto
+
+  from p2 ys
+      have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
+      by (intro r2, simp)
+  from this obtain as''
+      where yyas'': "yy <~~> as''"
+      and as''bs: "map (assocs G) as'' = map (assocs G) bs"
+      by auto
+
+  from as'yy and yyas''
+      have "\<exists>cs. as' <~~> cs \<and> map (assocs G) cs = map (assocs G) as''"
+      by (rule perm_map_switch)
+  from this obtain cs
+      where as'cs: "as' <~~> cs"
+      and csas'': "map (assocs G) cs = map (assocs G) as''"
+      by auto
+
+  from asas' and as'cs
+      have ascs: "as <~~> cs" by fast
+  from csas'' and as''bs
+      have "map (assocs G) cs = map (assocs G) bs" by simp
+  from ascs and this
+  show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" by fast
+qed
+
+lemma (in comm_monoid_cancel) fmset_ee:
+  assumes mset: "fmset G as = fmset G bs"
+    and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
+  shows "essentially_equal G as bs"
+proof -
+  from mset
+      have mpp: "map (assocs G) as <~~> map (assocs G) bs"
+      by (simp add: fmset_def multiset_of_eq_perm)
+
+  have "\<exists>cas. cas = map (assocs G) as" by simp
+  from this obtain cas where cas: "cas = map (assocs G) as" by simp
+
+  have "\<exists>cbs. cbs = map (assocs G) bs" by simp
+  from this obtain cbs where cbs: "cbs = map (assocs G) bs" by simp
+
+  from cas cbs mpp
+      have [rule_format]:
+           "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> 
+                     cbs = map (assocs G) bs) 
+                     \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
+      by (intro fmset_ee__hlp_induct, simp+)
+  with mpp cas cbs
+      have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
+      by simp
+
+  from this obtain as'
+      where tp: "as <~~> as'"
+      and tm: "map (assocs G) as' = map (assocs G) bs"
+      by auto
+  from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq)
+  from tp have "set as = set as'" by (simp add: multiset_of_eq_perm multiset_of_eq_setD)
+  with ascarr
+      have as'carr: "set as' \<subseteq> carrier G" by simp
+
+  from tm as'carr[THEN subsetD] bscarr[THEN subsetD]
+  have "as' [\<sim>] bs"
+    by (induct as' arbitrary: bs) (simp, fastsimp dest: assocs_eqD[THEN associated_sym])
+
+  from tp and this
+    show "essentially_equal G as bs" by (fast intro: essentially_equalI)
+qed
+
+lemma (in comm_monoid_cancel) ee_is_fmset:
+  assumes "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "essentially_equal G as bs = (fmset G as = fmset G bs)"
+using assms
+by (fast intro: ee_fmset fmset_ee)
+
+
+subsubsection {* Interpreting multisets as factorizations *}
+
+lemma (in monoid) mset_fmsetEx:
+  assumes elems: "\<And>X. X \<in> set_of Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
+  shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
+proof -
+  have "\<exists>Cs'. Cs = multiset_of Cs'"
+      by (rule surjE[OF surj_multiset_of], fast)
+  from this obtain Cs'
+      where Cs: "Cs = multiset_of Cs'"
+      by auto
+
+  have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> multiset_of (map (assocs G) cs) = Cs"
+  using elems
+  unfolding Cs
+    apply (induct Cs', simp)
+    apply clarsimp
+    apply (subgoal_tac "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and> 
+                             multiset_of (map (assocs G) cs) = multiset_of Cs'")
+  proof clarsimp
+    fix a Cs' cs 
+    assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
+      and csP: "\<forall>x\<in>set cs. P x"
+      and mset: "multiset_of (map (assocs G) cs) = multiset_of Cs'"
+    from ih
+        have "\<exists>x. P x \<and> a = assocs G x" by fast
+    from this obtain c
+        where cP: "P c"
+        and a: "a = assocs G c"
+        by auto
+    from cP csP
+        have tP: "\<forall>x\<in>set (c#cs). P x" by simp
+    from mset a
+    have "multiset_of (map (assocs G) (c#cs)) = multiset_of Cs' + {#a#}" by simp
+    from tP this
+    show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
+               multiset_of (map (assocs G) cs) =
+               multiset_of Cs' + {#a#}" by fast
+  qed simp
+  thus ?thesis by (simp add: fmset_def)
+qed
+
+lemma (in monoid) mset_wfactorsEx:
+  assumes elems: "\<And>X. X \<in> set_of Cs 
+                      \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
+  shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
+proof -
+  have "\<exists>cs. (\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c) \<and> fmset G cs = Cs"
+      by (intro mset_fmsetEx, rule elems)
+  from this obtain cs
+      where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c"
+      and Cs[symmetric]: "fmset G cs = Cs"
+      by auto
+
+  from p
+      have cscarr: "set cs \<subseteq> carrier G" by fast
+
+  from p
+      have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c"
+      by (intro wfactors_prod_exists) fast+
+  from this obtain c
+      where ccarr: "c \<in> carrier G"
+      and cfs: "wfactors G cs c"
+      by auto
+
+  with cscarr Cs
+      show ?thesis by fast
+qed
+
+
+subsubsection {* Multiplication on multisets *}
+
+lemma (in factorial_monoid) mult_wfactors_fmset:
+  assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+              "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
+  shows "fmset G cs = fmset G as + fmset G bs"
+proof -
+  from assms
+       have "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult)
+  with carr cfs
+       have "essentially_equal G cs (as@bs)" by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"], simp+)
+  with carr
+       have "fmset G cs = fmset G (as@bs)" by (intro ee_fmset, simp+)
+  also have "fmset G (as@bs) = fmset G as + fmset G bs" by (simp add: fmset_def)
+  finally show "fmset G cs = fmset G as + fmset G bs" .
+qed
+
+lemma (in factorial_monoid) mult_factors_fmset:
+  assumes afs: "factors G as a" and bfs: "factors G bs b" and cfs: "factors G cs (a \<otimes> b)"
+    and "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
+  shows "fmset G cs = fmset G as + fmset G bs"
+using assms
+by (blast intro: factors_wfactors mult_wfactors_fmset)
+
+lemma (in comm_monoid_cancel) fmset_wfactors_mult:
+  assumes mset: "fmset G cs = fmset G as + fmset G bs"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+          "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
+    and fs: "wfactors G as a"  "wfactors G bs b"  "wfactors G cs c"
+  shows "c \<sim> a \<otimes> b"
+proof -
+  from carr fs
+       have m: "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult)
+
+  from mset
+       have "fmset G cs = fmset G (as@bs)" by (simp add: fmset_def)
+  then have "essentially_equal G cs (as@bs)" by (rule fmset_ee) (simp add: carr)+
+  then show "c \<sim> a \<otimes> b" by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp add: assms m)+
+qed
+
+
+subsubsection {* Divisibility on multisets *}
+
+lemma (in factorial_monoid) divides_fmsubset:
+  assumes ab: "a divides b"
+    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
+  shows "fmset G as \<le># fmset G bs"
+using ab
+proof (elim dividesE)
+  fix c
+  assume ccarr: "c \<in> carrier G"
+  hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by (rule wfactors_exist)
+  from this obtain cs 
+      where cscarr: "set cs \<subseteq> carrier G"
+      and cfs: "wfactors G cs c" by auto
+  note carr = carr ccarr cscarr
+
+  assume "b = a \<otimes> c"
+  with afs bfs cfs carr
+      have "fmset G bs = fmset G as + fmset G cs"
+      by (intro mult_wfactors_fmset[OF afs cfs]) simp+
+
+  thus ?thesis by simp
+qed
+
+lemma (in comm_monoid_cancel) fmsubset_divides:
+  assumes msubset: "fmset G as \<le># fmset G bs"
+    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
+    and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+    and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
+  shows "a divides b"
+proof -
+  from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
+  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
+
+  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = fmset G bs - fmset G as"
+  proof (intro mset_wfactorsEx, simp)
+    fix X
+    assume "count (fmset G as) X < count (fmset G bs) X"
+    hence "0 < count (fmset G bs) X" by simp
+    hence "X \<in> set_of (fmset G bs)" by simp
+    hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
+    hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
+    from this obtain x
+        where xbs: "x \<in> set bs"
+        and X: "X = assocs G x"
+        by auto
+
+    with bscarr have xcarr: "x \<in> carrier G" by fast
+    from xbs birr have xirr: "irreducible G x" by simp
+
+    from xcarr and xirr and X
+        show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x" by fast
+  qed
+  from this obtain c cs
+      where ccarr: "c \<in> carrier G"
+      and cscarr: "set cs \<subseteq> carrier G" 
+      and csf: "wfactors G cs c"
+      and csmset: "fmset G cs = fmset G bs - fmset G as" by auto
+
+  from csmset msubset
+      have "fmset G bs = fmset G as + fmset G cs"
+      by (simp add: multiset_eq_conv_count_eq mset_le_def)
+  hence basc: "b \<sim> a \<otimes> c"
+      by (rule fmset_wfactors_mult) fact+
+
+  thus ?thesis
+  proof (elim associatedE2)
+    fix u
+    assume "u \<in> Units G"  "b = a \<otimes> c \<otimes> u"
+    with acarr ccarr
+        show "a divides b" by (fast intro: dividesI[of "c \<otimes> u"] m_assoc)
+  qed (simp add: acarr bcarr ccarr)+
+qed
+
+lemma (in factorial_monoid) divides_as_fmsubset:
+  assumes "wfactors G as a" and "wfactors G bs b"
+    and "a \<in> carrier G" and "b \<in> carrier G" 
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "a divides b = (fmset G as \<le># fmset G bs)"
+using assms
+by (blast intro: divides_fmsubset fmsubset_divides)
+
+
+text {* Proper factors on multisets *}
+
+lemma (in factorial_monoid) fmset_properfactor:
+  assumes asubb: "fmset G as \<le># fmset G bs"
+    and anb: "fmset G as \<noteq> fmset G bs"
+    and "wfactors G as a" and "wfactors G bs b"
+    and "a \<in> carrier G" and "b \<in> carrier G"
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "properfactor G a b"
+apply (rule properfactorI)
+apply (rule fmsubset_divides[of as bs], fact+)
+proof
+  assume "b divides a"
+  hence "fmset G bs \<le># fmset G as"
+      by (rule divides_fmsubset) fact+
+  with asubb
+      have "fmset G as = fmset G bs" by (simp add: mset_le_antisym)
+  with anb
+      show "False" ..
+qed
+
+lemma (in factorial_monoid) properfactor_fmset:
+  assumes pf: "properfactor G a b"
+    and "wfactors G as a" and "wfactors G bs b"
+    and "a \<in> carrier G" and "b \<in> carrier G"
+    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
+using pf
+apply (elim properfactorE)
+apply rule
+ apply (intro divides_fmsubset, assumption)
+  apply (rule assms)+
+proof
+  assume bna: "\<not> b divides a"
+  assume "fmset G as = fmset G bs"
+  then have "essentially_equal G as bs" by (rule fmset_ee) fact+
+  hence "a \<sim> b" by (rule ee_wfactorsD[of as bs]) fact+
+  hence "b divides a" by (elim associatedE)
+  with bna
+      show "False" ..
+qed
+
+
+subsection {* Irreducible elements are prime *}
+
+lemma (in factorial_monoid) irreducible_is_prime:
+  assumes pirr: "irreducible G p"
+    and pcarr: "p \<in> carrier G"
+  shows "prime G p"
+using pirr
+proof (elim irreducibleE, intro primeI)
+  fix a b
+  assume acarr: "a \<in> carrier G"  and bcarr: "b \<in> carrier G"
+    and pdvdab: "p divides (a \<otimes> b)"
+    and pnunit: "p \<notin> Units G"
+  assume irreduc[rule_format]:
+         "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
+  from pdvdab
+      have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)
+  from this obtain c
+      where ccarr: "c \<in> carrier G"
+      and abpc: "a \<otimes> b = p \<otimes> c"
+      by auto
+
+  from acarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" by (rule wfactors_exist)
+  from this obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" by auto
+
+  from bcarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs b" by (rule wfactors_exist)
+  from this obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" by auto
+
+  from ccarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs c" by (rule wfactors_exist)
+  from this obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" by auto
+
+  note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr
+
+  from afs and bfs
+      have abfs: "wfactors G (as @ bs) (a \<otimes> b)" by (rule wfactors_mult) fact+
+
+  from pirr cfs
+      have pcfs: "wfactors G (p # cs) (p \<otimes> c)" by (rule wfactors_mult_single) fact+
+  with abpc
+      have abfs': "wfactors G (p # cs) (a \<otimes> b)" by simp
+
+  from abfs' abfs
+      have "essentially_equal G (p # cs) (as @ bs)"
+      by (rule wfactors_unique) simp+
+
+  hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"
+      by (fast elim: essentially_equalE)
+  from this obtain ds
+      where "p # cs <~~> ds"
+      and dsassoc: "ds [\<sim>] (as @ bs)"
+      by auto
+
+  then have "p \<in> set ds"
+       by (simp add: perm_set_eq[symmetric])
+  with dsassoc
+       have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"
+       unfolding list_all2_conv_all_nth set_conv_nth
+       by force
+
+  from this obtain p'
+       where "p' \<in> set (as@bs)"
+       and pp': "p \<sim> p'"
+       by auto
+
+  hence "p' \<in> set as \<or> p' \<in> set bs" by simp
+  moreover
+  {
+    assume p'elem: "p' \<in> set as"
+    with ascarr have [simp]: "p' \<in> carrier G" by fast
+
+    note pp'
+    also from afs
+         have "p' divides a" by (rule wfactors_dividesI) fact+
+    finally
+         have "p divides a" by simp
+  }
+  moreover
+  {
+    assume p'elem: "p' \<in> set bs"
+    with bscarr have [simp]: "p' \<in> carrier G" by fast
+
+    note pp'
+    also from bfs
+         have "p' divides b" by (rule wfactors_dividesI) fact+
+    finally
+         have "p divides b" by simp
+  }
+  ultimately
+      show "p divides a \<or> p divides b" by fast
+qed
+
+
+--"A version using @{const factors}, more complicated"
+lemma (in factorial_monoid) factors_irreducible_is_prime:
+  assumes pirr: "irreducible G p"
+    and pcarr: "p \<in> carrier G"
+  shows "prime G p"
+using pirr
+apply (elim irreducibleE, intro primeI)
+ apply assumption
+proof -
+  fix a b
+  assume acarr: "a \<in> carrier G" 
+    and bcarr: "b \<in> carrier G"
+    and pdvdab: "p divides (a \<otimes> b)"
+  assume irreduc[rule_format]:
+         "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
+  from pdvdab
+      have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)
+  from this obtain c
+      where ccarr: "c \<in> carrier G"
+      and abpc: "a \<otimes> b = p \<otimes> c"
+      by auto
+  note [simp] = pcarr acarr bcarr ccarr
+
+  show "p divides a \<or> p divides b"
+  proof (cases "a \<in> Units G")
+    assume aunit: "a \<in> Units G"
+
+    note pdvdab
+    also have "a \<otimes> b = b \<otimes> a" by (simp add: m_comm)
+    also from aunit
+         have bab: "b \<otimes> a \<sim> b"
+         by (intro associatedI2[of "a"], simp+)
+    finally
+         have "p divides b" by simp
+    thus "p divides a \<or> p divides b" ..
+  next
+    assume anunit: "a \<notin> Units G"
+
+    show "p divides a \<or> p divides b"
+    proof (cases "b \<in> Units G")
+      assume bunit: "b \<in> Units G"
+
+      note pdvdab
+      also from bunit
+           have baa: "a \<otimes> b \<sim> a"
+           by (intro associatedI2[of "b"], simp+)
+      finally
+           have "p divides a" by simp
+      thus "p divides a \<or> p divides b" ..
+    next
+      assume bnunit: "b \<notin> Units G"
+
+      have cnunit: "c \<notin> Units G"
+      proof (rule ccontr, simp)
+        assume cunit: "c \<in> Units G"
+        from bnunit
+             have "properfactor G a (a \<otimes> b)"
+             by (intro properfactorI3[of _ _ b], simp+)
+        also note abpc
+        also from cunit
+             have "p \<otimes> c \<sim> p"
+             by (intro associatedI2[of c], simp+)
+        finally
+             have "properfactor G a p" by simp
+
+        with acarr
+             have "a \<in> Units G" by (fast intro: irreduc)
+        with anunit
+             show "False" ..
+      qed
+
+      have abnunit: "a \<otimes> b \<notin> Units G"
+      proof clarsimp
+        assume abunit: "a \<otimes> b \<in> Units G"
+        hence "a \<in> Units G" by (rule unit_factor) fact+
+        with anunit
+             show "False" ..
+      qed
+
+      from acarr anunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (rule factors_exist)
+      then obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a" by auto
+
+      from bcarr bnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs b" by (rule factors_exist)
+      then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b" by auto
+
+      from ccarr cnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs c" by (rule factors_exist)
+      then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c" by auto
+
+      note [simp] = ascarr bscarr cscarr
+
+      from afac and bfac
+          have abfac: "factors G (as @ bs) (a \<otimes> b)" by (rule factors_mult) fact+
+
+      from pirr cfac
+          have pcfac: "factors G (p # cs) (p \<otimes> c)" by (rule factors_mult_single) fact+
+      with abpc
+          have abfac': "factors G (p # cs) (a \<otimes> b)" by simp
+
+      from abfac' abfac
+          have "essentially_equal G (p # cs) (as @ bs)"
+          by (rule factors_unique) (fact | simp)+
+
+      hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"
+          by (fast elim: essentially_equalE)
+      from this obtain ds
+          where "p # cs <~~> ds"
+          and dsassoc: "ds [\<sim>] (as @ bs)"
+          by auto
+
+      then have "p \<in> set ds"
+           by (simp add: perm_set_eq[symmetric])
+      with dsassoc
+           have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"
+           unfolding list_all2_conv_all_nth set_conv_nth
+           by force
+
+      from this obtain p'
+	  where "p' \<in> set (as@bs)"
+	  and pp': "p \<sim> p'" by auto
+
+      hence "p' \<in> set as \<or> p' \<in> set bs" by simp
+      moreover
+      {
+	assume p'elem: "p' \<in> set as"
+	with ascarr have [simp]: "p' \<in> carrier G" by fast
+
+	note pp'
+	also from afac p'elem
+	     have "p' divides a" by (rule factors_dividesI) fact+
+	finally
+	     have "p divides a" by simp
+      }
+      moreover
+      {
+	assume p'elem: "p' \<in> set bs"
+	with bscarr have [simp]: "p' \<in> carrier G" by fast
+
+	note pp'
+	also from bfac
+	     have "p' divides b" by (rule factors_dividesI) fact+
+	finally have "p divides b" by simp
+      }
+      ultimately
+	  show "p divides a \<or> p divides b" by fast
+    qed
+  qed
+qed
+
+
+subsection {* Greatest common divisors and lowest common multiples *}
+
+subsubsection {* Definitions *}
+
+constdefs (structure G)
+  isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
+  "x gcdof a b \<equiv> x divides a \<and> x divides b \<and> 
+                 (\<forall>y\<in>carrier G. (y divides a \<and> y divides b \<longrightarrow> y divides x))"
+
+  islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
+  "x lcmof a b \<equiv> a divides x \<and> b divides x \<and> 
+                 (\<forall>y\<in>carrier G. (a divides y \<and> b divides y \<longrightarrow> x divides y))"
+
+constdefs (structure G)
+  somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof a b"
+
+  somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
+
+constdefs (structure G)
+  "SomeGcd G A == ginf (division_rel G) A"
+
+
+locale gcd_condition_monoid = comm_monoid_cancel +
+  assumes gcdof_exists:
+          "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b"
+
+locale primeness_condition_monoid = comm_monoid_cancel +
+  assumes irreducible_prime:
+          "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"
+
+locale divisor_chain_condition_monoid = comm_monoid_cancel +
+  assumes division_wellfounded:
+          "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
+
+
+subsubsection {* Connections to \texttt{Lattice.thy} *}
+
+lemma gcdof_ggreatestLower:
+  fixes G (structure)
+  assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "(x \<in> carrier G \<and> x gcdof a b) =
+         ggreatest (division_rel G) x (Lower (division_rel G) {a, b})"
+unfolding isgcd_def ggreatest_def Lower_def elem_def
+proof (simp, safe)
+  fix xa
+  assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
+  assume r2[rule_format]: "\<forall>y\<in>carrier G. y divides a \<and> y divides b \<longrightarrow> y divides x"
+
+  assume "xa \<in> carrier G"  "x divides a"  "x divides b"
+  with carr
+  show "xa divides x"
+      by (fast intro: r1 r2)
+next
+  fix a' y
+  assume r1[rule_format]:
+         "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> l divides x} \<inter> carrier G.
+           xa divides x"
+  assume "y \<in> carrier G"  "y divides a"  "y divides b"
+  with carr
+       show "y divides x"
+       by (fast intro: r1)
+qed (simp, simp)
+
+lemma lcmof_gleastUpper:
+  fixes G (structure)
+  assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "(x \<in> carrier G \<and> x lcmof a b) =
+         gleast (division_rel G) x (Upper (division_rel G) {a, b})"
+unfolding islcm_def gleast_def Upper_def elem_def
+proof (simp, safe)
+  fix xa
+  assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
+  assume r2[rule_format]: "\<forall>y\<in>carrier G. a divides y \<and> b divides y \<longrightarrow> x divides y"
+
+  assume "xa \<in> carrier G"  "a divides x"  "b divides x"
+  with carr
+  show "x divides xa"
+      by (fast intro: r1 r2)
+next
+  fix a' y
+  assume r1[rule_format]:
+         "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides l} \<inter> carrier G.
+           x divides xa"
+  assume "y \<in> carrier G"  "a divides y"  "b divides y"
+  with carr
+       show "x divides y"
+       by (fast intro: r1)
+qed (simp, simp)
+
+lemma somegcd_gmeet:
+  fixes G (structure)
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "somegcd G a b = gmeet (division_rel G) a b"
+unfolding somegcd_def gmeet_def ginf_def
+by (simp add: gcdof_ggreatestLower[OF carr])
+
+lemma (in monoid) isgcd_divides_l:
+  assumes "a divides b"
+    and "a \<in> carrier G"  "b \<in> carrier G"
+  shows "a gcdof a b"
+using assms
+unfolding isgcd_def
+by fast
+
+lemma (in monoid) isgcd_divides_r:
+  assumes "b divides a"
+    and "a \<in> carrier G"  "b \<in> carrier G"
+  shows "b gcdof a b"
+using assms
+unfolding isgcd_def
+by fast
+
+
+subsubsection {* Existence of gcd and lcm *}
+
+lemma (in factorial_monoid) gcdof_exists:
+  assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+  shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"
+proof -
+  from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist)
+  from this obtain as
+      where ascarr: "set as \<subseteq> carrier G"
+      and afs: "wfactors G as a"
+      by auto
+  from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
+
+  from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist)
+  from this obtain bs
+      where bscarr: "set bs \<subseteq> carrier G"
+      and bfs: "wfactors G bs b"
+      by auto
+  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
+
+  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> 
+               fmset G cs = fmset G as #\<inter> fmset G bs"
+  proof (intro mset_wfactorsEx)
+    fix X
+    assume "X \<in> set_of (fmset G as #\<inter> fmset G bs)"
+    hence "X \<in> set_of (fmset G as)" by (simp add: multiset_inter_def)
+    hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
+    hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
+    from this obtain x
+        where X: "X = assocs G x"
+        and xas: "x \<in> set as"
+        by auto
+    with ascarr have xcarr: "x \<in> carrier G" by fast
+    from xas airr have xirr: "irreducible G x" by simp
+ 
+    from xcarr and xirr and X
+        show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
+  qed
+
+  from this obtain c cs
+      where ccarr: "c \<in> carrier G"
+      and cscarr: "set cs \<subseteq> carrier G" 
+      and csirr: "wfactors G cs c"
+      and csmset: "fmset G cs = fmset G as #\<inter> fmset G bs" by auto
+
+  have "c gcdof a b"
+  proof (simp add: isgcd_def, safe)
+    from csmset
+        have "fmset G cs \<le># fmset G as"
+        by (simp add: multiset_inter_def mset_le_def)
+    thus "c divides a" by (rule fmsubset_divides) fact+
+  next
+    from csmset
+        have "fmset G cs \<le># fmset G bs"
+        by (simp add: multiset_inter_def mset_le_def, force)
+    thus "c divides b" by (rule fmsubset_divides) fact+
+  next
+    fix y
+    assume ycarr: "y \<in> carrier G"
+    hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist)
+    from this obtain ys
+        where yscarr: "set ys \<subseteq> carrier G"
+        and yfs: "wfactors G ys y"
+        by auto
+
+    assume "y divides a"
+    hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
+
+    assume "y divides b"
+    hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
+
+    from ya yb csmset
+    have "fmset G ys \<le># fmset G cs" by (simp add: mset_le_def multiset_inter_count)
+    thus "y divides c" by (rule fmsubset_divides) fact+
+  qed
+
+  with ccarr
+      show "\<exists>c. c \<in> carrier G \<and> c gcdof a b" by fast
+qed
+
+lemma (in factorial_monoid) lcmof_exists:
+  assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+  shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"
+proof -
+  from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist)
+  from this obtain as
+      where ascarr: "set as \<subseteq> carrier G"
+      and afs: "wfactors G as a"
+      by auto
+  from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
+
+  from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist)
+  from this obtain bs
+      where bscarr: "set bs \<subseteq> carrier G"
+      and bfs: "wfactors G bs b"
+      by auto
+  from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
+
+  have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> 
+               fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
+  proof (intro mset_wfactorsEx)
+    fix X
+    assume "X \<in> set_of ((fmset G as - fmset G bs) + fmset G bs)"
+    hence "X \<in> set_of (fmset G as) \<or> X \<in> set_of (fmset G bs)"
+       by (cases "X :# fmset G bs", simp, simp)
+    moreover
+    {
+      assume "X \<in> set_of (fmset G as)"
+      hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
+      hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
+      from this obtain x
+          where xas: "x \<in> set as"
+          and X: "X = assocs G x" by auto
+
+      with ascarr have xcarr: "x \<in> carrier G" by fast
+      from xas airr have xirr: "irreducible G x" by simp
+
+      from xcarr and xirr and X
+          have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
+    }
+    moreover
+    {
+      assume "X \<in> set_of (fmset G bs)"
+      hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
+      hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
+      from this obtain x
+          where xbs: "x \<in> set bs"
+          and X: "X = assocs G x" by auto
+
+      with bscarr have xcarr: "x \<in> carrier G" by fast
+      from xbs birr have xirr: "irreducible G x" by simp
+
+      from xcarr and xirr and X
+          have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
+    }
+    ultimately
+    show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast
+  qed
+
+  from this obtain c cs
+      where ccarr: "c \<in> carrier G"
+      and cscarr: "set cs \<subseteq> carrier G" 
+      and csirr: "wfactors G cs c"
+      and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs" by auto
+
+  have "c lcmof a b"
+  proof (simp add: islcm_def, safe)
+    from csmset have "fmset G as \<le># fmset G cs" by (simp add: mset_le_def, force)
+    thus "a divides c" by (rule fmsubset_divides) fact+
+  next
+    from csmset have "fmset G bs \<le># fmset G cs" by (simp add: mset_le_def)
+    thus "b divides c" by (rule fmsubset_divides) fact+
+  next
+    fix y
+    assume ycarr: "y \<in> carrier G"
+    hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist)
+    from this obtain ys
+        where yscarr: "set ys \<subseteq> carrier G"
+        and yfs: "wfactors G ys y"
+        by auto
+
+    assume "a divides y"
+    hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
+
+    assume "b divides y"
+    hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
+
+    from ya yb csmset
+    have "fmset G cs \<le># fmset G ys"
+      apply (simp add: mset_le_def, clarify)
+      apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
+       apply simp
+      apply simp
+    done
+    thus "c divides y" by (rule fmsubset_divides) fact+
+  qed
+
+  with ccarr
+      show "\<exists>c. c \<in> carrier G \<and> c lcmof a b" by fast
+qed
+
+
+subsection {* Conditions for factoriality *}
+
+subsubsection {* Gcd condition *}
+
+lemma (in gcd_condition_monoid) division_glower_semilattice [simp]:
+  shows "glower_semilattice (division_rel G)"
+proof -
+  interpret gpartial_order ["division_rel G"] ..
+  show ?thesis
+  apply (unfold_locales, simp_all)
+  proof -
+    fix x y
+    assume carr: "x \<in> carrier G"  "y \<in> carrier G"
+    hence "\<exists>z. z \<in> carrier G \<and> z gcdof x y" by (rule gcdof_exists)
+    from this obtain z
+        where zcarr: "z \<in> carrier G"
+        and isgcd: "z gcdof x y"
+        by auto
+    with carr
+    have "ggreatest (division_rel G) z (Lower (division_rel G) {x, y})"
+        by (subst gcdof_ggreatestLower[symmetric], simp+)
+    thus "\<exists>z. ggreatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
+  qed
+qed
+
+lemma (in gcd_condition_monoid) gcdof_cong_l:
+  assumes a'a: "a' \<sim> a"
+    and agcd: "a gcdof b c"
+    and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "a' gcdof b c"
+proof -
+  note carr = a'carr carr'
+  interpret glower_semilattice ["division_rel G"] by simp
+  have "a' \<in> carrier G \<and> a' gcdof b c"
+    apply (simp add: gcdof_ggreatestLower carr')
+    apply (subst ggreatest_Lower_cong_l[of _ a])
+       apply (simp add: a'a)
+      apply (simp add: carr)
+     apply (simp add: carr)
+    apply (simp add: carr)
+    apply (simp add: gcdof_ggreatestLower[symmetric] agcd carr)
+  done
+  thus ?thesis ..
+qed
+
+lemma (in gcd_condition_monoid) gcd_closed [simp]:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "somegcd G a b \<in> carrier G"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet[OF carr])
+    apply (rule gmeet_closed[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_isgcd:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "(somegcd G a b) gcdof a b"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  from carr
+  have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
+    apply (subst gcdof_ggreatestLower, simp, simp)
+    apply (simp add: somegcd_gmeet[OF carr] gmeet_def)
+    apply (rule ginf_of_two_ggreatest[simplified], assumption+)
+  done
+  thus "(somegcd G a b) gcdof a b" by simp
+qed
+
+lemma (in gcd_condition_monoid) gcd_exists:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "\<exists>x\<in>carrier G. x = somegcd G a b"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet[OF carr])
+    apply (rule gmeet_closed[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_divides_l:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "(somegcd G a b) divides a"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet[OF carr])
+    apply (rule gmeet_left[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_divides_r:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "(somegcd G a b) divides b"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet[OF carr])
+    apply (rule gmeet_right[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_divides:
+  assumes sub: "z divides x"  "z divides y"
+    and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
+  shows "z divides (somegcd G x y)"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet L)
+    apply (rule gmeet_le[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_cong_l:
+  assumes xx': "x \<sim> x'"
+    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  shows "somegcd G x y \<sim> somegcd G x' y"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet carr)
+    apply (rule gmeet_cong_l[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_cong_r:
+  assumes carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
+    and yy': "y \<sim> y'"
+  shows "somegcd G x y \<sim> somegcd G x y'"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: somegcd_gmeet carr)
+    apply (rule gmeet_cong_r[simplified], fact+)
+  done
+qed
+
+(*
+lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
+  assumes carr: "b \<in> carrier G"
+  shows "asc_cong (\<lambda>a. somegcd G a b)"
+using carr
+unfolding CONG_def
+by clarsimp (blast intro: gcd_cong_l)
+
+lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
+  assumes carr: "a \<in> carrier G"
+  shows "asc_cong (\<lambda>b. somegcd G a b)"
+using carr
+unfolding CONG_def
+by clarsimp (blast intro: gcd_cong_r)
+
+lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] = 
+    assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
+*)
+
+lemma (in gcd_condition_monoid) gcdI:
+  assumes dvd: "a divides b"  "a divides c"
+    and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a"
+    and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
+  shows "a \<sim> somegcd G b c"
+apply (simp add: somegcd_def)
+apply (rule someI2_ex)
+ apply (rule exI[of _ a], simp add: isgcd_def)
+ apply (simp add: assms)
+apply (simp add: isgcd_def assms, clarify)
+apply (insert assms, blast intro: associatedI)
+done
+
+lemma (in gcd_condition_monoid) gcdI2:
+  assumes "a gcdof b c"
+    and "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
+  shows "a \<sim> somegcd G b c"
+using assms
+unfolding isgcd_def
+by (blast intro: gcdI)
+
+lemma (in gcd_condition_monoid) SomeGcd_ex:
+  assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
+  shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (simp add: SomeGcd_def)
+    apply (rule finite_ginf_closed[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_assoc:
+  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+  show ?thesis
+    apply (subst (2 3) somegcd_gmeet, (simp add: carr)+)
+    apply (simp add: somegcd_gmeet carr)
+    apply (rule gmeet_assoc[simplified], fact+)
+  done
+qed
+
+lemma (in gcd_condition_monoid) gcd_mult:
+  assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
+  shows "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
+proof - (* following Jacobson, Basic Algebra, p.140 *)
+  let ?d = "somegcd G a b"
+  let ?e = "somegcd G (c \<otimes> a) (c \<otimes> b)"
+  note carr[simp] = acarr bcarr ccarr
+  have dcarr: "?d \<in> carrier G" by simp
+  have ecarr: "?e \<in> carrier G" by simp
+  note carr = carr dcarr ecarr
+
+  have "?d divides a" by (simp add: gcd_divides_l)
+  hence cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)
+
+  have "?d divides b" by (simp add: gcd_divides_r)
+  hence cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)
+  
+  from cd'ca cd'cb
+      have cd'e: "c \<otimes> ?d divides ?e"
+      by (rule gcd_divides) simp+
+
+  hence "\<exists>u. u \<in> carrier G \<and> ?e = c \<otimes> ?d \<otimes> u"
+      by (elim dividesE, fast)
+  from this obtain u
+      where ucarr[simp]: "u \<in> carrier G"
+      and e_cdu: "?e = c \<otimes> ?d \<otimes> u"
+      by auto
+
+  note carr = carr ucarr
+
+  have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp+
+  hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> a = ?e \<otimes> x"
+      by (elim dividesE, fast)
+  from this obtain x
+      where xcarr: "x \<in> carrier G"
+      and ca_ex: "c \<otimes> a = ?e \<otimes> x"
+      by auto
+  with e_cdu
+      have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x" by simp
+
+  from ca_cdux xcarr
+       have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc)
+  then have "a = ?d \<otimes> u \<otimes> x" by (rule l_cancel[of c a]) (simp add: xcarr)+
+  hence du'a: "?d \<otimes> u divides a" by (rule dividesI[OF xcarr])
+
+  have "?e divides c \<otimes> b" by (intro gcd_divides_r, simp+)
+  hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> b = ?e \<otimes> x"
+      by (elim dividesE, fast)
+  from this obtain x
+      where xcarr: "x \<in> carrier G"
+      and cb_ex: "c \<otimes> b = ?e \<otimes> x"
+      by auto
+  with e_cdu
+      have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x" by simp
+
+  from cb_cdux xcarr
+      have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc)
+  with xcarr
+      have "b = ?d \<otimes> u \<otimes> x" by (intro l_cancel[of c b], simp+)
+  hence du'b: "?d \<otimes> u divides b" by (intro dividesI[OF xcarr])
+
+  from du'a du'b carr
+      have du'd: "?d \<otimes> u divides ?d"
+      by (intro gcd_divides, simp+)
+  hence uunit: "u \<in> Units G"
+  proof (elim dividesE)
+    fix v
+    assume vcarr[simp]: "v \<in> carrier G"
+    assume d: "?d = ?d \<otimes> u \<otimes> v"
+    have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact
+    also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)
+    finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .
+    hence i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp+
+    hence i1: "\<one> = v \<otimes> u" by (simp add: m_comm)
+    from vcarr i1[symmetric] i2[symmetric]
+        show "u \<in> Units G"
+        by (unfold Units_def, simp, fast)
+  qed
+
+  from e_cdu uunit
+      have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"
+      by (intro associatedI2[of u], simp+)
+  from this[symmetric]
+      show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp
+qed
+
+lemma (in monoid) assoc_subst:
+  assumes ab: "a \<sim> b"
+    and cP: "ALL a b. a : carrier G & b : carrier G & a \<sim> b
+      --> f a : carrier G & f b : carrier G & f a \<sim> f b"
+    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+  shows "f a \<sim> f b"
+  using assms by auto
+
+lemma (in gcd_condition_monoid) relprime_mult:
+  assumes abrelprime: "somegcd G a b \<sim> \<one>" and acrelprime: "somegcd G a c \<sim> \<one>"
+    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  shows "somegcd G a (b \<otimes> c) \<sim> \<one>"
+proof -
+  have "c = c \<otimes> \<one>" by simp
+  also from abrelprime[symmetric]
+       have "\<dots> \<sim> c \<otimes> somegcd G a b"
+	 by (rule assoc_subst) (simp add: mult_cong_r)+
+  also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by (rule gcd_mult) fact+
+  finally
+       have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp
+
+  from carr
+       have a: "a \<sim> somegcd G a (c \<otimes> a)"
+       by (fast intro: gcdI divides_prod_l)
+
+  have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)" by (simp add: m_comm)
+  also from a
+       have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"
+	 by (rule assoc_subst) (simp add: gcd_cong_l)+
+  also from gcd_assoc
+       have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"
+       by (rule assoc_subst) simp+
+  also from c[symmetric]
+       have "\<dots> \<sim> somegcd G a c"
+	 by (rule assoc_subst) (simp add: gcd_cong_r)+
+  also note acrelprime
+  finally
+       show "somegcd G a (b \<otimes> c) \<sim> \<one>" by simp
+qed
+
+lemma (in gcd_condition_monoid) primeness_condition:
+  "primeness_condition_monoid G"
+apply unfold_locales
+apply (rule primeI)
+ apply (elim irreducibleE, assumption)
+proof -
+  fix p a b
+  assume pcarr: "p \<in> carrier G" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
+    and pirr: "irreducible G p"
+    and pdvdab: "p divides a \<otimes> b"
+  from pirr
+      have pnunit: "p \<notin> Units G"
+      and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
+      by - (fast elim: irreducibleE)+
+
+  show "p divides a \<or> p divides b"
+  proof (rule ccontr, clarsimp)
+    assume npdvda: "\<not> p divides a"
+    with pcarr acarr
+    have "\<one> \<sim> somegcd G p a"
+    apply (intro gcdI, simp, simp, simp)
+      apply (fast intro: unit_divides)
+     apply (fast intro: unit_divides)
+    apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
+    apply (rule r, rule, assumption)
+    apply (rule properfactorI, assumption)
+    proof (rule ccontr, simp)
+      fix y
+      assume ycarr: "y \<in> carrier G"
+      assume "p divides y"
+      also assume "y divides a"
+      finally
+          have "p divides a" by (simp add: pcarr ycarr acarr)
+      with npdvda
+          show "False" ..
+    qed simp+
+    with pcarr acarr
+        have pa: "somegcd G p a \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed)
+
+    assume npdvdb: "\<not> p divides b"
+    with pcarr bcarr
+    have "\<one> \<sim> somegcd G p b"
+    apply (intro gcdI, simp, simp, simp)
+      apply (fast intro: unit_divides)
+     apply (fast intro: unit_divides)
+    apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
+    apply (rule r, rule, assumption)
+    apply (rule properfactorI, assumption)
+    proof (rule ccontr, simp)
+      fix y
+      assume ycarr: "y \<in> carrier G"
+      assume "p divides y"
+      also assume "y divides b"
+      finally have "p divides b" by (simp add: pcarr ycarr bcarr)
+      with npdvdb
+          show "False" ..
+    qed simp+
+    with pcarr bcarr
+        have pb: "somegcd G p b \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed)
+
+    from pcarr acarr bcarr pdvdab
+        have "p gcdof p (a \<otimes> b)" by (fast intro: isgcd_divides_l)
+
+    with pcarr acarr bcarr
+         have "p \<sim> somegcd G p (a \<otimes> b)" by (fast intro: gcdI2)
+    also from pa pb pcarr acarr bcarr
+         have "somegcd G p (a \<otimes> b) \<sim> \<one>" by (rule relprime_mult)
+    finally have "p \<sim> \<one>" by (simp add: pcarr acarr bcarr)
+
+    with pcarr
+        have "p \<in> Units G" by (fast intro: assoc_unit_l)
+    with pnunit
+        show "False" ..
+  qed
+qed
+
+interpretation gcd_condition_monoid \<subseteq> primeness_condition_monoid
+  by (rule primeness_condition)
+
+
+subsubsection {* Divisor chain condition *}
+
+lemma (in divisor_chain_condition_monoid) wfactors_exist:
+  assumes acarr: "a \<in> carrier G"
+  shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
+proof -
+  have r[rule_format]: "a \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"
+    apply (rule wf_induct[OF division_wellfounded])
+  proof -
+    fix x
+    assume ih: "\<forall>y. (y, x) \<in> {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}
+                    \<longrightarrow> y \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y)"
+
+    show "x \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as x)"
+    apply clarify
+    apply (cases "x \<in> Units G")
+     apply (rule exI[of _ "[]"], simp)
+    apply (cases "irreducible G x")
+     apply (rule exI[of _ "[x]"], simp add: wfactors_def)
+    proof -
+      assume xcarr: "x \<in> carrier G"
+        and xnunit: "x \<notin> Units G"
+        and xnirr: "\<not> irreducible G x"
+      hence "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G"
+        apply - apply (rule ccontr, simp)
+        apply (subgoal_tac "irreducible G x", simp)
+        apply (rule irreducibleI, simp, simp)
+      done
+      from this obtain y
+          where ycarr: "y \<in> carrier G"
+          and ynunit: "y \<notin> Units G"
+          and pfyx: "properfactor G y x"
+          by auto
+
+      have ih':
+           "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk>
+                \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"
+          by (rule ih[rule_format, simplified]) (simp add: xcarr)+
+
+      from ycarr pfyx
+          have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"
+          by (rule ih')
+      from this obtain ys
+          where yscarr: "set ys \<subseteq> carrier G"
+          and yfs: "wfactors G ys y"
+          by auto
+
+      from pfyx
+          have "y divides x"
+          and nyx: "\<not> y \<sim> x"
+          by - (fast elim: properfactorE2)+
+      hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
+          by (fast elim: dividesE)
+
+      from this obtain z
+          where zcarr: "z \<in> carrier G"
+          and x: "x = y \<otimes> z"
+          by auto
+
+      from zcarr ycarr
+      have "properfactor G z x"
+        apply (subst x)
+        apply (intro properfactorI3[of _ _ y])
+         apply (simp add: m_comm)
+        apply (simp add: ynunit)+
+      done
+      with zcarr
+          have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as z"
+          by (rule ih')
+      from this obtain zs
+          where zscarr: "set zs \<subseteq> carrier G"
+          and zfs: "wfactors G zs z"
+          by auto
+
+      from yscarr zscarr
+          have xscarr: "set (ys@zs) \<subseteq> carrier G" by simp
+      from yfs zfs ycarr zcarr yscarr zscarr
+          have "wfactors G (ys@zs) (y\<otimes>z)" by (rule wfactors_mult)
+      hence "wfactors G (ys@zs) x" by (simp add: x)
+
+      from xscarr this
+          show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x" by fast
+    qed
+  qed
+
+  from acarr
+      show ?thesis by (rule r)
+qed
+
+
+subsubsection {* Primeness condition *}
+
+lemma (in comm_monoid_cancel) multlist_prime_pos:
+  assumes carr: "a \<in> carrier G"  "set as \<subseteq> carrier G"
+    and aprime: "prime G a"
+    and "a divides (foldr (op \<otimes>) as \<one>)"
+  shows "\<exists>i<length as. a divides (as!i)"
+proof -
+  have r[rule_format]:
+       "set as \<subseteq> carrier G \<and> a divides (foldr (op \<otimes>) as \<one>)
+        \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"
+    apply (induct as)
+     apply clarsimp defer 1
+     apply clarsimp defer 1
+  proof -
+    assume "a divides \<one>"
+    with carr
+        have "a \<in> Units G"
+        by (fast intro: divides_unit[of a \<one>])
+    with aprime
+        show "False" by (elim primeE, simp)
+  next
+    fix aa as
+    assume ih[rule_format]: "a divides foldr op \<otimes> as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"
+      and carr': "aa \<in> carrier G"  "set as \<subseteq> carrier G"
+      and "a divides aa \<otimes> foldr op \<otimes> as \<one>"
+    with carr aprime
+        have "a divides aa \<or> a divides foldr op \<otimes> as \<one>"
+        by (intro prime_divides) simp+
+    moreover {
+      assume "a divides aa"
+      hence p1: "a divides (aa#as)!0" by simp
+      have "0 < Suc (length as)" by simp
+      with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast
+    }
+    moreover {
+      assume "a divides foldr op \<otimes> as \<one>"
+      hence "\<exists>i. i < length as \<and> a divides as ! i" by (rule ih)
+      from this obtain i where "a divides as ! i" and len: "i < length as" by auto
+      hence p1: "a divides (aa#as) ! (Suc i)" by simp
+      from len have "Suc i < Suc (length as)" by simp
+      with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by force
+   }
+   ultimately
+      show "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast
+  qed
+
+  from assms
+      show ?thesis
+      by (intro r, safe)
+qed
+
+lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
+  "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> 
+           wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
+apply (induct as)
+apply clarsimp defer 1
+apply clarsimp defer 1
+proof -
+  fix a as'
+  assume acarr: "a \<in> carrier G"
+    and "wfactors G [] a"
+  hence aunit: "a \<in> Units G"
+    apply (elim wfactorsE)
+    apply (simp, rule assoc_unit_r[of "\<one>"], simp+)
+  done
+
+  assume "set as' \<subseteq> carrier G"  "wfactors G as' a"
+  with aunit
+      have "as' = []"
+      by (intro unit_wfactors_empty[of a])
+  thus "essentially_equal G [] as'" by simp
+next
+  fix a as ah as'
+  assume ih[rule_format]: 
+         "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> 
+                  wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
+    and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
+    and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
+    and afs: "wfactors G (ah # as) a"
+    and afs': "wfactors G as' a"
+  hence ahdvda: "ah divides a"
+      by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
+  hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
+  from this obtain a'
+      where a'carr: "a' \<in> carrier G"
+      and a: "a = ah \<otimes> a'"
+      by auto
+  have a'fs: "wfactors G as a'"
+    apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
+    apply (simp add: a, insert ascarr a'carr)
+    apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
+  done
+
+  from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
+  with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)
+
+  note carr [simp] = acarr ahcarr ascarr as'carr a'carr
+
+  note ahdvda
+  also from afs'
+       have "a divides (foldr (op \<otimes>) as' \<one>)"
+       by (elim wfactorsE associatedE, simp)
+  finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp
+
+  with ahprime
+      have "\<exists>i<length as'. ah divides as'!i"
+      by (intro multlist_prime_pos, simp+)
+  from this obtain i
+      where len: "i<length as'" and ahdvd: "ah divides as'!i"
+      by auto
+  from afs' carr have irrasi: "irreducible G (as'!i)"
+      by (fast intro: nth_mem[OF len] elim: wfactorsE)
+  from len carr
+      have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
+  note carr = carr asicarr
+
+  from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
+  from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
+
+  with carr irrasi[simplified asi]
+      have asiah: "as'!i \<sim> ah" apply -
+    apply (elim irreducible_prodE[of "ah" "x"], assumption+)
+     apply (rule associatedI2[of x], assumption+)
+    apply (rule irreducibleE[OF ahirr], simp)
+  done
+
+  note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
+  note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
+  note carr = carr partscarr
+
+  have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
+    apply (intro wfactors_prod_exists)
+    using setparts afs' by (fast elim: wfactorsE, simp)
+  from this obtain aa_1
+      where aa1carr: "aa_1 \<in> carrier G"
+      and aa1fs: "wfactors G (take i as') aa_1"
+      by auto
+
+  have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
+    apply (intro wfactors_prod_exists)
+    using setparts afs' by (fast elim: wfactorsE, simp)
+  from this obtain aa_2
+      where aa2carr: "aa_2 \<in> carrier G"
+      and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
+      by auto
+
+  note carr = carr aa1carr[simp] aa2carr[simp]
+
+  from aa1fs aa2fs
+      have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
+      by (intro wfactors_mult, simp+)
+  hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
+      apply (intro wfactors_mult_single)
+      using setparts afs'
+      by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+)
+
+  from aa2carr carr aa1fs aa2fs
+      have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
+    apply (intro wfactors_mult_single)
+        apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
+       apply (fast intro: nth_mem[OF len])
+      apply fast
+     apply fast
+    apply assumption
+  done
+  with len carr aa1carr aa2carr aa1fs
+      have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
+    apply (intro wfactors_mult)
+         apply fast
+        apply (simp, (fast intro: nth_mem[OF len])?)+
+  done
+
+  from len
+      have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
+      by (simp add: drop_Suc_conv_tl)
+  with carr
+      have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
+      by simp
+
+  with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
+      have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
+    apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'"  "as'"])
+          apply fast+
+        apply (simp, fast)
+  done
+  then
+  have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
+    apply (simp add: m_assoc[symmetric])
+    apply (simp add: m_comm)
+  done
+  from carr asiah
+  have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
+      apply (intro mult_cong_l)
+      apply (fast intro: associated_sym, simp+)
+  done
+  also note t1
+  finally
+      have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
+
+  with carr aa1carr aa2carr a'carr nth_mem[OF len]
+      have a': "aa_1 \<otimes> aa_2 \<sim> a'"
+      by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
+
+  note v1
+  also note a'
+  finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp
+
+  from a'fs this carr
+      have "essentially_equal G as (take i as' @ drop (Suc i) as')"
+      by (intro ih[of a']) simp
+
+  hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+    apply (elim essentially_equalE) apply (fastsimp intro: essentially_equalI)
+  done
+
+  from carr
+  have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
+                                 (as' ! i # take i as' @ drop (Suc i) as')"
+  proof (intro essentially_equalI)
+    show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
+        by simp
+  next show "ah # take i as' @ drop (Suc i) as' [\<sim>]
+       as' ! i # take i as' @ drop (Suc i) as'"
+    apply (simp add: list_all2_append)
+    apply (simp add: asiah[symmetric] ahcarr asicarr)
+    done
+  qed
+
+  note ee1
+  also note ee2
+  also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
+                                 (take i as' @ as' ! i # drop (Suc i) as')"
+    apply (intro essentially_equalI)
+    apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> 
+                        take i as' @ as' ! i # drop (Suc i) as'")
+apply simp
+     apply (rule perm_append_Cons)
+    apply simp
+  done
+  finally
+      have "essentially_equal G (ah # as) 
+                                (take i as' @ as' ! i # drop (Suc i) as')" by simp
+
+  thus "essentially_equal G (ah # as) as'" by (subst as', assumption)
+qed
+
+lemma (in primeness_condition_monoid) wfactors_unique:
+  assumes "wfactors G as a"  "wfactors G as' a"
+    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
+  shows "essentially_equal G as as'"
+apply (rule wfactors_unique__hlp_induct[rule_format, of a])
+apply (simp add: assms)
+done
+
+
+subsubsection {* Application to factorial monoids *}
+
+text {* Number of factors for wellfoundedness *}
+
+constdefs
+  factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat"
+  "factorcount G a == THE c. (ALL as. set as \<subseteq> carrier G \<and> 
+                                      wfactors G as a \<longrightarrow> c = length as)"
+
+lemma (in monoid) ee_length:
+  assumes ee: "essentially_equal G as bs"
+  shows "length as = length bs"
+apply (rule essentially_equalE[OF ee])
+apply (subgoal_tac "length as = length fs1'")
+ apply (simp add: list_all2_lengthD)
+apply (simp add: perm_length)
+done
+
+lemma (in factorial_monoid) factorcount_exists:
+  assumes carr[simp]: "a \<in> carrier G"
+  shows "EX c. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"
+proof -
+  have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (intro wfactors_exist, simp)
+  from this obtain as
+      where ascarr[simp]: "set as \<subseteq> carrier G"
+      and afs: "wfactors G as a"
+      by (auto simp del: carr)
+
+  have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
+  proof clarify
+    fix as'
+    assume [simp]: "set as' \<subseteq> carrier G"
+      and bfs: "wfactors G as' a"
+    from afs bfs
+        have "essentially_equal G as as'"
+        by (intro ee_wfactorsI[of a a as as'], simp+)
+    thus "length as = length as'" by (rule ee_length)
+  qed
+  thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
+qed
+
+lemma (in factorial_monoid) factorcount_unique:
+  assumes afs: "wfactors G as a"
+    and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"
+  shows "factorcount G a = length as"
+proof -
+  have "EX ac. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" by (rule factorcount_exists, simp)
+  from this obtain ac where
+      alen: "ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
+      by auto
+  have ac: "ac = factorcount G a"
+    apply (simp add: factorcount_def)
+    apply (rule theI2)
+      apply (rule alen)
+     apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
+    apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
+  done
+
+  from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
+  with ac show ?thesis by simp
+qed
+
+lemma (in factorial_monoid) divides_fcount:
+  assumes dvd: "a divides b"
+    and acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
+  shows "factorcount G a <= factorcount G b"
+apply (rule dividesE[OF dvd])
+proof -
+  fix c
+  from assms
+      have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast
+  from this obtain as
+      where ascarr: "set as \<subseteq> carrier G"
+      and afs: "wfactors G as a"
+      by auto
+  with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique)
+
+  assume ccarr: "c \<in> carrier G"
+  hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast
+  from this obtain cs
+      where cscarr: "set cs \<subseteq> carrier G"
+      and cfs: "wfactors G cs c"
+      by auto
+
+  note [simp] = acarr bcarr ccarr ascarr cscarr
+
+  assume b: "b = a \<otimes> c"
+  from afs cfs
+      have "wfactors G (as@cs) (a \<otimes> c)" by (intro wfactors_mult, simp+)
+  with b have "wfactors G (as@cs) b" by simp
+  hence "factorcount G b = length (as@cs)" by (intro factorcount_unique, simp+)
+  hence "factorcount G b = length as + length cs" by simp
+  with fca show ?thesis by simp
+qed
+
+lemma (in factorial_monoid) associated_fcount:
+  assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
+    and asc: "a \<sim> b"
+  shows "factorcount G a = factorcount G b"
+apply (rule associatedE[OF asc])
+apply (drule divides_fcount[OF _ acarr bcarr])
+apply (drule divides_fcount[OF _ bcarr acarr])
+apply simp
+done
+
+lemma (in factorial_monoid) properfactor_fcount:
+  assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
+    and pf: "properfactor G a b"
+  shows "factorcount G a < factorcount G b"
+apply (rule properfactorE[OF pf], elim dividesE)
+proof -
+  fix c
+  from assms
+  have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast
+  from this obtain as
+      where ascarr: "set as \<subseteq> carrier G"
+      and afs: "wfactors G as a"
+      by auto
+  with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique)
+
+  assume ccarr: "c \<in> carrier G"
+  hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast
+  from this obtain cs
+      where cscarr: "set cs \<subseteq> carrier G"
+      and cfs: "wfactors G cs c"
+      by auto
+
+  assume b: "b = a \<otimes> c"
+
+  have "wfactors G (as@cs) (a \<otimes> c)" by (rule wfactors_mult) fact+
+  with b
+      have "wfactors G (as@cs) b" by simp
+  with ascarr cscarr bcarr
+      have "factorcount G b = length (as@cs)" by (simp add: factorcount_unique)
+  hence fcb: "factorcount G b = length as + length cs" by simp
+
+  assume nbdvda: "\<not> b divides a"
+  have "c \<notin> Units G"
+  proof (rule ccontr, simp)
+    assume cunit:"c \<in> Units G"
+
+    have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" by (simp add: b)
+    also with ccarr acarr cunit
+        have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
+    also with ccarr cunit
+        have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
+    also with acarr
+        have "\<dots> = a" by simp
+    finally have "a = b \<otimes> inv c" by simp
+    with ccarr cunit
+    have "b divides a" by (fast intro: dividesI[of "inv c"])
+    with nbdvda show False by simp
+  qed
+
+  with cfs have "length cs > 0"
+  apply -
+  apply (rule ccontr, simp)
+  proof -
+    assume "wfactors G [] c"
+    hence "\<one> \<sim> c" by (elim wfactorsE, simp)
+    with ccarr
+        have cunit: "c \<in> Units G" by (intro assoc_unit_r[of "\<one>" "c"], simp+)
+    assume "c \<notin> Units G"
+    with cunit show "False" by simp
+  qed
+
+  with fca fcb show ?thesis by simp
+qed
+
+interpretation factorial_monoid \<subseteq> divisor_chain_condition_monoid
+apply unfold_locales
+apply (rule wfUNIVI)
+apply (rule measure_induct[of "factorcount G"])
+apply simp (* slow *) (*
+  [1]Applying congruence rule:
+  \<lbrakk>factorcount G y < factorcount G xa \<equiv> ?P'; ?P' \<Longrightarrow> P y \<equiv> ?Q'\<rbrakk> \<Longrightarrow> factorcount G y < factorcount G xa \<longrightarrow> P y \<equiv> ?P' \<longrightarrow> ?Q'
+
+  trace_simp_depth_limit exceeded!
+*)
+proof -
+  fix P x
+  assume r1[rule_format]:
+         "\<forall>y. (\<forall>z. z \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G z y \<longrightarrow> P z) \<longrightarrow> P y"
+    and r2[rule_format]: "\<forall>y. factorcount G y < factorcount G x \<longrightarrow> P y"
+  show "P x"
+    apply (rule r1)
+    apply (rule r2)
+    apply (rule properfactor_fcount, simp+)
+  done
+qed
+
+interpretation factorial_monoid \<subseteq> primeness_condition_monoid
+  by (unfold_locales, rule irreducible_is_prime)
+
+
+lemma (in factorial_monoid) primeness_condition:
+  shows "primeness_condition_monoid G"
+by unfold_locales
+
+lemma (in factorial_monoid) gcd_condition [simp]:
+  shows "gcd_condition_monoid G"
+by (unfold_locales, rule gcdof_exists)
+
+interpretation factorial_monoid \<subseteq> gcd_condition_monoid
+  by (unfold_locales, rule gcdof_exists)
+
+lemma (in factorial_monoid) division_glattice [simp]:
+  shows "glattice (division_rel G)"
+proof -
+  interpret glower_semilattice ["division_rel G"] by simp
+
+  show "glattice (division_rel G)"
+  apply (unfold_locales, simp_all)
+  proof -
+    fix x y
+    assume carr: "x \<in> carrier G"  "y \<in> carrier G"
+
+    hence "\<exists>z. z \<in> carrier G \<and> z lcmof x y" by (rule lcmof_exists)
+    from this obtain z
+        where zcarr: "z \<in> carrier G"
+        and isgcd: "z lcmof x y"
+        by auto
+    with carr
+    have "gleast (division_rel G) z (Upper (division_rel G) {x, y})"
+        by (simp add: lcmof_gleastUpper[symmetric])
+    thus "\<exists>z. gleast (division_rel G) z (Upper (division_rel G) {x, y})" by fast
+  qed
+qed
+
+
+subsection {* Factoriality theorems *}
+
+theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
+  shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = 
+         factorial_monoid G"
+apply rule
+proof clarify
+  assume dcc: "divisor_chain_condition_monoid G"
+     and pc: "primeness_condition_monoid G"
+  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
+  interpret primeness_condition_monoid ["G"] by (rule pc)
+
+  show "factorial_monoid G"
+      by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
+next
+  assume fm: "factorial_monoid G"
+  interpret factorial_monoid ["G"] by (rule fm)
+  show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
+      by rule unfold_locales
+qed
+
+theorem factorial_condition_two: (* Jacobson theorem 2.22 *)
+  shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
+apply rule
+proof clarify
+    assume dcc: "divisor_chain_condition_monoid G"
+     and gc: "gcd_condition_monoid G"
+  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
+  interpret gcd_condition_monoid ["G"] by (rule gc)
+  show "factorial_monoid G"
+      by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
+next
+  assume fm: "factorial_monoid G"
+  interpret factorial_monoid ["G"] by (rule fm)
+  show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
+      by rule unfold_locales
+qed
+
+end
diff -r ef4b26efa8b6 -r ed7a2e0fab59 src/HOL/Algebra/GLattice.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/GLattice.thy	Tue Jul 29 16:19:49 2008 +0200
@@ -0,0 +1,1181 @@
+(*
+  Title:     HOL/Algebra/Lattice.thy
+  Id:        $Id$
+  Author:    Clemens Ballarin, started 7 November 2003
+  Copyright: Clemens Ballarin
+*)
+
+theory GLattice imports Congruence begin
+
+(* FIXME: unify with Lattice.thy *)
+
+
+section {* Orders and Lattices *}
+
+subsection {* Partial Orders *}
+
+record 'a gorder = "'a eq_object" +
+  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
+
+locale gpartial_order = equivalence L +
+  assumes le_refl [intro, simp]:
+      "x \<in> carrier L ==> x \<sqsubseteq> x"
+    and le_anti_sym [intro]:
+      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
+    and le_trans [trans]:
+      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
+    and le_cong:
+      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
+
+constdefs (structure L)
+  glless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
+  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
+
+
+subsubsection {* The order relation *}
+
+context gpartial_order begin
+
+lemma le_cong_l [intro, trans]:
+  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+  by (auto intro: le_cong [THEN iffD2])
+
+lemma le_cong_r [intro, trans]:
+  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+  by (auto intro: le_cong [THEN iffD1])
+
+lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
+  by (simp add: le_cong_l)
+
+end
+
+lemma gllessI:
+  fixes R (structure)
+  assumes "x \<sqsubseteq> y" and "~(x .= y)"
+  shows "x \<sqsubset> y"
+  using assms
+  unfolding glless_def
+  by simp
+
+lemma gllessD1:
+  fixes R (structure)
+  assumes "x \<sqsubset> y"
+  shows "x \<sqsubseteq> y"
+  using assms
+  unfolding glless_def
+  by simp
+
+lemma gllessD2:
+  fixes R (structure)
+  assumes "x \<sqsubset> y"
+  shows "\<not> (x .= y)"
+  using assms
+  unfolding glless_def
+  by simp
+
+lemma gllessE:
+  fixes R (structure)
+  assumes p: "x \<sqsubset> y"
+    and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+  using p
+  by (blast dest: gllessD1 gllessD2 e)
+
+(*
+lemma (in gpartial_order) lless_cong_l [trans]:
+  assumes xx': "x \<doteq> x'"
+    and xy: "x' \<sqsubset> y"
+    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubseteq> y"
+using xy
+unfolding lless_def
+proof clarify
+  note xx'
+  also assume "x' \<sqsubseteq> y"
+  finally show "x \<sqsubseteq> y" by (simp add: carr)
+qed
+*)
+
+lemma (in gpartial_order) glless_cong_l [trans]:
+  assumes xx': "x .= x'"
+    and xy: "x' \<sqsubset> y"
+    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubset> y"
+  using assms
+  apply (elim gllessE, intro gllessI)
+  apply (iprover intro: le_cong_l)
+  apply (iprover intro: trans sym)
+  done
+
+(*
+lemma (in gpartial_order) lless_cong_r:
+  assumes xy: "x \<sqsubset> y"
+    and  yy': "y \<doteq> y'"
+    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+  shows "x \<sqsubseteq> y'"
+using xy
+unfolding lless_def
+proof clarify
+  assume "x \<sqsubseteq> y"
+  also note yy'
+  finally show "x \<sqsubseteq> y'" by (simp add: carr)
+qed
+*)
+
+lemma (in gpartial_order) glless_cong_r [trans]:
+  assumes xy: "x \<sqsubset> y"
+    and  yy': "y .= y'"
+    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+  shows "x \<sqsubset> y'"
+  using assms
+  apply (elim gllessE, intro gllessI)
+  apply (iprover intro: le_cong_r)
+  apply (iprover intro: trans sym)
+  done
+
+(*
+lemma (in gpartial_order) glless_antisym:
+  assumes "a \<in> carrier L" "b \<in> carrier L"
+    and "a \<sqsubset> b" "b \<sqsubset> a"
+  shows "a \<doteq> b"
+  using assms
+  by (elim gllessE) (rule gle_anti_sym)
+
+lemma (in gpartial_order) glless_trans [trans]:
+  assumes "a .\<sqsubset> b" "b .\<sqsubset> c"
+    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
+  shows "a .\<sqsubset> c"
+using assms
+apply (elim gllessE, intro gllessI)
+ apply (iprover dest: le_trans)
+proof (rule ccontr, simp)
+  assume ab: "a \<sqsubseteq> b" and bc: "b \<sqsubseteq> c"
+    and ac: "a \<doteq> c"
+    and nbc: "\<not> b \<doteq> c"
+  note ac[symmetric]
+  also note ab
+  finally have "c \<sqsubseteq> b" by simp
+  with bc have "b \<doteq> c" by (iprover intro: gle_anti_sym carr)
+  with nbc
+      show "False" by simp
+qed
+*)
+
+subsubsection {* Upper and lower bounds of a set *}
+
+constdefs (structure L)
+  Upper :: "[_, 'a set] => 'a set"
+  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
+
+  Lower :: "[_, 'a set] => 'a set"
+  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
+
+lemma Upper_closed [intro!, simp]:
+  "Upper L A \<subseteq> carrier L"
+  by (unfold Upper_def) clarify
+
+lemma Upper_memD [dest]:
+  fixes L (structure)
+  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
+  by (unfold Upper_def) blast
+
+lemma (in gpartial_order) Upper_elemD [dest]:
+  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
+  unfolding Upper_def elem_def
+  by (blast dest: sym)
+
+lemma Upper_memI:
+  fixes L (structure)
+  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
+  by (unfold Upper_def) blast
+
+lemma (in gpartial_order) Upper_elemI:
+  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
+  unfolding Upper_def by blast
+
+lemma Upper_antimono:
+  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
+  by (unfold Upper_def) blast
+
+lemma (in gpartial_order) Upper_is_closed [simp]:
+  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
+  by (rule is_closedI) (blast intro: Upper_memI)+
+
+lemma (in gpartial_order) Upper_mem_cong:
+  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
+    and aa': "a .= a'"
+    and aelem: "a \<in> Upper L A"
+  shows "a' \<in> Upper L A"
+proof (rule Upper_memI[OF _ a'carr])
+  fix y
+  assume yA: "y \<in> A"
+  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
+  also note aa'
+  finally
+      show "y \<sqsubseteq> a'"
+      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
+qed
+
+lemma (in gpartial_order) Upper_cong:
+  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "Upper L A = Upper L A'"
+unfolding Upper_def
+apply rule
+ apply (rule, clarsimp) defer 1
+ apply (rule, clarsimp) defer 1
+proof -
+  fix x a'
+  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
+    and a'A': "a' \<in> A'"
+  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
+
+  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
+  from this obtain a
+      where aA: "a \<in> A"
+      and a'a: "a' .= a"
+      by auto
+  note [simp] = subsetD[OF Acarr aA] carr
+
+  note a'a
+  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
+  finally show "a' \<sqsubseteq> x" by simp
+next
+  fix x a
+  assume carr: "x \<in> carrier L" "a \<in> carrier L"
+    and aA: "a \<in> A"
+  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
+
+  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
+  from this obtain a'
+      where a'A': "a' \<in> A'"
+      and aa': "a .= a'"
+      by auto
+  note [simp] = subsetD[OF A'carr a'A'] carr
+
+  note aa'
+  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
+  finally show "a \<sqsubseteq> x" by simp
+qed
+
+lemma Lower_closed [intro!, simp]:
+  "Lower L A \<subseteq> carrier L"
+  by (unfold Lower_def) clarify
+
+lemma Lower_memD [dest]:
+  fixes L (structure)
+  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
+  by (unfold Lower_def) blast
+
+lemma Lower_memI:
+  fixes L (structure)
+  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
+  by (unfold Lower_def) blast
+
+lemma Lower_antimono:
+  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
+  by (unfold Lower_def) blast
+
+lemma (in gpartial_order) Lower_is_closed [simp]:
+  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
+  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
+
+lemma (in gpartial_order) Lower_mem_cong:
+  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
+    and aa': "a .= a'"
+    and aelem: "a \<in> Lower L A"
+  shows "a' \<in> Lower L A"
+using assms Lower_closed[of L A]
+by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
+
+lemma (in gpartial_order) Lower_cong:
+  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "Lower L A = Lower L A'"
+using Lower_memD[of y]
+unfolding Lower_def
+apply safe
+ apply clarsimp defer 1
+ apply clarsimp defer 1
+proof -
+  fix x a'
+  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
+    and a'A': "a' \<in> A'"
+  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
+  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
+
+  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
+  from this obtain a
+      where aA: "a \<in> A"
+      and a'a: "a' .= a"
+      by auto
+
+  from aA and subsetD[OF Acarr aA]
+      have "x \<sqsubseteq> a" by (rule aLxCond)
+  also note a'a[symmetric]
+  finally
+      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
+next
+  fix x a
+  assume carr: "x \<in> carrier L" "a \<in> carrier L"
+    and aA: "a \<in> A"
+  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
+  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
+
+  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
+  from this obtain a'
+      where a'A': "a' \<in> A'"
+      and aa': "a .= a'"
+      by auto
+  from a'A' and subsetD[OF A'carr a'A']
+      have "x \<sqsubseteq> a'" by (rule a'LxCond)
+  also note aa'[symmetric]
+  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
+qed
+
+
+subsubsection {* Least and greatest, as predicate *}
+
+constdefs (structure L)
+  gleast :: "[_, 'a, 'a set] => bool"
+  "gleast L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
+
+  ggreatest :: "[_, 'a, 'a set] => bool"
+  "ggreatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
+
+lemma gleast_closed [intro, simp]:
+  "gleast L l A ==> l \<in> carrier L"
+  by (unfold gleast_def) fast
+
+lemma gleast_mem:
+  "gleast L l A ==> l \<in> A"
+  by (unfold gleast_def) fast
+
+lemma (in gpartial_order) gleast_unique:
+  "[| gleast L x A; gleast L y A |] ==> x .= y"
+  by (unfold gleast_def) blast
+
+lemma gleast_le:
+  fixes L (structure)
+  shows "[| gleast L x A; a \<in> A |] ==> x \<sqsubseteq> a"
+  by (unfold gleast_def) fast
+
+lemma (in gpartial_order) gleast_cong:
+  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> gleast L x A = gleast L x' A"
+  by (unfold gleast_def) (auto dest: sym)
+
+text {* @{const gleast} is not congruent in the second parameter for 
+  @{term [locale=gpartial_order] "A {.=} A'"} *}
+
+lemma (in gpartial_order) gleast_Upper_cong_l:
+  assumes "x .= x'"
+    and "x \<in> carrier L" "x' \<in> carrier L"
+    and "A \<subseteq> carrier L"
+  shows "gleast L x (Upper L A) = gleast L x' (Upper L A)"
+  apply (rule gleast_cong) using assms by auto
+
+lemma (in gpartial_order) gleast_Upper_cong_r:
+  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
+    and AA': "A {.=} A'"
+  shows "gleast L x (Upper L A) = gleast L x (Upper L A')"
+apply (subgoal_tac "Upper L A = Upper L A'", simp)
+by (rule Upper_cong) fact+
+
+lemma gleast_UpperI:
+  fixes L (structure)
+  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
+    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
+    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
+  shows "gleast L s (Upper L A)"
+proof -
+  have "Upper L A \<subseteq> carrier L" by simp
+  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
+  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
+  ultimately show ?thesis by (simp add: gleast_def)
+qed
+
+lemma gleast_Upper_above:
+  fixes L (structure)
+  shows "[| gleast L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
+  by (unfold gleast_def) blast
+
+lemma ggreatest_closed [intro, simp]:
+  "ggreatest L l A ==> l \<in> carrier L"
+  by (unfold ggreatest_def) fast
+
+lemma ggreatest_mem:
+  "ggreatest L l A ==> l \<in> A"
+  by (unfold ggreatest_def) fast
+
+lemma (in gpartial_order) ggreatest_unique:
+  "[| ggreatest L x A; ggreatest L y A |] ==> x .= y"
+  by (unfold ggreatest_def) blast
+
+lemma ggreatest_le:
+  fixes L (structure)
+  shows "[| ggreatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
+  by (unfold ggreatest_def) fast
+
+lemma (in gpartial_order) ggreatest_cong:
+  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
+  ggreatest L x A = ggreatest L x' A"
+  by (unfold ggreatest_def) (auto dest: sym)
+
+text {* @{const ggreatest} is not congruent in the second parameter for 
+  @{term [locale=gpartial_order] "A {.=} A'"} *}
+
+lemma (in gpartial_order) ggreatest_Lower_cong_l:
+  assumes "x .= x'"
+    and "x \<in> carrier L" "x' \<in> carrier L"
+    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
+  shows "ggreatest L x (Lower L A) = ggreatest L x' (Lower L A)"
+  apply (rule ggreatest_cong) using assms by auto
+
+lemma (in gpartial_order) ggreatest_Lower_cong_r:
+  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "ggreatest L x (Lower L A) = ggreatest L x (Lower L A')"
+apply (subgoal_tac "Lower L A = Lower L A'", simp)
+by (rule Lower_cong) fact+
+
+lemma ggreatest_LowerI:
+  fixes L (structure)
+  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
+    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
+    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
+  shows "ggreatest L i (Lower L A)"
+proof -
+  have "Lower L A \<subseteq> carrier L" by simp
+  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
+  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
+  ultimately show ?thesis by (simp add: ggreatest_def)
+qed
+
+lemma ggreatest_Lower_below:
+  fixes L (structure)
+  shows "[| ggreatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
+  by (unfold ggreatest_def) blast
+
+text {* Supremum and infimum *}
+
+constdefs (structure L)
+  gsup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
+  "\<Squnion>A == SOME x. gleast L x (Upper L A)"
+
+  ginf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
+  "\<Sqinter>A == SOME x. ggreatest L x (Lower L A)"
+
+  gjoin :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
+  "x \<squnion> y == \<Squnion> {x, y}"
+
+  gmeet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
+  "x \<sqinter> y == \<Sqinter> {x, y}"
+
+
+subsection {* Lattices *}
+
+locale gupper_semilattice = gpartial_order +
+  assumes gsup_of_two_exists:
+    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. gleast L s (Upper L {x, y})"
+
+locale glower_semilattice = gpartial_order +
+  assumes ginf_of_two_exists:
+    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. ggreatest L s (Lower L {x, y})"
+
+locale glattice = gupper_semilattice + glower_semilattice
+
+
+subsubsection {* Supremum *}
+
+lemma (in gupper_semilattice) gjoinI:
+  "[| !!l. gleast L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
+  ==> P (x \<squnion> y)"
+proof (unfold gjoin_def gsup_def)
+  assume L: "x \<in> carrier L"  "y \<in> carrier L"
+    and P: "!!l. gleast L l (Upper L {x, y}) ==> P l"
+  with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
+  with L show "P (SOME l. gleast L l (Upper L {x, y}))"
+    by (fast intro: someI2 P)
+qed
+
+lemma (in gupper_semilattice) gjoin_closed [simp]:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
+  by (rule gjoinI) (rule gleast_closed)
+
+lemma (in gupper_semilattice) gjoin_cong_l:
+  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+    and xx': "x .= x'"
+  shows "x \<squnion> y .= x' \<squnion> y"
+proof (rule gjoinI, rule gjoinI)
+  fix a b
+  from xx' carr
+      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
+
+  assume gleasta: "gleast L a (Upper L {x, y})"
+  assume "gleast L b (Upper L {x', y})"
+  with carr
+      have gleastb: "gleast L b (Upper L {x, y})"
+      by (simp add: gleast_Upper_cong_r[OF _ _ seq])
+
+  from gleasta gleastb
+      show "a .= b" by (rule gleast_unique)
+qed (rule carr)+
+
+lemma (in gupper_semilattice) gjoin_cong_r:
+  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+    and yy': "y .= y'"
+  shows "x \<squnion> y .= x \<squnion> y'"
+proof (rule gjoinI, rule gjoinI)
+  fix a b
+  have "{x, y} = {y, x}" by fast
+  also from carr yy'
+      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
+  also have "{y', x} = {x, y'}" by fast
+  finally
+      have seq: "{x, y} {.=} {x, y'}" .
+
+  assume gleasta: "gleast L a (Upper L {x, y})"
+  assume "gleast L b (Upper L {x, y'})"
+  with carr
+      have gleastb: "gleast L b (Upper L {x, y})"
+      by (simp add: gleast_Upper_cong_r[OF _ _ seq])
+
+  from gleasta gleastb
+      show "a .= b" by (rule gleast_unique)
+qed (rule carr)+
+
+lemma (in gpartial_order) gsup_of_singletonI:      (* only reflexivity needed ? *)
+  "x \<in> carrier L ==> gleast L x (Upper L {x})"
+  by (rule gleast_UpperI) auto
+
+lemma (in gpartial_order) gsup_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Squnion>{x} .= x"
+  unfolding gsup_def
+  by (rule someI2) (auto intro: gleast_unique gsup_of_singletonI)
+
+lemma (in gpartial_order) gsup_of_singleton_closed [simp]:
+  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
+  unfolding gsup_def
+  by (rule someI2) (auto intro: gsup_of_singletonI)
+
+text {* Condition on @{text A}: supremum exists. *}
+
+lemma (in gupper_semilattice) gsup_insertI:
+  "[| !!s. gleast L s (Upper L (insert x A)) ==> P s;
+  gleast L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
+  ==> P (\<Squnion>(insert x A))"
+proof (unfold gsup_def)
+  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
+    and P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
+    and gleast_a: "gleast L a (Upper L A)"
+  from L gleast_a have La: "a \<in> carrier L" by simp
+  from L gsup_of_two_exists gleast_a
+  obtain s where gleast_s: "gleast L s (Upper L {a, x})" by blast
+  show "P (SOME l. gleast L l (Upper L (insert x A)))"
+  proof (rule someI2)
+    show "gleast L s (Upper L (insert x A))"
+    proof (rule gleast_UpperI)
+      fix z
+      assume "z \<in> insert x A"
+      then show "z \<sqsubseteq> s"
+      proof
+        assume "z = x" then show ?thesis
+          by (simp add: gleast_Upper_above [OF gleast_s] L La)
+      next
+        assume "z \<in> A"
+        with L gleast_s gleast_a show ?thesis
+          by (rule_tac le_trans [where y = a]) (auto dest: gleast_Upper_above)
+      qed
+    next
+      fix y
+      assume y: "y \<in> Upper L (insert x A)"
+      show "s \<sqsubseteq> y"
+      proof (rule gleast_le [OF gleast_s], rule Upper_memI)
+	fix z
+	assume z: "z \<in> {a, x}"
+	then show "z \<sqsubseteq> y"
+	proof
+          have y': "y \<in> Upper L A"
+            apply (rule subsetD [where A = "Upper L (insert x A)"])
+             apply (rule Upper_antimono)
+	     apply blast
+	    apply (rule y)
+            done
+          assume "z = a"
+          with y' gleast_a show ?thesis by (fast dest: gleast_le)
+	next
+	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
+          with y L show ?thesis by blast
+	qed
+      qed (rule Upper_closed [THEN subsetD, OF y])
+    next
+      from L show "insert x A \<subseteq> carrier L" by simp
+      from gleast_s show "s \<in> carrier L" by simp
+    qed
+  qed (rule P)
+qed
+
+lemma (in gupper_semilattice) finite_gsup_gleast:
+  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> gleast L (\<Squnion>A) (Upper L A)"
+proof (induct set: finite)
+  case empty
+  then show ?case by simp
+next
+  case (insert x A)
+  show ?case
+  proof (cases "A = {}")
+    case True
+    with insert show ?thesis
+      by simp (simp add: gleast_cong [OF gsup_of_singleton]
+	gsup_of_singleton_closed gsup_of_singletonI)
+	(* The above step is hairy; gleast_cong can make simp loop.
+	Would want special version of simp to apply gleast_cong. *)
+  next
+    case False
+    with insert have "gleast L (\<Squnion>A) (Upper L A)" by simp
+    with _ show ?thesis
+      by (rule gsup_insertI) (simp_all add: insert [simplified])
+  qed
+qed
+
+lemma (in gupper_semilattice) finite_gsup_insertI:
+  assumes P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
+    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
+  shows "P (\<Squnion> (insert x A))"
+proof (cases "A = {}")
+  case True with P and xA show ?thesis
+    by (simp add: finite_gsup_gleast)
+next
+  case False with P and xA show ?thesis
+    by (simp add: gsup_insertI finite_gsup_gleast)
+qed
+
+lemma (in gupper_semilattice) finite_gsup_closed [simp]:
+  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
+proof (induct set: finite)
+  case empty then show ?case by simp
+next
+  case insert then show ?case
+    by - (rule finite_gsup_insertI, simp_all)
+qed
+
+lemma (in gupper_semilattice) gjoin_left:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
+  by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
+
+lemma (in gupper_semilattice) gjoin_right:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
+  by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
+
+lemma (in gupper_semilattice) gsup_of_two_gleast:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> gleast L (\<Squnion>{x, y}) (Upper L {x, y})"
+proof (unfold gsup_def)
+  assume L: "x \<in> carrier L"  "y \<in> carrier L"
+  with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
+  with L show "gleast L (SOME z. gleast L z (Upper L {x, y})) (Upper L {x, y})"
+  by (fast intro: someI2 gleast_unique)  (* blast fails *)
+qed
+
+lemma (in gupper_semilattice) gjoin_le:
+  assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
+    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
+  shows "x \<squnion> y \<sqsubseteq> z"
+proof (rule gjoinI [OF _ x y])
+  fix s
+  assume "gleast L s (Upper L {x, y})"
+  with sub z show "s \<sqsubseteq> z" by (fast elim: gleast_le intro: Upper_memI)
+qed
+
+lemma (in gupper_semilattice) gjoin_assoc_lemma:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
+proof (rule finite_gsup_insertI)
+  -- {* The textbook argument in Jacobson I, p 457 *}
+  fix s
+  assume gsup: "gleast L s (Upper L {x, y, z})"
+  show "x \<squnion> (y \<squnion> z) .= s"
+  proof (rule le_anti_sym)
+    from gsup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
+      by (fastsimp intro!: gjoin_le elim: gleast_Upper_above)
+  next
+    from gsup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
+    by (erule_tac gleast_le)
+      (blast intro!: Upper_memI intro: le_trans gjoin_left gjoin_right gjoin_closed)
+  qed (simp_all add: L gleast_closed [OF gsup])
+qed (simp_all add: L)
+
+text {* Commutativity holds for @{text "="}. *}
+
+lemma gjoin_comm:
+  fixes L (structure)
+  shows "x \<squnion> y = y \<squnion> x"
+  by (unfold gjoin_def) (simp add: insert_commute)
+
+lemma (in gupper_semilattice) gjoin_assoc:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
+proof -
+  (* FIXME: could be simplified by improved simp: uniform use of .=,
+     omit [symmetric] in last step. *)
+  have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: gjoin_comm)
+  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: gjoin_assoc_lemma)
+  also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
+  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: gjoin_assoc_lemma [symmetric])
+  finally show ?thesis by (simp add: L)
+qed
+
+
+subsubsection {* Infimum *}
+
+lemma (in glower_semilattice) gmeetI:
+  "[| !!i. ggreatest L i (Lower L {x, y}) ==> P i;
+  x \<in> carrier L; y \<in> carrier L |]
+  ==> P (x \<sqinter> y)"
+proof (unfold gmeet_def ginf_def)
+  assume L: "x \<in> carrier L"  "y \<in> carrier L"
+    and P: "!!g. ggreatest L g (Lower L {x, y}) ==> P g"
+  with ginf_of_two_exists obtain i where "ggreatest L i (Lower L {x, y})" by fast
+  with L show "P (SOME g. ggreatest L g (Lower L {x, y}))"
+  by (fast intro: someI2 ggreatest_unique P)
+qed
+
+lemma (in glower_semilattice) gmeet_closed [simp]:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
+  by (rule gmeetI) (rule ggreatest_closed)
+
+lemma (in glower_semilattice) gmeet_cong_l:
+  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+    and xx': "x .= x'"
+  shows "x \<sqinter> y .= x' \<sqinter> y"
+proof (rule gmeetI, rule gmeetI)
+  fix a b
+  from xx' carr
+      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
+
+  assume ggreatesta: "ggreatest L a (Lower L {x, y})"
+  assume "ggreatest L b (Lower L {x', y})"
+  with carr
+      have ggreatestb: "ggreatest L b (Lower L {x, y})"
+      by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
+
+  from ggreatesta ggreatestb
+      show "a .= b" by (rule ggreatest_unique)
+qed (rule carr)+
+
+lemma (in glower_semilattice) gmeet_cong_r:
+  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+    and yy': "y .= y'"
+  shows "x \<sqinter> y .= x \<sqinter> y'"
+proof (rule gmeetI, rule gmeetI)
+  fix a b
+  have "{x, y} = {y, x}" by fast
+  also from carr yy'
+      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
+  also have "{y', x} = {x, y'}" by fast
+  finally
+      have seq: "{x, y} {.=} {x, y'}" .
+
+  assume ggreatesta: "ggreatest L a (Lower L {x, y})"
+  assume "ggreatest L b (Lower L {x, y'})"
+  with carr
+      have ggreatestb: "ggreatest L b (Lower L {x, y})"
+      by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
+
+  from ggreatesta ggreatestb
+      show "a .= b" by (rule ggreatest_unique)
+qed (rule carr)+
+
+lemma (in gpartial_order) ginf_of_singletonI:      (* only reflexivity needed ? *)
+  "x \<in> carrier L ==> ggreatest L x (Lower L {x})"
+  by (rule ggreatest_LowerI) auto
+
+lemma (in gpartial_order) ginf_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
+  unfolding ginf_def
+  by (rule someI2) (auto intro: ggreatest_unique ginf_of_singletonI)
+
+lemma (in gpartial_order) ginf_of_singleton_closed:
+  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
+  unfolding ginf_def
+  by (rule someI2) (auto intro: ginf_of_singletonI)
+
+text {* Condition on @{text A}: infimum exists. *}
+
+lemma (in glower_semilattice) ginf_insertI:
+  "[| !!i. ggreatest L i (Lower L (insert x A)) ==> P i;
+  ggreatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
+  ==> P (\<Sqinter>(insert x A))"
+proof (unfold ginf_def)
+  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
+    and P: "!!g. ggreatest L g (Lower L (insert x A)) ==> P g"
+    and ggreatest_a: "ggreatest L a (Lower L A)"
+  from L ggreatest_a have La: "a \<in> carrier L" by simp
+  from L ginf_of_two_exists ggreatest_a
+  obtain i where ggreatest_i: "ggreatest L i (Lower L {a, x})" by blast
+  show "P (SOME g. ggreatest L g (Lower L (insert x A)))"
+  proof (rule someI2)
+    show "ggreatest L i (Lower L (insert x A))"
+    proof (rule ggreatest_LowerI)
+      fix z
+      assume "z \<in> insert x A"
+      then show "i \<sqsubseteq> z"
+      proof
+        assume "z = x" then show ?thesis
+          by (simp add: ggreatest_Lower_below [OF ggreatest_i] L La)
+      next
+        assume "z \<in> A"
+        with L ggreatest_i ggreatest_a show ?thesis
+          by (rule_tac le_trans [where y = a]) (auto dest: ggreatest_Lower_below)
+      qed
+    next
+      fix y
+      assume y: "y \<in> Lower L (insert x A)"
+      show "y \<sqsubseteq> i"
+      proof (rule ggreatest_le [OF ggreatest_i], rule Lower_memI)
+	fix z
+	assume z: "z \<in> {a, x}"
+	then show "y \<sqsubseteq> z"
+	proof
+          have y': "y \<in> Lower L A"
+            apply (rule subsetD [where A = "Lower L (insert x A)"])
+            apply (rule Lower_antimono)
+	     apply blast
+	    apply (rule y)
+            done
+          assume "z = a"
+          with y' ggreatest_a show ?thesis by (fast dest: ggreatest_le)
+	next
+          assume "z \<in> {x}"
+          with y L show ?thesis by blast
+	qed
+      qed (rule Lower_closed [THEN subsetD, OF y])
+    next
+      from L show "insert x A \<subseteq> carrier L" by simp
+      from ggreatest_i show "i \<in> carrier L" by simp
+    qed
+  qed (rule P)
+qed
+
+lemma (in glower_semilattice) finite_ginf_ggreatest:
+  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> ggreatest L (\<Sqinter>A) (Lower L A)"
+proof (induct set: finite)
+  case empty then show ?case by simp
+next
+  case (insert x A)
+  show ?case
+  proof (cases "A = {}")
+    case True
+    with insert show ?thesis
+      by simp (simp add: ggreatest_cong [OF ginf_of_singleton]
+	ginf_of_singleton_closed ginf_of_singletonI)
+  next
+    case False
+    from insert show ?thesis
+    proof (rule_tac ginf_insertI)
+      from False insert show "ggreatest L (\<Sqinter>A) (Lower L A)" by simp
+    qed simp_all
+  qed
+qed
+
+lemma (in glower_semilattice) finite_ginf_insertI:
+  assumes P: "!!i. ggreatest L i (Lower L (insert x A)) ==> P i"
+    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
+  shows "P (\<Sqinter> (insert x A))"
+proof (cases "A = {}")
+  case True with P and xA show ?thesis
+    by (simp add: finite_ginf_ggreatest)
+next
+  case False with P and xA show ?thesis
+    by (simp add: ginf_insertI finite_ginf_ggreatest)
+qed
+
+lemma (in glower_semilattice) finite_ginf_closed [simp]:
+  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
+proof (induct set: finite)
+  case empty then show ?case by simp
+next
+  case insert then show ?case
+    by (rule_tac finite_ginf_insertI) (simp_all)
+qed
+
+lemma (in glower_semilattice) gmeet_left:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
+  by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
+
+lemma (in glower_semilattice) gmeet_right:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
+  by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
+
+lemma (in glower_semilattice) ginf_of_two_ggreatest:
+  "[| x \<in> carrier L; y \<in> carrier L |] ==>
+  ggreatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
+proof (unfold ginf_def)
+  assume L: "x \<in> carrier L"  "y \<in> carrier L"
+  with ginf_of_two_exists obtain s where "ggreatest L s (Lower L {x, y})" by fast
+  with L
+  show "ggreatest L (SOME z. ggreatest L z (Lower L {x, y})) (Lower L {x, y})"
+  by (fast intro: someI2 ggreatest_unique)  (* blast fails *)
+qed
+
+lemma (in glower_semilattice) gmeet_le:
+  assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
+    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
+  shows "z \<sqsubseteq> x \<sqinter> y"
+proof (rule gmeetI [OF _ x y])
+  fix i
+  assume "ggreatest L i (Lower L {x, y})"
+  with sub z show "z \<sqsubseteq> i" by (fast elim: ggreatest_le intro: Lower_memI)
+qed
+
+lemma (in glower_semilattice) gmeet_assoc_lemma:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
+proof (rule finite_ginf_insertI)
+  txt {* The textbook argument in Jacobson I, p 457 *}
+  fix i
+  assume ginf: "ggreatest L i (Lower L {x, y, z})"
+  show "x \<sqinter> (y \<sqinter> z) .= i"
+  proof (rule le_anti_sym)
+    from ginf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
+      by (fastsimp intro!: gmeet_le elim: ggreatest_Lower_below)
+  next
+    from ginf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
+    by (erule_tac ggreatest_le)
+      (blast intro!: Lower_memI intro: le_trans gmeet_left gmeet_right gmeet_closed)
+  qed (simp_all add: L ggreatest_closed [OF ginf])
+qed (simp_all add: L)
+
+lemma gmeet_comm:
+  fixes L (structure)
+  shows "x \<sqinter> y = y \<sqinter> x"
+  by (unfold gmeet_def) (simp add: insert_commute)
+
+lemma (in glower_semilattice) gmeet_assoc:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
+proof -
+  (* FIXME: improved simp, see gjoin_assoc above *)
+  have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: gmeet_comm)
+  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: gmeet_assoc_lemma)
+  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
+  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: gmeet_assoc_lemma [symmetric])
+  finally show ?thesis by (simp add: L)
+qed
+
+
+subsection {* Total Orders *}
+
+locale gtotal_order = gpartial_order +
+  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
+
+text {* Introduction rule: the usual definition of total order *}
+
+lemma (in gpartial_order) gtotal_orderI:
+  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
+  shows "gtotal_order L"
+  by unfold_locales (rule total)
+
+text {* Total orders are lattices. *}
+
+interpretation gtotal_order < glattice
+proof unfold_locales
+  fix x y
+  assume L: "x \<in> carrier L"  "y \<in> carrier L"
+  show "EX s. gleast L s (Upper L {x, y})"
+  proof -
+    note total L
+    moreover
+    {
+      assume "x \<sqsubseteq> y"
+      with L have "gleast L y (Upper L {x, y})"
+        by (rule_tac gleast_UpperI) auto
+    }
+    moreover
+    {
+      assume "y \<sqsubseteq> x"
+      with L have "gleast L x (Upper L {x, y})"
+        by (rule_tac gleast_UpperI) auto
+    }
+    ultimately show ?thesis by blast
+  qed
+next
+  fix x y
+  assume L: "x \<in> carrier L"  "y \<in> carrier L"
+  show "EX i. ggreatest L i (Lower L {x, y})"
+  proof -
+    note total L
+    moreover
+    {
+      assume "y \<sqsubseteq> x"
+      with L have "ggreatest L y (Lower L {x, y})"
+        by (rule_tac ggreatest_LowerI) auto
+    }
+    moreover
+    {
+      assume "x \<sqsubseteq> y"
+      with L have "ggreatest L x (Lower L {x, y})"
+        by (rule_tac ggreatest_LowerI) auto
+    }
+    ultimately show ?thesis by blast
+  qed
+qed
+
+
+subsection {* Complete lattices *}
+
+locale complete_lattice = glattice +
+  assumes gsup_exists:
+    "[| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
+    and ginf_exists:
+    "[| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
+
+text {* Introduction rule: the usual definition of complete lattice *}
+
+lemma (in gpartial_order) complete_latticeI:
+  assumes gsup_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
+    and ginf_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
+  shows "complete_lattice L"
+  by unfold_locales (auto intro: gsup_exists ginf_exists)
+
+constdefs (structure L)
+  top :: "_ => 'a" ("\<top>\<index>")
+  "\<top> == gsup L (carrier L)"
+
+  bottom :: "_ => 'a" ("\<bottom>\<index>")
+  "\<bottom> == ginf L (carrier L)"
+
+
+lemma (in complete_lattice) gsupI:
+  "[| !!l. gleast L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
+  ==> P (\<Squnion>A)"
+proof (unfold gsup_def)
+  assume L: "A \<subseteq> carrier L"
+    and P: "!!l. gleast L l (Upper L A) ==> P l"
+  with gsup_exists obtain s where "gleast L s (Upper L A)" by blast
+  with L show "P (SOME l. gleast L l (Upper L A))"
+  by (fast intro: someI2 gleast_unique P)
+qed
+
+lemma (in complete_lattice) gsup_closed [simp]:
+  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
+  by (rule gsupI) simp_all
+
+lemma (in complete_lattice) top_closed [simp, intro]:
+  "\<top> \<in> carrier L"
+  by (unfold top_def) simp
+
+lemma (in complete_lattice) ginfI:
+  "[| !!i. ggreatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
+  ==> P (\<Sqinter>A)"
+proof (unfold ginf_def)
+  assume L: "A \<subseteq> carrier L"
+    and P: "!!l. ggreatest L l (Lower L A) ==> P l"
+  with ginf_exists obtain s where "ggreatest L s (Lower L A)" by blast
+  with L show "P (SOME l. ggreatest L l (Lower L A))"
+  by (fast intro: someI2 ggreatest_unique P)
+qed
+
+lemma (in complete_lattice) ginf_closed [simp]:
+  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
+  by (rule ginfI) simp_all
+
+lemma (in complete_lattice) bottom_closed [simp, intro]:
+  "\<bottom> \<in> carrier L"
+  by (unfold bottom_def) simp
+
+text {* Jacobson: Theorem 8.1 *}
+
+lemma Lower_empty [simp]:
+  "Lower L {} = carrier L"
+  by (unfold Lower_def) simp
+
+lemma Upper_empty [simp]:
+  "Upper L {} = carrier L"
+  by (unfold Upper_def) simp
+
+theorem (in gpartial_order) complete_lattice_criterion1:
+  assumes top_exists: "EX g. ggreatest L g (carrier L)"
+    and ginf_exists:
+      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. ggreatest L i (Lower L A)"
+  shows "complete_lattice L"
+proof (rule complete_latticeI)
+  from top_exists obtain top where top: "ggreatest L top (carrier L)" ..
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  let ?B = "Upper L A"
+  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: ggreatest_le)
+  then have B_non_empty: "?B ~= {}" by fast
+  have B_L: "?B \<subseteq> carrier L" by simp
+  from ginf_exists [OF B_L B_non_empty]
+  obtain b where b_ginf_B: "ggreatest L b (Lower L ?B)" ..
+  have "gleast L b (Upper L A)"
+apply (rule gleast_UpperI)
+   apply (rule ggreatest_le [where A = "Lower L ?B"])
+    apply (rule b_ginf_B)
+   apply (rule Lower_memI)
+    apply (erule Upper_memD [THEN conjunct1])
+     apply assumption
+    apply (rule L)
+   apply (fast intro: L [THEN subsetD])
+  apply (erule ggreatest_Lower_below [OF b_ginf_B])
+  apply simp
+ apply (rule L)
+apply (rule ggreatest_closed [OF b_ginf_B])
+done
+  then show "EX s. gleast L s (Upper L A)" ..
+next
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  show "EX i. ggreatest L i (Lower L A)"
+  proof (cases "A = {}")
+    case True then show ?thesis
+      by (simp add: top_exists)
+  next
+    case False with L show ?thesis
+      by (rule ginf_exists)
+  qed
+qed
+
+(* TODO: prove dual version *)
+
+
+subsection {* Examples *}
+
+(* Not so useful for the generalised version.
+
+subsubsection {* Powerset of a Set is a Complete Lattice *}
+
+theorem powerset_is_complete_lattice:
+  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
+  (is "complete_lattice ?L")
+proof (rule gpartial_order.complete_latticeI)
+  show "gpartial_order ?L"
+    by (rule gpartial_order.intro) auto
+next
+  fix B
+  assume B: "B \<subseteq> carrier ?L"
+  show "EX s. gleast ?L s (Upper ?L B)"
+  proof
+    from B show "gleast ?L (\<Union> B) (Upper ?L B)"
+      by (fastsimp intro!: gleast_UpperI simp: Upper_def)
+  qed
+next
+  fix B
+  assume B: "B \<subseteq> carrier ?L"
+  show "EX i. ggreatest ?L i (Lower ?L B)"
+  proof
+    from B show "ggreatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
+      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
+	@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
+      by (fastsimp intro!: ggreatest_LowerI simp: Lower_def)
+  qed
+qed
+
+text {* An other example, that of the lattice of subgroups of a group,
+  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
+
+*)
+
+end