99 | "Pc c \<otimes> PX P i Q = |
100 | "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 (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 | "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 (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 | "Pinj x P \<otimes> Pinj y Q = |
104 (if x = y then mkPinj x (P \<otimes> Q) else |
105 (if x = y then mkPinj x (P \<otimes> Q) |
|
106 else |
105 (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q) |
107 (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q) |
106 else mkPinj x (Pinj (y - x) Q \<otimes> P)))" |
108 else mkPinj x (Pinj (y - x) Q \<otimes> P)))" |
107 | "Pinj x P \<otimes> PX Q y R = |
109 | "Pinj x P \<otimes> PX Q y R = |
108 (if x = 0 then P \<otimes> PX Q y R else |
110 (if x = 0 then P \<otimes> PX Q y R |
|
111 else |
109 (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P) |
112 (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)))" |
113 else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))" |
111 | "PX P x R \<otimes> Pinj y Q = |
114 | "PX P x R \<otimes> Pinj y Q = |
112 (if y = 0 then PX P x R \<otimes> Q else |
115 (if y = 0 then PX P x R \<otimes> Q |
|
116 else |
113 (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q) |
117 (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)))" |
118 else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))" |
115 | "PX P1 x P2 \<otimes> PX Q1 y Q2 = |
119 | "PX P1 x P2 \<otimes> PX Q1 y Q2 = |
116 mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus> |
120 mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus> |
117 (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus> |
121 (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus> |
118 (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))" |
122 (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))" |
119 by pat_completeness auto |
123 by pat_completeness auto |
120 termination by (relation "measure (\<lambda>(x, y). size x + size y)") |
124 termination by (relation "measure (\<lambda>(x, y). size x + size y)") |
121 (auto simp add: mkPinj_def split: pol.split) |
125 (auto simp add: mkPinj_def split: pol.split) |
122 |
126 |
123 text \<open>Negation\<close> |
127 text \<open>Negation\<close> |
124 primrec neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol" |
128 primrec neg :: "'a::comm_ring pol \<Rightarrow> 'a pol" |
125 where |
129 where |
126 "neg (Pc c) = Pc (-c)" |
130 "neg (Pc c) = Pc (-c)" |
127 | "neg (Pinj i P) = Pinj i (neg P)" |
131 | "neg (Pinj i P) = Pinj i (neg P)" |
128 | "neg (PX P x Q) = PX (neg P) x (neg Q)" |
132 | "neg (PX P x Q) = PX (neg P) x (neg Q)" |
129 |
133 |
130 text \<open>Substraction\<close> |
134 text \<open>Substraction\<close> |
131 definition sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65) |
135 definition sub :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65) |
132 where "sub P Q = P \<oplus> neg Q" |
136 where "sub P Q = P \<oplus> neg Q" |
133 |
137 |
134 text \<open>Square for Fast Exponentation\<close> |
138 text \<open>Square for Fast Exponentation\<close> |
135 primrec sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol" |
139 primrec sqr :: "'a::comm_ring_1 pol \<Rightarrow> 'a pol" |
136 where |
140 where |
137 "sqr (Pc c) = Pc (c * c)" |
141 "sqr (Pc c) = Pc (c * c)" |
138 | "sqr (Pinj i P) = mkPinj i (sqr P)" |
142 | "sqr (Pinj i P) = mkPinj i (sqr P)" |
139 | "sqr (PX A x B) = |
143 | "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)" |
144 mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)" |
141 |
145 |
142 text \<open>Fast Exponentation\<close> |
146 text \<open>Fast Exponentation\<close> |
143 |
147 |
144 fun pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol" |
148 fun pow :: "nat \<Rightarrow> 'a::comm_ring_1 pol \<Rightarrow> 'a pol" |
145 where |
149 where |
146 pow_if [simp del]: "pow n P = |
150 pow_if [simp del]: "pow n P = |
147 (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P) |
151 (if n = 0 then Pc 1 |
|
152 else if even n then pow (n div 2) (sqr P) |
148 else P \<otimes> pow (n div 2) (sqr P))" |
153 else P \<otimes> pow (n div 2) (sqr P))" |
149 |
154 |
150 lemma pow_simps [simp]: |
155 lemma pow_simps [simp]: |
151 "pow 0 P = Pc 1" |
156 "pow 0 P = Pc 1" |
152 "pow (2 * n) P = pow n (sqr P)" |
157 "pow (2 * n) P = pow n (sqr P)" |
153 "pow (Suc (2 * n)) P = P \<otimes> pow n (sqr P)" |
158 "pow (Suc (2 * n)) P = P \<otimes> pow n (sqr P)" |
154 by (simp_all add: pow_if) |
159 by (simp_all add: pow_if) |
155 |
160 |
156 lemma even_pow: |
161 lemma even_pow: "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)" |
157 "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)" |
|
158 by (erule evenE) simp |
162 by (erule evenE) simp |
159 |
163 |
160 lemma odd_pow: |
164 lemma odd_pow: "odd n \<Longrightarrow> pow n P = P \<otimes> pow (n div 2) (sqr P)" |
161 "odd n \<Longrightarrow> pow n P = P \<otimes> pow (n div 2) (sqr P)" |
|
162 by (erule oddE) simp |
165 by (erule oddE) simp |
163 |
166 |
164 |
167 |
165 text \<open>Normalization of polynomial expressions\<close> |
168 text \<open>Normalization of polynomial expressions\<close> |
166 |
169 |
167 primrec norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol" |
170 primrec norm :: "'a::comm_ring_1 polex \<Rightarrow> 'a pol" |
168 where |
171 where |
169 "norm (Pol P) = P" |
172 "norm (Pol P) = P" |
170 | "norm (Add P Q) = norm P \<oplus> norm Q" |
173 | "norm (Add P Q) = norm P \<oplus> norm Q" |
171 | "norm (Sub P Q) = norm P \<ominus> norm Q" |
174 | "norm (Sub P Q) = norm P \<ominus> norm Q" |
172 | "norm (Mul P Q) = norm P \<otimes> norm Q" |
175 | "norm (Mul P Q) = norm P \<otimes> norm Q" |
202 assume "x > y" |
205 assume "x > y" |
203 with 6 show ?case by (simp add: mkPinj_ci algebra_simps) |
206 with 6 show ?case by (simp add: mkPinj_ci algebra_simps) |
204 qed |
207 qed |
205 next |
208 next |
206 case (7 x P Q y R) |
209 case (7 x P Q y R) |
207 have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
210 consider "x = 0" | "x = 1" | "x > 1" by arith |
208 moreover |
211 then show ?case |
209 { assume "x = 0" with 7 have ?case by simp } |
212 proof cases |
210 moreover |
213 case 1 |
211 { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) } |
214 with 7 show ?thesis by simp |
212 moreover |
215 next |
213 { assume "x > 1" from 7 have ?case by (cases x) simp_all } |
216 case 2 |
214 ultimately show ?case by blast |
217 with 7 show ?thesis by (simp add: algebra_simps) |
|
218 next |
|
219 case 3 |
|
220 from 7 show ?thesis by (cases x) simp_all |
|
221 qed |
215 next |
222 next |
216 case (8 P x R y Q) |
223 case (8 P x R y Q) |
217 have "y = 0 \<or> y = 1 \<or> y > 1" by arith |
224 then show ?case by simp |
218 moreover |
|
219 { assume "y = 0" with 8 have ?case by simp } |
|
220 moreover |
|
221 { assume "y = 1" with 8 have ?case by simp } |
|
222 moreover |
|
223 { assume "y > 1" with 8 have ?case by simp } |
|
224 ultimately show ?case by blast |
|
225 next |
225 next |
226 case (9 P1 x P2 Q1 y Q2) |
226 case (9 P1 x P2 Q1 y Q2) |
227 show ?case |
227 consider "x = y" | d where "d + x = y" | d where "d + y = x" |
228 proof (rule linorder_cases) |
228 by atomize_elim arith |
229 assume a: "x < y" hence "EX d. d + x = y" by arith |
229 then show ?case |
230 with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps) |
230 proof cases |
231 next |
231 case 1 |
232 assume a: "y < x" hence "EX d. d + y = x" by arith |
232 with 9 show ?thesis by (simp add: mkPX_ci algebra_simps) |
233 with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps) |
233 next |
234 next |
234 case 2 |
235 assume "x = y" |
235 with 9 show ?thesis by (auto simp add: mkPX_ci power_add algebra_simps) |
236 with 9 show ?case by (simp add: mkPX_ci algebra_simps) |
236 next |
|
237 case 3 |
|
238 with 9 show ?thesis by (auto simp add: power_add mkPX_ci algebra_simps) |
237 qed |
239 qed |
238 qed (auto simp add: algebra_simps) |
240 qed (auto simp add: algebra_simps) |
239 |
241 |
240 text \<open>Multiplication\<close> |
242 text \<open>Multiplication\<close> |
241 lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q" |
243 lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q" |
255 lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n" |
257 lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n" |
256 proof (induct n arbitrary: P rule: less_induct) |
258 proof (induct n arbitrary: P rule: less_induct) |
257 case (less k) |
259 case (less k) |
258 show ?case |
260 show ?case |
259 proof (cases "k = 0") |
261 proof (cases "k = 0") |
260 case True then show ?thesis by simp |
262 case True |
261 next |
263 then show ?thesis by simp |
262 case False then have "k > 0" by simp |
264 next |
|
265 case False |
|
266 then have "k > 0" by simp |
263 then have "k div 2 < k" by arith |
267 then have "k div 2 < k" by arith |
264 with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) ^ (k div 2)" |
268 with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) ^ (k div 2)" |
265 by simp |
269 by simp |
266 show ?thesis |
270 show ?thesis |
267 proof (cases "even k") |
271 proof (cases "even k") |
268 case True with * show ?thesis |
272 case True |
269 by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] even_two_times_div_two) |
273 with * show ?thesis |
|
274 by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] |
|
275 mult_2 [symmetric] even_two_times_div_two) |
270 next |
276 next |
271 case False with * show ?thesis |
277 case False |
272 by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric]) |
278 with * show ?thesis |
|
279 by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] |
|
280 mult_2 [symmetric] power_Suc [symmetric]) |
273 qed |
281 qed |
274 qed |
282 qed |
275 qed |
283 qed |
276 |
284 |
277 text \<open>Normalization preserves semantics\<close> |
285 text \<open>Normalization preserves semantics\<close> |