17516

1 
(* ID: $Id$


2 
Author: Bernhard Haeupler


3 


4 
Proving equalities in commutative rings done "right" in Isabelle/HOL.


5 
*)


6 


7 
header {* Proving equalities in commutative rings *}


8 


9 
theory Commutative_Ring


10 
imports Main


11 
uses ("comm_ring.ML")


12 
begin


13 


14 
text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}


15 


16 
datatype 'a pol =


17 
Pc 'a


18 
 Pinj nat "'a pol"


19 
 PX "'a pol" nat "'a pol"


20 


21 
datatype 'a polex =


22 
Pol "'a pol"


23 
 Add "'a polex" "'a polex"


24 
 Sub "'a polex" "'a polex"


25 
 Mul "'a polex" "'a polex"


26 
 Pow "'a polex" nat


27 
 Neg "'a polex"


28 


29 
text {* Interpretation functions for the shadow syntax. *}


30 


31 
consts


32 
Ipol :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a pol \<Rightarrow> 'a"


33 
Ipolex :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a polex \<Rightarrow> 'a"


34 


35 
primrec


36 
"Ipol l (Pc c) = c"


37 
"Ipol l (Pinj i P) = Ipol (drop i l) P"


38 
"Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"


39 


40 
primrec


41 
"Ipolex l (Pol P) = Ipol l P"


42 
"Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"


43 
"Ipolex l (Sub P Q) = Ipolex l P  Ipolex l Q"


44 
"Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"


45 
"Ipolex l (Pow p n) = Ipolex l p ^ n"


46 
"Ipolex l (Neg P) =  Ipolex l P"


47 


48 
text {* Create polynomial normalized polynomials given normalized inputs. *}


49 

19736

50 
definition

17516

51 
mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"

19736

52 
"mkPinj x P = (case P of

17516

53 
Pc c \<Rightarrow> Pc c 


54 
Pinj y P \<Rightarrow> Pinj (x + y) P 


55 
PX p1 y p2 \<Rightarrow> Pinj x P)"


56 

19736

57 
definition

17516

58 
mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"

19736

59 
"mkPX P i Q = (case P of

17516

60 
Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) 


61 
Pinj j R \<Rightarrow> PX P i Q 


62 
PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"


63 


64 
text {* Defining the basic ring operations on normalized polynomials *}


65 


66 
consts


67 
add :: "'a::{comm_ring,recpower} pol \<times> 'a pol \<Rightarrow> 'a pol"


68 
mul :: "'a::{comm_ring,recpower} pol \<times> 'a pol \<Rightarrow> 'a pol"


69 
neg :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"


70 
sqr :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"


71 
pow :: "'a::{comm_ring,recpower} pol \<times> nat \<Rightarrow> 'a pol"


72 


73 
text {* Addition *}


74 
recdef add "measure (\<lambda>(x, y). size x + size y)"


75 
"add (Pc a, Pc b) = Pc (a + b)"


76 
"add (Pc c, Pinj i P) = Pinj i (add (P, Pc c))"


77 
"add (Pinj i P, Pc c) = Pinj i (add (P, Pc c))"


78 
"add (Pc c, PX P i Q) = PX P i (add (Q, Pc c))"


79 
"add (PX P i Q, Pc c) = PX P i (add (Q, Pc c))"


80 
"add (Pinj x P, Pinj y Q) =


81 
(if x=y then mkPinj x (add (P, Q))


82 
else (if x>y then mkPinj y (add (Pinj (xy) P, Q))


83 
else mkPinj x (add (Pinj (yx) Q, P)) ))"


84 
"add (Pinj x P, PX Q y R) =


85 
(if x=0 then add(P, PX Q y R)


86 
else (if x=1 then PX Q y (add (R, P))


87 
else PX Q y (add (R, Pinj (x  1) P))))"


88 
"add (PX P x R, Pinj y Q) =


89 
(if y=0 then add(PX P x R, Q)


90 
else (if y=1 then PX P x (add (R, Q))


91 
else PX P x (add (R, Pinj (y  1) Q))))"


92 
"add (PX P1 x P2, PX Q1 y Q2) =


93 
(if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2))


94 
else (if x>y then mkPX (add (PX P1 (xy) (Pc 0), Q1)) y (add (P2,Q2))


95 
else mkPX (add (PX Q1 (yx) (Pc 0), P1)) x (add (P2,Q2)) ))"


96 


97 
text {* Multiplication *}


98 
recdef mul "measure (\<lambda>(x, y). size x + size y)"


99 
"mul (Pc a, Pc b) = Pc (a*b)"


100 
"mul (Pc c, Pinj i P) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"


101 
"mul (Pinj i P, Pc c) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"


102 
"mul (Pc c, PX P i Q) =


103 
(if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"


104 
"mul (PX P i Q, Pc c) =


105 
(if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"


106 
"mul (Pinj x P, Pinj y Q) =


107 
(if x=y then mkPinj x (mul (P, Q))


108 
else (if x>y then mkPinj y (mul (Pinj (xy) P, Q))


109 
else mkPinj x (mul (Pinj (yx) Q, P)) ))"


110 
"mul (Pinj x P, PX Q y R) =


111 
(if x=0 then mul(P, PX Q y R)


112 
else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P))


113 
else mkPX (mul (Pinj x P, Q)) y (mul (R, Pinj (x  1) P))))"


114 
"mul (PX P x R, Pinj y Q) =


115 
(if y=0 then mul(PX P x R, Q)


116 
else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q))


117 
else mkPX (mul (Pinj y Q, P)) x (mul (R, Pinj (y  1) Q))))"


118 
"mul (PX P1 x P2, PX Q1 y Q2) =


119 
add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)),


120 
add (mkPX (mul (P1, mkPinj 1 Q2)) x (Pc 0), mkPX (mul (Q1, mkPinj 1 P2)) y (Pc 0)) )"


121 
(hints simp add: mkPinj_def split: pol.split)


122 


123 
text {* Negation*}


124 
primrec


125 
"neg (Pc c) = Pc (c)"


126 
"neg (Pinj i P) = Pinj i (neg P)"


127 
"neg (PX P x Q) = PX (neg P) x (neg Q)"


128 


129 
text {* Substraction *}

19736

130 
definition

17516

131 
sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"

19736

132 
"sub p q = add (p, neg q)"

17516

133 


134 
text {* Square for Fast Exponentation *}


135 
primrec


136 
"sqr (Pc c) = Pc (c * c)"


137 
"sqr (Pinj i P) = mkPinj i (sqr P)"


138 
"sqr (PX A x B) = add (mkPX (sqr A) (x + x) (sqr B),


139 
mkPX (mul (mul (Pc (1 + 1), A), mkPinj 1 B)) x (Pc 0))"


140 


141 
text {* Fast Exponentation *}


142 
lemma pow_wf:"odd n \<Longrightarrow> (n::nat) div 2 < n" by (cases n) auto


143 
recdef pow "measure (\<lambda>(x, y). y)"


144 
"pow (p, 0) = Pc 1"


145 
"pow (p, n) = (if even n then (pow (sqr p, n div 2)) else mul (p, pow (sqr p, n div 2)))"


146 
(hints simp add: pow_wf)


147 


148 
lemma pow_if:


149 
"pow (p,n) =


150 
(if n = 0 then Pc 1 else if even n then pow (sqr p, n div 2)


151 
else mul (p, pow (sqr p, n div 2)))"


152 
by (cases n) simp_all


153 


154 
(*


155 
lemma number_of_nat_B0: "(number_of (w BIT bit.B0) ::nat) = 2* (number_of w)"


156 
by simp


157 


158 
lemma number_of_nat_even: "even (number_of (w BIT bit.B0)::nat)"


159 
by simp


160 


161 
lemma pow_even : "pow (p, number_of(w BIT bit.B0)) = pow (sqr p, number_of w)"


162 
( is "pow(?p,?n) = pow (_,?n2)")


163 
proof


164 
have "even ?n" by simp


165 
hence "pow (p, ?n) = pow (sqr p, ?n div 2)"


166 
apply simp


167 
apply (cases "IntDef.neg (number_of w)")


168 
apply simp


169 
done


170 
*)


171 


172 
text {* Normalization of polynomial expressions *}


173 


174 
consts norm :: "'a::{comm_ring,recpower} polex \<Rightarrow> 'a pol"


175 
primrec


176 
"norm (Pol P) = P"


177 
"norm (Add P Q) = add (norm P, norm Q)"


178 
"norm (Sub p q) = sub (norm p) (norm q)"


179 
"norm (Mul P Q) = mul (norm P, norm Q)"


180 
"norm (Pow p n) = pow (norm p, n)"


181 
"norm (Neg P) = neg (norm P)"


182 


183 
text {* mkPinj preserve semantics *}


184 
lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"


185 
by (induct B) (auto simp add: mkPinj_def ring_eq_simps)


186 


187 
text {* mkPX preserves semantics *}


188 
lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"


189 
by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add ring_eq_simps)


190 


191 
text {* Correctness theorems for the implemented operations *}


192 


193 
text {* Negation *}


194 
lemma neg_ci: "\<And>l. Ipol l (neg P) = (Ipol l P)"


195 
by (induct P) auto


196 


197 
text {* Addition *}


198 
lemma add_ci: "\<And>l. Ipol l (add (P, Q)) = Ipol l P + Ipol l Q"


199 
proof (induct P Q rule: add.induct)


200 
case (6 x P y Q)


201 
show ?case


202 
proof (rule linorder_cases)


203 
assume "x < y"


204 
with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)


205 
next


206 
assume "x = y"


207 
with 6 show ?case by (simp add: mkPinj_ci)


208 
next


209 
assume "x > y"


210 
with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)


211 
qed


212 
next


213 
case (7 x P Q y R)


214 
have "x = 0 \<or> x = 1 \<or> x > 1" by arith


215 
moreover


216 
{ assume "x = 0" with 7 have ?case by simp }


217 
moreover


218 
{ assume "x = 1" with 7 have ?case by (simp add: ring_eq_simps) }


219 
moreover


220 
{ assume "x > 1" from 7 have ?case by (cases x) simp_all }


221 
ultimately show ?case by blast


222 
next


223 
case (8 P x R y Q)


224 
have "y = 0 \<or> y = 1 \<or> y > 1" by arith


225 
moreover


226 
{ assume "y = 0" with 8 have ?case by simp }


227 
moreover


228 
{ assume "y = 1" with 8 have ?case by simp }


229 
moreover


230 
{ assume "y > 1" with 8 have ?case by simp }


231 
ultimately show ?case by blast


232 
next


233 
case (9 P1 x P2 Q1 y Q2)


234 
show ?case


235 
proof (rule linorder_cases)


236 
assume a: "x < y" hence "EX d. d + x = y" by arith


237 
with 9 a show ?case by (auto simp add: mkPX_ci power_add ring_eq_simps)


238 
next


239 
assume a: "y < x" hence "EX d. d + y = x" by arith


240 
with 9 a show ?case by (auto simp add: power_add mkPX_ci ring_eq_simps)


241 
next


242 
assume "x = y"


243 
with 9 show ?case by (simp add: mkPX_ci ring_eq_simps)


244 
qed


245 
qed (auto simp add: ring_eq_simps)


246 


247 
text {* Multiplication *}


248 
lemma mul_ci: "\<And>l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"


249 
by (induct P Q rule: mul.induct)


250 
(simp_all add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)


251 


252 
text {* Substraction *}


253 
lemma sub_ci: "Ipol l (sub p q) = Ipol l p  Ipol l q"


254 
by (simp add: add_ci neg_ci sub_def)


255 


256 
text {* Square *}


257 
lemma sqr_ci:"\<And>ls. Ipol ls (sqr p) = Ipol ls p * Ipol ls p"


258 
by (induct p) (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_eq_simps power_add)


259 


260 


261 
text {* Power *}


262 
lemma even_pow:"even n \<Longrightarrow> pow (p, n) = pow (sqr p, n div 2)" by (induct n) simp_all


263 


264 
lemma pow_ci: "\<And>p. Ipol ls (pow (p, n)) = (Ipol ls p) ^ n"


265 
proof (induct n rule: nat_less_induct)


266 
case (1 k)


267 
have two:"2 = Suc (Suc 0)" by simp


268 
show ?case


269 
proof (cases k)


270 
case (Suc l)


271 
show ?thesis


272 
proof cases


273 
assume EL: "even l"


274 
have "Suc l div 2 = l div 2"


275 
by (simp add: nat_number even_nat_plus_one_div_two [OF EL])


276 
moreover


277 
from Suc have "l < k" by simp


278 
with 1 have "\<forall>p. Ipol ls (pow (p, l)) = Ipol ls p ^ l" by simp


279 
moreover


280 
note Suc EL even_nat_plus_one_div_two [OF EL]


281 
ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow)


282 
next


283 
assume OL: "odd l"


284 
with prems have "\<lbrakk>\<forall>m<Suc l. \<forall>p. Ipol ls (pow (p, m)) = Ipol ls p ^ m; k = Suc l; odd l\<rbrakk> \<Longrightarrow> \<forall>p. Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l"


285 
proof(cases l)


286 
case (Suc w)


287 
from prems have EW: "even w" by simp


288 
from two have two_times:"(2 * (w div 2))= w"


289 
by (simp only: even_nat_div_two_times_two[OF EW])


290 
have A: "\<And>p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))"


291 
by (simp add: power_Suc)


292 
from A two [symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2"


293 
by simp


294 
with prems show ?thesis


295 
by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)


296 
qed simp


297 
with prems show ?thesis by simp


298 
qed


299 
next


300 
case 0


301 
then show ?thesis by simp


302 
qed


303 
qed


304 


305 
text {* Normalization preserves semantics *}


306 
lemma norm_ci:"Ipolex l Pe = Ipol l (norm Pe)"


307 
by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)


308 


309 
text {* Reflection lemma: Key to the (incomplete) decision procedure *}


310 
lemma norm_eq:


311 
assumes eq: "norm P1 = norm P2"


312 
shows "Ipolex l P1 = Ipolex l P2"


313 
proof 


314 
from eq have "Ipol l (norm P1) = Ipol l (norm P2)" by simp


315 
thus ?thesis by (simp only: norm_ci)


316 
qed


317 


318 


319 
use "comm_ring.ML"

18708

320 
setup CommRing.setup

17516

321 


322 
end
