author | haftmann |
Wed, 18 Feb 2015 22:46:47 +0100 | |
changeset 59553 | e87974cd9b86 |
parent 59551 | 5283e349b339 |
child 59554 | 4044f53326c9 |
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_rules: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
76 |
"(a * m) + (b * m) = (a + b) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
77 |
"(a * m) + m = (a + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
78 |
"m + (a * m) = (a + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
79 |
"m + m = (1 + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
80 |
"0 + a = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
81 |
"a + 0 = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
82 |
"a * b = b * a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
83 |
"(a + b) * c = (a * c) + (b * c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
84 |
"0 * a = 0" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
85 |
"a * 0 = 0" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
86 |
"1 * a = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
87 |
"a * 1 = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
88 |
"(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
89 |
"(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
90 |
"(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
91 |
"(lx * ly) * rx = (lx * rx) * ly" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
92 |
"(lx * ly) * rx = lx * (ly * rx)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
93 |
"lx * (rx * ry) = (lx * rx) * ry" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
94 |
"lx * (rx * ry) = rx * (lx * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
95 |
"(a + b) + (c + d) = (a + c) + (b + d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
96 |
"(a + b) + c = a + (b + c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
97 |
"a + (c + d) = c + (a + d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
98 |
"(a + b) + c = (a + c) + b" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
99 |
"a + c = c + a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
100 |
"a + (c + d) = (a + c) + d" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
101 |
"(x ^ p) * (x ^ q) = x ^ (p + q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
102 |
"x * (x ^ q) = x ^ (Suc q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
103 |
"(x ^ q) * x = x ^ (Suc q)" |
53076 | 104 |
"x * x = x\<^sup>2" |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
105 |
"(x * y) ^ q = (x ^ q) * (y ^ q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
106 |
"(x ^ p) ^ q = x ^ (p * q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
107 |
"x ^ 0 = 1" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
108 |
"x ^ 1 = x" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
109 |
"x * (y + z) = (x * y) + (x * z)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
110 |
"x ^ (Suc q) = x * (x ^ q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
111 |
"x ^ (2*n) = (x ^ n) * (x ^ n)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
37946
diff
changeset
|
112 |
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
|
113 |
power_mult_distrib power_mult del: one_add_one) |
23252 | 114 |
|
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
115 |
declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_axioms} |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
116 |
{semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}], |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
117 |
@{thms normalizing_semiring_rules}), ring = ([], []), field = ([], []), idom = [], ideal = []}\<close> |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
118 |
|
36871 | 119 |
end |
23252 | 120 |
|
36871 | 121 |
context comm_ring_1 |
122 |
begin |
|
123 |
||
36872 | 124 |
lemma normalizing_ring_rules: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
125 |
"- x = (- 1) * x" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
126 |
"x - y = x + (- y)" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53076
diff
changeset
|
127 |
by simp_all |
23252 | 128 |
|
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
129 |
declaration \<open>Semiring_Normalizer.declare @{thm comm_ring_1_axioms} |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
130 |
{semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
131 |
ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], @{thms normalizing_ring_rules}), field = ([], []), idom = [], ideal = []}\<close> |
30866 | 132 |
|
36871 | 133 |
end |
134 |
||
36873 | 135 |
context comm_semiring_1_cancel_crossproduct |
36871 | 136 |
begin |
137 |
||
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
138 |
declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
139 |
{semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
140 |
ring = ([], []), field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ideal = []}\<close> |
23252 | 141 |
|
36871 | 142 |
end |
23252 | 143 |
|
36871 | 144 |
context idom |
145 |
begin |
|
146 |
||
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
147 |
declaration \<open>Semiring_Normalizer.declare @{thm idom_axioms} |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
148 |
{semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_ring_1_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
149 |
ring = Semiring_Normalizer.the_ring @{context} @{thm comm_ring_1_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
150 |
field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
151 |
ideal = @{thms right_minus_eq add_0_iff}}\<close> |
23252 | 152 |
|
36871 | 153 |
end |
154 |
||
155 |
context field |
|
156 |
begin |
|
157 |
||
36872 | 158 |
lemmas normalizing_field_rules = divide_inverse inverse_eq_divide |
28402 | 159 |
|
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
160 |
declaration \<open>Semiring_Normalizer.declare @{thm field_axioms} |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
161 |
{semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
162 |
ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
163 |
field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms normalizing_field_rules}), |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
164 |
idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms}, |
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
165 |
ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\<close> |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
166 |
|
36871 | 167 |
end |
168 |
||
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
169 |
hide_fact (open) normalizing_semiring_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
170 |
|
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
171 |
hide_fact (open) normalizing_ring_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
172 |
|
59553
e87974cd9b86
explicit declaration allows cumulative declaration
haftmann
parents:
59551
diff
changeset
|
173 |
hide_fact (open) normalizing_field_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
174 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
48891
diff
changeset
|
175 |
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
|
176 |
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
|
177 |
|
28402 | 178 |
end |