author  ballarin 
Tue, 02 Sep 2008 17:31:20 +0200  
changeset 28085  914183e229e9 
parent 27717  21bbd410ba04 
child 28524  644b62cf678f 
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 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

8 
imports QuotRing Int Primes 
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 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

65 
subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *} 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

66 

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

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

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

69 
"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

70 

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

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

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

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

74 

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

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

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

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

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

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

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

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

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

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

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

85 

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

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

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

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

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

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

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

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

93 
*) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

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

95 

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

96 
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

97 
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

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

99 

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

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

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

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

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

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

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

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

107 
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

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

109 

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

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

111 
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

112 

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

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

114 
{ 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

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

116 
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

117 
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

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

119 

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

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

121 
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

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

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

124 
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

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

126 

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

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

128 
{ 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

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

130 
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

131 
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

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

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

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

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

136 
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

137 
qed 
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 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

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

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

142 

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

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

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

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

146 
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

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

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

149 
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

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

151 

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

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

153 
{ 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

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

155 
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

156 
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

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

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

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

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

161 
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

162 
qed 
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 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

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

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

167 

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

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

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

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

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

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

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

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

175 
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

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

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

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

179 

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

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

181 
{ 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

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

183 
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

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

185 
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

186 
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

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

188 
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

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

190 

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

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

192 
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

193 

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

194 

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

195 
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

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

197 

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

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

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

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

201 
"(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

202 
"(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

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

204 
"(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

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

206 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27717
diff
changeset

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

208 
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

209 
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

210 
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

211 
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

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

213 
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

214 
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

215 
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

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

217 
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

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

219 
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

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

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

222 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27717
diff
changeset

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

224 
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

225 
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

226 
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

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

228 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

248 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27717
diff
changeset

249 
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

250 
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

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

252 

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

253 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

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

255 

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

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

257 
"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

258 
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

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

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

261 

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

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

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

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

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

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

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

268 

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

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

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

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

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

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

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

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

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

277 
apply clarsimp defer 1 
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 (elim exE) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

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

283 

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

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

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

286 
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

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

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

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

290 
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

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

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

293 

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

294 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

308 
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

309 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

340 

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

341 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

342 
subsection {* Ideals and Divisibility *} 
20318
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 
lemma int_Idl_subset_ideal: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

345 
"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

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

347 

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

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

349 
"(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

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

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

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

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

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

355 

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

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

357 
"(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

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

359 
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

360 
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

361 

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

362 
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

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

364 
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

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

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

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

368 

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

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

370 
"(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

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

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

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

374 

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

375 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

376 
subsection {* Ideals and the Modulus *} 
20318
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 
constdefs 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

380 
"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

381 

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

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

383 
ZMod_def genideal_def 
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 
lemma rcos_zfact: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

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

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

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

390 
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

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

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

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

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

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

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

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

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

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

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

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

402 

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

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

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

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

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

407 
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

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

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

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

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

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

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

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

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

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

417 

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

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

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

420 
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

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

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

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

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

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

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

427 

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

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

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

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

431 
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

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

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

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

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

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

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

438 
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

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

440 
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

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

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

443 

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

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

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

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

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

448 
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

449 
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

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

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

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

453 

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

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

455 
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

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

457 

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

458 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

459 
subsection {* Factorization *} 
20318
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 
constdefs 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset

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

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

464 

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

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

466 

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

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

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

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

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

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

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

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

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

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

476 

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

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

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

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

480 
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

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

482 

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

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

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

485 
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

486 
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

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

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

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

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

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

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

493 

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

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

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

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

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

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

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

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

501 

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

502 
end 