author  ballarin 
Wed, 30 Jul 2008 19:03:33 +0200  
changeset 27713  95b36bfe7fc4 
parent 25919  8b1c0d434824 
child 27717  21bbd410ba04 
permissions  rwrr 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

1 
(* 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

2 
Title: HOL/Algebra/IntRing.thy 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

3 
Id: $Id$ 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

4 
Author: Stephan Hohe, TU Muenchen 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

5 
*) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

6 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

7 
theory IntRing 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24131
diff
changeset

8 
imports QuotRing Int 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

9 
begin 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

10 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

11 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

12 
section {* The Ring of Integers *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

13 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

14 
subsection {* Some properties of @{typ int} *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

15 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

16 
lemma dvds_imp_abseq: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

17 
"\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

18 
apply (subst abs_split, rule conjI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

19 
apply (clarsimp, subst abs_split, rule conjI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

20 
apply (clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

21 
apply (cases "k=0", simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

22 
apply (cases "l=0", simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

23 
apply (simp add: zdvd_anti_sym) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

24 
apply clarsimp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

25 
apply (cases "k=0", simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

26 
apply (simp add: zdvd_anti_sym) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

27 
apply (clarsimp, subst abs_split, rule conjI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

28 
apply (clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

29 
apply (cases "l=0", simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

30 
apply (simp add: zdvd_anti_sym) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

31 
apply (clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

32 
apply (subgoal_tac "l = k", simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

33 
apply (intro zdvd_anti_sym, simp+) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

34 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

35 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

36 
lemma abseq_imp_dvd: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

37 
assumes a_lk: "abs l = abs (k::int)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

38 
shows "l dvd k" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

39 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

40 
from a_lk 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

41 
have "nat (abs l) = nat (abs k)" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

42 
hence "nat (abs l) dvd nat (abs k)" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

43 
hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

44 
hence "abs l dvd k" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

45 
thus "l dvd k" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

46 
apply (unfold dvd_def, cases "l<0") 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

47 
defer 1 apply clarsimp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

48 
proof (clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

49 
fix k 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

50 
assume l0: "l < 0" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

51 
have " (l * k) = l * (k)" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

52 
thus "\<exists>ka.  (l * k) = l * ka" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

53 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

54 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

55 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

56 
lemma dvds_eq_abseq: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

57 
"(l dvd k \<and> k dvd l) = (abs l = abs (k::int))" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

58 
apply rule 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

59 
apply (simp add: dvds_imp_abseq) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

60 
apply (rule conjI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

61 
apply (simp add: abseq_imp_dvd)+ 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

62 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

63 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

64 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

65 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

66 
subsection {* The Set of Integers as Algebraic Structure *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

67 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

68 
subsubsection {* Definition of @{text "\<Z>"} *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

69 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

70 
constdefs 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

71 
int_ring :: "int ring" ("\<Z>") 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

72 
"int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

73 

23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

74 
lemma int_Zcarr [intro!, simp]: 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

75 
"k \<in> carrier \<Z>" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

76 
by (simp add: int_ring_def) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

77 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

78 
lemma int_is_cring: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

79 
"cring \<Z>" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

80 
unfolding int_ring_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

81 
apply (rule cringI) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

82 
apply (rule abelian_groupI, simp_all) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

83 
defer 1 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

84 
apply (rule comm_monoidI, simp_all) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

85 
apply (rule zadd_zmult_distrib) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

86 
apply (fast intro: zadd_zminus_inverse2) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

87 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

88 

23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

89 
(* 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

90 
lemma int_is_domain: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

91 
"domain \<Z>" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

92 
apply (intro domain.intro domain_axioms.intro) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

93 
apply (rule int_is_cring) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

94 
apply (unfold int_ring_def, simp+) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

95 
done 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

96 
*) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

97 
subsubsection {* Interpretations *} 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

98 

23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

99 
text {* Since definitions of derived operations are global, their 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

100 
interpretation needs to be done as early as possible  that is, 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

101 
with as few assumptions as possible. *} 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

102 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

103 
interpretation int: monoid ["\<Z>"] 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

104 
where "carrier \<Z> = UNIV" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

105 
and "mult \<Z> x y = x * y" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

106 
and "one \<Z> = 1" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

107 
and "pow \<Z> x n = x^n" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

108 
proof  
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

109 
 "Specification" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

110 
show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

111 
then interpret int: monoid ["\<Z>"] . 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

112 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

113 
 "Carrier" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

114 
show "carrier \<Z> = UNIV" by (simp add: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

115 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

116 
 "Operations" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

117 
{ fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) } 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

118 
note mult = this 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

119 
show one: "one \<Z> = 1" by (simp add: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

120 
show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+ 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

121 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

122 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

123 
interpretation int: comm_monoid ["\<Z>"] 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

124 
where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

125 
proof  
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

126 
 "Specification" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

127 
show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

128 
then interpret int: comm_monoid ["\<Z>"] . 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

129 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

130 
 "Operations" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

131 
{ fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) } 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

132 
note mult = this 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

133 
have one: "one \<Z> = 1" by (simp add: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

134 
show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

135 
proof (cases "finite A") 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

136 
case True then show ?thesis proof induct 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

137 
case empty show ?case by (simp add: one) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

138 
next 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

139 
case insert then show ?case by (simp add: Pi_def mult) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

140 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

141 
next 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

142 
case False then show ?thesis by (simp add: finprod_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

143 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

144 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

145 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

146 
interpretation int: abelian_monoid ["\<Z>"] 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

147 
where "zero \<Z> = 0" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

148 
and "add \<Z> x y = x + y" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

149 
and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

150 
proof  
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

151 
 "Specification" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

152 
show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

153 
then interpret int: abelian_monoid ["\<Z>"] . 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

154 

23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

155 
 "Operations" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

156 
{ fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) } 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

157 
note add = this 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

158 
show zero: "zero \<Z> = 0" by (simp add: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

159 
show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

160 
proof (cases "finite A") 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

161 
case True then show ?thesis proof induct 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

162 
case empty show ?case by (simp add: zero) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

163 
next 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

164 
case insert then show ?case by (simp add: Pi_def add) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

165 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

166 
next 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

167 
case False then show ?thesis by (simp add: finsum_def finprod_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

168 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

169 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

170 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

171 
interpretation int: abelian_group ["\<Z>"] 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

172 
where "a_inv \<Z> x =  x" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

173 
and "a_minus \<Z> x y = x  y" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

174 
proof  
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

175 
 "Specification" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

176 
show "abelian_group \<Z>" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

177 
proof (rule abelian_groupI) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

178 
show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

179 
by (simp add: int_ring_def) arith 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

180 
qed (auto simp: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

181 
then interpret int: abelian_group ["\<Z>"] . 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

182 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

183 
 "Operations" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

184 
{ fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) } 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

185 
note add = this 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

186 
have zero: "zero \<Z> = 0" by (simp add: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

187 
{ fix x 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

188 
have "add \<Z> (x) x = zero \<Z>" by (simp add: add zero) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

189 
then show "a_inv \<Z> x =  x" by (simp add: int.minus_equality) } 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

190 
note a_inv = this 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

191 
show "a_minus \<Z> x y = x  y" by (simp add: int.minus_eq add a_inv) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

192 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

193 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

194 
interpretation int: "domain" ["\<Z>"] 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

195 
by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

196 

54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

197 

24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

198 
text {* Removal of occurrences of @{term UNIV} in interpretation result 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

199 
 experimental. *} 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

200 

1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

201 
lemma UNIV: 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

202 
"x \<in> UNIV = True" 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

203 
"A \<subseteq> UNIV = True" 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

204 
"(ALL x : UNIV. P x) = (ALL x. P x)" 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

205 
"(EX x : UNIV. P x) = (EX x. P x)" 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

206 
"(True > Q) = Q" 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

207 
"(True ==> PROP R) == PROP R" 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

208 
by simp_all 
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

209 

1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

210 
interpretation int [unfolded UNIV]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

211 
partial_order ["( carrier = UNIV::int set, eq = op =, le = op \<le> )"] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

212 
where "carrier ( carrier = UNIV::int set, eq = op =, le = op \<le> ) = UNIV" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

213 
and "le ( carrier = UNIV::int set, eq = op =, le = op \<le> ) x y = (x \<le> y)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

214 
and "lless ( carrier = UNIV::int set, eq = op =, le = op \<le> ) x y = (x < y)" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

215 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

216 
show "partial_order ( carrier = UNIV::int set, eq = op =, le = op \<le> )" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

217 
by unfold_locales simp_all 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

218 
show "carrier ( carrier = UNIV::int set, eq = op =, le = op \<le> ) = UNIV" 
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

219 
by simp 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

220 
show "le ( carrier = UNIV::int set, eq = op =, le = op \<le> ) x y = (x \<le> y)" 
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

221 
by simp 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

222 
show "lless ( carrier = UNIV::int set, eq = op =, le = op \<le> ) x y = (x < y)" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

223 
by (simp add: lless_def) auto 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

224 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

225 

24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

226 
interpretation int [unfolded UNIV]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

227 
lattice ["( carrier = UNIV::int set, eq = op =, le = op \<le> )"] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

228 
where "join ( carrier = UNIV::int set, eq = op =, le = op \<le> ) x y = max x y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

229 
and "meet ( carrier = UNIV::int set, eq = op =, le = op \<le> ) x y = min x y" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

230 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

231 
let ?Z = "( carrier = UNIV::int set, eq = op =, le = op \<le> )" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

232 
show "lattice ?Z" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

233 
apply unfold_locales 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

234 
apply (simp add: least_def Upper_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

235 
apply arith 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

236 
apply (simp add: greatest_def Lower_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

237 
apply arith 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

238 
done 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

239 
then interpret int: lattice ["?Z"] . 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

240 
show "join ?Z x y = max x y" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

241 
apply (rule int.joinI) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

242 
apply (simp_all add: least_def Upper_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

243 
apply arith 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

244 
done 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

245 
show "meet ?Z x y = min x y" 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

246 
apply (rule int.meetI) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

247 
apply (simp_all add: greatest_def Lower_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

248 
apply arith 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

249 
done 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

250 
qed 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

251 

24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset

252 
interpretation int [unfolded UNIV]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset

253 
total_order ["( carrier = UNIV::int set, eq = op =, le = op \<le> )"] 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

254 
by unfold_locales clarsimp 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

255 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

256 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

257 
subsubsection {* Generated Ideals of @{text "\<Z>"} *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

258 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

259 
lemma int_Idl: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

260 
"Idl\<^bsub>\<Z>\<^esub> {a} = {x * a  x. True}" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

261 
apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

262 
apply (simp add: cgenideal_def int_ring_def) 
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

263 
done 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

264 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

265 
lemma multiples_principalideal: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

266 
"principalideal {x * a  x. True } \<Z>" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

267 
apply (subst int_Idl[symmetric], rule principalidealI) 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

268 
apply (rule int.genideal_ideal, simp) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

269 
apply fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

270 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

271 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

272 
lemma prime_primeideal: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

273 
assumes prime: "prime (nat p)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

274 
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

275 
apply (rule primeidealI) 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

276 
apply (rule int.genideal_ideal, simp) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

277 
apply (rule int_is_cring) 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

278 
apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

279 
apply (simp add: int_ring_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

280 
apply clarsimp defer 1 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

281 
apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

282 
apply (simp add: int_ring_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

283 
apply (elim exE) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

284 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

285 
fix a b x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

286 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

287 
from prime 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

288 
have ppos: "0 <= p" by (simp add: prime_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

289 
have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

290 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

291 
fix x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

292 
assume "nat p dvd nat (abs x)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

293 
hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

294 
thus "p dvd x" by (simp add: ppos) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

295 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

296 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

297 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

298 
assume "a * b = x * p" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

299 
hence "p dvd a * b" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

300 
hence "nat p dvd nat (abs (a * b))" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

301 
apply (subst nat_dvd_iff, clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

302 
apply (rule conjI, clarsimp, simp add: zabs_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

303 
proof (clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

304 
assume a: " ~ 0 <= p" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

305 
from prime 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

306 
have "0 < p" by (simp add: prime_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

307 
from a and this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

308 
have "False" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

309 
thus "nat (abs (a * b)) = 0" .. 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

310 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

311 
hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

312 
hence "nat p dvd nat (abs a)  nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

313 
hence "p dvd a  p dvd b" by (fast intro: unnat) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

314 
thus "(EX x. a = x * p)  (EX x. b = x * p)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

315 
proof 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

316 
assume "p dvd a" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

317 
hence "EX x. a = p * x" by (simp add: dvd_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

318 
from this obtain x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

319 
where "a = p * x" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

320 
hence "a = x * p" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

321 
hence "EX x. a = x * p" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

322 
thus "(EX x. a = x * p)  (EX x. b = x * p)" .. 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

323 
next 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

324 
assume "p dvd b" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

325 
hence "EX x. b = p * x" by (simp add: dvd_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

326 
from this obtain x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

327 
where "b = p * x" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

328 
hence "b = x * p" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

329 
hence "EX x. b = x * p" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

330 
thus "(EX x. a = x * p)  (EX x. b = x * p)" .. 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

331 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

332 
next 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

333 
assume "UNIV = {uu. EX x. uu = x * p}" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

334 
from this obtain x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

335 
where "1 = x * p" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

336 
from this [symmetric] 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

337 
have "p * x = 1" by (subst zmult_commute) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

338 
hence "\<bar>p * x\<bar> = 1" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

339 
hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

340 
from this and prime 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

341 
show "False" by (simp add: prime_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

342 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

343 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

344 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

345 
subsubsection {* Ideals and Divisibility *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

346 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

347 
lemma int_Idl_subset_ideal: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

348 
"Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

349 
by (rule int.Idl_subset_ideal', simp+) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

350 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

351 
lemma Idl_subset_eq_dvd: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

352 
"(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

353 
apply (subst int_Idl_subset_ideal, subst int_Idl, simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

354 
apply (rule, clarify) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

355 
apply (simp add: dvd_def, clarify) 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

356 
apply (simp add: int.m_comm) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

357 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

358 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

359 
lemma dvds_eq_Idl: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

360 
"(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

361 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

362 
have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

363 
have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

364 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

365 
have "(l dvd k \<and> k dvd l) = ((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}))" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

366 
by (subst a, subst b, simp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

367 
also have "((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" by (rule, fast+) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

368 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

369 
show ?thesis . 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

370 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

371 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

372 
lemma Idl_eq_abs: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

373 
"(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

374 
apply (subst dvds_eq_abseq[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

375 
apply (rule dvds_eq_Idl[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

376 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

377 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

378 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

379 
subsubsection {* Ideals and the Modulus *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

380 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

381 
constdefs 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

382 
ZMod :: "int => int => int set" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

383 
"ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

384 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

385 
lemmas ZMod_defs = 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

386 
ZMod_def genideal_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

387 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

388 
lemma rcos_zfact: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

389 
assumes kIl: "k \<in> ZMod l r" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

390 
shows "EX x. k = x * l + r" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

391 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

392 
from kIl[unfolded ZMod_def] 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

393 
have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

394 
from this obtain xl 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

395 
where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

396 
and k: "k = xl + r" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

397 
by auto 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

398 
from xl obtain x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

399 
where "xl = x * l" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

400 
by (simp add: int_Idl, fast) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

401 
from k and this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

402 
have "k = x * l + r" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

403 
thus "\<exists>x. k = x * l + r" .. 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

404 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

405 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

406 
lemma ZMod_imp_zmod: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

407 
assumes zmods: "ZMod m a = ZMod m b" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

408 
shows "a mod m = b mod m" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

409 
proof  
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

410 
interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

411 
from zmods 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

412 
have "b \<in> ZMod m a" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

413 
unfolding ZMod_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

414 
by (simp add: a_repr_independenceD) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

415 
from this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

416 
have "EX x. b = x * m + a" by (rule rcos_zfact) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

417 
from this obtain x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

418 
where "b = x * m + a" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

419 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

420 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

421 
hence "b mod m = (x * m + a) mod m" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

422 
also 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

423 
have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

424 
also 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

425 
have "\<dots> = a mod m" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

426 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

427 
have "b mod m = a mod m" . 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

428 
thus "a mod m = b mod m" .. 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

429 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

430 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

431 
lemma ZMod_mod: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

432 
shows "ZMod m a = ZMod m (a mod m)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

433 
proof  
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

434 
interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

435 
show ?thesis 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

436 
unfolding ZMod_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

437 
apply (rule a_repr_independence'[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

438 
apply (simp add: int_Idl a_r_coset_defs) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

439 
apply (simp add: int_ring_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

440 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

441 
have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

442 
hence "a = (a div m) * m + (a mod m)" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

443 
thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

444 
qed simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

445 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

446 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

447 
lemma zmod_imp_ZMod: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

448 
assumes modeq: "a mod m = b mod m" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

449 
shows "ZMod m a = ZMod m b" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

450 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

451 
have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

452 
also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

453 
also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

454 
finally show ?thesis . 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

455 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

456 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

457 
corollary ZMod_eq_mod: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

458 
shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

459 
by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

460 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

461 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

462 
subsubsection {* Factorization *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

463 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

464 
constdefs 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

465 
ZFact :: "int \<Rightarrow> int set ring" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

466 
"ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

467 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

468 
lemmas ZFact_defs = ZFact_def FactRing_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

469 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

470 
lemma ZFact_is_cring: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

471 
shows "cring (ZFact k)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

472 
apply (unfold ZFact_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

473 
apply (rule ideal.quotient_is_cring) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

474 
apply (intro ring.genideal_ideal) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

475 
apply (simp add: cring.axioms[OF int_is_cring] ring.intro) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

476 
apply simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

477 
apply (rule int_is_cring) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

478 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

479 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

480 
lemma ZFact_zero: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

481 
"carrier (ZFact 0) = (\<Union>a. {{a}})" 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

482 
apply (insert int.genideal_zero) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

483 
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

484 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

485 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

486 
lemma ZFact_one: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

487 
"carrier (ZFact 1) = {UNIV}" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

488 
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) 
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset

489 
apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps]) 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

490 
apply (rule, rule, clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

491 
apply (rule, rule, clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

492 
apply (rule, clarsimp, arith) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

493 
apply (rule, clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

494 
apply (rule exI[of _ "0"], clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

495 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

496 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

497 
lemma ZFact_prime_is_domain: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

498 
assumes pprime: "prime (nat p)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

499 
shows "domain (ZFact p)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

500 
apply (unfold ZFact_def) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

501 
apply (rule primeideal.quotient_is_domain) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

502 
apply (rule prime_primeideal[OF pprime]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

503 
done 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

504 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

505 
end 