src/HOL/Decision_Procs/Commutative_Ring.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 58259 52c35a59bbf5 child 58310 91ea607a34d8 permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Author:     Bernhard Haeupler
3 Proving equalities in commutative rings done "right" in Isabelle/HOL.
4 *)
6 header {* Proving equalities in commutative rings *}
8 theory Commutative_Ring
9 imports Parity
10 begin
12 text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
14 datatype_new 'a pol =
15     Pc 'a
16   | Pinj nat "'a pol"
17   | PX "'a pol" nat "'a pol"
19 datatype_new 'a polex =
20     Pol "'a pol"
21   | Add "'a polex" "'a polex"
22   | Sub "'a polex" "'a polex"
23   | Mul "'a polex" "'a polex"
24   | Pow "'a polex" nat
25   | Neg "'a polex"
27 text {* Interpretation functions for the shadow syntax. *}
29 primrec Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
30 where
31     "Ipol l (Pc c) = c"
32   | "Ipol l (Pinj i P) = Ipol (drop i l) P"
33   | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
35 primrec Ipolex :: "'a::{comm_ring_1} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
36 where
37     "Ipolex l (Pol P) = Ipol l P"
38   | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
39   | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
40   | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
41   | "Ipolex l (Pow p n) = Ipolex l p ^ n"
42   | "Ipolex l (Neg P) = - Ipolex l P"
44 text {* Create polynomial normalized polynomials given normalized inputs. *}
46 definition mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
47 where
48   "mkPinj x P = (case P of
49     Pc c \<Rightarrow> Pc c |
50     Pinj y P \<Rightarrow> Pinj (x + y) P |
51     PX p1 y p2 \<Rightarrow> Pinj x P)"
53 definition mkPX :: "'a::comm_ring pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
54 where
55   "mkPX P i Q =
56     (case P of
57       Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q
58     | Pinj j R \<Rightarrow> PX P i Q
59     | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)"
61 text {* Defining the basic ring operations on normalized polynomials *}
63 lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
64   by (cases p) simp_all
66 function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<oplus>" 65)
67 where
68   "Pc a \<oplus> Pc b = Pc (a + b)"
69 | "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
70 | "Pinj i P \<oplus> Pc c = Pinj i (P \<oplus> Pc c)"
71 | "Pc c \<oplus> PX P i Q = PX P i (Q \<oplus> Pc c)"
72 | "PX P i Q \<oplus> Pc c = PX P i (Q \<oplus> Pc c)"
73 | "Pinj x P \<oplus> Pinj y Q =
74     (if x = y then mkPinj x (P \<oplus> Q)
75      else (if x > y then mkPinj y (Pinj (x - y) P \<oplus> Q)
76        else mkPinj x (Pinj (y - x) Q \<oplus> P)))"
77 | "Pinj x P \<oplus> PX Q y R =
78     (if x = 0 then P \<oplus> PX Q y R
79      else (if x = 1 then PX Q y (R \<oplus> P)
80        else PX Q y (R \<oplus> Pinj (x - 1) P)))"
81 | "PX P x R \<oplus> Pinj y Q =
82     (if y = 0 then PX P x R \<oplus> Q
83      else (if y = 1 then PX P x (R \<oplus> Q)
84        else PX P x (R \<oplus> Pinj (y - 1) Q)))"
85 | "PX P1 x P2 \<oplus> PX Q1 y Q2 =
86     (if x = y then mkPX (P1 \<oplus> Q1) x (P2 \<oplus> Q2)
87      else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<oplus> Q1) y (P2 \<oplus> Q2)
88        else mkPX (PX Q1 (y-x) (Pc 0) \<oplus> P1) x (P2 \<oplus> Q2)))"
89 by pat_completeness auto
90 termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
92 function mul :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<otimes>" 70)
93 where
94   "Pc a \<otimes> Pc b = Pc (a * b)"
95 | "Pc c \<otimes> Pinj i P =
96     (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
97 | "Pinj i P \<otimes> Pc c =
98     (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
99 | "Pc c \<otimes> PX P i Q =
100     (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
101 | "PX P i Q \<otimes> Pc c =
102     (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
103 | "Pinj x P \<otimes> Pinj y Q =
104     (if x = y then mkPinj x (P \<otimes> Q) else
105        (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q)
106          else mkPinj x (Pinj (y - x) Q \<otimes> P)))"
107 | "Pinj x P \<otimes> PX Q y R =
108     (if x = 0 then P \<otimes> PX Q y R else
109        (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P)
110          else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))"
111 | "PX P x R \<otimes> Pinj y Q =
112     (if y = 0 then PX P x R \<otimes> Q else
113        (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q)
114          else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))"
115 | "PX P1 x P2 \<otimes> PX Q1 y Q2 =
116     mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus>
117       (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus>
118         (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))"
119 by pat_completeness auto
120 termination by (relation "measure (\<lambda>(x, y). size x + size y)")
121   (auto simp add: mkPinj_def split: pol.split)
123 text {* Negation*}
124 primrec neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
125 where
126   "neg (Pc c) = Pc (-c)"
127 | "neg (Pinj i P) = Pinj i (neg P)"
128 | "neg (PX P x Q) = PX (neg P) x (neg Q)"
130 text {* Substraction *}
131 definition sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<ominus>" 65)
132   where "sub P Q = P \<oplus> neg Q"
134 text {* Square for Fast Exponentation *}
135 primrec sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
136 where
137   "sqr (Pc c) = Pc (c * c)"
138 | "sqr (Pinj i P) = mkPinj i (sqr P)"
139 | "sqr (PX A x B) =
140     mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
142 text {* Fast Exponentation *}
143 fun pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
144 where
145   "pow 0 P = Pc 1"
146 | "pow n P =
147     (if even n then pow (n div 2) (sqr P)
148      else P \<otimes> pow (n div 2) (sqr P))"
150 lemma pow_if:
151   "pow n P =
152    (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
153     else P \<otimes> pow (n div 2) (sqr P))"
154   by (cases n) simp_all
157 text {* Normalization of polynomial expressions *}
159 primrec norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
160 where
161   "norm (Pol P) = P"
162 | "norm (Add P Q) = norm P \<oplus> norm Q"
163 | "norm (Sub P Q) = norm P \<ominus> norm Q"
164 | "norm (Mul P Q) = norm P \<otimes> norm Q"
165 | "norm (Pow P n) = pow n (norm P)"
166 | "norm (Neg P) = neg (norm P)"
168 text {* mkPinj preserve semantics *}
169 lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
170   by (induct B) (auto simp add: mkPinj_def algebra_simps)
172 text {* mkPX preserves semantics *}
173 lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
174   by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
176 text {* Correctness theorems for the implemented operations *}
178 text {* Negation *}
179 lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
180   by (induct P arbitrary: l) auto
182 text {* Addition *}
183 lemma add_ci: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
184 proof (induct P Q arbitrary: l rule: add.induct)
185   case (6 x P y Q)
186   show ?case
187   proof (rule linorder_cases)
188     assume "x < y"
189     with 6 show ?case by (simp add: mkPinj_ci algebra_simps)
190   next
191     assume "x = y"
192     with 6 show ?case by (simp add: mkPinj_ci)
193   next
194     assume "x > y"
195     with 6 show ?case by (simp add: mkPinj_ci algebra_simps)
196   qed
197 next
198   case (7 x P Q y R)
199   have "x = 0 \<or> x = 1 \<or> x > 1" by arith
200   moreover
201   { assume "x = 0" with 7 have ?case by simp }
202   moreover
203   { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) }
204   moreover
205   { assume "x > 1" from 7 have ?case by (cases x) simp_all }
206   ultimately show ?case by blast
207 next
208   case (8 P x R y Q)
209   have "y = 0 \<or> y = 1 \<or> y > 1" by arith
210   moreover
211   { assume "y = 0" with 8 have ?case by simp }
212   moreover
213   { assume "y = 1" with 8 have ?case by simp }
214   moreover
215   { assume "y > 1" with 8 have ?case by simp }
216   ultimately show ?case by blast
217 next
218   case (9 P1 x P2 Q1 y Q2)
219   show ?case
220   proof (rule linorder_cases)
221     assume a: "x < y" hence "EX d. d + x = y" by arith
222     with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps)
223   next
224     assume a: "y < x" hence "EX d. d + y = x" by arith
225     with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps)
226   next
227     assume "x = y"
228     with 9 show ?case by (simp add: mkPX_ci algebra_simps)
229   qed
230 qed (auto simp add: algebra_simps)
232 text {* Multiplication *}
233 lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
234   by (induct P Q arbitrary: l rule: mul.induct)
237 text {* Substraction *}
238 lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
239   by (simp add: add_ci neg_ci sub_def)
241 text {* Square *}
242 lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
243   by (induct P arbitrary: ls)
246 text {* Power *}
247 lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
248   by (induct n) simp_all
250 lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
251 proof (induct n arbitrary: P rule: nat_less_induct)
252   case (1 k)
253   show ?case
254   proof (cases k)
255     case 0
256     then show ?thesis by simp
257   next
258     case (Suc l)
259     show ?thesis
260     proof cases
261       assume "even l"
262       then have "Suc l div 2 = l div 2"
263         by (simp add: eval_nat_numeral even_nat_plus_one_div_two)
264       moreover
265       from Suc have "l < k" by simp
266       with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
267       moreover
268       note Suc `even l` even_nat_plus_one_div_two
269       ultimately show ?thesis by (auto simp add: mul_ci even_pow)
270     next
271       assume "odd l"
272       {
273         fix p
274         have "Ipol ls (sqr P) ^ (Suc l div 2) = Ipol ls P ^ Suc l"
275         proof (cases l)
276           case 0
277           with `odd l` show ?thesis by simp
278         next
279           case (Suc w)
280           with `odd l` have "even w" by simp
281           have two_times: "2 * (w div 2) = w"
282             by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
283           have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
284             by simp
285           then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
286             by (simp add: numerals)
287           with Suc show ?thesis
288             by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
289                      simp del: power_Suc)
290         qed
291       } with 1 Suc `odd l` show ?thesis by simp
292     qed
293   qed
294 qed
296 text {* Normalization preserves semantics  *}
297 lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
298   by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
300 text {* Reflection lemma: Key to the (incomplete) decision procedure *}
301 lemma norm_eq:
302   assumes "norm P1 = norm P2"
303   shows "Ipolex l P1 = Ipolex l P2"
304 proof -
305   from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
306   then show ?thesis by (simp only: norm_ci)
307 qed
310 ML_file "commutative_ring_tac.ML"
312 method_setup comm_ring = {*
313   Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
314 *} "reflective decision procedure for equalities over commutative rings"
316 end