added Commutative_Ring (from Main HOL);
authorwenzelm
Tue Sep 20 14:10:29 2005 +0200 (2005-09-20 ago)
changeset 1751645164074dad4
parent 17515 830bc15e692c
child 17517 9dc9d3005ed2
added Commutative_Ring (from Main HOL);
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Library.thy
src/HOL/Library/comm_ring.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Tue Sep 20 14:10:29 2005 +0200
     1.3 @@ -0,0 +1,327 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Bernhard Haeupler
     1.6 +
     1.7 +Proving equalities in commutative rings done "right" in Isabelle/HOL.
     1.8 +*)
     1.9 +
    1.10 +header {* Proving equalities in commutative rings *}
    1.11 +
    1.12 +theory Commutative_Ring
    1.13 +imports Main
    1.14 +uses ("comm_ring.ML")
    1.15 +begin
    1.16 +
    1.17 +text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
    1.18 +
    1.19 +datatype 'a pol =
    1.20 +    Pc 'a
    1.21 +  | Pinj nat "'a pol"
    1.22 +  | PX "'a pol" nat "'a pol"
    1.23 +
    1.24 +datatype 'a polex =
    1.25 +  Pol "'a pol"
    1.26 +  | Add "'a polex" "'a polex"
    1.27 +  | Sub "'a polex" "'a polex"
    1.28 +  | Mul "'a polex" "'a polex"
    1.29 +  | Pow "'a polex" nat
    1.30 +  | Neg "'a polex"
    1.31 +
    1.32 +text {* Interpretation functions for the shadow syntax. *}
    1.33 +
    1.34 +consts
    1.35 +  Ipol :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a pol \<Rightarrow> 'a"
    1.36 +  Ipolex :: "'a::{comm_ring,recpower} list \<Rightarrow> 'a polex \<Rightarrow> 'a"
    1.37 +
    1.38 +primrec
    1.39 +  "Ipol l (Pc c) = c"
    1.40 +  "Ipol l (Pinj i P) = Ipol (drop i l) P"
    1.41 +  "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
    1.42 +
    1.43 +primrec
    1.44 +  "Ipolex l (Pol P) = Ipol l P"
    1.45 +  "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
    1.46 +  "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
    1.47 +  "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
    1.48 +  "Ipolex l (Pow p n) = Ipolex l p ^ n"
    1.49 +  "Ipolex l (Neg P) = - Ipolex l P"
    1.50 +
    1.51 +text {* Create polynomial normalized polynomials given normalized inputs. *}
    1.52 +
    1.53 +constdefs
    1.54 +  mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
    1.55 +  "mkPinj x P \<equiv> (case P of
    1.56 +    Pc c \<Rightarrow> Pc c |
    1.57 +    Pinj y P \<Rightarrow> Pinj (x + y) P |
    1.58 +    PX p1 y p2 \<Rightarrow> Pinj x P)"
    1.59 +
    1.60 +constdefs
    1.61 +  mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
    1.62 +  "mkPX P i Q == (case P of
    1.63 +    Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
    1.64 +    Pinj j R \<Rightarrow> PX P i Q |
    1.65 +    PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
    1.66 +
    1.67 +text {* Defining the basic ring operations on normalized polynomials *}
    1.68 +
    1.69 +consts
    1.70 +  add :: "'a::{comm_ring,recpower} pol \<times> 'a pol \<Rightarrow> 'a pol"
    1.71 +  mul :: "'a::{comm_ring,recpower} pol \<times> 'a pol \<Rightarrow> 'a pol"
    1.72 +  neg :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
    1.73 +  sqr :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol"
    1.74 +  pow :: "'a::{comm_ring,recpower} pol \<times> nat \<Rightarrow> 'a pol"
    1.75 +
    1.76 +text {* Addition *}
    1.77 +recdef add "measure (\<lambda>(x, y). size x + size y)"
    1.78 +  "add (Pc a, Pc b) = Pc (a + b)"
    1.79 +  "add (Pc c, Pinj i P) = Pinj i (add (P, Pc c))"
    1.80 +  "add (Pinj i P, Pc c) = Pinj i (add (P, Pc c))"
    1.81 +  "add (Pc c, PX P i Q) = PX P i (add (Q, Pc c))"
    1.82 +  "add (PX P i Q, Pc c) = PX P i (add (Q, Pc c))"
    1.83 +  "add (Pinj x P, Pinj y Q) =
    1.84 +  (if x=y then mkPinj x (add (P, Q))
    1.85 +   else (if x>y then mkPinj y (add (Pinj (x-y) P, Q))
    1.86 +         else mkPinj x (add (Pinj (y-x) Q, P)) ))"
    1.87 +  "add (Pinj x P, PX Q y R) =
    1.88 +  (if x=0 then add(P, PX Q y R)
    1.89 +   else (if x=1 then PX Q y (add (R, P))
    1.90 +         else PX Q y (add (R, Pinj (x - 1) P))))"
    1.91 +  "add (PX P x R, Pinj y Q) =
    1.92 +  (if y=0 then add(PX P x R, Q)
    1.93 +   else (if y=1 then PX P x (add (R, Q))
    1.94 +         else PX P x (add (R, Pinj (y - 1) Q))))"
    1.95 +  "add (PX P1 x P2, PX Q1 y Q2) =
    1.96 +  (if x=y then mkPX (add (P1, Q1)) x (add (P2, Q2))
    1.97 +  else (if x>y then mkPX (add (PX P1 (x-y) (Pc 0), Q1)) y (add (P2,Q2))
    1.98 +        else mkPX (add (PX Q1 (y-x) (Pc 0), P1)) x (add (P2,Q2)) ))"
    1.99 +
   1.100 +text {* Multiplication *}
   1.101 +recdef mul "measure (\<lambda>(x, y). size x + size y)"
   1.102 +  "mul (Pc a, Pc b) = Pc (a*b)"
   1.103 +  "mul (Pc c, Pinj i P) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"
   1.104 +  "mul (Pinj i P, Pc c) = (if c=0 then Pc 0 else mkPinj i (mul (P, Pc c)))"
   1.105 +  "mul (Pc c, PX P i Q) =
   1.106 +  (if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"
   1.107 +  "mul (PX P i Q, Pc c) =
   1.108 +  (if c=0 then Pc 0 else mkPX (mul (P, Pc c)) i (mul (Q, Pc c)))"
   1.109 +  "mul (Pinj x P, Pinj y Q) =
   1.110 +  (if x=y then mkPinj x (mul (P, Q))
   1.111 +   else (if x>y then mkPinj y (mul (Pinj (x-y) P, Q))
   1.112 +         else mkPinj x (mul (Pinj (y-x) Q, P)) ))"
   1.113 +  "mul (Pinj x P, PX Q y R) =
   1.114 +  (if x=0 then mul(P, PX Q y R)
   1.115 +   else (if x=1 then mkPX (mul (Pinj x P, Q)) y (mul (R, P))
   1.116 +         else mkPX (mul (Pinj x P, Q)) y (mul (R, Pinj (x - 1) P))))"
   1.117 +  "mul (PX P x R, Pinj y Q) =
   1.118 +  (if y=0 then mul(PX P x R, Q)
   1.119 +   else (if y=1 then mkPX (mul (Pinj y Q, P)) x (mul (R, Q))
   1.120 +         else mkPX (mul (Pinj y Q, P)) x (mul (R, Pinj (y - 1) Q))))"
   1.121 +  "mul (PX P1 x P2, PX Q1 y Q2) =
   1.122 +  add (mkPX (mul (P1, Q1)) (x+y) (mul (P2, Q2)),
   1.123 +  add (mkPX (mul (P1, mkPinj 1 Q2)) x (Pc 0), mkPX (mul (Q1, mkPinj 1 P2)) y (Pc 0)) )"
   1.124 +(hints simp add: mkPinj_def split: pol.split)
   1.125 +
   1.126 +text {* Negation*}
   1.127 +primrec
   1.128 +  "neg (Pc c) = Pc (-c)"
   1.129 +  "neg (Pinj i P) = Pinj i (neg P)"
   1.130 +  "neg (PX P x Q) = PX (neg P) x (neg Q)"
   1.131 +
   1.132 +text {* Substraction *}
   1.133 +constdefs
   1.134 +  sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
   1.135 +  "sub p q \<equiv> add (p, neg q)"
   1.136 +
   1.137 +text {* Square for Fast Exponentation *}
   1.138 +primrec
   1.139 +  "sqr (Pc c) = Pc (c * c)"
   1.140 +  "sqr (Pinj i P) = mkPinj i (sqr P)"
   1.141 +  "sqr (PX A x B) = add (mkPX (sqr A) (x + x) (sqr B),
   1.142 +    mkPX (mul (mul (Pc (1 + 1), A), mkPinj 1 B)) x (Pc 0))"
   1.143 +
   1.144 +text {* Fast Exponentation *}
   1.145 +lemma pow_wf:"odd n \<Longrightarrow> (n::nat) div 2 < n" by (cases n) auto
   1.146 +recdef pow "measure (\<lambda>(x, y). y)"
   1.147 +  "pow (p, 0) = Pc 1"
   1.148 +  "pow (p, n) = (if even n then (pow (sqr p, n div 2)) else mul (p, pow (sqr p, n div 2)))"
   1.149 +(hints simp add: pow_wf)
   1.150 +
   1.151 +lemma pow_if:
   1.152 +  "pow (p,n) =
   1.153 +   (if n = 0 then Pc 1 else if even n then pow (sqr p, n div 2)
   1.154 +    else mul (p, pow (sqr p, n div 2)))"
   1.155 +  by (cases n) simp_all
   1.156 +
   1.157 +(*
   1.158 +lemma number_of_nat_B0: "(number_of (w BIT bit.B0) ::nat) = 2* (number_of w)"
   1.159 +by simp
   1.160 +
   1.161 +lemma number_of_nat_even: "even (number_of (w BIT bit.B0)::nat)"
   1.162 +by simp
   1.163 +
   1.164 +lemma pow_even : "pow (p, number_of(w BIT bit.B0)) = pow (sqr p, number_of w)"
   1.165 +  ( is "pow(?p,?n) = pow (_,?n2)")
   1.166 +proof-
   1.167 +  have "even ?n" by simp
   1.168 +  hence "pow (p, ?n) = pow (sqr p, ?n div 2)"
   1.169 +    apply simp
   1.170 +    apply (cases "IntDef.neg (number_of w)")
   1.171 +    apply simp
   1.172 +    done
   1.173 +*)
   1.174 +
   1.175 +text {* Normalization of polynomial expressions *}
   1.176 +
   1.177 +consts norm :: "'a::{comm_ring,recpower} polex \<Rightarrow> 'a pol"
   1.178 +primrec
   1.179 +  "norm (Pol P) = P"
   1.180 +  "norm (Add P Q) = add (norm P, norm Q)"
   1.181 +  "norm (Sub p q) = sub (norm p) (norm q)"
   1.182 +  "norm (Mul P Q) = mul (norm P, norm Q)"
   1.183 +  "norm (Pow p n) = pow (norm p, n)"
   1.184 +  "norm (Neg P) = neg (norm P)"
   1.185 +
   1.186 +text {* mkPinj preserve semantics *}
   1.187 +lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
   1.188 +  by (induct B) (auto simp add: mkPinj_def ring_eq_simps)
   1.189 +
   1.190 +text {* mkPX preserves semantics *}
   1.191 +lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
   1.192 +  by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add ring_eq_simps)
   1.193 +
   1.194 +text {* Correctness theorems for the implemented operations *}
   1.195 +
   1.196 +text {* Negation *}
   1.197 +lemma neg_ci: "\<And>l. Ipol l (neg P) = -(Ipol l P)"
   1.198 +  by (induct P) auto
   1.199 +
   1.200 +text {* Addition *}
   1.201 +lemma add_ci: "\<And>l. Ipol l (add (P, Q)) = Ipol l P + Ipol l Q"
   1.202 +proof (induct P Q rule: add.induct)
   1.203 +  case (6 x P y Q)
   1.204 +  show ?case
   1.205 +  proof (rule linorder_cases)
   1.206 +    assume "x < y"
   1.207 +    with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)
   1.208 +  next
   1.209 +    assume "x = y"
   1.210 +    with 6 show ?case by (simp add: mkPinj_ci)
   1.211 +  next
   1.212 +    assume "x > y"
   1.213 +    with 6 show ?case by (simp add: mkPinj_ci ring_eq_simps)
   1.214 +  qed
   1.215 +next
   1.216 +  case (7 x P Q y R)
   1.217 +  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
   1.218 +  moreover
   1.219 +  { assume "x = 0" with 7 have ?case by simp }
   1.220 +  moreover
   1.221 +  { assume "x = 1" with 7 have ?case by (simp add: ring_eq_simps) }
   1.222 +  moreover
   1.223 +  { assume "x > 1" from 7 have ?case by (cases x) simp_all }
   1.224 +  ultimately show ?case by blast
   1.225 +next
   1.226 +  case (8 P x R y Q)
   1.227 +  have "y = 0 \<or> y = 1 \<or> y > 1" by arith
   1.228 +  moreover
   1.229 +  { assume "y = 0" with 8 have ?case by simp }
   1.230 +  moreover
   1.231 +  { assume "y = 1" with 8 have ?case by simp }
   1.232 +  moreover
   1.233 +  { assume "y > 1" with 8 have ?case by simp }
   1.234 +  ultimately show ?case by blast
   1.235 +next
   1.236 +  case (9 P1 x P2 Q1 y Q2)
   1.237 +  show ?case
   1.238 +  proof (rule linorder_cases)
   1.239 +    assume a: "x < y" hence "EX d. d + x = y" by arith
   1.240 +    with 9 a show ?case by (auto simp add: mkPX_ci power_add ring_eq_simps)
   1.241 +  next
   1.242 +    assume a: "y < x" hence "EX d. d + y = x" by arith
   1.243 +    with 9 a show ?case by (auto simp add: power_add mkPX_ci ring_eq_simps)
   1.244 +  next
   1.245 +    assume "x = y"
   1.246 +    with 9 show ?case by (simp add: mkPX_ci ring_eq_simps)
   1.247 +  qed
   1.248 +qed (auto simp add: ring_eq_simps)
   1.249 +
   1.250 +text {* Multiplication *}
   1.251 +lemma mul_ci: "\<And>l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"
   1.252 +  by (induct P Q rule: mul.induct)
   1.253 +    (simp_all add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
   1.254 +
   1.255 +text {* Substraction *}
   1.256 +lemma sub_ci: "Ipol l (sub p q) = Ipol l p - Ipol l q"
   1.257 +  by (simp add: add_ci neg_ci sub_def)
   1.258 +
   1.259 +text {* Square *}
   1.260 +lemma sqr_ci:"\<And>ls. Ipol ls (sqr p) = Ipol ls p * Ipol ls p"
   1.261 +  by (induct p) (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_eq_simps power_add)
   1.262 +
   1.263 +
   1.264 +text {* Power *}
   1.265 +lemma even_pow:"even n \<Longrightarrow> pow (p, n) = pow (sqr p, n div 2)" by (induct n) simp_all
   1.266 +
   1.267 +lemma pow_ci: "\<And>p. Ipol ls (pow (p, n)) = (Ipol ls p) ^ n"
   1.268 +proof (induct n rule: nat_less_induct)
   1.269 +  case (1 k)
   1.270 +  have two:"2 = Suc (Suc 0)" by simp
   1.271 +  show ?case
   1.272 +  proof (cases k)
   1.273 +    case (Suc l)
   1.274 +    show ?thesis
   1.275 +    proof cases
   1.276 +      assume EL: "even l"
   1.277 +      have "Suc l div 2 = l div 2"
   1.278 +        by (simp add: nat_number even_nat_plus_one_div_two [OF EL])
   1.279 +      moreover
   1.280 +      from Suc have "l < k" by simp
   1.281 +      with 1 have "\<forall>p. Ipol ls (pow (p, l)) = Ipol ls p ^ l" by simp
   1.282 +      moreover
   1.283 +      note Suc EL even_nat_plus_one_div_two [OF EL]
   1.284 +      ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow)
   1.285 +    next
   1.286 +      assume OL: "odd l"
   1.287 +      with prems have "\<lbrakk>\<forall>m<Suc l. \<forall>p. Ipol ls (pow (p, m)) = Ipol ls p ^ m; k = Suc l; odd l\<rbrakk> \<Longrightarrow> \<forall>p. Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l"
   1.288 +      proof(cases l)
   1.289 +        case (Suc w)
   1.290 +        from prems have EW: "even w" by simp
   1.291 +        from two have two_times:"(2 * (w div 2))= w"
   1.292 +          by (simp only: even_nat_div_two_times_two[OF EW])
   1.293 +        have A: "\<And>p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))"
   1.294 +          by (simp add: power_Suc)
   1.295 +        from A two [symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2"
   1.296 +          by simp
   1.297 +        with prems show ?thesis
   1.298 +          by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
   1.299 +      qed simp
   1.300 +      with prems show ?thesis by simp
   1.301 +    qed
   1.302 +  next
   1.303 +    case 0
   1.304 +    then show ?thesis by simp
   1.305 +  qed
   1.306 +qed
   1.307 +
   1.308 +text {* Normalization preserves semantics  *}
   1.309 +lemma norm_ci:"Ipolex l Pe = Ipol l (norm Pe)"
   1.310 +  by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
   1.311 +
   1.312 +text {* Reflection lemma: Key to the (incomplete) decision procedure *}
   1.313 +lemma norm_eq:
   1.314 +  assumes eq: "norm P1  = norm P2"
   1.315 +  shows "Ipolex l P1 = Ipolex l P2"
   1.316 +proof -
   1.317 +  from eq have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
   1.318 +  thus ?thesis by (simp only: norm_ci)
   1.319 +qed
   1.320 +
   1.321 +
   1.322 +text {* Code generation *}
   1.323 +(*
   1.324 +Does not work, since no generic ring operations implementation is there
   1.325 +generate_code ("ring.ML") test = "norm"*)
   1.326 +
   1.327 +use "comm_ring.ML"
   1.328 +setup "CommRing.setup"
   1.329 +
   1.330 +end
     2.1 --- a/src/HOL/Library/Library.thy	Tue Sep 20 14:06:00 2005 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Tue Sep 20 14:10:29 2005 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4    Word
     2.5    Zorn
     2.6    Char_ord
     2.7 +  Commutative_Ring
     2.8  begin
     2.9  end
    2.10  (*>*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/comm_ring.ML	Tue Sep 20 14:10:29 2005 +0200
     3.3 @@ -0,0 +1,142 @@
     3.4 +(*  ID:         $Id$
     3.5 +    Author:     Amine Chaieb
     3.6 +
     3.7 +Tactic for solving equalities over commutative rings.
     3.8 +*)
     3.9 +
    3.10 +signature COMM_RING =
    3.11 +sig
    3.12 +  val comm_ring_tac : int -> tactic
    3.13 +  val comm_ring_method: int -> Proof.method
    3.14 +  val algebra_method: int -> Proof.method
    3.15 +  val setup : (theory -> theory) list
    3.16 +end
    3.17 +
    3.18 +structure CommRing: COMM_RING =
    3.19 +struct
    3.20 +
    3.21 +(* The Cring exception for erronous uses of cring_tac *)
    3.22 +exception CRing of string;
    3.23 +
    3.24 +(* Zero and One of the commutative ring *)
    3.25 +fun cring_zero T = Const("0",T);
    3.26 +fun cring_one T = Const("1",T);
    3.27 +
    3.28 +(* reification functions *)
    3.29 +(* add two polynom expressions *)
    3.30 +fun polT t = Type ("Commutative_Ring.pol",[t]);
    3.31 +fun  polexT t = Type("Commutative_Ring.polex",[t]);
    3.32 +val nT = HOLogic.natT;
    3.33 +fun listT T = Type ("List.list",[T]);
    3.34 +
    3.35 +(* Reification of the constructors *)
    3.36 +(* Nat*)
    3.37 +val succ = Const("Suc",nT --> nT);
    3.38 +val zero = Const("0",nT);
    3.39 +val one = Const("1",nT);
    3.40 +
    3.41 +(* Lists *)
    3.42 +fun reif_list T [] = Const("List.list.Nil",listT T)
    3.43 +  | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T)
    3.44 +                             $x$(reif_list T xs);
    3.45 +
    3.46 +(* pol*)
    3.47 +fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
    3.48 +fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
    3.49 +fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
    3.50 +
    3.51 +(* polex *)
    3.52 +fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
    3.53 +fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
    3.54 +fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
    3.55 +fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
    3.56 +fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t);
    3.57 +fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t);
    3.58 +(* reification of natural numbers *)
    3.59 +fun reif_nat n =
    3.60 +    if n>0 then succ$(reif_nat (n-1))
    3.61 +    else if n=0 then zero
    3.62 +    else raise CRing "ring_tac: reif_nat negative n";
    3.63 +
    3.64 +(* reification of polynoms : primitive cring expressions *)
    3.65 +fun reif_pol T vs t =
    3.66 +    case t of
    3.67 +       Free(_,_) =>
    3.68 +        let val i = find_index_eq t vs
    3.69 +        in if i = 0
    3.70 +           then (pol_PX T)$((pol_Pc T)$ (cring_one T))
    3.71 +                          $one$((pol_Pc T)$(cring_zero T))
    3.72 +           else (pol_Pinj T)$(reif_nat i)$
    3.73 +                            ((pol_PX T)$((pol_Pc T)$ (cring_one T))
    3.74 +                                       $one$
    3.75 +                                       ((pol_Pc T)$(cring_zero T)))
    3.76 +        end
    3.77 +      | _ => (pol_Pc T)$ t;
    3.78 +
    3.79 +
    3.80 +(* reification of polynom expressions *)
    3.81 +fun reif_polex T vs t =
    3.82 +    case t of
    3.83 +        Const("op +",_)$a$b => (polex_add T)
    3.84 +                                   $ (reif_polex T vs a)$(reif_polex T vs b)
    3.85 +      | Const("op -",_)$a$b => (polex_sub T)
    3.86 +                                   $ (reif_polex T vs a)$(reif_polex T vs b)
    3.87 +      | Const("op *",_)$a$b =>  (polex_mul T)
    3.88 +                                    $ (reif_polex T vs a)$ (reif_polex T vs b)
    3.89 +      | Const("uminus",_)$a => (polex_neg T)
    3.90 +                                   $ (reif_polex T vs a)
    3.91 +      | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
    3.92 +
    3.93 +      | _ => (polex_pol T) $ (reif_pol T vs t);
    3.94 +
    3.95 +(* reification of the equation *)
    3.96 +val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}";
    3.97 +fun reif_eq sg (eq as Const("op =",Type("fun",a::_))$lhs$rhs) =
    3.98 +    if Sign.of_sort (the_context()) (a,cr_sort)
    3.99 +    then
   3.100 +        let val fs = term_frees eq
   3.101 +            val cvs = cterm_of sg (reif_list a fs)
   3.102 +            val clhs = cterm_of sg (reif_polex a fs lhs)
   3.103 +            val crhs = cterm_of sg (reif_polex a fs rhs)
   3.104 +            val ca = ctyp_of sg a
   3.105 +        in (ca,cvs,clhs, crhs)
   3.106 +        end
   3.107 +    else raise CRing "reif_eq: not an equation over comm_ring + recpower"
   3.108 +  | reif_eq sg _ = raise CRing "reif_eq: not an equation";
   3.109 +
   3.110 +(*The cring tactic  *)
   3.111 +(* Attention: You have to make sure that no t^0 is in the goal!! *)
   3.112 +(* Use simply rewriting t^0 = 1 *)
   3.113 +fun cring_ss sg = simpset_of sg
   3.114 +                           addsimps
   3.115 +                           (map thm ["mkPX_def", "mkPinj_def","sub_def",
   3.116 +                                     "power_add","even_def","pow_if"])
   3.117 +                           addsimps [sym OF [thm "power_add"]];
   3.118 +
   3.119 +val norm_eq = thm "norm_eq"
   3.120 +fun comm_ring_tac i =(fn st =>
   3.121 +    let
   3.122 +        val g = List.nth (prems_of st, i - 1)
   3.123 +        val sg = sign_of_thm st
   3.124 +        val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
   3.125 +        val norm_eq_th = simplify (cring_ss sg)
   3.126 +                        (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
   3.127 +                                                norm_eq)
   3.128 +    in ((cut_rules_tac [norm_eq_th] i)
   3.129 +            THEN (simp_tac (cring_ss sg) i)
   3.130 +            THEN (simp_tac (cring_ss sg) i)) st
   3.131 +    end);
   3.132 +
   3.133 +fun comm_ring_method i = Method.METHOD (fn facts =>
   3.134 +  Method.insert_tac facts 1 THEN comm_ring_tac i);
   3.135 +val algebra_method = comm_ring_method;
   3.136 +
   3.137 +val setup =
   3.138 +  [Method.add_method ("comm_ring",
   3.139 +     Method.no_args (comm_ring_method 1),
   3.140 +     "reflective decision procedure for equalities over commutative rings"),
   3.141 +   Method.add_method ("algebra",
   3.142 +     Method.no_args (algebra_method 1),
   3.143 +     "Method for proving algebraic properties: for now only comm_ring")];
   3.144 +
   3.145 +end;