author | wenzelm |
Tue, 09 Dec 2014 19:39:40 +0100 | |
changeset 59119 | c90c02940964 |
parent 58889 | 5b7a9633cfa8 |
child 59548 | d9304532c7ab |
permissions | -rw-r--r-- |
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset
|
1 |
(* Title: HOL/Semiring_Normalization.thy |
23252 | 2 |
Author: Amine Chaieb, TU Muenchen |
3 |
*) |
|
4 |
||
58889 | 5 |
section {* Semiring normalization *} |
28402 | 6 |
|
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset
|
7 |
theory Semiring_Normalization |
36699
816da1023508
moved nat_arith ot Nat_Numeral: clarified normalizer setup
haftmann
parents:
36698
diff
changeset
|
8 |
imports Numeral_Simprocs Nat_Transfer |
23252 | 9 |
begin |
10 |
||
36873 | 11 |
text {* Prelude *} |
12 |
||
13 |
class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + |
|
14 |
assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |
|
15 |
begin |
|
16 |
||
17 |
lemma crossproduct_noteq: |
|
18 |
"a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c" |
|
19 |
by (simp add: crossproduct_eq) |
|
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
20 |
|
36873 | 21 |
lemma add_scale_eq_noteq: |
22 |
"r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d" |
|
23 |
proof (rule notI) |
|
24 |
assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d" |
|
25 |
and eq: "a + (r * c) = b + (r * d)" |
|
26 |
have "(0 * d) + (r * c) = (0 * c) + (r * d)" |
|
27 |
using add_imp_eq eq mult_zero_left by (simp add: cnd) |
|
28 |
then show False using crossproduct_eq [of 0 d] nz cnd by simp |
|
29 |
qed |
|
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
30 |
|
36873 | 31 |
lemma add_0_iff: |
32 |
"b = b + a \<longleftrightarrow> a = 0" |
|
33 |
using add_imp_eq [of b a 0] by auto |
|
34 |
||
35 |
end |
|
36 |
||
37946 | 37 |
subclass (in idom) comm_semiring_1_cancel_crossproduct |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
38 |
proof |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
39 |
fix w x y z |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
40 |
show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
41 |
proof |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
42 |
assume "w * y + x * z = w * z + x * y" |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
43 |
then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
44 |
then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
45 |
then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
46 |
then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
47 |
then show "w = x \<or> y = z" by auto |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
54230
diff
changeset
|
48 |
qed (auto simp add: ac_simps) |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
49 |
qed |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
50 |
|
36873 | 51 |
instance nat :: comm_semiring_1_cancel_crossproduct |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
52 |
proof |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
53 |
fix w x y z :: nat |
36873 | 54 |
have aux: "\<And>y z. y < z \<Longrightarrow> w * y + x * z = w * z + x * y \<Longrightarrow> w = x" |
55 |
proof - |
|
56 |
fix y z :: nat |
|
57 |
assume "y < z" then have "\<exists>k. z = y + k \<and> k \<noteq> 0" by (intro exI [of _ "z - y"]) auto |
|
58 |
then obtain k where "z = y + k" and "k \<noteq> 0" by blast |
|
59 |
assume "w * y + x * z = w * z + x * y" |
|
60 |
then have "(w * y + x * y) + x * k = (w * y + x * y) + w * k" by (simp add: `z = y + k` algebra_simps) |
|
61 |
then have "x * k = w * k" by simp |
|
62 |
then show "w = x" using `k \<noteq> 0` by simp |
|
63 |
qed |
|
64 |
show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |
|
65 |
by (auto simp add: neq_iff dest!: aux) |
|
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
66 |
qed |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
67 |
|
36873 | 68 |
text {* Semiring normalization proper *} |
36871 | 69 |
|
58826 | 70 |
ML_file "Tools/semiring_normalizer.ML" |
23252 | 71 |
|
36871 | 72 |
context comm_semiring_1 |
73 |
begin |
|
74 |
||
36872 | 75 |
lemma normalizing_semiring_ops: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
76 |
shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
77 |
and "TERM 0" and "TERM 1" . |
23252 | 78 |
|
36872 | 79 |
lemma normalizing_semiring_rules: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
80 |
"(a * m) + (b * m) = (a + b) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
81 |
"(a * m) + m = (a + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
82 |
"m + (a * m) = (a + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
83 |
"m + m = (1 + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
84 |
"0 + a = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
85 |
"a + 0 = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
86 |
"a * b = b * a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
87 |
"(a + b) * c = (a * c) + (b * c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
88 |
"0 * a = 0" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
89 |
"a * 0 = 0" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
90 |
"1 * a = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
91 |
"a * 1 = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
92 |
"(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
93 |
"(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
94 |
"(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
95 |
"(lx * ly) * rx = (lx * rx) * ly" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
96 |
"(lx * ly) * rx = lx * (ly * rx)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
97 |
"lx * (rx * ry) = (lx * rx) * ry" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
98 |
"lx * (rx * ry) = rx * (lx * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
99 |
"(a + b) + (c + d) = (a + c) + (b + d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
100 |
"(a + b) + c = a + (b + c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
101 |
"a + (c + d) = c + (a + d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
102 |
"(a + b) + c = (a + c) + b" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
103 |
"a + c = c + a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
104 |
"a + (c + d) = (a + c) + d" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
105 |
"(x ^ p) * (x ^ q) = x ^ (p + q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
106 |
"x * (x ^ q) = x ^ (Suc q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
107 |
"(x ^ q) * x = x ^ (Suc q)" |
53076 | 108 |
"x * x = x\<^sup>2" |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
109 |
"(x * y) ^ q = (x ^ q) * (y ^ q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
110 |
"(x ^ p) ^ q = x ^ (p * q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
111 |
"x ^ 0 = 1" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
112 |
"x ^ 1 = x" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
113 |
"x * (y + z) = (x * y) + (x * z)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
114 |
"x ^ (Suc q) = x * (x ^ q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
115 |
"x ^ (2*n) = (x ^ n) * (x ^ n)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
116 |
"x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
37946
diff
changeset
|
117 |
by (simp_all add: algebra_simps power_add power2_eq_square |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
37946
diff
changeset
|
118 |
power_mult_distrib power_mult del: one_add_one) |
23252 | 119 |
|
36871 | 120 |
lemmas normalizing_comm_semiring_1_axioms = |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
121 |
comm_semiring_1_axioms [normalizer |
36872 | 122 |
semiring ops: normalizing_semiring_ops |
123 |
semiring rules: normalizing_semiring_rules] |
|
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
124 |
|
36871 | 125 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
126 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *} |
23573 | 127 |
|
36871 | 128 |
end |
23252 | 129 |
|
36871 | 130 |
context comm_ring_1 |
131 |
begin |
|
132 |
||
36872 | 133 |
lemma normalizing_ring_ops: shows "TERM (x- y)" and "TERM (- x)" . |
36871 | 134 |
|
36872 | 135 |
lemma normalizing_ring_rules: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
136 |
"- x = (- 1) * x" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
137 |
"x - y = x + (- y)" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53076
diff
changeset
|
138 |
by simp_all |
23252 | 139 |
|
36871 | 140 |
lemmas normalizing_comm_ring_1_axioms = |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
141 |
comm_ring_1_axioms [normalizer |
36872 | 142 |
semiring ops: normalizing_semiring_ops |
143 |
semiring rules: normalizing_semiring_rules |
|
144 |
ring ops: normalizing_ring_ops |
|
145 |
ring rules: normalizing_ring_rules] |
|
30866 | 146 |
|
36871 | 147 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
148 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *} |
23327 | 149 |
|
36871 | 150 |
end |
151 |
||
36873 | 152 |
context comm_semiring_1_cancel_crossproduct |
36871 | 153 |
begin |
154 |
||
155 |
declare |
|
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
156 |
normalizing_comm_semiring_1_axioms [normalizer del] |
23252 | 157 |
|
36871 | 158 |
lemmas |
36873 | 159 |
normalizing_comm_semiring_1_cancel_crossproduct_axioms = |
160 |
comm_semiring_1_cancel_crossproduct_axioms [normalizer |
|
36872 | 161 |
semiring ops: normalizing_semiring_ops |
162 |
semiring rules: normalizing_semiring_rules |
|
36873 | 163 |
idom rules: crossproduct_noteq add_scale_eq_noteq] |
23252 | 164 |
|
36871 | 165 |
declaration |
36873 | 166 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_crossproduct_axioms} *} |
23252 | 167 |
|
36871 | 168 |
end |
23252 | 169 |
|
36871 | 170 |
context idom |
171 |
begin |
|
172 |
||
173 |
declare normalizing_comm_ring_1_axioms [normalizer del] |
|
174 |
||
175 |
lemmas normalizing_idom_axioms = idom_axioms [normalizer |
|
36872 | 176 |
semiring ops: normalizing_semiring_ops |
177 |
semiring rules: normalizing_semiring_rules |
|
178 |
ring ops: normalizing_ring_ops |
|
179 |
ring rules: normalizing_ring_rules |
|
36873 | 180 |
idom rules: crossproduct_noteq add_scale_eq_noteq |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
181 |
ideal rules: right_minus_eq add_0_iff] |
23252 | 182 |
|
36871 | 183 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
184 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *} |
23252 | 185 |
|
36871 | 186 |
end |
187 |
||
188 |
context field |
|
189 |
begin |
|
190 |
||
36872 | 191 |
lemma normalizing_field_ops: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
192 |
shows "TERM (x / y)" and "TERM (inverse x)" . |
23327 | 193 |
|
36872 | 194 |
lemmas normalizing_field_rules = divide_inverse inverse_eq_divide |
28402 | 195 |
|
36871 | 196 |
lemmas normalizing_field_axioms = |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
197 |
field_axioms [normalizer |
36872 | 198 |
semiring ops: normalizing_semiring_ops |
199 |
semiring rules: normalizing_semiring_rules |
|
200 |
ring ops: normalizing_ring_ops |
|
201 |
ring rules: normalizing_ring_rules |
|
202 |
field ops: normalizing_field_ops |
|
203 |
field rules: normalizing_field_rules |
|
36873 | 204 |
idom rules: crossproduct_noteq add_scale_eq_noteq |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
205 |
ideal rules: right_minus_eq add_0_iff] |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
206 |
|
36871 | 207 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
208 |
{* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *} |
28402 | 209 |
|
36871 | 210 |
end |
211 |
||
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
212 |
hide_fact (open) normalizing_comm_semiring_1_axioms |
36873 | 213 |
normalizing_comm_semiring_1_cancel_crossproduct_axioms normalizing_semiring_ops normalizing_semiring_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
214 |
|
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
215 |
hide_fact (open) normalizing_comm_ring_1_axioms |
36872 | 216 |
normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
217 |
|
36872 | 218 |
hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
219 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
48891
diff
changeset
|
220 |
code_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
48891
diff
changeset
|
221 |
code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
37946
diff
changeset
|
222 |
|
28402 | 223 |
end |