moved Commutative_Ring into session Decision_Procs
authorhaftmann
Fri Oct 30 13:59:49 2009 +0100 (2009-10-30)
changeset 333569157d0f9f00e
parent 33351 37ec56ac3fd4
child 33357 2ca60fc13c5a
moved Commutative_Ring into session Decision_Procs
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Decision_Procs.thy
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
src/HOL/IsaMakefile
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Library.thy
src/HOL/Library/comm_ring.ML
src/HOL/ex/Codegenerator_Candidates.thy
src/HOL/ex/Commutative_RingEx.thy
src/HOL/ex/Commutative_Ring_Complete.thy
src/HOL/ex/ROOT.ML
     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",