author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 66453 | cc19f7ca2ed6 |
child 67123 | 3fe40ff1b921 |
permissions | -rw-r--r-- |
64962 | 1 |
(* Title: HOL/Decision_Procs/Algebra_Aux.thy |
2 |
Author: Stefan Berghofer |
|
3 |
*) |
|
4 |
||
5 |
section \<open>Things that can be added to the Algebra library\<close> |
|
6 |
||
7 |
theory Algebra_Aux |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
64998
diff
changeset
|
8 |
imports "HOL-Algebra.Ring" |
64962 | 9 |
begin |
10 |
||
11 |
definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where |
|
12 |
"\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> = (op \<oplus>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> ^^ n) \<zero>\<^bsub>R\<^esub>" |
|
13 |
||
14 |
definition of_integer :: "('a, 'm) ring_scheme \<Rightarrow> int \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<index>") where |
|
15 |
"\<guillemotleft>i\<guillemotright>\<^bsub>R\<^esub> = (if 0 \<le> i then \<guillemotleft>nat i\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> else \<ominus>\<^bsub>R\<^esub> \<guillemotleft>nat (- i)\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub>)" |
|
16 |
||
17 |
context ring begin |
|
18 |
||
19 |
lemma of_nat_0 [simp]: "\<guillemotleft>0\<guillemotright>\<^sub>\<nat> = \<zero>" |
|
20 |
by (simp add: of_natural_def) |
|
21 |
||
22 |
lemma of_nat_Suc [simp]: "\<guillemotleft>Suc n\<guillemotright>\<^sub>\<nat> = \<one> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>" |
|
23 |
by (simp add: of_natural_def) |
|
24 |
||
25 |
lemma of_int_0 [simp]: "\<guillemotleft>0\<guillemotright> = \<zero>" |
|
26 |
by (simp add: of_integer_def) |
|
27 |
||
28 |
lemma of_nat_closed [simp]: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat> \<in> carrier R" |
|
29 |
by (induct n) simp_all |
|
30 |
||
31 |
lemma of_int_closed [simp]: "\<guillemotleft>i\<guillemotright> \<in> carrier R" |
|
32 |
by (simp add: of_integer_def) |
|
33 |
||
34 |
lemma of_int_minus [simp]: "\<guillemotleft>- i\<guillemotright> = \<ominus> \<guillemotleft>i\<guillemotright>" |
|
35 |
by (simp add: of_integer_def) |
|
36 |
||
37 |
lemma of_nat_add [simp]: "\<guillemotleft>m + n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>" |
|
38 |
by (induct m) (simp_all add: a_ac) |
|
39 |
||
40 |
lemma of_nat_diff [simp]: "n \<le> m \<Longrightarrow> \<guillemotleft>m - n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>" |
|
41 |
proof (induct m arbitrary: n) |
|
42 |
case (Suc m) |
|
43 |
note Suc' = this |
|
44 |
show ?case |
|
45 |
proof (cases n) |
|
46 |
case (Suc k) |
|
47 |
with Suc' have "\<guillemotleft>Suc m - Suc k\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>" by simp |
|
48 |
also have "\<dots> = \<one> \<oplus> \<ominus> \<one> \<oplus> (\<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>)" |
|
49 |
by (simp add: r_neg) |
|
50 |
also have "\<dots> = \<guillemotleft>Suc m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>Suc k\<guillemotright>\<^sub>\<nat>" |
|
51 |
by (simp add: minus_eq minus_add a_ac) |
|
52 |
finally show ?thesis using Suc by simp |
|
53 |
qed (simp add: minus_eq) |
|
54 |
qed (simp add: minus_eq) |
|
55 |
||
56 |
lemma of_int_add [simp]: "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<oplus> \<guillemotleft>j\<guillemotright>" |
|
57 |
proof (cases "0 \<le> i") |
|
58 |
case True |
|
59 |
show ?thesis |
|
60 |
proof (cases "0 \<le> j") |
|
61 |
case True |
|
64998 | 62 |
with \<open>0 \<le> i\<close> show ?thesis by (simp add: of_integer_def nat_add_distrib) |
64962 | 63 |
next |
64 |
case False |
|
65 |
show ?thesis |
|
66 |
proof (cases "0 \<le> i + j") |
|
67 |
case True |
|
68 |
then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (i - (- j))\<guillemotright>\<^sub>\<nat>" |
|
69 |
by (simp add: of_integer_def) |
|
64998 | 70 |
also from True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close> |
64962 | 71 |
have "nat (i - (- j)) = nat i - nat (- j)" |
72 |
by (simp add: nat_diff_distrib) |
|
64998 | 73 |
finally show ?thesis using True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close> |
64962 | 74 |
by (simp add: minus_eq of_integer_def) |
75 |
next |
|
76 |
case False |
|
77 |
then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- j - i)\<guillemotright>\<^sub>\<nat>" |
|
78 |
by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac) |
|
64998 | 79 |
also from False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close> |
64962 | 80 |
have "nat (- j - i) = nat (- j) - nat i" |
81 |
by (simp add: nat_diff_distrib) |
|
64998 | 82 |
finally show ?thesis using False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close> |
64962 | 83 |
by (simp add: minus_eq minus_add a_ac of_integer_def) |
84 |
qed |
|
85 |
qed |
|
86 |
next |
|
87 |
case False |
|
88 |
show ?thesis |
|
89 |
proof (cases "0 \<le> j") |
|
90 |
case True |
|
91 |
show ?thesis |
|
92 |
proof (cases "0 \<le> i + j") |
|
93 |
case True |
|
94 |
then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (j - (- i))\<guillemotright>\<^sub>\<nat>" |
|
95 |
by (simp add: of_integer_def add_ac) |
|
64998 | 96 |
also from True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close> |
64962 | 97 |
have "nat (j - (- i)) = nat j - nat (- i)" |
98 |
by (simp add: nat_diff_distrib) |
|
64998 | 99 |
finally show ?thesis using True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close> |
64962 | 100 |
by (simp add: minus_eq minus_add a_ac of_integer_def) |
101 |
next |
|
102 |
case False |
|
103 |
then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- i - j)\<guillemotright>\<^sub>\<nat>" |
|
104 |
by (simp add: of_integer_def) |
|
64998 | 105 |
also from False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close> |
64962 | 106 |
have "nat (- i - j) = nat (- i) - nat j" |
107 |
by (simp add: nat_diff_distrib) |
|
64998 | 108 |
finally show ?thesis using False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close> |
64962 | 109 |
by (simp add: minus_eq minus_add of_integer_def) |
110 |
qed |
|
111 |
next |
|
112 |
case False |
|
64998 | 113 |
with \<open>\<not> 0 \<le> i\<close> show ?thesis |
64962 | 114 |
by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus |
115 |
del: add_uminus_conv_diff uminus_add_conv_diff) |
|
116 |
qed |
|
117 |
qed |
|
118 |
||
119 |
lemma of_int_diff [simp]: "\<guillemotleft>i - j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<ominus> \<guillemotleft>j\<guillemotright>" |
|
120 |
by (simp only: diff_conv_add_uminus of_int_add) (simp add: minus_eq) |
|
121 |
||
122 |
lemma of_nat_mult [simp]: "\<guillemotleft>i * j\<guillemotright>\<^sub>\<nat> = \<guillemotleft>i\<guillemotright>\<^sub>\<nat> \<otimes> \<guillemotleft>j\<guillemotright>\<^sub>\<nat>" |
|
123 |
by (induct i) (simp_all add: l_distr) |
|
124 |
||
125 |
lemma of_int_mult [simp]: "\<guillemotleft>i * j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<otimes> \<guillemotleft>j\<guillemotright>" |
|
126 |
proof (cases "0 \<le> i") |
|
127 |
case True |
|
128 |
show ?thesis |
|
129 |
proof (cases "0 \<le> j") |
|
130 |
case True |
|
64998 | 131 |
with \<open>0 \<le> i\<close> show ?thesis |
64962 | 132 |
by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff) |
133 |
next |
|
134 |
case False |
|
64998 | 135 |
with \<open>0 \<le> i\<close> show ?thesis |
64962 | 136 |
by (simp add: of_integer_def zero_le_mult_iff |
137 |
minus_mult_right nat_mult_distrib r_minus |
|
138 |
del: minus_mult_right [symmetric]) |
|
139 |
qed |
|
140 |
next |
|
141 |
case False |
|
142 |
show ?thesis |
|
143 |
proof (cases "0 \<le> j") |
|
144 |
case True |
|
64998 | 145 |
with \<open>\<not> 0 \<le> i\<close> show ?thesis |
64962 | 146 |
by (simp add: of_integer_def zero_le_mult_iff |
147 |
minus_mult_left nat_mult_distrib l_minus |
|
148 |
del: minus_mult_left [symmetric]) |
|
149 |
next |
|
150 |
case False |
|
64998 | 151 |
with \<open>\<not> 0 \<le> i\<close> show ?thesis |
64962 | 152 |
by (simp add: of_integer_def zero_le_mult_iff |
153 |
minus_mult_minus [of i j, symmetric] nat_mult_distrib |
|
154 |
l_minus r_minus |
|
155 |
del: minus_mult_minus |
|
156 |
minus_mult_left [symmetric] minus_mult_right [symmetric]) |
|
157 |
qed |
|
158 |
qed |
|
159 |
||
160 |
lemma of_int_1 [simp]: "\<guillemotleft>1\<guillemotright> = \<one>" |
|
161 |
by (simp add: of_integer_def) |
|
162 |
||
163 |
lemma of_int_2: "\<guillemotleft>2\<guillemotright> = \<one> \<oplus> \<one>" |
|
164 |
by (simp add: of_integer_def numeral_2_eq_2) |
|
165 |
||
166 |
lemma minus_0_r [simp]: "x \<in> carrier R \<Longrightarrow> x \<ominus> \<zero> = x" |
|
167 |
by (simp add: minus_eq) |
|
168 |
||
169 |
lemma minus_0_l [simp]: "x \<in> carrier R \<Longrightarrow> \<zero> \<ominus> x = \<ominus> x" |
|
170 |
by (simp add: minus_eq) |
|
171 |
||
172 |
lemma eq_diff0: |
|
173 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
|
174 |
shows "(x \<ominus> y = \<zero>) = (x = y)" |
|
175 |
proof |
|
176 |
assume "x \<ominus> y = \<zero>" |
|
177 |
with assms have "x \<oplus> (\<ominus> y \<oplus> y) = y" |
|
178 |
by (simp add: minus_eq a_assoc [symmetric]) |
|
179 |
with assms show "x = y" by (simp add: l_neg) |
|
180 |
next |
|
181 |
assume "x = y" |
|
182 |
with assms show "x \<ominus> y = \<zero>" by (simp add: minus_eq r_neg) |
|
183 |
qed |
|
184 |
||
185 |
lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x (^) (2::nat) = x \<otimes> x" |
|
186 |
by (simp add: numeral_eq_Suc) |
|
187 |
||
188 |
lemma eq_neg_iff_add_eq_0: |
|
189 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
|
190 |
shows "(x = \<ominus> y) = (x \<oplus> y = \<zero>)" |
|
191 |
proof |
|
192 |
assume "x = \<ominus> y" |
|
193 |
with assms show "x \<oplus> y = \<zero>" by (simp add: l_neg) |
|
194 |
next |
|
195 |
assume "x \<oplus> y = \<zero>" |
|
196 |
with assms have "x \<oplus> (y \<oplus> \<ominus> y) = \<zero> \<oplus> \<ominus> y" |
|
197 |
by (simp add: a_assoc [symmetric]) |
|
198 |
with assms show "x = \<ominus> y" |
|
199 |
by (simp add: r_neg) |
|
200 |
qed |
|
201 |
||
202 |
lemma neg_equal_iff_equal: |
|
203 |
assumes x: "x \<in> carrier R" and y: "y \<in> carrier R" |
|
204 |
shows "(\<ominus> x = \<ominus> y) = (x = y)" |
|
205 |
proof |
|
206 |
assume "\<ominus> x = \<ominus> y" |
|
207 |
then have "\<ominus> (\<ominus> x) = \<ominus> (\<ominus> y)" by simp |
|
208 |
with x y show "x = y" by simp |
|
209 |
next |
|
210 |
assume "x = y" |
|
211 |
then show "\<ominus> x = \<ominus> y" by simp |
|
212 |
qed |
|
213 |
||
214 |
lemma neg_equal_swap: |
|
215 |
assumes x: "x \<in> carrier R" and y: "y \<in> carrier R" |
|
216 |
shows "(\<ominus> x = y) = (x = \<ominus> y)" |
|
217 |
using assms neg_equal_iff_equal [of x "\<ominus> y"] |
|
218 |
by simp |
|
219 |
||
220 |
lemma mult2: "x \<in> carrier R \<Longrightarrow> x \<oplus> x = \<guillemotleft>2\<guillemotright> \<otimes> x" |
|
221 |
by (simp add: of_int_2 l_distr) |
|
222 |
||
223 |
end |
|
224 |
||
225 |
lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> (^) n" |
|
226 |
by (induct n) (simp_all add: m_ac) |
|
227 |
||
228 |
definition cring_class_ops :: "'a::comm_ring_1 ring" where |
|
229 |
"cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>" |
|
230 |
||
231 |
lemma cring_class: "cring cring_class_ops" |
|
232 |
apply unfold_locales |
|
233 |
apply (auto simp add: cring_class_ops_def ring_distribs Units_def) |
|
234 |
apply (rule_tac x="- x" in exI) |
|
235 |
apply simp |
|
236 |
done |
|
237 |
||
238 |
lemma carrier_class: "x \<in> carrier cring_class_ops" |
|
239 |
by (simp add: cring_class_ops_def) |
|
240 |
||
241 |
lemma zero_class: "\<zero>\<^bsub>cring_class_ops\<^esub> = 0" |
|
242 |
by (simp add: cring_class_ops_def) |
|
243 |
||
244 |
lemma one_class: "\<one>\<^bsub>cring_class_ops\<^esub> = 1" |
|
245 |
by (simp add: cring_class_ops_def) |
|
246 |
||
247 |
lemma plus_class: "x \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" |
|
248 |
by (simp add: cring_class_ops_def) |
|
249 |
||
250 |
lemma times_class: "x \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" |
|
251 |
by (simp add: cring_class_ops_def) |
|
252 |
||
253 |
lemma uminus_class: "\<ominus>\<^bsub>cring_class_ops\<^esub> x = - x" |
|
254 |
apply (simp add: a_inv_def m_inv_def cring_class_ops_def) |
|
255 |
apply (rule the_equality) |
|
256 |
apply (simp_all add: eq_neg_iff_add_eq_0) |
|
257 |
done |
|
258 |
||
259 |
lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" |
|
260 |
by (simp add: a_minus_def carrier_class plus_class uminus_class) |
|
261 |
||
262 |
lemma power_class: "x (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" |
|
263 |
by (induct n) (simp_all add: one_class times_class |
|
264 |
monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]] |
|
265 |
monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]) |
|
266 |
||
267 |
lemma of_nat_class: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" |
|
268 |
by (induct n) (simp_all add: cring_class_ops_def of_natural_def) |
|
269 |
||
270 |
lemma of_int_class: "\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub> = of_int i" |
|
271 |
by (simp add: of_integer_def of_nat_class uminus_class) |
|
272 |
||
273 |
lemmas class_simps = zero_class one_class plus_class minus_class uminus_class |
|
274 |
times_class power_class of_nat_class of_int_class carrier_class |
|
275 |
||
276 |
interpretation cring_class: cring "cring_class_ops::'a::comm_ring_1 ring" |
|
277 |
rewrites |
|
278 |
"(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and |
|
279 |
"(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and |
|
280 |
"(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and |
|
281 |
"(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and |
|
282 |
"\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and |
|
283 |
"(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and |
|
284 |
"(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and |
|
285 |
"\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and |
|
286 |
"((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and |
|
287 |
"(Int.of_int (numeral m)::'a) = numeral m" |
|
288 |
by (simp_all add: cring_class class_simps) |
|
289 |
||
290 |
lemma (in domain) nat_pow_eq_0_iff [simp]: |
|
291 |
"a \<in> carrier R \<Longrightarrow> (a (^) (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)" |
|
292 |
by (induct n) (auto simp add: integral_iff) |
|
293 |
||
294 |
lemma (in domain) square_eq_iff: |
|
295 |
assumes "x \<in> carrier R" "y \<in> carrier R" |
|
296 |
shows "(x \<otimes> x = y \<otimes> y) = (x = y \<or> x = \<ominus> y)" |
|
297 |
proof |
|
298 |
assume "x \<otimes> x = y \<otimes> y" |
|
299 |
with assms have "(x \<ominus> y) \<otimes> (x \<oplus> y) = x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) \<oplus> (y \<otimes> y \<oplus> \<ominus> (y \<otimes> y))" |
|
300 |
by (simp add: r_distr l_distr minus_eq r_minus m_comm a_ac) |
|
301 |
with assms show "x = y \<or> x = \<ominus> y" |
|
302 |
by (simp add: integral_iff eq_neg_iff_add_eq_0 eq_diff0 r_neg) |
|
303 |
next |
|
304 |
assume "x = y \<or> x = \<ominus> y" |
|
305 |
with assms show "x \<otimes> x = y \<otimes> y" by (auto simp add: l_minus r_minus) |
|
306 |
qed |
|
307 |
||
308 |
definition |
|
309 |
m_div :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oslash>\<index>" 70) where |
|
310 |
"x \<oslash>\<^bsub>G\<^esub> y = (if y = \<zero>\<^bsub>G\<^esub> then \<zero>\<^bsub>G\<^esub> else x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)" |
|
311 |
||
312 |
context field |
|
313 |
begin |
|
314 |
||
315 |
lemma inv_closed [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<in> carrier R" |
|
316 |
by (simp add: field_Units) |
|
317 |
||
318 |
lemma l_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<otimes> x = \<one>" |
|
319 |
by (simp add: field_Units) |
|
320 |
||
321 |
lemma r_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> x \<otimes> inv x = \<one>" |
|
322 |
by (simp add: field_Units) |
|
323 |
||
324 |
lemma inverse_unique: |
|
325 |
assumes a: "a \<in> carrier R" |
|
326 |
and b: "b \<in> carrier R" |
|
327 |
and ab: "a \<otimes> b = \<one>" |
|
328 |
shows "inv a = b" |
|
329 |
proof - |
|
330 |
have "a \<noteq> \<zero>" using ab b by (cases "a = \<zero>") simp_all |
|
331 |
moreover with a have "inv a \<otimes> (a \<otimes> b) = inv a" by (simp add: ab) |
|
332 |
ultimately show ?thesis using a b by (simp add: m_assoc [symmetric]) |
|
333 |
qed |
|
334 |
||
335 |
lemma nonzero_inverse_inverse_eq: |
|
336 |
"a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> inv (inv a) = a" |
|
337 |
by (rule inverse_unique) simp_all |
|
338 |
||
339 |
lemma inv_1 [simp]: "inv \<one> = \<one>" |
|
340 |
by (rule inverse_unique) simp_all |
|
341 |
||
342 |
lemma nonzero_inverse_mult_distrib: |
|
343 |
assumes "a \<in> carrier R" and "b \<in> carrier R" and "a \<noteq> \<zero>" and "b \<noteq> \<zero>" |
|
344 |
shows "inv (a \<otimes> b) = inv b \<otimes> inv a" |
|
345 |
proof - |
|
346 |
have "a \<otimes> (b \<otimes> inv b) \<otimes> inv a = \<one>" using assms by simp |
|
347 |
hence eq: "a \<otimes> b \<otimes> (inv b \<otimes> inv a) = \<one>" using assms |
|
348 |
by (simp only: m_assoc m_closed inv_closed assms) |
|
349 |
from inverse_unique [OF _ _ eq] assms |
|
350 |
show ?thesis by simp |
|
351 |
qed |
|
352 |
||
353 |
lemma nonzero_imp_inverse_nonzero: |
|
354 |
assumes "a \<in> carrier R" and "a \<noteq> \<zero>" |
|
355 |
shows "inv a \<noteq> \<zero>" |
|
356 |
proof |
|
357 |
assume ianz: "inv a = \<zero>" |
|
358 |
from assms |
|
359 |
have "\<one> = a \<otimes> inv a" by simp |
|
360 |
also with assms have "... = \<zero>" by (simp add: ianz) |
|
361 |
finally have "\<one> = \<zero>" . |
|
362 |
thus False by (simp add: eq_commute) |
|
363 |
qed |
|
364 |
||
365 |
lemma nonzero_divide_divide_eq_left: |
|
366 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> |
|
367 |
a \<oslash> b \<oslash> c = a \<oslash> (b \<otimes> c)" |
|
368 |
by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff) |
|
369 |
||
370 |
lemma nonzero_times_divide_eq: |
|
371 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow> |
|
372 |
b \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<otimes> (c \<oslash> d) = (a \<otimes> c) \<oslash> (b \<otimes> d)" |
|
373 |
by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff) |
|
374 |
||
375 |
lemma nonzero_divide_divide_eq: |
|
376 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow> |
|
377 |
b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<oslash> (c \<oslash> d) = (a \<otimes> d) \<oslash> (b \<otimes> c)" |
|
378 |
by (simp add: m_div_def nonzero_inverse_mult_distrib |
|
379 |
nonzero_imp_inverse_nonzero nonzero_inverse_inverse_eq m_ac integral_iff) |
|
380 |
||
381 |
lemma divide_1 [simp]: "x \<in> carrier R \<Longrightarrow> x \<oslash> \<one> = x" |
|
382 |
by (simp add: m_div_def) |
|
383 |
||
384 |
lemma add_frac_eq: |
|
385 |
assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R" |
|
386 |
and "y \<noteq> \<zero>" and "z \<noteq> \<zero>" |
|
387 |
shows "x \<oslash> y \<oplus> w \<oslash> z = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)" |
|
388 |
proof - |
|
389 |
from assms |
|
390 |
have "x \<oslash> y \<oplus> w \<oslash> z = x \<otimes> inv y \<otimes> (z \<otimes> inv z) \<oplus> w \<otimes> inv z \<otimes> (y \<otimes> inv y)" |
|
391 |
by (simp add: m_div_def) |
|
392 |
also from assms have "\<dots> = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)" |
|
393 |
by (simp add: m_div_def nonzero_inverse_mult_distrib r_distr m_ac integral_iff del: r_inv) |
|
394 |
finally show ?thesis . |
|
395 |
qed |
|
396 |
||
397 |
lemma div_closed [simp]: |
|
398 |
"x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> y \<noteq> \<zero> \<Longrightarrow> x \<oslash> y \<in> carrier R" |
|
399 |
by (simp add: m_div_def) |
|
400 |
||
401 |
lemma minus_divide_left [simp]: |
|
402 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> \<ominus> (a \<oslash> b) = \<ominus> a \<oslash> b" |
|
403 |
by (simp add: m_div_def l_minus) |
|
404 |
||
405 |
lemma diff_frac_eq: |
|
406 |
assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R" |
|
407 |
and "y \<noteq> \<zero>" and "z \<noteq> \<zero>" |
|
408 |
shows "x \<oslash> y \<ominus> w \<oslash> z = (x \<otimes> z \<ominus> w \<otimes> y) \<oslash> (y \<otimes> z)" |
|
409 |
using assms |
|
410 |
by (simp add: minus_eq l_minus add_frac_eq) |
|
411 |
||
412 |
lemma nonzero_mult_divide_mult_cancel_left [simp]: |
|
413 |
assumes "a \<in> carrier R" and "b \<in> carrier R" and "c \<in> carrier R" |
|
414 |
and "b \<noteq> \<zero>" and "c \<noteq> \<zero>" |
|
415 |
shows "(c \<otimes> a) \<oslash> (c \<otimes> b) = a \<oslash> b" |
|
416 |
proof - |
|
417 |
from assms have "(c \<otimes> a) \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)" |
|
418 |
by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff) |
|
419 |
also from assms have "\<dots> = a \<otimes> inv b \<otimes> (inv c \<otimes> c)" |
|
420 |
by (simp add: m_ac) |
|
421 |
also from assms have "\<dots> = a \<otimes> inv b" by simp |
|
422 |
finally show ?thesis using assms by (simp add: m_div_def) |
|
423 |
qed |
|
424 |
||
425 |
lemma times_divide_eq_left [simp]: |
|
426 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> |
|
427 |
(b \<oslash> c) \<otimes> a = b \<otimes> a \<oslash> c" |
|
428 |
by (simp add: m_div_def m_ac) |
|
429 |
||
430 |
lemma times_divide_eq_right [simp]: |
|
431 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> |
|
432 |
a \<otimes> (b \<oslash> c) = a \<otimes> b \<oslash> c" |
|
433 |
by (simp add: m_div_def m_ac) |
|
434 |
||
435 |
lemma nonzero_power_divide: |
|
436 |
"a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> |
|
437 |
(a \<oslash> b) (^) (n::nat) = a (^) n \<oslash> b (^) n" |
|
438 |
by (induct n) (simp_all add: nonzero_divide_divide_eq_left) |
|
439 |
||
440 |
lemma r_diff_distr: |
|
441 |
"x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow> |
|
442 |
z \<otimes> (x \<ominus> y) = z \<otimes> x \<ominus> z \<otimes> y" |
|
443 |
by (simp add: minus_eq r_distr r_minus) |
|
444 |
||
445 |
lemma divide_zero_left [simp]: |
|
446 |
"a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> \<zero> \<oslash> a = \<zero>" |
|
447 |
by (simp add: m_div_def) |
|
448 |
||
449 |
lemma divide_self: "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> a \<oslash> a = \<one>" |
|
450 |
by (simp add: m_div_def) |
|
451 |
||
452 |
lemma divide_eq_0_iff: |
|
453 |
assumes "a \<in> carrier R" |
|
454 |
and "b \<in> carrier R" |
|
455 |
and "b \<noteq> \<zero>" |
|
456 |
shows "(a \<oslash> b = \<zero>) = (a = \<zero>)" |
|
457 |
proof |
|
458 |
assume "a = \<zero>" |
|
459 |
with assms show "a \<oslash> b = \<zero>" by simp |
|
460 |
next |
|
461 |
assume "a \<oslash> b = \<zero>" |
|
462 |
with assms have "b \<otimes> (a \<oslash> b) = b \<otimes> \<zero>" by simp |
|
463 |
also from assms have "b \<otimes> (a \<oslash> b) = b \<otimes> a \<oslash> b" by simp |
|
464 |
also from assms have "b \<otimes> a = a \<otimes> b" by (simp add: m_comm) |
|
465 |
also from assms have "a \<otimes> b \<oslash> b = a \<otimes> (b \<oslash> b)" by simp |
|
466 |
also from assms have "b \<oslash> b = \<one>" by (simp add: divide_self) |
|
467 |
finally show "a = \<zero>" using assms by simp |
|
468 |
qed |
|
469 |
||
470 |
end |
|
471 |
||
472 |
lemma field_class: "field (cring_class_ops::'a::field ring)" |
|
473 |
apply unfold_locales |
|
474 |
apply (simp_all add: cring_class_ops_def) |
|
475 |
apply (auto simp add: Units_def) |
|
476 |
apply (rule_tac x="1 / x" in exI) |
|
477 |
apply simp |
|
478 |
done |
|
479 |
||
480 |
lemma div_class: "(x::'a::field) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y" |
|
481 |
apply (simp add: m_div_def m_inv_def class_simps) |
|
482 |
apply (rule impI) |
|
483 |
apply (rule ssubst [OF the_equality, of _ "1 / y"]) |
|
484 |
apply simp_all |
|
485 |
apply (drule conjunct2) |
|
486 |
apply (drule_tac f="\<lambda>x. x / y" in arg_cong) |
|
487 |
apply simp |
|
488 |
done |
|
489 |
||
490 |
interpretation field_class: field "cring_class_ops::'a::field ring" |
|
491 |
rewrites |
|
492 |
"(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and |
|
493 |
"(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and |
|
494 |
"(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and |
|
495 |
"(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and |
|
496 |
"\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and |
|
497 |
"(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and |
|
498 |
"(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and |
|
499 |
"\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and |
|
500 |
"((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and |
|
501 |
"(x::'a) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y" and |
|
502 |
"(Int.of_int (numeral m)::'a) = numeral m" |
|
503 |
by (simp_all add: field_class class_simps div_class) |
|
504 |
||
505 |
end |