1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Fri Oct 30 13:59:49 2009 +0100
1.3 @@ -0,0 +1,319 @@
1.4 +(* Author: Bernhard Haeupler
1.5 +
1.6 +Proving equalities in commutative rings done "right" in Isabelle/HOL.
1.7 +*)
1.8 +
1.9 +header {* Proving equalities in commutative rings *}
1.10 +
1.11 +theory Commutative_Ring
1.12 +imports Main Parity
1.13 +uses ("commutative_ring_tac.ML")
1.14 +begin
1.15 +
1.16 +text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
1.17 +
1.18 +datatype 'a pol =
1.19 + Pc 'a
1.20 + | Pinj nat "'a pol"
1.21 + | PX "'a pol" nat "'a pol"
1.22 +
1.23 +datatype 'a polex =
1.24 + Pol "'a pol"
1.25 + | Add "'a polex" "'a polex"
1.26 + | Sub "'a polex" "'a polex"
1.27 + | Mul "'a polex" "'a polex"
1.28 + | Pow "'a polex" nat
1.29 + | Neg "'a polex"
1.30 +
1.31 +text {* Interpretation functions for the shadow syntax. *}
1.32 +
1.33 +primrec
1.34 + Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
1.35 +where
1.36 + "Ipol l (Pc c) = c"
1.37 + | "Ipol l (Pinj i P) = Ipol (drop i l) P"
1.38 + | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
1.39 +
1.40 +primrec
1.41 + Ipolex :: "'a::{comm_ring_1} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
1.42 +where
1.43 + "Ipolex l (Pol P) = Ipol l P"
1.44 + | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
1.45 + | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
1.46 + | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
1.47 + | "Ipolex l (Pow p n) = Ipolex l p ^ n"
1.48 + | "Ipolex l (Neg P) = - Ipolex l P"
1.49 +
1.50 +text {* Create polynomial normalized polynomials given normalized inputs. *}
1.51 +
1.52 +definition
1.53 + mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
1.54 + "mkPinj x P = (case P of
1.55 + Pc c \<Rightarrow> Pc c |
1.56 + Pinj y P \<Rightarrow> Pinj (x + y) P |
1.57 + PX p1 y p2 \<Rightarrow> Pinj x P)"
1.58 +
1.59 +definition
1.60 + mkPX :: "'a::{comm_ring} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
1.61 + "mkPX P i Q = (case P of
1.62 + Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
1.63 + Pinj j R \<Rightarrow> PX P i Q |
1.64 + PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
1.65 +
1.66 +text {* Defining the basic ring operations on normalized polynomials *}
1.67 +
1.68 +function
1.69 + add :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
1.70 +where
1.71 + "Pc a \<oplus> Pc b = Pc (a + b)"
1.72 + | "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
1.73 + | "Pinj i P \<oplus> Pc c = Pinj i (P \<oplus> Pc c)"
1.74 + | "Pc c \<oplus> PX P i Q = PX P i (Q \<oplus> Pc c)"
1.75 + | "PX P i Q \<oplus> Pc c = PX P i (Q \<oplus> Pc c)"
1.76 + | "Pinj x P \<oplus> Pinj y Q =
1.77 + (if x = y then mkPinj x (P \<oplus> Q)
1.78 + else (if x > y then mkPinj y (Pinj (x - y) P \<oplus> Q)
1.79 + else mkPinj x (Pinj (y - x) Q \<oplus> P)))"
1.80 + | "Pinj x P \<oplus> PX Q y R =
1.81 + (if x = 0 then P \<oplus> PX Q y R
1.82 + else (if x = 1 then PX Q y (R \<oplus> P)
1.83 + else PX Q y (R \<oplus> Pinj (x - 1) P)))"
1.84 + | "PX P x R \<oplus> Pinj y Q =
1.85 + (if y = 0 then PX P x R \<oplus> Q
1.86 + else (if y = 1 then PX P x (R \<oplus> Q)
1.87 + else PX P x (R \<oplus> Pinj (y - 1) Q)))"
1.88 + | "PX P1 x P2 \<oplus> PX Q1 y Q2 =
1.89 + (if x = y then mkPX (P1 \<oplus> Q1) x (P2 \<oplus> Q2)
1.90 + else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<oplus> Q1) y (P2 \<oplus> Q2)
1.91 + else mkPX (PX Q1 (y-x) (Pc 0) \<oplus> P1) x (P2 \<oplus> Q2)))"
1.92 +by pat_completeness auto
1.93 +termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
1.94 +
1.95 +function
1.96 + mul :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
1.97 +where
1.98 + "Pc a \<otimes> Pc b = Pc (a * b)"
1.99 + | "Pc c \<otimes> Pinj i P =
1.100 + (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
1.101 + | "Pinj i P \<otimes> Pc c =
1.102 + (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
1.103 + | "Pc c \<otimes> PX P i Q =
1.104 + (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
1.105 + | "PX P i Q \<otimes> Pc c =
1.106 + (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
1.107 + | "Pinj x P \<otimes> Pinj y Q =
1.108 + (if x = y then mkPinj x (P \<otimes> Q) else
1.109 + (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q)
1.110 + else mkPinj x (Pinj (y - x) Q \<otimes> P)))"
1.111 + | "Pinj x P \<otimes> PX Q y R =
1.112 + (if x = 0 then P \<otimes> PX Q y R else
1.113 + (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P)
1.114 + else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))"
1.115 + | "PX P x R \<otimes> Pinj y Q =
1.116 + (if y = 0 then PX P x R \<otimes> Q else
1.117 + (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q)
1.118 + else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))"
1.119 + | "PX P1 x P2 \<otimes> PX Q1 y Q2 =
1.120 + mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus>
1.121 + (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus>
1.122 + (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))"
1.123 +by pat_completeness auto
1.124 +termination by (relation "measure (\<lambda>(x, y). size x + size y)")
1.125 + (auto simp add: mkPinj_def split: pol.split)
1.126 +
1.127 +text {* Negation*}
1.128 +primrec
1.129 + neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
1.130 +where
1.131 + "neg (Pc c) = Pc (-c)"
1.132 + | "neg (Pinj i P) = Pinj i (neg P)"
1.133 + | "neg (PX P x Q) = PX (neg P) x (neg Q)"
1.134 +
1.135 +text {* Substraction *}
1.136 +definition
1.137 + sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
1.138 +where
1.139 + "sub P Q = P \<oplus> neg Q"
1.140 +
1.141 +text {* Square for Fast Exponentation *}
1.142 +primrec
1.143 + sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
1.144 +where
1.145 + "sqr (Pc c) = Pc (c * c)"
1.146 + | "sqr (Pinj i P) = mkPinj i (sqr P)"
1.147 + | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<oplus>
1.148 + mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
1.149 +
1.150 +text {* Fast Exponentation *}
1.151 +fun
1.152 + pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
1.153 +where
1.154 + "pow 0 P = Pc 1"
1.155 + | "pow n P = (if even n then pow (n div 2) (sqr P)
1.156 + else P \<otimes> pow (n div 2) (sqr P))"
1.157 +
1.158 +lemma pow_if:
1.159 + "pow n P =
1.160 + (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
1.161 + else P \<otimes> pow (n div 2) (sqr P))"
1.162 + by (cases n) simp_all
1.163 +
1.164 +
1.165 +text {* Normalization of polynomial expressions *}
1.166 +
1.167 +primrec
1.168 + norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
1.169 +where
1.170 + "norm (Pol P) = P"
1.171 + | "norm (Add P Q) = norm P \<oplus> norm Q"
1.172 + | "norm (Sub P Q) = norm P \<ominus> norm Q"
1.173 + | "norm (Mul P Q) = norm P \<otimes> norm Q"
1.174 + | "norm (Pow P n) = pow n (norm P)"
1.175 + | "norm (Neg P) = neg (norm P)"
1.176 +
1.177 +text {* mkPinj preserve semantics *}
1.178 +lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
1.179 + by (induct B) (auto simp add: mkPinj_def algebra_simps)
1.180 +
1.181 +text {* mkPX preserves semantics *}
1.182 +lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
1.183 + by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
1.184 +
1.185 +text {* Correctness theorems for the implemented operations *}
1.186 +
1.187 +text {* Negation *}
1.188 +lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
1.189 + by (induct P arbitrary: l) auto
1.190 +
1.191 +text {* Addition *}
1.192 +lemma add_ci: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
1.193 +proof (induct P Q arbitrary: l rule: add.induct)
1.194 + case (6 x P y Q)
1.195 + show ?case
1.196 + proof (rule linorder_cases)
1.197 + assume "x < y"
1.198 + with 6 show ?case by (simp add: mkPinj_ci algebra_simps)
1.199 + next
1.200 + assume "x = y"
1.201 + with 6 show ?case by (simp add: mkPinj_ci)
1.202 + next
1.203 + assume "x > y"
1.204 + with 6 show ?case by (simp add: mkPinj_ci algebra_simps)
1.205 + qed
1.206 +next
1.207 + case (7 x P Q y R)
1.208 + have "x = 0 \<or> x = 1 \<or> x > 1" by arith
1.209 + moreover
1.210 + { assume "x = 0" with 7 have ?case by simp }
1.211 + moreover
1.212 + { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) }
1.213 + moreover
1.214 + { assume "x > 1" from 7 have ?case by (cases x) simp_all }
1.215 + ultimately show ?case by blast
1.216 +next
1.217 + case (8 P x R y Q)
1.218 + have "y = 0 \<or> y = 1 \<or> y > 1" by arith
1.219 + moreover
1.220 + { assume "y = 0" with 8 have ?case by simp }
1.221 + moreover
1.222 + { assume "y = 1" with 8 have ?case by simp }
1.223 + moreover
1.224 + { assume "y > 1" with 8 have ?case by simp }
1.225 + ultimately show ?case by blast
1.226 +next
1.227 + case (9 P1 x P2 Q1 y Q2)
1.228 + show ?case
1.229 + proof (rule linorder_cases)
1.230 + assume a: "x < y" hence "EX d. d + x = y" by arith
1.231 + with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps)
1.232 + next
1.233 + assume a: "y < x" hence "EX d. d + y = x" by arith
1.234 + with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps)
1.235 + next
1.236 + assume "x = y"
1.237 + with 9 show ?case by (simp add: mkPX_ci algebra_simps)
1.238 + qed
1.239 +qed (auto simp add: algebra_simps)
1.240 +
1.241 +text {* Multiplication *}
1.242 +lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
1.243 + by (induct P Q arbitrary: l rule: mul.induct)
1.244 + (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add)
1.245 +
1.246 +text {* Substraction *}
1.247 +lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
1.248 + by (simp add: add_ci neg_ci sub_def)
1.249 +
1.250 +text {* Square *}
1.251 +lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
1.252 + by (induct P arbitrary: ls)
1.253 + (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
1.254 +
1.255 +text {* Power *}
1.256 +lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
1.257 + by (induct n) simp_all
1.258 +
1.259 +lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
1.260 +proof (induct n arbitrary: P rule: nat_less_induct)
1.261 + case (1 k)
1.262 + show ?case
1.263 + proof (cases k)
1.264 + case 0
1.265 + then show ?thesis by simp
1.266 + next
1.267 + case (Suc l)
1.268 + show ?thesis
1.269 + proof cases
1.270 + assume "even l"
1.271 + then have "Suc l div 2 = l div 2"
1.272 + by (simp add: nat_number even_nat_plus_one_div_two)
1.273 + moreover
1.274 + from Suc have "l < k" by simp
1.275 + with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
1.276 + moreover
1.277 + note Suc `even l` even_nat_plus_one_div_two
1.278 + ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow)
1.279 + next
1.280 + assume "odd l"
1.281 + {
1.282 + fix p
1.283 + have "Ipol ls (sqr P) ^ (Suc l div 2) = Ipol ls P ^ Suc l"
1.284 + proof (cases l)
1.285 + case 0
1.286 + with `odd l` show ?thesis by simp
1.287 + next
1.288 + case (Suc w)
1.289 + with `odd l` have "even w" by simp
1.290 + have two_times: "2 * (w div 2) = w"
1.291 + by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
1.292 + have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
1.293 + by (simp add: power_Suc)
1.294 + then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
1.295 + by (simp add: numerals)
1.296 + with Suc show ?thesis
1.297 + by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
1.298 + simp del: power_Suc)
1.299 + qed
1.300 + } with 1 Suc `odd l` show ?thesis by simp
1.301 + qed
1.302 + qed
1.303 +qed
1.304 +
1.305 +text {* Normalization preserves semantics *}
1.306 +lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
1.307 + by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
1.308 +
1.309 +text {* Reflection lemma: Key to the (incomplete) decision procedure *}
1.310 +lemma norm_eq:
1.311 + assumes "norm P1 = norm P2"
1.312 + shows "Ipolex l P1 = Ipolex l P2"
1.313 +proof -
1.314 + from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
1.315 + then show ?thesis by (simp only: norm_ci)
1.316 +qed
1.317 +
1.318 +
1.319 +use "commutative_ring_tac.ML"
1.320 +setup Commutative_Ring_Tac.setup
1.321 +
1.322 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Fri Oct 30 13:59:49 2009 +0100
2.3 @@ -0,0 +1,391 @@
2.4 +(* Author: Bernhard Haeupler
2.5 +
2.6 +This theory is about of the relative completeness of method comm-ring
2.7 +method. As long as the reified atomic polynomials of type 'a pol are
2.8 +in normal form, the cring method is complete.
2.9 +*)
2.10 +
2.11 +header {* Proof of the relative completeness of method comm-ring *}
2.12 +
2.13 +theory Commutative_Ring_Complete
2.14 +imports Commutative_Ring
2.15 +begin
2.16 +
2.17 +text {* Formalization of normal form *}
2.18 +fun
2.19 + isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
2.20 +where
2.21 + "isnorm (Pc c) \<longleftrightarrow> True"
2.22 + | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
2.23 + | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"
2.24 + | "isnorm (Pinj 0 P) \<longleftrightarrow> False"
2.25 + | "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"
2.26 + | "isnorm (PX P 0 Q) \<longleftrightarrow> False"
2.27 + | "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"
2.28 + | "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"
2.29 + | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
2.30 +
2.31 +(* Some helpful lemmas *)
2.32 +lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
2.33 +by(cases P, auto)
2.34 +
2.35 +lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
2.36 +by(cases i, auto)
2.37 +
2.38 +lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
2.39 +by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
2.40 +
2.41 +lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
2.42 +by(cases i, auto, cases P, auto, case_tac pol2, auto)
2.43 +
2.44 +lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
2.45 +by(cases i, auto, cases P, auto, case_tac pol2, auto)
2.46 +
2.47 +lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)"
2.48 +apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
2.49 +apply(case_tac nat, auto simp add: norm_Pinj_0_False)
2.50 +by(case_tac pol, auto) (case_tac y, auto)
2.51 +
2.52 +lemma norm_PXtrans:
2.53 + assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
2.54 + shows "isnorm (PX P x Q2)"
2.55 +proof(cases P)
2.56 + case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
2.57 +next
2.58 + case Pc from prems show ?thesis by(cases x, auto)
2.59 +next
2.60 + case Pinj from prems show ?thesis by(cases x, auto)
2.61 +qed
2.62 +
2.63 +lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)"
2.64 +proof(cases P)
2.65 + case (PX p1 y p2)
2.66 + from prems show ?thesis by(cases x, auto, cases p2, auto)
2.67 +next
2.68 + case Pc
2.69 + from prems show ?thesis by(cases x, auto)
2.70 +next
2.71 + case Pinj
2.72 + from prems show ?thesis by(cases x, auto)
2.73 +qed
2.74 +
2.75 +text {* mkPX conserves normalizedness (@{text "_cn"}) *}
2.76 +lemma mkPX_cn:
2.77 + assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q"
2.78 + shows "isnorm (mkPX P x Q)"
2.79 +proof(cases P)
2.80 + case (Pc c)
2.81 + from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
2.82 +next
2.83 + case (Pinj i Q)
2.84 + from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
2.85 +next
2.86 + case (PX P1 y P2)
2.87 + from prems have Y0:"y>0" by(cases y, auto)
2.88 + from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
2.89 + with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
2.90 +qed
2.91 +
2.92 +text {* add conserves normalizedness *}
2.93 +lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
2.94 +proof(induct P Q rule: add.induct)
2.95 + case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
2.96 +next
2.97 + case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
2.98 +next
2.99 + case (4 c P2 i Q2)
2.100 + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
2.101 + with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
2.102 +next
2.103 + case (5 P2 i Q2 c)
2.104 + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
2.105 + with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
2.106 +next
2.107 + case (6 x P2 y Q2)
2.108 + from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False)
2.109 + from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False)
2.110 + have "x < y \<or> x = y \<or> x > y" by arith
2.111 + moreover
2.112 + { assume "x<y" hence "EX d. y=d+x" by arith
2.113 + then obtain d where "y=d+x"..
2.114 + moreover
2.115 + note prems X0
2.116 + moreover
2.117 + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
2.118 + moreover
2.119 + with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
2.120 + ultimately have ?case by (simp add: mkPinj_cn)}
2.121 + moreover
2.122 + { assume "x=y"
2.123 + moreover
2.124 + from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
2.125 + moreover
2.126 + note prems Y0
2.127 + moreover
2.128 + ultimately have ?case by (simp add: mkPinj_cn) }
2.129 + moreover
2.130 + { assume "x>y" hence "EX d. x=d+y" by arith
2.131 + then obtain d where "x=d+y"..
2.132 + moreover
2.133 + note prems Y0
2.134 + moreover
2.135 + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
2.136 + moreover
2.137 + with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
2.138 + ultimately have ?case by (simp add: mkPinj_cn)}
2.139 + ultimately show ?case by blast
2.140 +next
2.141 + case (7 x P2 Q2 y R)
2.142 + have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
2.143 + moreover
2.144 + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
2.145 + moreover
2.146 + { assume "x=1"
2.147 + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
2.148 + with prems have "isnorm (R \<oplus> P2)" by simp
2.149 + with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
2.150 + moreover
2.151 + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
2.152 + then obtain d where X:"x=Suc (Suc d)" ..
2.153 + from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
2.154 + with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
2.155 + with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
2.156 + with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
2.157 + ultimately show ?case by blast
2.158 +next
2.159 + case (8 Q2 y R x P2)
2.160 + have "x = 0 \<or> x = 1 \<or> x > 1" by arith
2.161 + moreover
2.162 + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
2.163 + moreover
2.164 + { assume "x=1"
2.165 + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
2.166 + with prems have "isnorm (R \<oplus> P2)" by simp
2.167 + with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
2.168 + moreover
2.169 + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
2.170 + then obtain d where X:"x=Suc (Suc d)" ..
2.171 + from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
2.172 + with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
2.173 + with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
2.174 + with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
2.175 + ultimately show ?case by blast
2.176 +next
2.177 + case (9 P1 x P2 Q1 y Q2)
2.178 + from prems have Y0:"y>0" by(cases y, auto)
2.179 + from prems have X0:"x>0" by(cases x, auto)
2.180 + from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
2.181 + from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
2.182 + have "y < x \<or> x = y \<or> x < y" by arith
2.183 + moreover
2.184 + {assume sm1:"y < x" hence "EX d. x=d+y" by arith
2.185 + then obtain d where sm2:"x=d+y"..
2.186 + note prems NQ1 NP1 NP2 NQ2 sm1 sm2
2.187 + moreover
2.188 + have "isnorm (PX P1 d (Pc 0))"
2.189 + proof(cases P1)
2.190 + case (PX p1 y p2)
2.191 + with prems show ?thesis by(cases d, simp,cases p2, auto)
2.192 + next case Pc from prems show ?thesis by(cases d, auto)
2.193 + next case Pinj from prems show ?thesis by(cases d, auto)
2.194 + qed
2.195 + ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
2.196 + with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
2.197 + moreover
2.198 + {assume "x=y"
2.199 + from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
2.200 + with Y0 prems have ?case by (simp add: mkPX_cn) }
2.201 + moreover
2.202 + {assume sm1:"x<y" hence "EX d. y=d+x" by arith
2.203 + then obtain d where sm2:"y=d+x"..
2.204 + note prems NQ1 NP1 NP2 NQ2 sm1 sm2
2.205 + moreover
2.206 + have "isnorm (PX Q1 d (Pc 0))"
2.207 + proof(cases Q1)
2.208 + case (PX p1 y p2)
2.209 + with prems show ?thesis by(cases d, simp,cases p2, auto)
2.210 + next case Pc from prems show ?thesis by(cases d, auto)
2.211 + next case Pinj from prems show ?thesis by(cases d, auto)
2.212 + qed
2.213 + ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
2.214 + with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
2.215 + ultimately show ?case by blast
2.216 +qed simp
2.217 +
2.218 +text {* mul concerves normalizedness *}
2.219 +lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
2.220 +proof(induct P Q rule: mul.induct)
2.221 + case (2 c i P2) thus ?case
2.222 + by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
2.223 +next
2.224 + case (3 i P2 c) thus ?case
2.225 + by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
2.226 +next
2.227 + case (4 c P2 i Q2)
2.228 + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
2.229 + with prems show ?case
2.230 + by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
2.231 +next
2.232 + case (5 P2 i Q2 c)
2.233 + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
2.234 + with prems show ?case
2.235 + by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
2.236 +next
2.237 + case (6 x P2 y Q2)
2.238 + have "x < y \<or> x = y \<or> x > y" by arith
2.239 + moreover
2.240 + { assume "x<y" hence "EX d. y=d+x" by arith
2.241 + then obtain d where "y=d+x"..
2.242 + moreover
2.243 + note prems
2.244 + moreover
2.245 + from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False)
2.246 + moreover
2.247 + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
2.248 + moreover
2.249 + with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
2.250 + ultimately have ?case by (simp add: mkPinj_cn)}
2.251 + moreover
2.252 + { assume "x=y"
2.253 + moreover
2.254 + from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
2.255 + moreover
2.256 + with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
2.257 + moreover
2.258 + note prems
2.259 + moreover
2.260 + ultimately have ?case by (simp add: mkPinj_cn) }
2.261 + moreover
2.262 + { assume "x>y" hence "EX d. x=d+y" by arith
2.263 + then obtain d where "x=d+y"..
2.264 + moreover
2.265 + note prems
2.266 + moreover
2.267 + from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
2.268 + moreover
2.269 + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
2.270 + moreover
2.271 + with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
2.272 + ultimately have ?case by (simp add: mkPinj_cn) }
2.273 + ultimately show ?case by blast
2.274 +next
2.275 + case (7 x P2 Q2 y R)
2.276 + from prems have Y0:"y>0" by(cases y, auto)
2.277 + have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
2.278 + moreover
2.279 + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
2.280 + moreover
2.281 + { assume "x=1"
2.282 + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
2.283 + with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
2.284 + with Y0 prems have ?case by (simp add: mkPX_cn)}
2.285 + moreover
2.286 + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
2.287 + then obtain d where X:"x=Suc (Suc d)" ..
2.288 + from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
2.289 + moreover
2.290 + from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
2.291 + moreover
2.292 + from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
2.293 + moreover
2.294 + note prems
2.295 + ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
2.296 + with Y0 X have ?case by (simp add: mkPX_cn)}
2.297 + ultimately show ?case by blast
2.298 +next
2.299 + case (8 Q2 y R x P2)
2.300 + from prems have Y0:"y>0" by(cases y, auto)
2.301 + have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
2.302 + moreover
2.303 + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
2.304 + moreover
2.305 + { assume "x=1"
2.306 + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
2.307 + with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
2.308 + with Y0 prems have ?case by (simp add: mkPX_cn) }
2.309 + moreover
2.310 + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
2.311 + then obtain d where X:"x=Suc (Suc d)" ..
2.312 + from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
2.313 + moreover
2.314 + from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
2.315 + moreover
2.316 + from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
2.317 + moreover
2.318 + note prems
2.319 + ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
2.320 + with Y0 X have ?case by (simp add: mkPX_cn) }
2.321 + ultimately show ?case by blast
2.322 +next
2.323 + case (9 P1 x P2 Q1 y Q2)
2.324 + from prems have X0:"x>0" by(cases x, auto)
2.325 + from prems have Y0:"y>0" by(cases y, auto)
2.326 + note prems
2.327 + moreover
2.328 + from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
2.329 + moreover
2.330 + from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
2.331 + ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
2.332 + "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
2.333 + by (auto simp add: mkPinj_cn)
2.334 + with prems X0 Y0 have
2.335 + "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
2.336 + "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
2.337 + "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
2.338 + by (auto simp add: mkPX_cn)
2.339 + thus ?case by (simp add: add_cn)
2.340 +qed(simp)
2.341 +
2.342 +text {* neg conserves normalizedness *}
2.343 +lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
2.344 +proof (induct P)
2.345 + case (Pinj i P2)
2.346 + from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
2.347 + with prems show ?case by(cases P2, auto, cases i, auto)
2.348 +next
2.349 + case (PX P1 x P2)
2.350 + from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
2.351 + with prems show ?case
2.352 + proof(cases P1)
2.353 + case (PX p1 y p2)
2.354 + with prems show ?thesis by(cases x, auto, cases p2, auto)
2.355 + next
2.356 + case Pinj
2.357 + with prems show ?thesis by(cases x, auto)
2.358 + qed(cases x, auto)
2.359 +qed(simp)
2.360 +
2.361 +text {* sub conserves normalizedness *}
2.362 +lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
2.363 +by (simp add: sub_def add_cn neg_cn)
2.364 +
2.365 +text {* sqr conserves normalizizedness *}
2.366 +lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
2.367 +proof(induct P)
2.368 + case (Pinj i Q)
2.369 + from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
2.370 +next
2.371 + case (PX P1 x P2)
2.372 + from prems have "x+x~=0" "isnorm P2" "isnorm P1" by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
2.373 + with prems have
2.374 + "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
2.375 + and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
2.376 + by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
2.377 + thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
2.378 +qed simp
2.379 +
2.380 +text {* pow conserves normalizedness *}
2.381 +lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)"
2.382 +proof (induct n arbitrary: P rule: nat_less_induct)
2.383 + case (1 k)
2.384 + show ?case
2.385 + proof (cases "k=0")
2.386 + case False
2.387 + then have K2:"k div 2 < k" by (cases k, auto)
2.388 + from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
2.389 + with prems K2 show ?thesis
2.390 + by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
2.391 + qed simp
2.392 +qed
2.393 +
2.394 +end
3.1 --- a/src/HOL/Decision_Procs/Decision_Procs.thy Fri Oct 30 01:32:06 2009 +0100
3.2 +++ b/src/HOL/Decision_Procs/Decision_Procs.thy Fri Oct 30 13:59:49 2009 +0100
3.3 @@ -1,7 +1,10 @@
3.4 -header {* Various decision procedures. typically involving reflection *}
3.5 +header {* Various decision procedures, typically involving reflection *}
3.6
3.7 theory Decision_Procs
3.8 -imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" Parametric_Ferrante_Rackoff
3.9 +imports
3.10 + Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order Parametric_Ferrante_Rackoff
3.11 + Commutative_Ring_Complete
3.12 + "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
3.13 begin
3.14
3.15 end
3.16 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Oct 30 13:59:49 2009 +0100
4.3 @@ -0,0 +1,104 @@
4.4 +(* Author: Amine Chaieb
4.5 +
4.6 +Tactic for solving equalities over commutative rings.
4.7 +*)
4.8 +
4.9 +signature COMMUTATIVE_RING_TAC =
4.10 +sig
4.11 + val tac: Proof.context -> int -> tactic
4.12 + val setup: theory -> theory
4.13 +end
4.14 +
4.15 +structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
4.16 +struct
4.17 +
4.18 +(* Zero and One of the commutative ring *)
4.19 +fun cring_zero T = Const (@{const_name HOL.zero}, T);
4.20 +fun cring_one T = Const (@{const_name HOL.one}, T);
4.21 +
4.22 +(* reification functions *)
4.23 +(* add two polynom expressions *)
4.24 +fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]);
4.25 +fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
4.26 +
4.27 +(* pol *)
4.28 +fun pol_Pc t = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
4.29 +fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
4.30 +fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
4.31 +
4.32 +(* polex *)
4.33 +fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
4.34 +fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
4.35 +fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
4.36 +fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
4.37 +fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
4.38 +fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
4.39 +
4.40 +(* reification of polynoms : primitive cring expressions *)
4.41 +fun reif_pol T vs (t as Free _) =
4.42 + let
4.43 + val one = @{term "1::nat"};
4.44 + val i = find_index (fn t' => t' = t) vs
4.45 + in if i = 0
4.46 + then pol_PX T $ (pol_Pc T $ cring_one T)
4.47 + $ one $ (pol_Pc T $ cring_zero T)
4.48 + else pol_Pinj T $ HOLogic.mk_nat i
4.49 + $ (pol_PX T $ (pol_Pc T $ cring_one T)
4.50 + $ one $ (pol_Pc T $ cring_zero T))
4.51 + end
4.52 + | reif_pol T vs t = pol_Pc T $ t;
4.53 +
4.54 +(* reification of polynom expressions *)
4.55 +fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
4.56 + polex_add T $ reif_polex T vs a $ reif_polex T vs b
4.57 + | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
4.58 + polex_sub T $ reif_polex T vs a $ reif_polex T vs b
4.59 + | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
4.60 + polex_mul T $ reif_polex T vs a $ reif_polex T vs b
4.61 + | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
4.62 + polex_neg T $ reif_polex T vs a
4.63 + | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
4.64 + polex_pow T $ reif_polex T vs a $ n
4.65 + | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
4.66 +
4.67 +(* reification of the equation *)
4.68 +val cr_sort = @{sort "comm_ring_1"};
4.69 +
4.70 +fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
4.71 + if Sign.of_sort thy (T, cr_sort) then
4.72 + let
4.73 + val fs = OldTerm.term_frees eq;
4.74 + val cvs = cterm_of thy (HOLogic.mk_list T fs);
4.75 + val clhs = cterm_of thy (reif_polex T fs lhs);
4.76 + val crhs = cterm_of thy (reif_polex T fs rhs);
4.77 + val ca = ctyp_of thy T;
4.78 + in (ca, cvs, clhs, crhs) end
4.79 + else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
4.80 + | reif_eq _ _ = error "reif_eq: not an equation";
4.81 +
4.82 +(* The cring tactic *)
4.83 +(* Attention: You have to make sure that no t^0 is in the goal!! *)
4.84 +(* Use simply rewriting t^0 = 1 *)
4.85 +val cring_simps =
4.86 + [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
4.87 + @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
4.88 +
4.89 +fun tac ctxt = SUBGOAL (fn (g, i) =>
4.90 + let
4.91 + val thy = ProofContext.theory_of ctxt;
4.92 + val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*)
4.93 + addsimps cring_simps;
4.94 + val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
4.95 + val norm_eq_th =
4.96 + simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
4.97 + in
4.98 + cut_rules_tac [norm_eq_th] i
4.99 + THEN (simp_tac cring_ss i)
4.100 + THEN (simp_tac cring_ss i)
4.101 + end);
4.102 +
4.103 +val setup =
4.104 + Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac))
4.105 + "reflective decision procedure for equalities over commutative rings";
4.106 +
4.107 +end;
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Fri Oct 30 13:59:49 2009 +0100
5.3 @@ -0,0 +1,48 @@
5.4 +(* Author: Bernhard Haeupler *)
5.5 +
5.6 +header {* Some examples demonstrating the comm-ring method *}
5.7 +
5.8 +theory Commutative_Ring_Ex
5.9 +imports Commutative_Ring
5.10 +begin
5.11 +
5.12 +lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
5.13 +by comm_ring
5.14 +
5.15 +lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y"
5.16 +by comm_ring
5.17 +
5.18 +lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x"
5.19 +by comm_ring
5.20 +
5.21 +lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3"
5.22 +by comm_ring
5.23 +
5.24 +lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y"
5.25 +by comm_ring
5.26 +
5.27 +lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c"
5.28 +by comm_ring
5.29 +
5.30 +lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c"
5.31 +by comm_ring
5.32 +
5.33 +lemma "(a::int)*b + a*c = a*(b+c)"
5.34 +by comm_ring
5.35 +
5.36 +lemma "(a::int)^2 - b^2 = (a - b) * (a + b)"
5.37 +by comm_ring
5.38 +
5.39 +lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)"
5.40 +by comm_ring
5.41 +
5.42 +lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)"
5.43 +by comm_ring
5.44 +
5.45 +lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)"
5.46 +by comm_ring
5.47 +
5.48 +lemma "(a::int)^10 - b^10 = (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9 )"
5.49 +by comm_ring
5.50 +
5.51 +end
6.1 --- a/src/HOL/IsaMakefile Fri Oct 30 01:32:06 2009 +0100
6.2 +++ b/src/HOL/IsaMakefile Fri Oct 30 13:59:49 2009 +0100
6.3 @@ -248,12 +248,12 @@
6.4 Groebner_Basis.thy \
6.5 Hilbert_Choice.thy \
6.6 Int.thy \
6.7 - IntDiv.thy \
6.8 List.thy \
6.9 Main.thy \
6.10 Map.thy \
6.11 Nat_Numeral.thy \
6.12 Nat_Transfer.thy \
6.13 + Numeral_Simprocs.thy \
6.14 Presburger.thy \
6.15 Predicate_Compile.thy \
6.16 Quickcheck.thy \
6.17 @@ -382,7 +382,6 @@
6.18 Library/While_Combinator.thy Library/Product_ord.thy \
6.19 Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \
6.20 Library/Sublist_Order.thy Library/List_lexord.thy \
6.21 - Library/Commutative_Ring.thy Library/comm_ring.ML \
6.22 Library/Coinductive_List.thy Library/AssocList.thy \
6.23 Library/Formal_Power_Series.thy Library/Binomial.thy \
6.24 Library/Eval_Witness.thy Library/Code_Char.thy \
6.25 @@ -785,6 +784,9 @@
6.26
6.27 $(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
6.28 Decision_Procs/Approximation.thy \
6.29 + Decision_Procs/Commutative_Ring.thy \
6.30 + Decision_Procs/Commutative_Ring_Complete.thy \
6.31 + Decision_Procs/commutative_ring_tac.ML \
6.32 Decision_Procs/Cooper.thy \
6.33 Decision_Procs/cooper_tac.ML \
6.34 Decision_Procs/Dense_Linear_Order.thy \
6.35 @@ -795,6 +797,7 @@
6.36 Decision_Procs/Decision_Procs.thy \
6.37 Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
6.38 Decision_Procs/ex/Approximation_Ex.thy \
6.39 + Decision_Procs/ex/Commutative_Ring_Ex.thy \
6.40 Decision_Procs/ROOT.ML
6.41 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
6.42
6.43 @@ -937,7 +940,7 @@
6.44
6.45 HOL-ex: HOL $(LOG)/HOL-ex.gz
6.46
6.47 -$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
6.48 +$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
6.49 Number_Theory/Primes.thy \
6.50 Tools/Predicate_Compile/predicate_compile_core.ML \
6.51 ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
6.52 @@ -945,8 +948,8 @@
6.53 ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
6.54 ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \
6.55 ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \
6.56 - ex/Codegenerator_Test.thy ex/Coherent.thy ex/Commutative_RingEx.thy \
6.57 - ex/Commutative_Ring_Complete.thy ex/Efficient_Nat_examples.thy \
6.58 + ex/Codegenerator_Test.thy ex/Coherent.thy \
6.59 + ex/Efficient_Nat_examples.thy \
6.60 ex/Eval_Examples.thy ex/Fundefs.thy ex/Groebner_Examples.thy \
6.61 ex/Guess.thy ex/HarmonicSeries.thy ex/Hebrew.thy \
6.62 ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
7.1 --- a/src/HOL/Library/Commutative_Ring.thy Fri Oct 30 01:32:06 2009 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,319 +0,0 @@
7.4 -(* Author: Bernhard Haeupler
7.5 -
7.6 -Proving equalities in commutative rings done "right" in Isabelle/HOL.
7.7 -*)
7.8 -
7.9 -header {* Proving equalities in commutative rings *}
7.10 -
7.11 -theory Commutative_Ring
7.12 -imports List Parity Main
7.13 -uses ("comm_ring.ML")
7.14 -begin
7.15 -
7.16 -text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
7.17 -
7.18 -datatype 'a pol =
7.19 - Pc 'a
7.20 - | Pinj nat "'a pol"
7.21 - | PX "'a pol" nat "'a pol"
7.22 -
7.23 -datatype 'a polex =
7.24 - Pol "'a pol"
7.25 - | Add "'a polex" "'a polex"
7.26 - | Sub "'a polex" "'a polex"
7.27 - | Mul "'a polex" "'a polex"
7.28 - | Pow "'a polex" nat
7.29 - | Neg "'a polex"
7.30 -
7.31 -text {* Interpretation functions for the shadow syntax. *}
7.32 -
7.33 -primrec
7.34 - Ipol :: "'a::{comm_ring_1} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
7.35 -where
7.36 - "Ipol l (Pc c) = c"
7.37 - | "Ipol l (Pinj i P) = Ipol (drop i l) P"
7.38 - | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
7.39 -
7.40 -primrec
7.41 - Ipolex :: "'a::{comm_ring_1} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
7.42 -where
7.43 - "Ipolex l (Pol P) = Ipol l P"
7.44 - | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
7.45 - | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
7.46 - | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
7.47 - | "Ipolex l (Pow p n) = Ipolex l p ^ n"
7.48 - | "Ipolex l (Neg P) = - Ipolex l P"
7.49 -
7.50 -text {* Create polynomial normalized polynomials given normalized inputs. *}
7.51 -
7.52 -definition
7.53 - mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
7.54 - "mkPinj x P = (case P of
7.55 - Pc c \<Rightarrow> Pc c |
7.56 - Pinj y P \<Rightarrow> Pinj (x + y) P |
7.57 - PX p1 y p2 \<Rightarrow> Pinj x P)"
7.58 -
7.59 -definition
7.60 - mkPX :: "'a::{comm_ring} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
7.61 - "mkPX P i Q = (case P of
7.62 - Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
7.63 - Pinj j R \<Rightarrow> PX P i Q |
7.64 - PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
7.65 -
7.66 -text {* Defining the basic ring operations on normalized polynomials *}
7.67 -
7.68 -function
7.69 - add :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65)
7.70 -where
7.71 - "Pc a \<oplus> Pc b = Pc (a + b)"
7.72 - | "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
7.73 - | "Pinj i P \<oplus> Pc c = Pinj i (P \<oplus> Pc c)"
7.74 - | "Pc c \<oplus> PX P i Q = PX P i (Q \<oplus> Pc c)"
7.75 - | "PX P i Q \<oplus> Pc c = PX P i (Q \<oplus> Pc c)"
7.76 - | "Pinj x P \<oplus> Pinj y Q =
7.77 - (if x = y then mkPinj x (P \<oplus> Q)
7.78 - else (if x > y then mkPinj y (Pinj (x - y) P \<oplus> Q)
7.79 - else mkPinj x (Pinj (y - x) Q \<oplus> P)))"
7.80 - | "Pinj x P \<oplus> PX Q y R =
7.81 - (if x = 0 then P \<oplus> PX Q y R
7.82 - else (if x = 1 then PX Q y (R \<oplus> P)
7.83 - else PX Q y (R \<oplus> Pinj (x - 1) P)))"
7.84 - | "PX P x R \<oplus> Pinj y Q =
7.85 - (if y = 0 then PX P x R \<oplus> Q
7.86 - else (if y = 1 then PX P x (R \<oplus> Q)
7.87 - else PX P x (R \<oplus> Pinj (y - 1) Q)))"
7.88 - | "PX P1 x P2 \<oplus> PX Q1 y Q2 =
7.89 - (if x = y then mkPX (P1 \<oplus> Q1) x (P2 \<oplus> Q2)
7.90 - else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<oplus> Q1) y (P2 \<oplus> Q2)
7.91 - else mkPX (PX Q1 (y-x) (Pc 0) \<oplus> P1) x (P2 \<oplus> Q2)))"
7.92 -by pat_completeness auto
7.93 -termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
7.94 -
7.95 -function
7.96 - mul :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<otimes>" 70)
7.97 -where
7.98 - "Pc a \<otimes> Pc b = Pc (a * b)"
7.99 - | "Pc c \<otimes> Pinj i P =
7.100 - (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
7.101 - | "Pinj i P \<otimes> Pc c =
7.102 - (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
7.103 - | "Pc c \<otimes> PX P i Q =
7.104 - (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
7.105 - | "PX P i Q \<otimes> Pc c =
7.106 - (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
7.107 - | "Pinj x P \<otimes> Pinj y Q =
7.108 - (if x = y then mkPinj x (P \<otimes> Q) else
7.109 - (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q)
7.110 - else mkPinj x (Pinj (y - x) Q \<otimes> P)))"
7.111 - | "Pinj x P \<otimes> PX Q y R =
7.112 - (if x = 0 then P \<otimes> PX Q y R else
7.113 - (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P)
7.114 - else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))"
7.115 - | "PX P x R \<otimes> Pinj y Q =
7.116 - (if y = 0 then PX P x R \<otimes> Q else
7.117 - (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q)
7.118 - else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))"
7.119 - | "PX P1 x P2 \<otimes> PX Q1 y Q2 =
7.120 - mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus>
7.121 - (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus>
7.122 - (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))"
7.123 -by pat_completeness auto
7.124 -termination by (relation "measure (\<lambda>(x, y). size x + size y)")
7.125 - (auto simp add: mkPinj_def split: pol.split)
7.126 -
7.127 -text {* Negation*}
7.128 -primrec
7.129 - neg :: "'a::{comm_ring} pol \<Rightarrow> 'a pol"
7.130 -where
7.131 - "neg (Pc c) = Pc (-c)"
7.132 - | "neg (Pinj i P) = Pinj i (neg P)"
7.133 - | "neg (PX P x Q) = PX (neg P) x (neg Q)"
7.134 -
7.135 -text {* Substraction *}
7.136 -definition
7.137 - sub :: "'a::{comm_ring} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<ominus>" 65)
7.138 -where
7.139 - "sub P Q = P \<oplus> neg Q"
7.140 -
7.141 -text {* Square for Fast Exponentation *}
7.142 -primrec
7.143 - sqr :: "'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
7.144 -where
7.145 - "sqr (Pc c) = Pc (c * c)"
7.146 - | "sqr (Pinj i P) = mkPinj i (sqr P)"
7.147 - | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<oplus>
7.148 - mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
7.149 -
7.150 -text {* Fast Exponentation *}
7.151 -fun
7.152 - pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
7.153 -where
7.154 - "pow 0 P = Pc 1"
7.155 - | "pow n P = (if even n then pow (n div 2) (sqr P)
7.156 - else P \<otimes> pow (n div 2) (sqr P))"
7.157 -
7.158 -lemma pow_if:
7.159 - "pow n P =
7.160 - (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
7.161 - else P \<otimes> pow (n div 2) (sqr P))"
7.162 - by (cases n) simp_all
7.163 -
7.164 -
7.165 -text {* Normalization of polynomial expressions *}
7.166 -
7.167 -primrec
7.168 - norm :: "'a::{comm_ring_1} polex \<Rightarrow> 'a pol"
7.169 -where
7.170 - "norm (Pol P) = P"
7.171 - | "norm (Add P Q) = norm P \<oplus> norm Q"
7.172 - | "norm (Sub P Q) = norm P \<ominus> norm Q"
7.173 - | "norm (Mul P Q) = norm P \<otimes> norm Q"
7.174 - | "norm (Pow P n) = pow n (norm P)"
7.175 - | "norm (Neg P) = neg (norm P)"
7.176 -
7.177 -text {* mkPinj preserve semantics *}
7.178 -lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
7.179 - by (induct B) (auto simp add: mkPinj_def algebra_simps)
7.180 -
7.181 -text {* mkPX preserves semantics *}
7.182 -lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
7.183 - by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
7.184 -
7.185 -text {* Correctness theorems for the implemented operations *}
7.186 -
7.187 -text {* Negation *}
7.188 -lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
7.189 - by (induct P arbitrary: l) auto
7.190 -
7.191 -text {* Addition *}
7.192 -lemma add_ci: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
7.193 -proof (induct P Q arbitrary: l rule: add.induct)
7.194 - case (6 x P y Q)
7.195 - show ?case
7.196 - proof (rule linorder_cases)
7.197 - assume "x < y"
7.198 - with 6 show ?case by (simp add: mkPinj_ci algebra_simps)
7.199 - next
7.200 - assume "x = y"
7.201 - with 6 show ?case by (simp add: mkPinj_ci)
7.202 - next
7.203 - assume "x > y"
7.204 - with 6 show ?case by (simp add: mkPinj_ci algebra_simps)
7.205 - qed
7.206 -next
7.207 - case (7 x P Q y R)
7.208 - have "x = 0 \<or> x = 1 \<or> x > 1" by arith
7.209 - moreover
7.210 - { assume "x = 0" with 7 have ?case by simp }
7.211 - moreover
7.212 - { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) }
7.213 - moreover
7.214 - { assume "x > 1" from 7 have ?case by (cases x) simp_all }
7.215 - ultimately show ?case by blast
7.216 -next
7.217 - case (8 P x R y Q)
7.218 - have "y = 0 \<or> y = 1 \<or> y > 1" by arith
7.219 - moreover
7.220 - { assume "y = 0" with 8 have ?case by simp }
7.221 - moreover
7.222 - { assume "y = 1" with 8 have ?case by simp }
7.223 - moreover
7.224 - { assume "y > 1" with 8 have ?case by simp }
7.225 - ultimately show ?case by blast
7.226 -next
7.227 - case (9 P1 x P2 Q1 y Q2)
7.228 - show ?case
7.229 - proof (rule linorder_cases)
7.230 - assume a: "x < y" hence "EX d. d + x = y" by arith
7.231 - with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps)
7.232 - next
7.233 - assume a: "y < x" hence "EX d. d + y = x" by arith
7.234 - with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps)
7.235 - next
7.236 - assume "x = y"
7.237 - with 9 show ?case by (simp add: mkPX_ci algebra_simps)
7.238 - qed
7.239 -qed (auto simp add: algebra_simps)
7.240 -
7.241 -text {* Multiplication *}
7.242 -lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
7.243 - by (induct P Q arbitrary: l rule: mul.induct)
7.244 - (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add)
7.245 -
7.246 -text {* Substraction *}
7.247 -lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
7.248 - by (simp add: add_ci neg_ci sub_def)
7.249 -
7.250 -text {* Square *}
7.251 -lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
7.252 - by (induct P arbitrary: ls)
7.253 - (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
7.254 -
7.255 -text {* Power *}
7.256 -lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
7.257 - by (induct n) simp_all
7.258 -
7.259 -lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
7.260 -proof (induct n arbitrary: P rule: nat_less_induct)
7.261 - case (1 k)
7.262 - show ?case
7.263 - proof (cases k)
7.264 - case 0
7.265 - then show ?thesis by simp
7.266 - next
7.267 - case (Suc l)
7.268 - show ?thesis
7.269 - proof cases
7.270 - assume "even l"
7.271 - then have "Suc l div 2 = l div 2"
7.272 - by (simp add: nat_number even_nat_plus_one_div_two)
7.273 - moreover
7.274 - from Suc have "l < k" by simp
7.275 - with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
7.276 - moreover
7.277 - note Suc `even l` even_nat_plus_one_div_two
7.278 - ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow)
7.279 - next
7.280 - assume "odd l"
7.281 - {
7.282 - fix p
7.283 - have "Ipol ls (sqr P) ^ (Suc l div 2) = Ipol ls P ^ Suc l"
7.284 - proof (cases l)
7.285 - case 0
7.286 - with `odd l` show ?thesis by simp
7.287 - next
7.288 - case (Suc w)
7.289 - with `odd l` have "even w" by simp
7.290 - have two_times: "2 * (w div 2) = w"
7.291 - by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
7.292 - have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
7.293 - by (simp add: power_Suc)
7.294 - then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
7.295 - by (simp add: numerals)
7.296 - with Suc show ?thesis
7.297 - by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
7.298 - simp del: power_Suc)
7.299 - qed
7.300 - } with 1 Suc `odd l` show ?thesis by simp
7.301 - qed
7.302 - qed
7.303 -qed
7.304 -
7.305 -text {* Normalization preserves semantics *}
7.306 -lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
7.307 - by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
7.308 -
7.309 -text {* Reflection lemma: Key to the (incomplete) decision procedure *}
7.310 -lemma norm_eq:
7.311 - assumes "norm P1 = norm P2"
7.312 - shows "Ipolex l P1 = Ipolex l P2"
7.313 -proof -
7.314 - from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
7.315 - then show ?thesis by (simp only: norm_ci)
7.316 -qed
7.317 -
7.318 -
7.319 -use "comm_ring.ML"
7.320 -setup CommRing.setup
7.321 -
7.322 -end
8.1 --- a/src/HOL/Library/Library.thy Fri Oct 30 01:32:06 2009 +0100
8.2 +++ b/src/HOL/Library/Library.thy Fri Oct 30 13:59:49 2009 +0100
8.3 @@ -11,7 +11,6 @@
8.4 Code_Char_chr
8.5 Code_Integer
8.6 Coinductive_List
8.7 - Commutative_Ring
8.8 Continuity
8.9 ContNotDenum
8.10 Countable
9.1 --- a/src/HOL/Library/comm_ring.ML Fri Oct 30 01:32:06 2009 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,109 +0,0 @@
9.4 -(* Author: Amine Chaieb
9.5 -
9.6 -Tactic for solving equalities over commutative rings.
9.7 -*)
9.8 -
9.9 -signature COMM_RING =
9.10 -sig
9.11 - val comm_ring_tac : Proof.context -> int -> tactic
9.12 - val setup : theory -> theory
9.13 -end
9.14 -
9.15 -structure CommRing: COMM_RING =
9.16 -struct
9.17 -
9.18 -(* The Cring exception for erronous uses of cring_tac *)
9.19 -exception CRing of string;
9.20 -
9.21 -(* Zero and One of the commutative ring *)
9.22 -fun cring_zero T = Const (@{const_name HOL.zero}, T);
9.23 -fun cring_one T = Const (@{const_name HOL.one}, T);
9.24 -
9.25 -(* reification functions *)
9.26 -(* add two polynom expressions *)
9.27 -fun polT t = Type ("Commutative_Ring.pol", [t]);
9.28 -fun polexT t = Type ("Commutative_Ring.polex", [t]);
9.29 -
9.30 -(* pol *)
9.31 -fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
9.32 -fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
9.33 -fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
9.34 -
9.35 -(* polex *)
9.36 -fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
9.37 -fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
9.38 -fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
9.39 -fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
9.40 -fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
9.41 -fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);
9.42 -
9.43 -(* reification of polynoms : primitive cring expressions *)
9.44 -fun reif_pol T vs (t as Free _) =
9.45 - let
9.46 - val one = @{term "1::nat"};
9.47 - val i = find_index (fn t' => t' = t) vs
9.48 - in if i = 0
9.49 - then pol_PX T $ (pol_Pc T $ cring_one T)
9.50 - $ one $ (pol_Pc T $ cring_zero T)
9.51 - else pol_Pinj T $ HOLogic.mk_nat i
9.52 - $ (pol_PX T $ (pol_Pc T $ cring_one T)
9.53 - $ one $ (pol_Pc T $ cring_zero T))
9.54 - end
9.55 - | reif_pol T vs t = pol_Pc T $ t;
9.56 -
9.57 -(* reification of polynom expressions *)
9.58 -fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
9.59 - polex_add T $ reif_polex T vs a $ reif_polex T vs b
9.60 - | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
9.61 - polex_sub T $ reif_polex T vs a $ reif_polex T vs b
9.62 - | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
9.63 - polex_mul T $ reif_polex T vs a $ reif_polex T vs b
9.64 - | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
9.65 - polex_neg T $ reif_polex T vs a
9.66 - | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
9.67 - polex_pow T $ reif_polex T vs a $ n
9.68 - | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
9.69 -
9.70 -(* reification of the equation *)
9.71 -val cr_sort = @{sort "comm_ring_1"};
9.72 -
9.73 -fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
9.74 - if Sign.of_sort thy (T, cr_sort) then
9.75 - let
9.76 - val fs = OldTerm.term_frees eq;
9.77 - val cvs = cterm_of thy (HOLogic.mk_list T fs);
9.78 - val clhs = cterm_of thy (reif_polex T fs lhs);
9.79 - val crhs = cterm_of thy (reif_polex T fs rhs);
9.80 - val ca = ctyp_of thy T;
9.81 - in (ca, cvs, clhs, crhs) end
9.82 - else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
9.83 - | reif_eq _ _ = raise CRing "reif_eq: not an equation";
9.84 -
9.85 -(* The cring tactic *)
9.86 -(* Attention: You have to make sure that no t^0 is in the goal!! *)
9.87 -(* Use simply rewriting t^0 = 1 *)
9.88 -val cring_simps =
9.89 - [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
9.90 - @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
9.91 -
9.92 -fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
9.93 - let
9.94 - val thy = ProofContext.theory_of ctxt;
9.95 - val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*)
9.96 - addsimps cring_simps;
9.97 - val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
9.98 - val norm_eq_th =
9.99 - simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
9.100 - in
9.101 - cut_rules_tac [norm_eq_th] i
9.102 - THEN (simp_tac cring_ss i)
9.103 - THEN (simp_tac cring_ss i)
9.104 - end);
9.105 -
9.106 -val setup =
9.107 - Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
9.108 - "reflective decision procedure for equalities over commutative rings" #>
9.109 - Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
9.110 - "method for proving algebraic properties (same as comm_ring)";
9.111 -
9.112 -end;
10.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Fri Oct 30 01:32:06 2009 +0100
10.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Fri Oct 30 13:59:49 2009 +0100
10.3 @@ -9,7 +9,6 @@
10.4 AssocList
10.5 Binomial
10.6 Fset
10.7 - Commutative_Ring
10.8 Enum
10.9 List_Prefix
10.10 Nat_Infinity
10.11 @@ -22,7 +21,7 @@
10.12 Tree
10.13 While_Combinator
10.14 Word
10.15 - "~~/src/HOL/ex/Commutative_Ring_Complete"
10.16 + "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
10.17 "~~/src/HOL/ex/Records"
10.18 begin
10.19
11.1 --- a/src/HOL/ex/Commutative_RingEx.thy Fri Oct 30 01:32:06 2009 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,50 +0,0 @@
11.4 -(* ID: $Id$
11.5 - Author: Bernhard Haeupler
11.6 -*)
11.7 -
11.8 -header {* Some examples demonstrating the comm-ring method *}
11.9 -
11.10 -theory Commutative_RingEx
11.11 -imports Commutative_Ring
11.12 -begin
11.13 -
11.14 -lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
11.15 -by comm_ring
11.16 -
11.17 -lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y"
11.18 -by comm_ring
11.19 -
11.20 -lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x"
11.21 -by comm_ring
11.22 -
11.23 -lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3"
11.24 -by comm_ring
11.25 -
11.26 -lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y"
11.27 -by comm_ring
11.28 -
11.29 -lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c"
11.30 -by comm_ring
11.31 -
11.32 -lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c"
11.33 -by comm_ring
11.34 -
11.35 -lemma "(a::int)*b + a*c = a*(b+c)"
11.36 -by comm_ring
11.37 -
11.38 -lemma "(a::int)^2 - b^2 = (a - b) * (a + b)"
11.39 -by comm_ring
11.40 -
11.41 -lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)"
11.42 -by comm_ring
11.43 -
11.44 -lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)"
11.45 -by comm_ring
11.46 -
11.47 -lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)"
11.48 -by comm_ring
11.49 -
11.50 -lemma "(a::int)^10 - b^10 = (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9 )"
11.51 -by comm_ring
11.52 -
11.53 -end
12.1 --- a/src/HOL/ex/Commutative_Ring_Complete.thy Fri Oct 30 01:32:06 2009 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,391 +0,0 @@
12.4 -(* Author: Bernhard Haeupler
12.5 -
12.6 -This theory is about of the relative completeness of method comm-ring
12.7 -method. As long as the reified atomic polynomials of type 'a pol are
12.8 -in normal form, the cring method is complete.
12.9 -*)
12.10 -
12.11 -header {* Proof of the relative completeness of method comm-ring *}
12.12 -
12.13 -theory Commutative_Ring_Complete
12.14 -imports Commutative_Ring
12.15 -begin
12.16 -
12.17 -text {* Formalization of normal form *}
12.18 -fun
12.19 - isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
12.20 -where
12.21 - "isnorm (Pc c) \<longleftrightarrow> True"
12.22 - | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
12.23 - | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"
12.24 - | "isnorm (Pinj 0 P) \<longleftrightarrow> False"
12.25 - | "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"
12.26 - | "isnorm (PX P 0 Q) \<longleftrightarrow> False"
12.27 - | "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"
12.28 - | "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"
12.29 - | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
12.30 -
12.31 -(* Some helpful lemmas *)
12.32 -lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
12.33 -by(cases P, auto)
12.34 -
12.35 -lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
12.36 -by(cases i, auto)
12.37 -
12.38 -lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
12.39 -by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
12.40 -
12.41 -lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
12.42 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
12.43 -
12.44 -lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
12.45 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
12.46 -
12.47 -lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)"
12.48 -apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
12.49 -apply(case_tac nat, auto simp add: norm_Pinj_0_False)
12.50 -by(case_tac pol, auto) (case_tac y, auto)
12.51 -
12.52 -lemma norm_PXtrans:
12.53 - assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
12.54 - shows "isnorm (PX P x Q2)"
12.55 -proof(cases P)
12.56 - case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
12.57 -next
12.58 - case Pc from prems show ?thesis by(cases x, auto)
12.59 -next
12.60 - case Pinj from prems show ?thesis by(cases x, auto)
12.61 -qed
12.62 -
12.63 -lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)"
12.64 -proof(cases P)
12.65 - case (PX p1 y p2)
12.66 - from prems show ?thesis by(cases x, auto, cases p2, auto)
12.67 -next
12.68 - case Pc
12.69 - from prems show ?thesis by(cases x, auto)
12.70 -next
12.71 - case Pinj
12.72 - from prems show ?thesis by(cases x, auto)
12.73 -qed
12.74 -
12.75 -text {* mkPX conserves normalizedness (@{text "_cn"}) *}
12.76 -lemma mkPX_cn:
12.77 - assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q"
12.78 - shows "isnorm (mkPX P x Q)"
12.79 -proof(cases P)
12.80 - case (Pc c)
12.81 - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
12.82 -next
12.83 - case (Pinj i Q)
12.84 - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
12.85 -next
12.86 - case (PX P1 y P2)
12.87 - from prems have Y0:"y>0" by(cases y, auto)
12.88 - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
12.89 - with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
12.90 -qed
12.91 -
12.92 -text {* add conserves normalizedness *}
12.93 -lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
12.94 -proof(induct P Q rule: add.induct)
12.95 - case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
12.96 -next
12.97 - case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
12.98 -next
12.99 - case (4 c P2 i Q2)
12.100 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
12.101 - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
12.102 -next
12.103 - case (5 P2 i Q2 c)
12.104 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
12.105 - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
12.106 -next
12.107 - case (6 x P2 y Q2)
12.108 - from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False)
12.109 - from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False)
12.110 - have "x < y \<or> x = y \<or> x > y" by arith
12.111 - moreover
12.112 - { assume "x<y" hence "EX d. y=d+x" by arith
12.113 - then obtain d where "y=d+x"..
12.114 - moreover
12.115 - note prems X0
12.116 - moreover
12.117 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
12.118 - moreover
12.119 - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
12.120 - ultimately have ?case by (simp add: mkPinj_cn)}
12.121 - moreover
12.122 - { assume "x=y"
12.123 - moreover
12.124 - from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
12.125 - moreover
12.126 - note prems Y0
12.127 - moreover
12.128 - ultimately have ?case by (simp add: mkPinj_cn) }
12.129 - moreover
12.130 - { assume "x>y" hence "EX d. x=d+y" by arith
12.131 - then obtain d where "x=d+y"..
12.132 - moreover
12.133 - note prems Y0
12.134 - moreover
12.135 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
12.136 - moreover
12.137 - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
12.138 - ultimately have ?case by (simp add: mkPinj_cn)}
12.139 - ultimately show ?case by blast
12.140 -next
12.141 - case (7 x P2 Q2 y R)
12.142 - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
12.143 - moreover
12.144 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
12.145 - moreover
12.146 - { assume "x=1"
12.147 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
12.148 - with prems have "isnorm (R \<oplus> P2)" by simp
12.149 - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
12.150 - moreover
12.151 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
12.152 - then obtain d where X:"x=Suc (Suc d)" ..
12.153 - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
12.154 - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
12.155 - with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
12.156 - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
12.157 - ultimately show ?case by blast
12.158 -next
12.159 - case (8 Q2 y R x P2)
12.160 - have "x = 0 \<or> x = 1 \<or> x > 1" by arith
12.161 - moreover
12.162 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
12.163 - moreover
12.164 - { assume "x=1"
12.165 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
12.166 - with prems have "isnorm (R \<oplus> P2)" by simp
12.167 - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
12.168 - moreover
12.169 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
12.170 - then obtain d where X:"x=Suc (Suc d)" ..
12.171 - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
12.172 - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
12.173 - with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
12.174 - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
12.175 - ultimately show ?case by blast
12.176 -next
12.177 - case (9 P1 x P2 Q1 y Q2)
12.178 - from prems have Y0:"y>0" by(cases y, auto)
12.179 - from prems have X0:"x>0" by(cases x, auto)
12.180 - from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
12.181 - from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
12.182 - have "y < x \<or> x = y \<or> x < y" by arith
12.183 - moreover
12.184 - {assume sm1:"y < x" hence "EX d. x=d+y" by arith
12.185 - then obtain d where sm2:"x=d+y"..
12.186 - note prems NQ1 NP1 NP2 NQ2 sm1 sm2
12.187 - moreover
12.188 - have "isnorm (PX P1 d (Pc 0))"
12.189 - proof(cases P1)
12.190 - case (PX p1 y p2)
12.191 - with prems show ?thesis by(cases d, simp,cases p2, auto)
12.192 - next case Pc from prems show ?thesis by(cases d, auto)
12.193 - next case Pinj from prems show ?thesis by(cases d, auto)
12.194 - qed
12.195 - ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
12.196 - with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
12.197 - moreover
12.198 - {assume "x=y"
12.199 - from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
12.200 - with Y0 prems have ?case by (simp add: mkPX_cn) }
12.201 - moreover
12.202 - {assume sm1:"x<y" hence "EX d. y=d+x" by arith
12.203 - then obtain d where sm2:"y=d+x"..
12.204 - note prems NQ1 NP1 NP2 NQ2 sm1 sm2
12.205 - moreover
12.206 - have "isnorm (PX Q1 d (Pc 0))"
12.207 - proof(cases Q1)
12.208 - case (PX p1 y p2)
12.209 - with prems show ?thesis by(cases d, simp,cases p2, auto)
12.210 - next case Pc from prems show ?thesis by(cases d, auto)
12.211 - next case Pinj from prems show ?thesis by(cases d, auto)
12.212 - qed
12.213 - ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
12.214 - with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
12.215 - ultimately show ?case by blast
12.216 -qed simp
12.217 -
12.218 -text {* mul concerves normalizedness *}
12.219 -lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
12.220 -proof(induct P Q rule: mul.induct)
12.221 - case (2 c i P2) thus ?case
12.222 - by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
12.223 -next
12.224 - case (3 i P2 c) thus ?case
12.225 - by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
12.226 -next
12.227 - case (4 c P2 i Q2)
12.228 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
12.229 - with prems show ?case
12.230 - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
12.231 -next
12.232 - case (5 P2 i Q2 c)
12.233 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
12.234 - with prems show ?case
12.235 - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
12.236 -next
12.237 - case (6 x P2 y Q2)
12.238 - have "x < y \<or> x = y \<or> x > y" by arith
12.239 - moreover
12.240 - { assume "x<y" hence "EX d. y=d+x" by arith
12.241 - then obtain d where "y=d+x"..
12.242 - moreover
12.243 - note prems
12.244 - moreover
12.245 - from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False)
12.246 - moreover
12.247 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
12.248 - moreover
12.249 - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
12.250 - ultimately have ?case by (simp add: mkPinj_cn)}
12.251 - moreover
12.252 - { assume "x=y"
12.253 - moreover
12.254 - from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
12.255 - moreover
12.256 - with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
12.257 - moreover
12.258 - note prems
12.259 - moreover
12.260 - ultimately have ?case by (simp add: mkPinj_cn) }
12.261 - moreover
12.262 - { assume "x>y" hence "EX d. x=d+y" by arith
12.263 - then obtain d where "x=d+y"..
12.264 - moreover
12.265 - note prems
12.266 - moreover
12.267 - from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
12.268 - moreover
12.269 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
12.270 - moreover
12.271 - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
12.272 - ultimately have ?case by (simp add: mkPinj_cn) }
12.273 - ultimately show ?case by blast
12.274 -next
12.275 - case (7 x P2 Q2 y R)
12.276 - from prems have Y0:"y>0" by(cases y, auto)
12.277 - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
12.278 - moreover
12.279 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
12.280 - moreover
12.281 - { assume "x=1"
12.282 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
12.283 - with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
12.284 - with Y0 prems have ?case by (simp add: mkPX_cn)}
12.285 - moreover
12.286 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
12.287 - then obtain d where X:"x=Suc (Suc d)" ..
12.288 - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
12.289 - moreover
12.290 - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
12.291 - moreover
12.292 - from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
12.293 - moreover
12.294 - note prems
12.295 - ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
12.296 - with Y0 X have ?case by (simp add: mkPX_cn)}
12.297 - ultimately show ?case by blast
12.298 -next
12.299 - case (8 Q2 y R x P2)
12.300 - from prems have Y0:"y>0" by(cases y, auto)
12.301 - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
12.302 - moreover
12.303 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
12.304 - moreover
12.305 - { assume "x=1"
12.306 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
12.307 - with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
12.308 - with Y0 prems have ?case by (simp add: mkPX_cn) }
12.309 - moreover
12.310 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
12.311 - then obtain d where X:"x=Suc (Suc d)" ..
12.312 - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
12.313 - moreover
12.314 - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
12.315 - moreover
12.316 - from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
12.317 - moreover
12.318 - note prems
12.319 - ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
12.320 - with Y0 X have ?case by (simp add: mkPX_cn) }
12.321 - ultimately show ?case by blast
12.322 -next
12.323 - case (9 P1 x P2 Q1 y Q2)
12.324 - from prems have X0:"x>0" by(cases x, auto)
12.325 - from prems have Y0:"y>0" by(cases y, auto)
12.326 - note prems
12.327 - moreover
12.328 - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
12.329 - moreover
12.330 - from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
12.331 - ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
12.332 - "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
12.333 - by (auto simp add: mkPinj_cn)
12.334 - with prems X0 Y0 have
12.335 - "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
12.336 - "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
12.337 - "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
12.338 - by (auto simp add: mkPX_cn)
12.339 - thus ?case by (simp add: add_cn)
12.340 -qed(simp)
12.341 -
12.342 -text {* neg conserves normalizedness *}
12.343 -lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
12.344 -proof (induct P)
12.345 - case (Pinj i P2)
12.346 - from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
12.347 - with prems show ?case by(cases P2, auto, cases i, auto)
12.348 -next
12.349 - case (PX P1 x P2)
12.350 - from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
12.351 - with prems show ?case
12.352 - proof(cases P1)
12.353 - case (PX p1 y p2)
12.354 - with prems show ?thesis by(cases x, auto, cases p2, auto)
12.355 - next
12.356 - case Pinj
12.357 - with prems show ?thesis by(cases x, auto)
12.358 - qed(cases x, auto)
12.359 -qed(simp)
12.360 -
12.361 -text {* sub conserves normalizedness *}
12.362 -lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
12.363 -by (simp add: sub_def add_cn neg_cn)
12.364 -
12.365 -text {* sqr conserves normalizizedness *}
12.366 -lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
12.367 -proof(induct P)
12.368 - case (Pinj i Q)
12.369 - from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
12.370 -next
12.371 - case (PX P1 x P2)
12.372 - from prems have "x+x~=0" "isnorm P2" "isnorm P1" by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
12.373 - with prems have
12.374 - "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
12.375 - and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
12.376 - by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
12.377 - thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
12.378 -qed simp
12.379 -
12.380 -text {* pow conserves normalizedness *}
12.381 -lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)"
12.382 -proof (induct n arbitrary: P rule: nat_less_induct)
12.383 - case (1 k)
12.384 - show ?case
12.385 - proof (cases "k=0")
12.386 - case False
12.387 - then have K2:"k div 2 < k" by (cases k, auto)
12.388 - from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
12.389 - with prems K2 show ?thesis
12.390 - by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
12.391 - qed simp
12.392 -qed
12.393 -
12.394 -end
13.1 --- a/src/HOL/ex/ROOT.ML Fri Oct 30 01:32:06 2009 +0100
13.2 +++ b/src/HOL/ex/ROOT.ML Fri Oct 30 13:59:49 2009 +0100
13.3 @@ -45,8 +45,6 @@
13.4 "Groebner_Examples",
13.5 "MT",
13.6 "Unification",
13.7 - "Commutative_RingEx",
13.8 - "Commutative_Ring_Complete",
13.9 "Primrec",
13.10 "Tarski",
13.11 "Adder",