29 | Pow polex nat |
29 | Pow polex nat |
30 | Neg polex |
30 | Neg polex |
31 |
31 |
32 text \<open>Interpretation functions for the shadow syntax.\<close> |
32 text \<open>Interpretation functions for the shadow syntax.\<close> |
33 |
33 |
34 context cring begin |
34 context cring |
35 |
35 begin |
36 definition in_carrier :: "'a list \<Rightarrow> bool" where |
36 |
37 "in_carrier xs = (\<forall>x\<in>set xs. x \<in> carrier R)" |
37 definition in_carrier :: "'a list \<Rightarrow> bool" |
|
38 where "in_carrier xs \<longleftrightarrow> (\<forall>x\<in>set xs. x \<in> carrier R)" |
38 |
39 |
39 lemma in_carrier_Nil: "in_carrier []" |
40 lemma in_carrier_Nil: "in_carrier []" |
40 by (simp add: in_carrier_def) |
41 by (simp add: in_carrier_def) |
41 |
42 |
42 lemma in_carrier_Cons: "x \<in> carrier R \<Longrightarrow> in_carrier xs \<Longrightarrow> in_carrier (x # xs)" |
43 lemma in_carrier_Cons: "x \<in> carrier R \<Longrightarrow> in_carrier xs \<Longrightarrow> in_carrier (x # xs)" |
43 by (simp add: in_carrier_def) |
44 by (simp add: in_carrier_def) |
44 |
45 |
45 lemma drop_in_carrier [simp]: "in_carrier xs \<Longrightarrow> in_carrier (drop n xs)" |
46 lemma drop_in_carrier [simp]: "in_carrier xs \<Longrightarrow> in_carrier (drop n xs)" |
46 using set_drop_subset [of n xs] |
47 using set_drop_subset [of n xs] by (auto simp add: in_carrier_def) |
47 by (auto simp add: in_carrier_def) |
|
48 |
48 |
49 primrec head :: "'a list \<Rightarrow> 'a" |
49 primrec head :: "'a list \<Rightarrow> 'a" |
50 where |
50 where |
51 "head [] = \<zero>" |
51 "head [] = \<zero>" |
52 | "head (x # xs) = x" |
52 | "head (x # xs) = x" |
53 |
53 |
54 lemma head_closed [simp]: "in_carrier xs \<Longrightarrow> head xs \<in> carrier R" |
54 lemma head_closed [simp]: "in_carrier xs \<Longrightarrow> head xs \<in> carrier R" |
55 by (cases xs) (simp_all add: in_carrier_def) |
55 by (cases xs) (simp_all add: in_carrier_def) |
56 |
56 |
57 primrec Ipol :: "'a list \<Rightarrow> pol \<Rightarrow> 'a" |
57 primrec Ipol :: "'a list \<Rightarrow> pol \<Rightarrow> 'a" |
58 where |
58 where |
59 "Ipol l (Pc c) = \<guillemotleft>c\<guillemotright>" |
59 "Ipol l (Pc c) = \<guillemotleft>c\<guillemotright>" |
60 | "Ipol l (Pinj i P) = Ipol (drop i l) P" |
60 | "Ipol l (Pinj i P) = Ipol (drop i l) P" |
61 | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l (^) x \<oplus> Ipol (drop 1 l) Q" |
61 | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l (^) x \<oplus> Ipol (drop 1 l) Q" |
62 |
62 |
63 lemma Ipol_Pc: |
63 lemma Ipol_Pc: |
90 end |
89 end |
91 |
90 |
92 text \<open>Create polynomial normalized polynomials given normalized inputs.\<close> |
91 text \<open>Create polynomial normalized polynomials given normalized inputs.\<close> |
93 |
92 |
94 definition mkPinj :: "nat \<Rightarrow> pol \<Rightarrow> pol" |
93 definition mkPinj :: "nat \<Rightarrow> pol \<Rightarrow> pol" |
95 where |
94 where "mkPinj x P = |
96 "mkPinj x P = |
|
97 (case P of |
95 (case P of |
98 Pc c \<Rightarrow> Pc c |
96 Pc c \<Rightarrow> Pc c |
99 | Pinj y P \<Rightarrow> Pinj (x + y) P |
97 | Pinj y P \<Rightarrow> Pinj (x + y) P |
100 | PX p1 y p2 \<Rightarrow> Pinj x P)" |
98 | PX p1 y p2 \<Rightarrow> Pinj x P)" |
101 |
99 |
102 definition mkPX :: "pol \<Rightarrow> nat \<Rightarrow> pol \<Rightarrow> pol" |
100 definition mkPX :: "pol \<Rightarrow> nat \<Rightarrow> pol \<Rightarrow> pol" |
103 where |
101 where "mkPX P i Q = |
104 "mkPX P i Q = |
|
105 (case P of |
102 (case P of |
106 Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q |
103 Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q |
107 | Pinj j R \<Rightarrow> PX P i Q |
104 | Pinj j R \<Rightarrow> PX P i Q |
108 | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)" |
105 | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)" |
109 |
106 |
110 text \<open>Defining the basic ring operations on normalized polynomials\<close> |
107 text \<open>Defining the basic ring operations on normalized polynomials\<close> |
111 |
108 |
112 function add :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>+\<rangle>" 65) |
109 function add :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>+\<rangle>" 65) |
113 where |
110 where |
114 "Pc a \<langle>+\<rangle> Pc b = Pc (a + b)" |
111 "Pc a \<langle>+\<rangle> Pc b = Pc (a + b)" |
115 | "Pc c \<langle>+\<rangle> Pinj i P = Pinj i (P \<langle>+\<rangle> Pc c)" |
112 | "Pc c \<langle>+\<rangle> Pinj i P = Pinj i (P \<langle>+\<rangle> Pc c)" |
116 | "Pinj i P \<langle>+\<rangle> Pc c = Pinj i (P \<langle>+\<rangle> Pc c)" |
113 | "Pinj i P \<langle>+\<rangle> Pc c = Pinj i (P \<langle>+\<rangle> Pc c)" |
117 | "Pc c \<langle>+\<rangle> PX P i Q = PX P i (Q \<langle>+\<rangle> Pc c)" |
114 | "Pc c \<langle>+\<rangle> PX P i Q = PX P i (Q \<langle>+\<rangle> Pc c)" |
118 | "PX P i Q \<langle>+\<rangle> Pc c = PX P i (Q \<langle>+\<rangle> Pc c)" |
115 | "PX P i Q \<langle>+\<rangle> Pc c = PX P i (Q \<langle>+\<rangle> Pc c)" |
163 else mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Pinj (y - 1) Q)))" |
160 else mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Pinj (y - 1) Q)))" |
164 | "PX P1 x P2 \<langle>*\<rangle> PX Q1 y Q2 = |
161 | "PX P1 x P2 \<langle>*\<rangle> PX Q1 y Q2 = |
165 mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2) \<langle>+\<rangle> |
162 mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2) \<langle>+\<rangle> |
166 (mkPX (P1 \<langle>*\<rangle> mkPinj 1 Q2) x (Pc 0) \<langle>+\<rangle> |
163 (mkPX (P1 \<langle>*\<rangle> mkPinj 1 Q2) x (Pc 0) \<langle>+\<rangle> |
167 (mkPX (Q1 \<langle>*\<rangle> mkPinj 1 P2) y (Pc 0)))" |
164 (mkPX (Q1 \<langle>*\<rangle> mkPinj 1 P2) y (Pc 0)))" |
168 by pat_completeness auto |
165 by pat_completeness auto |
169 termination by (relation "measure (\<lambda>(x, y). size x + size y)") |
166 termination by (relation "measure (\<lambda>(x, y). size x + size y)") |
170 (auto simp add: mkPinj_def split: pol.split) |
167 (auto simp add: mkPinj_def split: pol.split) |
171 |
168 |
172 text \<open>Negation\<close> |
169 text \<open>Negation\<close> |
173 primrec neg :: "pol \<Rightarrow> pol" |
170 primrec neg :: "pol \<Rightarrow> pol" |
174 where |
171 where |
175 "neg (Pc c) = Pc (- c)" |
172 "neg (Pc c) = Pc (- c)" |
176 | "neg (Pinj i P) = Pinj i (neg P)" |
173 | "neg (Pinj i P) = Pinj i (neg P)" |
177 | "neg (PX P x Q) = PX (neg P) x (neg Q)" |
174 | "neg (PX P x Q) = PX (neg P) x (neg Q)" |
178 |
175 |
179 text \<open>Subtraction\<close> |
176 text \<open>Subtraction\<close> |
180 definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>-\<rangle>" 65) |
177 definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol" (infixl "\<langle>-\<rangle>" 65) |
181 where |
178 where "sub P Q = P \<langle>+\<rangle> neg Q" |
182 "sub P Q = P \<langle>+\<rangle> neg Q" |
|
183 |
179 |
184 text \<open>Square for Fast Exponentiation\<close> |
180 text \<open>Square for Fast Exponentiation\<close> |
185 primrec sqr :: "pol \<Rightarrow> pol" |
181 primrec sqr :: "pol \<Rightarrow> pol" |
186 where |
182 where |
187 "sqr (Pc c) = Pc (c * c)" |
183 "sqr (Pc c) = Pc (c * c)" |
188 | "sqr (Pinj i P) = mkPinj i (sqr P)" |
184 | "sqr (Pinj i P) = mkPinj i (sqr P)" |
189 | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<langle>+\<rangle> |
185 | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<langle>+\<rangle> mkPX (Pc 2 \<langle>*\<rangle> A \<langle>*\<rangle> mkPinj 1 B) x (Pc 0)" |
190 mkPX (Pc 2 \<langle>*\<rangle> A \<langle>*\<rangle> mkPinj 1 B) x (Pc 0)" |
|
191 |
186 |
192 text \<open>Fast Exponentiation\<close> |
187 text \<open>Fast Exponentiation\<close> |
193 |
188 |
194 fun pow :: "nat \<Rightarrow> pol \<Rightarrow> pol" |
189 fun pow :: "nat \<Rightarrow> pol \<Rightarrow> pol" |
195 where |
190 where pow_if [simp del]: "pow n P = |
196 pow_if [simp del]: "pow n P = |
|
197 (if n = 0 then Pc 1 |
191 (if n = 0 then Pc 1 |
198 else if even n then pow (n div 2) (sqr P) |
192 else if even n then pow (n div 2) (sqr P) |
199 else P \<langle>*\<rangle> pow (n div 2) (sqr P))" |
193 else P \<langle>*\<rangle> pow (n div 2) (sqr P))" |
200 |
194 |
201 lemma pow_simps [simp]: |
195 lemma pow_simps [simp]: |
358 datatype mon = |
352 datatype mon = |
359 Mc int |
353 Mc int |
360 | Minj nat mon |
354 | Minj nat mon |
361 | MX nat mon |
355 | MX nat mon |
362 |
356 |
363 primrec (in cring) |
357 primrec (in cring) Imon :: "'a list \<Rightarrow> mon \<Rightarrow> 'a" |
364 Imon :: "'a list \<Rightarrow> mon \<Rightarrow> 'a" |
358 where |
365 where |
|
366 "Imon l (Mc c) = \<guillemotleft>c\<guillemotright>" |
359 "Imon l (Mc c) = \<guillemotleft>c\<guillemotright>" |
367 | "Imon l (Minj i M) = Imon (drop i l) M" |
360 | "Imon l (Minj i M) = Imon (drop i l) M" |
368 | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l (^) x" |
361 | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l (^) x" |
369 |
362 |
370 lemma (in cring) Imon_closed [simp]: |
363 lemma (in cring) Imon_closed [simp]: "in_carrier l \<Longrightarrow> Imon l m \<in> carrier R" |
371 "in_carrier l \<Longrightarrow> Imon l m \<in> carrier R" |
|
372 by (induct m arbitrary: l) simp_all |
364 by (induct m arbitrary: l) simp_all |
373 |
365 |
374 definition |
366 definition mkMinj :: "nat \<Rightarrow> mon \<Rightarrow> mon" |
375 mkMinj :: "nat \<Rightarrow> mon \<Rightarrow> mon" where |
367 where "mkMinj i M = |
376 "mkMinj i M = (case M of |
368 (case M of |
377 Mc c \<Rightarrow> Mc c |
369 Mc c \<Rightarrow> Mc c |
378 | Minj j M \<Rightarrow> Minj (i + j) M |
370 | Minj j M \<Rightarrow> Minj (i + j) M |
379 | _ \<Rightarrow> Minj i M)" |
371 | _ \<Rightarrow> Minj i M)" |
380 |
372 |
381 definition |
373 definition Minj_pred :: "nat \<Rightarrow> mon \<Rightarrow> mon" |
382 Minj_pred :: "nat \<Rightarrow> mon \<Rightarrow> mon" where |
374 where "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)" |
383 "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)" |
|
384 |
375 |
385 primrec mkMX :: "nat \<Rightarrow> mon \<Rightarrow> mon" |
376 primrec mkMX :: "nat \<Rightarrow> mon \<Rightarrow> mon" |
386 where |
377 where |
387 "mkMX i (Mc c) = MX i (Mc c)" |
378 "mkMX i (Mc c) = MX i (Mc c)" |
388 | "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))" |
379 | "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))" |
389 | "mkMX i (MX j M) = MX (i + j) M" |
380 | "mkMX i (MX j M) = MX (i + j) M" |
390 |
381 |
391 lemma (in cring) mkMinj_correct: |
382 lemma (in cring) mkMinj_correct: "Imon l (mkMinj i M) = Imon l (Minj i M)" |
392 "Imon l (mkMinj i M) = Imon l (Minj i M)" |
|
393 by (simp add: mkMinj_def add.commute split: mon.split) |
383 by (simp add: mkMinj_def add.commute split: mon.split) |
394 |
384 |
395 lemma (in cring) Minj_pred_correct: |
385 lemma (in cring) Minj_pred_correct: "0 < i \<Longrightarrow> Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)" |
396 "0 < i \<Longrightarrow> Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)" |
|
397 by (simp add: Minj_pred_def mkMinj_correct) |
386 by (simp add: Minj_pred_def mkMinj_correct) |
398 |
387 |
399 lemma (in cring) mkMX_correct: |
388 lemma (in cring) mkMX_correct: "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l (^) i" |
400 "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l (^) i" |
389 by (induct M) |
401 by (induct M) (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split) |
390 (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split) |
402 |
391 |
403 fun cfactor :: "pol \<Rightarrow> int \<Rightarrow> pol \<times> pol" |
392 fun cfactor :: "pol \<Rightarrow> int \<Rightarrow> pol \<times> pol" |
404 where |
393 where |
405 "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))" |
394 "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))" |
406 | "cfactor (Pinj i P) c = |
395 | "cfactor (Pinj i P) c = |
407 (let (R, S) = cfactor P c |
396 (let (R, S) = cfactor P c |
408 in (mkPinj i R, mkPinj i S))" |
397 in (mkPinj i R, mkPinj i S))" |
409 | "cfactor (PX P i Q) c = |
398 | "cfactor (PX P i Q) c = |
410 (let |
399 (let |
411 (R1, S1) = cfactor P c; |
400 (R1, S1) = cfactor P c; |
412 (R2, S2) = cfactor Q c |
401 (R2, S2) = cfactor Q c |
413 in (mkPX R1 i R2, mkPX S1 i S2))" |
402 in (mkPX R1 i R2, mkPX S1 i S2))" |
414 |
403 |
415 lemma (in cring) cfactor_correct: |
404 lemma (in cring) cfactor_correct: |
416 "in_carrier l \<Longrightarrow> Ipol l P = Ipol l (fst (cfactor P c)) \<oplus> \<guillemotleft>c\<guillemotright> \<otimes> Ipol l (snd (cfactor P c))" |
405 "in_carrier l \<Longrightarrow> Ipol l P = Ipol l (fst (cfactor P c)) \<oplus> \<guillemotleft>c\<guillemotright> \<otimes> Ipol l (snd (cfactor P c))" |
417 proof (induct P c arbitrary: l rule: cfactor.induct) |
406 proof (induct P c arbitrary: l rule: cfactor.induct) |
418 case (1 c' c) |
407 case (1 c' c) |
428 show ?case |
417 show ?case |
429 by (simp add: mkPX_ci r_distr a_ac m_ac split_beta) |
418 by (simp add: mkPX_ci r_distr a_ac m_ac split_beta) |
430 qed |
419 qed |
431 |
420 |
432 fun mfactor :: "pol \<Rightarrow> mon \<Rightarrow> pol \<times> pol" |
421 fun mfactor :: "pol \<Rightarrow> mon \<Rightarrow> pol \<times> pol" |
433 where |
422 where |
434 "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)" |
423 "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)" |
435 | "mfactor (Pc d) M = (Pc d, Pc 0)" |
424 | "mfactor (Pc d) M = (Pc d, Pc 0)" |
436 | "mfactor (Pinj i P) (Minj j M) = |
425 | "mfactor (Pinj i P) (Minj j M) = |
437 (if i = j then |
426 (if i = j then |
438 let (R, S) = mfactor P M |
427 let (R, S) = mfactor P M |
439 in (mkPinj i R, mkPinj i S) |
428 in (mkPinj i R, mkPinj i S) |
440 else if i < j then |
429 else if i < j then |
441 let (R, S) = mfactor P (Minj (j - i) M) |
430 let (R, S) = mfactor P (Minj (j - i) M) |
442 in (mkPinj i R, mkPinj i S) |
431 in (mkPinj i R, mkPinj i S) |
443 else (Pinj i P, Pc 0))" |
432 else (Pinj i P, Pc 0))" |
444 | "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)" |
433 | "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)" |
445 | "mfactor (PX P i Q) (Minj j M) = |
434 | "mfactor (PX P i Q) (Minj j M) = |
446 (if j = 0 then mfactor (PX P i Q) M |
435 (if j = 0 then mfactor (PX P i Q) M |
447 else |
436 else |
448 let |
437 let |
449 (R1, S1) = mfactor P (Minj j M); |
438 (R1, S1) = mfactor P (Minj j M); |
450 (R2, S2) = mfactor Q (Minj_pred j M) |
439 (R2, S2) = mfactor Q (Minj_pred j M) |
451 in (mkPX R1 i R2, mkPX S1 i S2))" |
440 in (mkPX R1 i R2, mkPX S1 i S2))" |
452 | "mfactor (PX P i Q) (MX j M) = |
441 | "mfactor (PX P i Q) (MX j M) = |
453 (if i = j then |
442 (if i = j then |
454 let (R, S) = mfactor P (mkMinj 1 M) |
443 let (R, S) = mfactor P (mkMinj 1 M) |
455 in (mkPX R i Q, S) |
444 in (mkPX R i Q, S) |
456 else if i < j then |
445 else if i < j then |
457 let (R, S) = mfactor P (MX (j - i) M) |
446 let (R, S) = mfactor P (MX (j - i) M) |
458 in (mkPX R i Q, S) |
447 in (mkPX R i Q, S) |
459 else |
448 else |
460 let (R, S) = mfactor P (mkMinj 1 M) |
449 let (R, S) = mfactor P (mkMinj 1 M) |
461 in (mkPX R i Q, mkPX S (i - j) (Pc 0)))" |
450 in (mkPX R i Q, mkPX S (i - j) (Pc 0)))" |
462 |
451 |
463 lemmas mfactor_induct = mfactor.induct |
452 lemmas mfactor_induct = mfactor.induct |
464 [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX] |
453 [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX] |
465 |
454 |
466 lemma (in cring) mfactor_correct: |
455 lemma (in cring) mfactor_correct: |
513 by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult) |
502 by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult) |
514 (simp add: a_ac m_ac) |
503 (simp add: a_ac m_ac) |
515 qed |
504 qed |
516 |
505 |
517 primrec mon_of_pol :: "pol \<Rightarrow> mon option" |
506 primrec mon_of_pol :: "pol \<Rightarrow> mon option" |
518 where |
507 where |
519 "mon_of_pol (Pc c) = Some (Mc c)" |
508 "mon_of_pol (Pc c) = Some (Mc c)" |
520 | "mon_of_pol (Pinj i P) = (case mon_of_pol P of |
509 | "mon_of_pol (Pinj i P) = (case mon_of_pol P of |
521 None \<Rightarrow> None |
510 None \<Rightarrow> None |
522 | Some M \<Rightarrow> Some (mkMinj i M))" |
511 | Some M \<Rightarrow> Some (mkMinj i M))" |
523 | "mon_of_pol (PX P i Q) = |
512 | "mon_of_pol (PX P i Q) = |
524 (if Q = Pc 0 then (case mon_of_pol P of |
513 (if Q = Pc 0 then (case mon_of_pol P of |
525 None \<Rightarrow> None |
514 None \<Rightarrow> None |
526 | Some M \<Rightarrow> Some (mkMX i M)) |
515 | Some M \<Rightarrow> Some (mkMX i M)) |
527 else None)" |
516 else None)" |
528 |
517 |
529 lemma (in cring) mon_of_pol_correct: |
518 lemma (in cring) mon_of_pol_correct: |
530 assumes "in_carrier l" |
519 assumes "in_carrier l" |
531 and "mon_of_pol P = Some M" |
520 and "mon_of_pol P = Some M" |
532 shows "Ipol l P = Imon l M" |
521 shows "Ipol l P = Imon l M" |
533 using assms |
522 using assms |
534 proof (induct P arbitrary: M l) |
523 proof (induct P arbitrary: M l) |
535 case (PX P1 i P2) |
524 case (PX P1 i P2) |
536 from PX(1,3,4) |
525 from PX(1,3,4) |
537 show ?case |
526 show ?case |
538 by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm) |
527 by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm) |
539 qed (auto simp add: mkMinj_correct split: option.split_asm) |
528 qed (auto simp add: mkMinj_correct split: option.split_asm) |
540 |
529 |
541 fun (in cring) Ipolex_polex_list :: "'a list \<Rightarrow> (polex \<times> polex) list \<Rightarrow> bool" |
530 fun (in cring) Ipolex_polex_list :: "'a list \<Rightarrow> (polex \<times> polex) list \<Rightarrow> bool" |
542 where |
531 where |
543 "Ipolex_polex_list l [] = True" |
532 "Ipolex_polex_list l [] = True" |
544 | "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) \<and> Ipolex_polex_list l pps)" |
533 | "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) \<and> Ipolex_polex_list l pps)" |
545 |
534 |
546 fun (in cring) Imon_pol_list :: "'a list \<Rightarrow> (mon \<times> pol) list \<Rightarrow> bool" |
535 fun (in cring) Imon_pol_list :: "'a list \<Rightarrow> (mon \<times> pol) list \<Rightarrow> bool" |
547 where |
536 where |
548 "Imon_pol_list l [] = True" |
537 "Imon_pol_list l [] = True" |
549 | "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) \<and> Imon_pol_list l mps)" |
538 | "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) \<and> Imon_pol_list l mps)" |
550 |
539 |
551 fun mk_monpol_list :: "(polex \<times> polex) list \<Rightarrow> (mon \<times> pol) list" |
540 fun mk_monpol_list :: "(polex \<times> polex) list \<Rightarrow> (mon \<times> pol) list" |
552 where |
541 where |
553 "mk_monpol_list [] = []" |
542 "mk_monpol_list [] = []" |
554 | "mk_monpol_list ((P, Q) # pps) = |
543 | "mk_monpol_list ((P, Q) # pps) = |
555 (case mon_of_pol (norm P) of |
544 (case mon_of_pol (norm P) of |
556 None \<Rightarrow> mk_monpol_list pps |
545 None \<Rightarrow> mk_monpol_list pps |
557 | Some M \<Rightarrow> (M, norm Q) # mk_monpol_list pps)" |
546 | Some M \<Rightarrow> (M, norm Q) # mk_monpol_list pps)" |
558 |
547 |
559 lemma (in cring) mk_monpol_list_correct: |
548 lemma (in cring) mk_monpol_list_correct: |
560 "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow> Imon_pol_list l (mk_monpol_list pps)" |
549 "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow> Imon_pol_list l (mk_monpol_list pps)" |
561 by (induct pps rule: mk_monpol_list.induct) |
550 by (induct pps rule: mk_monpol_list.induct) |
562 (auto split: option.split |
551 (auto split: option.split simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric]) |
563 simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric]) |
552 |
564 |
553 definition ponesubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> pol option" |
565 definition ponesubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> pol option" where |
554 where "ponesubst P1 M P2 = |
566 "ponesubst P1 M P2 = |
555 (let (Q, R) = mfactor P1 M in |
567 (let (Q, R) = mfactor P1 M |
556 (case R of |
568 in case R of |
557 Pc c \<Rightarrow> if c = 0 then None else Some (add Q (mul P2 R)) |
569 Pc c \<Rightarrow> if c = 0 then None else Some (add Q (mul P2 R)) |
558 | _ \<Rightarrow> Some (add Q (mul P2 R))))" |
570 | _ \<Rightarrow> Some (add Q (mul P2 R)))" |
|
571 |
559 |
572 fun pnsubst1 :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol" |
560 fun pnsubst1 :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol" |
573 where |
561 where "pnsubst1 P1 M P2 n = |
574 "pnsubst1 P1 M P2 n = (case ponesubst P1 M P2 of |
562 (case ponesubst P1 M P2 of |
575 None \<Rightarrow> P1 |
563 None \<Rightarrow> P1 |
576 | Some P3 \<Rightarrow> if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))" |
564 | Some P3 \<Rightarrow> if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))" |
577 |
565 |
578 lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of |
566 lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of |
579 None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)" |
567 None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)" |
580 by (simp split: option.split) |
568 by (simp split: option.split) |
581 |
569 |
582 lemma pnsubst1_Suc [simp]: "pnsubst1 P1 M P2 (Suc n) = (case ponesubst P1 M P2 of |
570 lemma pnsubst1_Suc [simp]: |
583 None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubst1 P3 M P2 n)" |
571 "pnsubst1 P1 M P2 (Suc n) = |
|
572 (case ponesubst P1 M P2 of |
|
573 None \<Rightarrow> P1 |
|
574 | Some P3 \<Rightarrow> pnsubst1 P3 M P2 n)" |
584 by (simp split: option.split) |
575 by (simp split: option.split) |
585 |
576 |
586 declare pnsubst1.simps [simp del] |
577 declare pnsubst1.simps [simp del] |
587 |
578 |
588 definition pnsubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol option" where |
579 definition pnsubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol option" |
589 "pnsubst P1 M P2 n = (case ponesubst P1 M P2 of |
580 where "pnsubst P1 M P2 n = |
590 None \<Rightarrow> None |
581 (case ponesubst P1 M P2 of |
591 | Some P3 \<Rightarrow> Some (pnsubst1 P3 M P2 n))" |
582 None \<Rightarrow> None |
|
583 | Some P3 \<Rightarrow> Some (pnsubst1 P3 M P2 n))" |
592 |
584 |
593 fun psubstl1 :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol" |
585 fun psubstl1 :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol" |
594 where |
586 where |
595 "psubstl1 P1 [] n = P1" |
587 "psubstl1 P1 [] n = P1" |
596 | "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n" |
588 | "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n" |
597 |
589 |
598 fun psubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol option" |
590 fun psubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol option" |
599 where |
591 where |
600 "psubstl P1 [] n = None" |
592 "psubstl P1 [] n = None" |
601 | "psubstl P1 ((M, P2) # mps) n = (case pnsubst P1 M P2 n of |
593 | "psubstl P1 ((M, P2) # mps) n = |
602 None \<Rightarrow> psubstl P1 mps n |
594 (case pnsubst P1 M P2 n of |
603 | Some P3 \<Rightarrow> Some (psubstl1 P3 mps n))" |
595 None \<Rightarrow> psubstl P1 mps n |
|
596 | Some P3 \<Rightarrow> Some (psubstl1 P3 mps n))" |
604 |
597 |
605 fun pnsubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pol" |
598 fun pnsubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pol" |
606 where |
599 where "pnsubstl P1 mps m n = |
607 "pnsubstl P1 mps m n = (case psubstl P1 mps n of |
600 (case psubstl P1 mps n of |
608 None \<Rightarrow> P1 |
601 None \<Rightarrow> P1 |
609 | Some P3 \<Rightarrow> if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)" |
602 | Some P3 \<Rightarrow> if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)" |
610 |
603 |
611 lemma pnsubstl_0 [simp]: "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of |
604 lemma pnsubstl_0 [simp]: |
612 None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)" |
605 "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)" |
613 by (simp split: option.split) |
606 by (simp split: option.split) |
614 |
607 |
615 lemma pnsubstl_Suc [simp]: "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of |
608 lemma pnsubstl_Suc [simp]: |
616 None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubstl P3 mps m n)" |
609 "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubstl P3 mps m n)" |
617 by (simp split: option.split) |
610 by (simp split: option.split) |
618 |
611 |
619 declare pnsubstl.simps [simp del] |
612 declare pnsubstl.simps [simp del] |
620 |
613 |
621 lemma (in cring) ponesubst_correct: |
614 lemma (in cring) ponesubst_correct: |