# HG changeset patch
# User ballarin
# Date 1185283797 -7200
# Node ID 54fab60ddc970b69dca1e3d03e9342ba8eaa80ca
# Parent  48494ccfabaf70aa1d9382b80f7c75e1be402cac
Interpretation of rings (as integers) maps defined operations to defined
operations..

diff -r 48494ccfabaf -r 54fab60ddc97 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Tue Jul 24 15:21:54 2007 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Tue Jul 24 15:29:57 2007 +0200
@@ -71,9 +71,9 @@
   int_ring :: "int ring" ("\<Z>")
   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
 
-lemma int_Zcarr[simp,intro!]:
+lemma int_Zcarr [intro!, simp]:
   "k \<in> carrier \<Z>"
-by (simp add: int_ring_def)
+  by (simp add: int_ring_def)
 
 lemma int_is_cring:
   "cring \<Z>"
@@ -86,15 +86,153 @@
 apply (fast intro: zadd_zminus_inverse2)
 done
 
+(*
 lemma int_is_domain:
   "domain \<Z>"
 apply (intro domain.intro domain_axioms.intro)
   apply (rule int_is_cring)
  apply (unfold int_ring_def, simp+)
 done
+*)
+subsubsection {* Interpretations *}
 
-interpretation "domain" ["\<Z>"] by (rule int_is_domain)
+text {* Since definitions of derived operations are global, their
+  interpretation needs to be done as early as possible --- that is,
+  with as few assumptions as possible. *}
+
+interpretation int: monoid ["\<Z>"]
+  where "carrier \<Z> = UNIV"
+    and "mult \<Z> x y = x * y"
+    and "one \<Z> = 1"
+    and "pow \<Z> x n = x^n"
+proof -
+  -- "Specification"
+  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  then interpret int: monoid ["\<Z>"] .
+
+  -- "Carrier"
+  show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
+
+  -- "Operations"
+  { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
+  note mult = this
+  show one: "one \<Z> = 1" by (simp add: int_ring_def)
+  show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
+qed
+
+interpretation int: comm_monoid ["\<Z>"]
+  where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
+proof -
+  -- "Specification"
+  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  then interpret int: comm_monoid ["\<Z>"] .
+
+  -- "Operations"
+  { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
+  note mult = this
+  have one: "one \<Z> = 1" by (simp add: int_ring_def)
+  show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
+  proof (cases "finite A")
+    case True then show ?thesis proof induct
+      case empty show ?case by (simp add: one)
+    next
+      case insert then show ?case by (simp add: Pi_def mult)
+    qed
+  next
+    case False then show ?thesis by (simp add: finprod_def)
+  qed
+qed
+
+interpretation int: abelian_monoid ["\<Z>"]
+  where "zero \<Z> = 0"
+    and "add \<Z> x y = x + y"
+    and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
+proof -
+  -- "Specification"
+  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  then interpret int: abelian_monoid ["\<Z>"] .
 
+  -- "Operations"
+  { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
+  note add = this
+  show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
+  show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
+  proof (cases "finite A")
+    case True then show ?thesis proof induct
+      case empty show ?case by (simp add: zero)
+    next
+      case insert then show ?case by (simp add: Pi_def add)
+    qed
+  next
+    case False then show ?thesis by (simp add: finsum_def finprod_def)
+  qed
+qed
+
+interpretation int: abelian_group ["\<Z>"]
+  where "a_inv \<Z> x = - x"
+    and "a_minus \<Z> x y = x - y"
+proof -
+  -- "Specification"
+  show "abelian_group \<Z>"
+  proof (rule abelian_groupI)
+    show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
+      by (simp add: int_ring_def) arith
+  qed (auto simp: int_ring_def)
+  then interpret int: abelian_group ["\<Z>"] .
+
+  -- "Operations"
+  { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
+  note add = this
+  have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
+  { fix x
+    have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
+    then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
+  note a_inv = this
+  show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
+qed
+
+interpretation int: "domain" ["\<Z>"]
+  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
+
+
+interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
+  where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
+proof -
+  show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
+    by unfold_locales simp_all
+  show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
+    by (simp add: lless_def) auto
+qed
+
+interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
+  where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
+    and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
+proof -
+  let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
+  show "lattice ?Z"
+    apply unfold_locales
+    apply (simp add: least_def Upper_def)
+    apply arith
+    apply (simp add: greatest_def Lower_def)
+    apply arith
+    done
+  then interpret int: lattice ["?Z"] .
+  show "join ?Z x y = max x y"
+    apply (rule int.joinI)
+    apply (simp_all add: least_def Upper_def)
+    apply arith
+    done
+  show "meet ?Z x y = min x y"
+    apply (rule int.meetI)
+    apply (simp_all add: greatest_def Lower_def)
+    apply arith
+    done
+qed
+
+interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
+  by unfold_locales clarsimp
+
+(*
 lemma int_le_total_order:
   "total_order (| carrier = UNIV::int set, le = op \<le> |)"
   apply (rule partial_order.total_orderI)
@@ -150,20 +288,21 @@
   int [unfolded less_int join_int meet_int carrier_int]:
   total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   by (rule int_le_total_order)
+*)
 
 
 subsubsection {* Generated Ideals of @{text "\<Z>"} *}
 
 lemma int_Idl:
   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
-apply (subst cgenideal_eq_genideal[symmetric], simp add: int_ring_def)
-apply (simp add: cgenideal_def int_ring_def)
-done
+  apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
+  apply (simp add: cgenideal_def int_ring_def)
+  done
 
 lemma multiples_principalideal:
   "principalideal {x * a | x. True } \<Z>"
 apply (subst int_Idl[symmetric], rule principalidealI)
- apply (rule genideal_ideal, simp)
+ apply (rule int.genideal_ideal, simp)
 apply fast
 done
 
@@ -171,12 +310,12 @@
   assumes prime: "prime (nat p)"
   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
 apply (rule primeidealI)
-   apply (rule genideal_ideal, simp)
+   apply (rule int.genideal_ideal, simp)
   apply (rule int_is_cring)
- apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
+ apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
  apply (simp add: int_ring_def)
  apply clarsimp defer 1
- apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
+ apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
  apply (simp add: int_ring_def)
  apply (elim exE)
 proof -
@@ -244,14 +383,14 @@
 
 lemma int_Idl_subset_ideal:
   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
-by (rule Idl_subset_ideal', simp+)
+by (rule int.Idl_subset_ideal', simp+)
 
 lemma Idl_subset_eq_dvd:
   "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
 apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
 apply (rule, clarify)
 apply (simp add: dvd_def, clarify)
-apply (simp add: m_comm)
+apply (simp add: int.m_comm)
 done
 
 lemma dvds_eq_Idl:
@@ -305,7 +444,7 @@
   assumes zmods: "ZMod m a = ZMod m b"
   shows "a mod m = b mod m"
 proof -
-  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
+  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   from zmods
       have "b \<in> ZMod m a"
       unfolding ZMod_def
@@ -329,7 +468,7 @@
 lemma ZMod_mod:
   shows "ZMod m a = ZMod m (a mod m)"
 proof -
-  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast)
+  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   show ?thesis
       unfolding ZMod_def
   apply (rule a_repr_independence'[symmetric])
@@ -377,14 +516,14 @@
 
 lemma ZFact_zero:
   "carrier (ZFact 0) = (\<Union>a. {{a}})"
-apply (insert genideal_zero)
+apply (insert int.genideal_zero)
 apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
 done
 
 lemma ZFact_one:
   "carrier (ZFact 1) = {UNIV}"
 apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
-apply (subst genideal_one[unfolded int_ring_def, simplified ring_record_simps])
+apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
 apply (rule, rule, clarsimp)
  apply (rule, rule, clarsimp)
  apply (rule, clarsimp, arith)
diff -r 48494ccfabaf -r 54fab60ddc97 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Tue Jul 24 15:21:54 2007 +0200
+++ b/src/HOL/Algebra/Ring.thy	Tue Jul 24 15:29:57 2007 +0200
@@ -471,8 +471,8 @@
   with R show ?thesis by (simp add: a_assoc r_neg )
 qed
 
-lemma (in ring) minus_eq:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
+lemma (in abelian_group) minus_eq:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
   by (simp only: a_minus_def)
 
 text {* Setup algebra method: