--- 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)