author | haftmann |
Wed, 12 May 2010 12:31:52 +0200 | |
changeset 36871 | 3763c349c8c1 |
parent 36845 | d778c64fc35d |
child 36872 | 6520ba1256a6 |
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 |
||
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset
|
5 |
header {* 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 |
uses |
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
10 |
"Tools/semiring_normalizer.ML" |
23252 | 11 |
begin |
12 |
||
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
13 |
text {* FIXME prelude *} |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
14 |
|
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
15 |
class comm_semiring_1_cancel_norm (*FIXME name*) = comm_semiring_1_cancel + |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
16 |
assumes add_mult_solve: "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
|
17 |
|
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
18 |
sublocale idom < comm_semiring_1_cancel_norm |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
19 |
proof |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
20 |
fix w x y z |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
21 |
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
|
22 |
proof |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
23 |
assume "w * y + x * z = w * z + x * y" |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
then show "w = x \<or> y = z" by auto |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
29 |
qed (auto simp add: add_ac) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
30 |
qed |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
31 |
|
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
32 |
instance nat :: comm_semiring_1_cancel_norm |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
33 |
proof |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
34 |
fix w x y z :: nat |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
35 |
{ assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z" |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
36 |
hence "y < z \<or> y > z" by arith |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
37 |
moreover { |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
38 |
assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
39 |
then obtain k where kp: "k>0" and yz:"z = y + k" by blast |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
40 |
from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
41 |
hence "x*k = w*k" by simp |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
42 |
hence "w = x" using kp by simp } |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
43 |
moreover { |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
44 |
assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
45 |
then obtain k where kp: "k>0" and yz:"y = z + k" by blast |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
46 |
from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps) |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
47 |
hence "w*k = x*k" by simp |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
48 |
hence "w = x" using kp by simp } |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
49 |
ultimately have "w=x" by blast } |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
50 |
then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
51 |
qed |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
52 |
|
36871 | 53 |
text {* semiring normalization proper *} |
54 |
||
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
55 |
setup Semiring_Normalizer.setup |
23252 | 56 |
|
36871 | 57 |
context comm_semiring_1 |
58 |
begin |
|
59 |
||
60 |
lemma semiring_ops: |
|
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
61 |
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
|
62 |
and "TERM 0" and "TERM 1" . |
23252 | 63 |
|
36871 | 64 |
lemma semiring_rules: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
65 |
"(a * m) + (b * m) = (a + b) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
66 |
"(a * m) + m = (a + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
67 |
"m + (a * m) = (a + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
68 |
"m + m = (1 + 1) * m" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
69 |
"0 + a = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
70 |
"a + 0 = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
71 |
"a * b = b * a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
72 |
"(a + b) * c = (a * c) + (b * c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
73 |
"0 * a = 0" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
74 |
"a * 0 = 0" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
75 |
"1 * a = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
76 |
"a * 1 = a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
77 |
"(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
78 |
"(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
79 |
"(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
80 |
"(lx * ly) * rx = (lx * rx) * ly" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
81 |
"(lx * ly) * rx = lx * (ly * rx)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
82 |
"lx * (rx * ry) = (lx * rx) * ry" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
83 |
"lx * (rx * ry) = rx * (lx * ry)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
84 |
"(a + b) + (c + d) = (a + c) + (b + d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
85 |
"(a + b) + c = a + (b + c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
86 |
"a + (c + d) = c + (a + d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
87 |
"(a + b) + c = (a + c) + b" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
88 |
"a + c = c + a" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
89 |
"a + (c + d) = (a + c) + d" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
90 |
"(x ^ p) * (x ^ q) = x ^ (p + q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
91 |
"x * (x ^ q) = x ^ (Suc q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
92 |
"(x ^ q) * x = x ^ (Suc q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
93 |
"x * x = x ^ 2" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
94 |
"(x * y) ^ q = (x ^ q) * (y ^ q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
95 |
"(x ^ p) ^ q = x ^ (p * q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
96 |
"x ^ 0 = 1" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
97 |
"x ^ 1 = x" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
98 |
"x * (y + z) = (x * y) + (x * z)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
99 |
"x ^ (Suc q) = x * (x ^ q)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
100 |
"x ^ (2*n) = (x ^ n) * (x ^ n)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
101 |
"x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
102 |
by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult) |
23252 | 103 |
|
36871 | 104 |
lemmas normalizing_comm_semiring_1_axioms = |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
105 |
comm_semiring_1_axioms [normalizer |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
106 |
semiring ops: semiring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
107 |
semiring rules: semiring_rules] |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
108 |
|
36871 | 109 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
110 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *} |
23573 | 111 |
|
36871 | 112 |
end |
23252 | 113 |
|
36871 | 114 |
context comm_ring_1 |
115 |
begin |
|
116 |
||
117 |
lemma ring_ops: shows "TERM (x- y)" and "TERM (- x)" . |
|
118 |
||
119 |
lemma ring_rules: |
|
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
120 |
"- x = (- 1) * x" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
121 |
"x - y = x + (- y)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
122 |
by (simp_all add: diff_minus) |
23252 | 123 |
|
36871 | 124 |
lemmas normalizing_comm_ring_1_axioms = |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
125 |
comm_ring_1_axioms [normalizer |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
126 |
semiring ops: semiring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
127 |
semiring rules: semiring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
128 |
ring ops: ring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
129 |
ring rules: ring_rules] |
30866 | 130 |
|
36871 | 131 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
132 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *} |
23327 | 133 |
|
36871 | 134 |
end |
135 |
||
136 |
context comm_semiring_1_cancel_norm |
|
137 |
begin |
|
138 |
||
139 |
lemma noteq_reduce: |
|
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
140 |
"a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)" |
23252 | 141 |
proof- |
142 |
have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp |
|
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
143 |
also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
144 |
using add_mult_solve by blast |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
145 |
finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)" |
23252 | 146 |
by simp |
147 |
qed |
|
148 |
||
36871 | 149 |
lemma add_scale_eq_noteq: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
150 |
"\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)" |
23252 | 151 |
proof(clarify) |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
152 |
assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
153 |
and eq: "b + (r * c) = b + (r * d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
154 |
have "(0 * d) + (r * c) = (0 * c) + (r * d)" |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
155 |
using add_imp_eq eq mult_zero_left by simp |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
156 |
thus "False" using add_mult_solve[of 0 d] nz cnd by simp |
23252 | 157 |
qed |
158 |
||
36871 | 159 |
lemma add_0_iff: |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
160 |
"x = x + a \<longleftrightarrow> a = 0" |
25250
b3a485b98963
(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)
chaieb
parents:
23573
diff
changeset
|
161 |
proof- |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
162 |
have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
163 |
thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute) |
25250
b3a485b98963
(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)
chaieb
parents:
23573
diff
changeset
|
164 |
qed |
b3a485b98963
(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)
chaieb
parents:
23573
diff
changeset
|
165 |
|
36871 | 166 |
declare |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
167 |
normalizing_comm_semiring_1_axioms [normalizer del] |
23252 | 168 |
|
36871 | 169 |
lemmas |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
170 |
normalizing_comm_semiring_1_cancel_norm_axioms = |
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
171 |
comm_semiring_1_cancel_norm_axioms [normalizer |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
172 |
semiring ops: semiring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
173 |
semiring rules: semiring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
174 |
idom rules: noteq_reduce add_scale_eq_noteq] |
23252 | 175 |
|
36871 | 176 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
177 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *} |
23252 | 178 |
|
36871 | 179 |
end |
23252 | 180 |
|
36871 | 181 |
context idom |
182 |
begin |
|
183 |
||
184 |
declare normalizing_comm_ring_1_axioms [normalizer del] |
|
185 |
||
186 |
lemmas normalizing_idom_axioms = idom_axioms [normalizer |
|
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
187 |
semiring ops: semiring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
188 |
semiring rules: semiring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
189 |
ring ops: ring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
190 |
ring rules: ring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
191 |
idom rules: noteq_reduce add_scale_eq_noteq |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
192 |
ideal rules: right_minus_eq add_0_iff] |
23252 | 193 |
|
36871 | 194 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
195 |
{* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *} |
23252 | 196 |
|
36871 | 197 |
end |
198 |
||
199 |
context field |
|
200 |
begin |
|
201 |
||
202 |
lemma field_ops: |
|
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
203 |
shows "TERM (x / y)" and "TERM (inverse x)" . |
23327 | 204 |
|
36871 | 205 |
lemmas field_rules = divide_inverse inverse_eq_divide |
28402 | 206 |
|
36871 | 207 |
lemmas normalizing_field_axioms = |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
208 |
field_axioms [normalizer |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
209 |
semiring ops: semiring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
210 |
semiring rules: semiring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
211 |
ring ops: ring_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
212 |
ring rules: ring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
213 |
field ops: field_ops |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
214 |
field rules: field_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
215 |
idom rules: noteq_reduce add_scale_eq_noteq |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
216 |
ideal rules: right_minus_eq add_0_iff] |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
217 |
|
36871 | 218 |
declaration |
36756
c1ae8a0b4265
moved normalization proof tool infrastructure to canonical algebraic classes
haftmann
parents:
36753
diff
changeset
|
219 |
{* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *} |
28402 | 220 |
|
36871 | 221 |
end |
222 |
||
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
223 |
hide_fact (open) normalizing_comm_semiring_1_axioms |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
224 |
normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
225 |
|
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
226 |
hide_fact (open) normalizing_comm_ring_1_axioms |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
227 |
normalizing_idom_axioms ring_ops ring_rules |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
228 |
|
36871 | 229 |
hide_fact (open) normalizing_field_axioms field_ops field_rules |
36845
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
230 |
|
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
231 |
hide_fact (open) add_scale_eq_noteq noteq_reduce |
d778c64fc35d
Add rules directly to the corresponding class locales instead.
hoelzl
parents:
36756
diff
changeset
|
232 |
|
28402 | 233 |
end |