author wenzelm Tue Sep 20 14:10:29 2005 +0200 (2005-09-20) changeset 17516 45164074dad4 parent 17515 830bc15e692c child 17517 9dc9d3005ed2
 src/HOL/Library/Commutative_Ring.thy file | annotate | diff | revisions src/HOL/Library/Library.thy file | annotate | diff | revisions src/HOL/Library/comm_ring.ML file | annotate | diff | revisions
```     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.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.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.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.254 +
1.255 +text {* Substraction *}
1.256 +lemma sub_ci: "Ipol l (sub p q) = Ipol l p - Ipol l q"
1.258 +
1.259 +text {* Square *}
1.260 +lemma sqr_ci:"\<And>ls. Ipol ls (sqr p) = Ipol ls p * Ipol ls p"
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.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.115 +                           (map thm ["mkPX_def", "mkPinj_def","sub_def",
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 =