author ballarin Tue, 24 Jul 2007 15:29:57 +0200 changeset 23957 54fab60ddc97 parent 23956 48494ccfabaf child 23958 bb838771157f
Interpretation of rings (as integers) maps defined operations to defined operations..
 src/HOL/Algebra/IntRing.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Ring.thy file | annotate | diff | comparison | revisions
```--- 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>"

lemma int_is_cring:
"cring \<Z>"
@@ -86,15 +86,153 @@
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) }
+  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
+    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) }
+  have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
+  { fix x
+    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)
-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 clarsimp defer 1
- apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def)
+ apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_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)
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)```
```--- 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:```