# HG changeset patch # User haftmann # Date 1256907589 -3600 # Node ID 9157d0f9f00ec6dd2bba1200a5f03474dfc82d03 # Parent 37ec56ac3fd43b578fea01d413f7b6712bbc48aa moved Commutative_Ring into session Decision_Procs diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Decision_Procs/Commutative_Ring.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Fri Oct 30 13:59:49 2009 +0100 @@ -0,0 +1,319 @@ +(* Author: Bernhard Haeupler + +Proving equalities in commutative rings done "right" in Isabelle/HOL. +*) + +header {* Proving equalities in commutative rings *} + +theory Commutative_Ring +imports Main Parity +uses ("commutative_ring_tac.ML") +begin + +text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *} + +datatype 'a pol = + Pc 'a + | Pinj nat "'a pol" + | PX "'a pol" nat "'a pol" + +datatype 'a polex = + Pol "'a pol" + | Add "'a polex" "'a polex" + | Sub "'a polex" "'a polex" + | Mul "'a polex" "'a polex" + | Pow "'a polex" nat + | Neg "'a polex" + +text {* Interpretation functions for the shadow syntax. *} + +primrec + Ipol :: "'a::{comm_ring_1} list \ 'a pol \ 'a" +where + "Ipol l (Pc c) = c" + | "Ipol l (Pinj i P) = Ipol (drop i l) P" + | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q" + +primrec + Ipolex :: "'a::{comm_ring_1} list \ 'a polex \ 'a" +where + "Ipolex l (Pol P) = Ipol l P" + | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q" + | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q" + | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q" + | "Ipolex l (Pow p n) = Ipolex l p ^ n" + | "Ipolex l (Neg P) = - Ipolex l P" + +text {* Create polynomial normalized polynomials given normalized inputs. *} + +definition + mkPinj :: "nat \ 'a pol \ 'a pol" where + "mkPinj x P = (case P of + Pc c \ Pc c | + Pinj y P \ Pinj (x + y) P | + PX p1 y p2 \ Pinj x P)" + +definition + mkPX :: "'a::{comm_ring} pol \ nat \ 'a pol \ 'a pol" where + "mkPX P i Q = (case P of + Pc c \ (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) | + Pinj j R \ PX P i Q | + PX P2 i2 Q2 \ (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )" + +text {* Defining the basic ring operations on normalized polynomials *} + +function + add :: "'a::{comm_ring} pol \ 'a pol \ 'a pol" (infixl "\" 65) +where + "Pc a \ Pc b = Pc (a + b)" + | "Pc c \ Pinj i P = Pinj i (P \ Pc c)" + | "Pinj i P \ Pc c = Pinj i (P \ Pc c)" + | "Pc c \ PX P i Q = PX P i (Q \ Pc c)" + | "PX P i Q \ Pc c = PX P i (Q \ Pc c)" + | "Pinj x P \ Pinj y Q = + (if x = y then mkPinj x (P \ Q) + else (if x > y then mkPinj y (Pinj (x - y) P \ Q) + else mkPinj x (Pinj (y - x) Q \ P)))" + | "Pinj x P \ PX Q y R = + (if x = 0 then P \ PX Q y R + else (if x = 1 then PX Q y (R \ P) + else PX Q y (R \ Pinj (x - 1) P)))" + | "PX P x R \ Pinj y Q = + (if y = 0 then PX P x R \ Q + else (if y = 1 then PX P x (R \ Q) + else PX P x (R \ Pinj (y - 1) Q)))" + | "PX P1 x P2 \ PX Q1 y Q2 = + (if x = y then mkPX (P1 \ Q1) x (P2 \ Q2) + else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \ Q1) y (P2 \ Q2) + else mkPX (PX Q1 (y-x) (Pc 0) \ P1) x (P2 \ Q2)))" +by pat_completeness auto +termination by (relation "measure (\(x, y). size x + size y)") auto + +function + mul :: "'a::{comm_ring} pol \ 'a pol \ 'a pol" (infixl "\" 70) +where + "Pc a \ Pc b = Pc (a * b)" + | "Pc c \ Pinj i P = + (if c = 0 then Pc 0 else mkPinj i (P \ Pc c))" + | "Pinj i P \ Pc c = + (if c = 0 then Pc 0 else mkPinj i (P \ Pc c))" + | "Pc c \ PX P i Q = + (if c = 0 then Pc 0 else mkPX (P \ Pc c) i (Q \ Pc c))" + | "PX P i Q \ Pc c = + (if c = 0 then Pc 0 else mkPX (P \ Pc c) i (Q \ Pc c))" + | "Pinj x P \ Pinj y Q = + (if x = y then mkPinj x (P \ Q) else + (if x > y then mkPinj y (Pinj (x-y) P \ Q) + else mkPinj x (Pinj (y - x) Q \ P)))" + | "Pinj x P \ PX Q y R = + (if x = 0 then P \ PX Q y R else + (if x = 1 then mkPX (Pinj x P \ Q) y (R \ P) + else mkPX (Pinj x P \ Q) y (R \ Pinj (x - 1) P)))" + | "PX P x R \ Pinj y Q = + (if y = 0 then PX P x R \ Q else + (if y = 1 then mkPX (Pinj y Q \ P) x (R \ Q) + else mkPX (Pinj y Q \ P) x (R \ Pinj (y - 1) Q)))" + | "PX P1 x P2 \ PX Q1 y Q2 = + mkPX (P1 \ Q1) (x + y) (P2 \ Q2) \ + (mkPX (P1 \ mkPinj 1 Q2) x (Pc 0) \ + (mkPX (Q1 \ mkPinj 1 P2) y (Pc 0)))" +by pat_completeness auto +termination by (relation "measure (\(x, y). size x + size y)") + (auto simp add: mkPinj_def split: pol.split) + +text {* Negation*} +primrec + neg :: "'a::{comm_ring} pol \ 'a pol" +where + "neg (Pc c) = Pc (-c)" + | "neg (Pinj i P) = Pinj i (neg P)" + | "neg (PX P x Q) = PX (neg P) x (neg Q)" + +text {* Substraction *} +definition + sub :: "'a::{comm_ring} pol \ 'a pol \ 'a pol" (infixl "\" 65) +where + "sub P Q = P \ neg Q" + +text {* Square for Fast Exponentation *} +primrec + sqr :: "'a::{comm_ring_1} pol \ 'a pol" +where + "sqr (Pc c) = Pc (c * c)" + | "sqr (Pinj i P) = mkPinj i (sqr P)" + | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \ + mkPX (Pc (1 + 1) \ A \ mkPinj 1 B) x (Pc 0)" + +text {* Fast Exponentation *} +fun + pow :: "nat \ 'a::{comm_ring_1} pol \ 'a pol" +where + "pow 0 P = Pc 1" + | "pow n P = (if even n then pow (n div 2) (sqr P) + else P \ pow (n div 2) (sqr P))" + +lemma pow_if: + "pow n P = + (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P) + else P \ pow (n div 2) (sqr P))" + by (cases n) simp_all + + +text {* Normalization of polynomial expressions *} + +primrec + norm :: "'a::{comm_ring_1} polex \ 'a pol" +where + "norm (Pol P) = P" + | "norm (Add P Q) = norm P \ norm Q" + | "norm (Sub P Q) = norm P \ norm Q" + | "norm (Mul P Q) = norm P \ norm Q" + | "norm (Pow P n) = pow n (norm P)" + | "norm (Neg P) = neg (norm P)" + +text {* mkPinj preserve semantics *} +lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)" + by (induct B) (auto simp add: mkPinj_def algebra_simps) + +text {* mkPX preserves semantics *} +lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)" + by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps) + +text {* Correctness theorems for the implemented operations *} + +text {* Negation *} +lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)" + by (induct P arbitrary: l) auto + +text {* Addition *} +lemma add_ci: "Ipol l (P \ Q) = Ipol l P + Ipol l Q" +proof (induct P Q arbitrary: l rule: add.induct) + case (6 x P y Q) + show ?case + proof (rule linorder_cases) + assume "x < y" + with 6 show ?case by (simp add: mkPinj_ci algebra_simps) + next + assume "x = y" + with 6 show ?case by (simp add: mkPinj_ci) + next + assume "x > y" + with 6 show ?case by (simp add: mkPinj_ci algebra_simps) + qed +next + case (7 x P Q y R) + have "x = 0 \ x = 1 \ x > 1" by arith + moreover + { assume "x = 0" with 7 have ?case by simp } + moreover + { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) } + moreover + { assume "x > 1" from 7 have ?case by (cases x) simp_all } + ultimately show ?case by blast +next + case (8 P x R y Q) + have "y = 0 \ y = 1 \ y > 1" by arith + moreover + { assume "y = 0" with 8 have ?case by simp } + moreover + { assume "y = 1" with 8 have ?case by simp } + moreover + { assume "y > 1" with 8 have ?case by simp } + ultimately show ?case by blast +next + case (9 P1 x P2 Q1 y Q2) + show ?case + proof (rule linorder_cases) + assume a: "x < y" hence "EX d. d + x = y" by arith + with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps) + next + assume a: "y < x" hence "EX d. d + y = x" by arith + with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps) + next + assume "x = y" + with 9 show ?case by (simp add: mkPX_ci algebra_simps) + qed +qed (auto simp add: algebra_simps) + +text {* Multiplication *} +lemma mul_ci: "Ipol l (P \ Q) = Ipol l P * Ipol l Q" + by (induct P Q arbitrary: l rule: mul.induct) + (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add) + +text {* Substraction *} +lemma sub_ci: "Ipol l (P \ Q) = Ipol l P - Ipol l Q" + by (simp add: add_ci neg_ci sub_def) + +text {* Square *} +lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P" + by (induct P arbitrary: ls) + (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add) + +text {* Power *} +lemma even_pow:"even n \ pow n P = pow (n div 2) (sqr P)" + by (induct n) simp_all + +lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n" +proof (induct n arbitrary: P rule: nat_less_induct) + case (1 k) + show ?case + proof (cases k) + case 0 + then show ?thesis by simp + next + case (Suc l) + show ?thesis + proof cases + assume "even l" + then have "Suc l div 2 = l div 2" + by (simp add: nat_number even_nat_plus_one_div_two) + moreover + from Suc have "l < k" by simp + with 1 have "\P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp + moreover + note Suc `even l` even_nat_plus_one_div_two + ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow) + next + assume "odd l" + { + fix p + have "Ipol ls (sqr P) ^ (Suc l div 2) = Ipol ls P ^ Suc l" + proof (cases l) + case 0 + with `odd l` show ?thesis by simp + next + case (Suc w) + with `odd l` have "even w" by simp + have two_times: "2 * (w div 2) = w" + by (simp only: numerals even_nat_div_two_times_two [OF `even w`]) + have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)" + by (simp add: power_Suc) + then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2" + by (simp add: numerals) + with Suc show ?thesis + by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci + simp del: power_Suc) + qed + } with 1 Suc `odd l` show ?thesis by simp + qed + qed +qed + +text {* Normalization preserves semantics *} +lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)" + by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci) + +text {* Reflection lemma: Key to the (incomplete) decision procedure *} +lemma norm_eq: + assumes "norm P1 = norm P2" + shows "Ipolex l P1 = Ipolex l P2" +proof - + from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp + then show ?thesis by (simp only: norm_ci) +qed + + +use "commutative_ring_tac.ML" +setup Commutative_Ring_Tac.setup + +end diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Fri Oct 30 13:59:49 2009 +0100 @@ -0,0 +1,391 @@ +(* Author: Bernhard Haeupler + +This theory is about of the relative completeness of method comm-ring +method. As long as the reified atomic polynomials of type 'a pol are +in normal form, the cring method is complete. +*) + +header {* Proof of the relative completeness of method comm-ring *} + +theory Commutative_Ring_Complete +imports Commutative_Ring +begin + +text {* Formalization of normal form *} +fun + isnorm :: "('a::{comm_ring}) pol \ bool" +where + "isnorm (Pc c) \ True" + | "isnorm (Pinj i (Pc c)) \ False" + | "isnorm (Pinj i (Pinj j Q)) \ False" + | "isnorm (Pinj 0 P) \ False" + | "isnorm (Pinj i (PX Q1 j Q2)) \ isnorm (PX Q1 j Q2)" + | "isnorm (PX P 0 Q) \ False" + | "isnorm (PX (Pc c) i Q) \ c \ 0 \ isnorm Q" + | "isnorm (PX (PX P1 j (Pc c)) i Q) \ c \ 0 \ isnorm (PX P1 j (Pc c)) \ isnorm Q" + | "isnorm (PX P i Q) \ isnorm P \ isnorm Q" + +(* Some helpful lemmas *) +lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False" +by(cases P, auto) + +lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False" +by(cases i, auto) + +lemma norm_Pinj:"isnorm (Pinj i Q) \ isnorm Q" +by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto + +lemma norm_PX2:"isnorm (PX P i Q) \ isnorm Q" +by(cases i, auto, cases P, auto, case_tac pol2, auto) + +lemma norm_PX1:"isnorm (PX P i Q) \ isnorm P" +by(cases i, auto, cases P, auto, case_tac pol2, auto) + +lemma mkPinj_cn:"\y~=0; isnorm Q\ \ isnorm (mkPinj y Q)" +apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split) +apply(case_tac nat, auto simp add: norm_Pinj_0_False) +by(case_tac pol, auto) (case_tac y, auto) + +lemma norm_PXtrans: + assumes A:"isnorm (PX P x Q)" and "isnorm Q2" + shows "isnorm (PX P x Q2)" +proof(cases P) + case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto) +next + case Pc from prems show ?thesis by(cases x, auto) +next + case Pinj from prems show ?thesis by(cases x, auto) +qed + +lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)" +proof(cases P) + case (PX p1 y p2) + from prems show ?thesis by(cases x, auto, cases p2, auto) +next + case Pc + from prems show ?thesis by(cases x, auto) +next + case Pinj + from prems show ?thesis by(cases x, auto) +qed + +text {* mkPX conserves normalizedness (@{text "_cn"}) *} +lemma mkPX_cn: + assumes "x \ 0" and "isnorm P" and "isnorm Q" + shows "isnorm (mkPX P x Q)" +proof(cases P) + case (Pc c) + from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) +next + case (Pinj i Q) + from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) +next + case (PX P1 y P2) + from prems have Y0:"y>0" by(cases y, auto) + from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2]) + with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto) +qed + +text {* add conserves normalizedness *} +lemma add_cn:"isnorm P \ isnorm Q \ isnorm (P \ Q)" +proof(induct P Q rule: add.induct) + case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all) +next + case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all) +next + case (4 c P2 i Q2) + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) + with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) +next + case (5 P2 i Q2 c) + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) + with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) +next + case (6 x P2 y Q2) + from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False) + from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False) + have "x < y \ x = y \ x > y" by arith + moreover + { assume "xy" hence "EX d. x=d+y" by arith + then obtain d where "x=d+y".. + moreover + note prems Y0 + moreover + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + moreover + with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) + ultimately have ?case by (simp add: mkPinj_cn)} + ultimately show ?case by blast +next + case (7 x P2 Q2 y R) + have "x=0 \ (x = 1) \ (x > 1)" by arith + moreover + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + moreover + { assume "x=1" + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) + with prems have "isnorm (R \ P2)" by simp + with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + moreover + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith + then obtain d where X:"x=Suc (Suc d)" .. + from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) + with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) + with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact + with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + ultimately show ?case by blast +next + case (8 Q2 y R x P2) + have "x = 0 \ x = 1 \ x > 1" by arith + moreover + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + moreover + { assume "x=1" + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) + with prems have "isnorm (R \ P2)" by simp + with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + moreover + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith + then obtain d where X:"x=Suc (Suc d)" .. + from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) + with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) + with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact + with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + ultimately show ?case by blast +next + case (9 P1 x P2 Q1 y Q2) + from prems have Y0:"y>0" by(cases y, auto) + from prems have X0:"x>0" by(cases x, auto) + from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) + from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2]) + have "y < x \ x = y \ x < y" by arith + moreover + {assume sm1:"y < x" hence "EX d. x=d+y" by arith + then obtain d where sm2:"x=d+y".. + note prems NQ1 NP1 NP2 NQ2 sm1 sm2 + moreover + have "isnorm (PX P1 d (Pc 0))" + proof(cases P1) + case (PX p1 y p2) + with prems show ?thesis by(cases d, simp,cases p2, auto) + next case Pc from prems show ?thesis by(cases d, auto) + next case Pinj from prems show ?thesis by(cases d, auto) + qed + ultimately have "isnorm (P2 \ Q2)" "isnorm (PX P1 (x - y) (Pc 0) \ Q1)" by auto + with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)} + moreover + {assume "x=y" + from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \ Q2)" "isnorm (P1 \ Q1)" by auto + with Y0 prems have ?case by (simp add: mkPX_cn) } + moreover + {assume sm1:"x Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \ P1)" by auto + with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)} + ultimately show ?case by blast +qed simp + +text {* mul concerves normalizedness *} +lemma mul_cn :"isnorm P \ isnorm Q \ isnorm (P \ Q)" +proof(induct P Q rule: mul.induct) + case (2 c i P2) thus ?case + by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) +next + case (3 i P2 c) thus ?case + by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) +next + case (4 c P2 i Q2) + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) + with prems show ?case + by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn) +next + case (5 P2 i Q2 c) + from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) + with prems show ?case + by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn) +next + case (6 x P2 y Q2) + have "x < y \ x = y \ x > y" by arith + moreover + { assume "x0" by (cases x, auto simp add: norm_Pinj_0_False) + moreover + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + moreover + with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) + ultimately have ?case by (simp add: mkPinj_cn)} + moreover + { assume "x=y" + moreover + from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + moreover + with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) + moreover + note prems + moreover + ultimately have ?case by (simp add: mkPinj_cn) } + moreover + { assume "x>y" hence "EX d. x=d+y" by arith + then obtain d where "x=d+y".. + moreover + note prems + moreover + from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) + moreover + from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + moreover + with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) + ultimately have ?case by (simp add: mkPinj_cn) } + ultimately show ?case by blast +next + case (7 x P2 Q2 y R) + from prems have Y0:"y>0" by(cases y, auto) + have "x=0 \ (x = 1) \ (x > 1)" by arith + moreover + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + moreover + { assume "x=1" + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) + with prems have "isnorm (R \ P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) + with Y0 prems have ?case by (simp add: mkPX_cn)} + moreover + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith + then obtain d where X:"x=Suc (Suc d)" .. + from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) + moreover + from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) + moreover + from prems have "isnorm (Pinj x P2)" by(cases P2, auto) + moreover + note prems + ultimately have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" by auto + with Y0 X have ?case by (simp add: mkPX_cn)} + ultimately show ?case by blast +next + case (8 Q2 y R x P2) + from prems have Y0:"y>0" by(cases y, auto) + have "x=0 \ (x = 1) \ (x > 1)" by arith + moreover + { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + moreover + { assume "x=1" + from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) + with prems have "isnorm (R \ P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) + with Y0 prems have ?case by (simp add: mkPX_cn) } + moreover + { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith + then obtain d where X:"x=Suc (Suc d)" .. + from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) + moreover + from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) + moreover + from prems have "isnorm (Pinj x P2)" by(cases P2, auto) + moreover + note prems + ultimately have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" by auto + with Y0 X have ?case by (simp add: mkPX_cn) } + ultimately show ?case by blast +next + case (9 P1 x P2 Q1 y Q2) + from prems have X0:"x>0" by(cases x, auto) + from prems have Y0:"y>0" by(cases y, auto) + note prems + moreover + from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) + moreover + from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) + ultimately have "isnorm (P1 \ Q1)" "isnorm (P2 \ Q2)" + "isnorm (P1 \ mkPinj 1 Q2)" "isnorm (Q1 \ mkPinj 1 P2)" + by (auto simp add: mkPinj_cn) + with prems X0 Y0 have + "isnorm (mkPX (P1 \ Q1) (x + y) (P2 \ Q2))" + "isnorm (mkPX (P1 \ mkPinj (Suc 0) Q2) x (Pc 0))" + "isnorm (mkPX (Q1 \ mkPinj (Suc 0) P2) y (Pc 0))" + by (auto simp add: mkPX_cn) + thus ?case by (simp add: add_cn) +qed(simp) + +text {* neg conserves normalizedness *} +lemma neg_cn: "isnorm P \ isnorm (neg P)" +proof (induct P) + case (Pinj i P2) + from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2]) + with prems show ?case by(cases P2, auto, cases i, auto) +next + case (PX P1 x P2) + from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) + with prems show ?case + proof(cases P1) + case (PX p1 y p2) + with prems show ?thesis by(cases x, auto, cases p2, auto) + next + case Pinj + with prems show ?thesis by(cases x, auto) + qed(cases x, auto) +qed(simp) + +text {* sub conserves normalizedness *} +lemma sub_cn:"isnorm p \ isnorm q \ isnorm (p \ q)" +by (simp add: sub_def add_cn neg_cn) + +text {* sqr conserves normalizizedness *} +lemma sqr_cn:"isnorm P \ isnorm (sqr P)" +proof(induct P) + case (Pinj i Q) + from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) +next + case (PX P1 x P2) + 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]) + with prems have + "isnorm (mkPX (Pc (1 + 1) \ P1 \ mkPinj (Suc 0) P2) x (Pc 0))" + and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" + by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) + thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) +qed simp + +text {* pow conserves normalizedness *} +lemma pow_cn:"isnorm P \ isnorm (pow n P)" +proof (induct n arbitrary: P rule: nat_less_induct) + case (1 k) + show ?case + proof (cases "k=0") + case False + then have K2:"k div 2 < k" by (cases k, auto) + from prems have "isnorm (sqr P)" by (simp add: sqr_cn) + with prems K2 show ?thesis + by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) + qed simp +qed + +end diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Decision_Procs/Decision_Procs.thy --- a/src/HOL/Decision_Procs/Decision_Procs.thy Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Decision_Procs/Decision_Procs.thy Fri Oct 30 13:59:49 2009 +0100 @@ -1,7 +1,10 @@ -header {* Various decision procedures. typically involving reflection *} +header {* Various decision procedures, typically involving reflection *} theory Decision_Procs -imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" Parametric_Ferrante_Rackoff +imports + Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order Parametric_Ferrante_Rackoff + Commutative_Ring_Complete + "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" begin end \ No newline at end of file diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Decision_Procs/commutative_ring_tac.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Oct 30 13:59:49 2009 +0100 @@ -0,0 +1,104 @@ +(* Author: Amine Chaieb + +Tactic for solving equalities over commutative rings. +*) + +signature COMMUTATIVE_RING_TAC = +sig + val tac: Proof.context -> int -> tactic + val setup: theory -> theory +end + +structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC = +struct + +(* Zero and One of the commutative ring *) +fun cring_zero T = Const (@{const_name HOL.zero}, T); +fun cring_one T = Const (@{const_name HOL.one}, T); + +(* reification functions *) +(* add two polynom expressions *) +fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]); +fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]); + +(* pol *) +fun pol_Pc t = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t); +fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t); +fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t); + +(* polex *) +fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t); +fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t); +fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t); +fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t); +fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t); +fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t); + +(* reification of polynoms : primitive cring expressions *) +fun reif_pol T vs (t as Free _) = + let + val one = @{term "1::nat"}; + val i = find_index (fn t' => t' = t) vs + in if i = 0 + then pol_PX T $ (pol_Pc T $ cring_one T) + $ one $ (pol_Pc T $ cring_zero T) + else pol_Pinj T $ HOLogic.mk_nat i + $ (pol_PX T $ (pol_Pc T $ cring_one T) + $ one $ (pol_Pc T $ cring_zero T)) + end + | reif_pol T vs t = pol_Pc T $ t; + +(* reification of polynom expressions *) +fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) = + polex_add T $ reif_polex T vs a $ reif_polex T vs b + | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) = + polex_sub T $ reif_polex T vs a $ reif_polex T vs b + | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) = + polex_mul T $ reif_polex T vs a $ reif_polex T vs b + | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) = + polex_neg T $ reif_polex T vs a + | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) = + polex_pow T $ reif_polex T vs a $ n + | reif_polex T vs t = polex_pol T $ reif_pol T vs t; + +(* reification of the equation *) +val cr_sort = @{sort "comm_ring_1"}; + +fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) = + if Sign.of_sort thy (T, cr_sort) then + let + val fs = OldTerm.term_frees eq; + val cvs = cterm_of thy (HOLogic.mk_list T fs); + val clhs = cterm_of thy (reif_polex T fs lhs); + val crhs = cterm_of thy (reif_polex T fs rhs); + val ca = ctyp_of thy T; + in (ca, cvs, clhs, crhs) end + else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort) + | reif_eq _ _ = error "reif_eq: not an equation"; + +(* The cring tactic *) +(* Attention: You have to make sure that no t^0 is in the goal!! *) +(* Use simply rewriting t^0 = 1 *) +val cring_simps = + [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add}, + @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]]; + +fun tac ctxt = SUBGOAL (fn (g, i) => + let + val thy = ProofContext.theory_of ctxt; + val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*) + addsimps cring_simps; + val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g) + val norm_eq_th = + simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq}) + in + cut_rules_tac [norm_eq_th] i + THEN (simp_tac cring_ss i) + THEN (simp_tac cring_ss i) + end); + +val setup = + Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac)) + "reflective decision procedure for equalities over commutative rings"; + +end; diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Fri Oct 30 13:59:49 2009 +0100 @@ -0,0 +1,48 @@ +(* Author: Bernhard Haeupler *) + +header {* Some examples demonstrating the comm-ring method *} + +theory Commutative_Ring_Ex +imports Commutative_Ring +begin + +lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" +by comm_ring + +lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" +by comm_ring + +lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x" +by comm_ring + +lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3" +by comm_ring + +lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y" +by comm_ring + +lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c" +by comm_ring + +lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c" +by comm_ring + +lemma "(a::int)*b + a*c = a*(b+c)" +by comm_ring + +lemma "(a::int)^2 - b^2 = (a - b) * (a + b)" +by comm_ring + +lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)" +by comm_ring + +lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)" +by comm_ring + +lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)" +by comm_ring + +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 )" +by comm_ring + +end diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/IsaMakefile Fri Oct 30 13:59:49 2009 +0100 @@ -248,12 +248,12 @@ Groebner_Basis.thy \ Hilbert_Choice.thy \ Int.thy \ - IntDiv.thy \ List.thy \ Main.thy \ Map.thy \ Nat_Numeral.thy \ Nat_Transfer.thy \ + Numeral_Simprocs.thy \ Presburger.thy \ Predicate_Compile.thy \ Quickcheck.thy \ @@ -382,7 +382,6 @@ Library/While_Combinator.thy Library/Product_ord.thy \ Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \ Library/Sublist_Order.thy Library/List_lexord.thy \ - Library/Commutative_Ring.thy Library/comm_ring.ML \ Library/Coinductive_List.thy Library/AssocList.thy \ Library/Formal_Power_Series.thy Library/Binomial.thy \ Library/Eval_Witness.thy Library/Code_Char.thy \ @@ -785,6 +784,9 @@ $(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \ Decision_Procs/Approximation.thy \ + Decision_Procs/Commutative_Ring.thy \ + Decision_Procs/Commutative_Ring_Complete.thy \ + Decision_Procs/commutative_ring_tac.ML \ Decision_Procs/Cooper.thy \ Decision_Procs/cooper_tac.ML \ Decision_Procs/Dense_Linear_Order.thy \ @@ -795,6 +797,7 @@ Decision_Procs/Decision_Procs.thy \ Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ Decision_Procs/ex/Approximation_Ex.thy \ + Decision_Procs/ex/Commutative_Ring_Ex.thy \ Decision_Procs/ROOT.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs @@ -937,7 +940,7 @@ HOL-ex: HOL $(LOG)/HOL-ex.gz -$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ +$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ Number_Theory/Primes.thy \ Tools/Predicate_Compile/predicate_compile_core.ML \ ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \ @@ -945,8 +948,8 @@ ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \ ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \ - ex/Codegenerator_Test.thy ex/Coherent.thy ex/Commutative_RingEx.thy \ - ex/Commutative_Ring_Complete.thy ex/Efficient_Nat_examples.thy \ + ex/Codegenerator_Test.thy ex/Coherent.thy \ + ex/Efficient_Nat_examples.thy \ ex/Eval_Examples.thy ex/Fundefs.thy ex/Groebner_Examples.thy \ ex/Guess.thy ex/HarmonicSeries.thy ex/Hebrew.thy \ ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Library/Commutative_Ring.thy --- a/src/HOL/Library/Commutative_Ring.thy Fri Oct 30 01:32:06 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,319 +0,0 @@ -(* Author: Bernhard Haeupler - -Proving equalities in commutative rings done "right" in Isabelle/HOL. -*) - -header {* Proving equalities in commutative rings *} - -theory Commutative_Ring -imports List Parity Main -uses ("comm_ring.ML") -begin - -text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *} - -datatype 'a pol = - Pc 'a - | Pinj nat "'a pol" - | PX "'a pol" nat "'a pol" - -datatype 'a polex = - Pol "'a pol" - | Add "'a polex" "'a polex" - | Sub "'a polex" "'a polex" - | Mul "'a polex" "'a polex" - | Pow "'a polex" nat - | Neg "'a polex" - -text {* Interpretation functions for the shadow syntax. *} - -primrec - Ipol :: "'a::{comm_ring_1} list \ 'a pol \ 'a" -where - "Ipol l (Pc c) = c" - | "Ipol l (Pinj i P) = Ipol (drop i l) P" - | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q" - -primrec - Ipolex :: "'a::{comm_ring_1} list \ 'a polex \ 'a" -where - "Ipolex l (Pol P) = Ipol l P" - | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q" - | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q" - | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q" - | "Ipolex l (Pow p n) = Ipolex l p ^ n" - | "Ipolex l (Neg P) = - Ipolex l P" - -text {* Create polynomial normalized polynomials given normalized inputs. *} - -definition - mkPinj :: "nat \ 'a pol \ 'a pol" where - "mkPinj x P = (case P of - Pc c \ Pc c | - Pinj y P \ Pinj (x + y) P | - PX p1 y p2 \ Pinj x P)" - -definition - mkPX :: "'a::{comm_ring} pol \ nat \ 'a pol \ 'a pol" where - "mkPX P i Q = (case P of - Pc c \ (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) | - Pinj j R \ PX P i Q | - PX P2 i2 Q2 \ (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )" - -text {* Defining the basic ring operations on normalized polynomials *} - -function - add :: "'a::{comm_ring} pol \ 'a pol \ 'a pol" (infixl "\" 65) -where - "Pc a \ Pc b = Pc (a + b)" - | "Pc c \ Pinj i P = Pinj i (P \ Pc c)" - | "Pinj i P \ Pc c = Pinj i (P \ Pc c)" - | "Pc c \ PX P i Q = PX P i (Q \ Pc c)" - | "PX P i Q \ Pc c = PX P i (Q \ Pc c)" - | "Pinj x P \ Pinj y Q = - (if x = y then mkPinj x (P \ Q) - else (if x > y then mkPinj y (Pinj (x - y) P \ Q) - else mkPinj x (Pinj (y - x) Q \ P)))" - | "Pinj x P \ PX Q y R = - (if x = 0 then P \ PX Q y R - else (if x = 1 then PX Q y (R \ P) - else PX Q y (R \ Pinj (x - 1) P)))" - | "PX P x R \ Pinj y Q = - (if y = 0 then PX P x R \ Q - else (if y = 1 then PX P x (R \ Q) - else PX P x (R \ Pinj (y - 1) Q)))" - | "PX P1 x P2 \ PX Q1 y Q2 = - (if x = y then mkPX (P1 \ Q1) x (P2 \ Q2) - else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \ Q1) y (P2 \ Q2) - else mkPX (PX Q1 (y-x) (Pc 0) \ P1) x (P2 \ Q2)))" -by pat_completeness auto -termination by (relation "measure (\(x, y). size x + size y)") auto - -function - mul :: "'a::{comm_ring} pol \ 'a pol \ 'a pol" (infixl "\" 70) -where - "Pc a \ Pc b = Pc (a * b)" - | "Pc c \ Pinj i P = - (if c = 0 then Pc 0 else mkPinj i (P \ Pc c))" - | "Pinj i P \ Pc c = - (if c = 0 then Pc 0 else mkPinj i (P \ Pc c))" - | "Pc c \ PX P i Q = - (if c = 0 then Pc 0 else mkPX (P \ Pc c) i (Q \ Pc c))" - | "PX P i Q \ Pc c = - (if c = 0 then Pc 0 else mkPX (P \ Pc c) i (Q \ Pc c))" - | "Pinj x P \ Pinj y Q = - (if x = y then mkPinj x (P \ Q) else - (if x > y then mkPinj y (Pinj (x-y) P \ Q) - else mkPinj x (Pinj (y - x) Q \ P)))" - | "Pinj x P \ PX Q y R = - (if x = 0 then P \ PX Q y R else - (if x = 1 then mkPX (Pinj x P \ Q) y (R \ P) - else mkPX (Pinj x P \ Q) y (R \ Pinj (x - 1) P)))" - | "PX P x R \ Pinj y Q = - (if y = 0 then PX P x R \ Q else - (if y = 1 then mkPX (Pinj y Q \ P) x (R \ Q) - else mkPX (Pinj y Q \ P) x (R \ Pinj (y - 1) Q)))" - | "PX P1 x P2 \ PX Q1 y Q2 = - mkPX (P1 \ Q1) (x + y) (P2 \ Q2) \ - (mkPX (P1 \ mkPinj 1 Q2) x (Pc 0) \ - (mkPX (Q1 \ mkPinj 1 P2) y (Pc 0)))" -by pat_completeness auto -termination by (relation "measure (\(x, y). size x + size y)") - (auto simp add: mkPinj_def split: pol.split) - -text {* Negation*} -primrec - neg :: "'a::{comm_ring} pol \ 'a pol" -where - "neg (Pc c) = Pc (-c)" - | "neg (Pinj i P) = Pinj i (neg P)" - | "neg (PX P x Q) = PX (neg P) x (neg Q)" - -text {* Substraction *} -definition - sub :: "'a::{comm_ring} pol \ 'a pol \ 'a pol" (infixl "\" 65) -where - "sub P Q = P \ neg Q" - -text {* Square for Fast Exponentation *} -primrec - sqr :: "'a::{comm_ring_1} pol \ 'a pol" -where - "sqr (Pc c) = Pc (c * c)" - | "sqr (Pinj i P) = mkPinj i (sqr P)" - | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \ - mkPX (Pc (1 + 1) \ A \ mkPinj 1 B) x (Pc 0)" - -text {* Fast Exponentation *} -fun - pow :: "nat \ 'a::{comm_ring_1} pol \ 'a pol" -where - "pow 0 P = Pc 1" - | "pow n P = (if even n then pow (n div 2) (sqr P) - else P \ pow (n div 2) (sqr P))" - -lemma pow_if: - "pow n P = - (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P) - else P \ pow (n div 2) (sqr P))" - by (cases n) simp_all - - -text {* Normalization of polynomial expressions *} - -primrec - norm :: "'a::{comm_ring_1} polex \ 'a pol" -where - "norm (Pol P) = P" - | "norm (Add P Q) = norm P \ norm Q" - | "norm (Sub P Q) = norm P \ norm Q" - | "norm (Mul P Q) = norm P \ norm Q" - | "norm (Pow P n) = pow n (norm P)" - | "norm (Neg P) = neg (norm P)" - -text {* mkPinj preserve semantics *} -lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)" - by (induct B) (auto simp add: mkPinj_def algebra_simps) - -text {* mkPX preserves semantics *} -lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)" - by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps) - -text {* Correctness theorems for the implemented operations *} - -text {* Negation *} -lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)" - by (induct P arbitrary: l) auto - -text {* Addition *} -lemma add_ci: "Ipol l (P \ Q) = Ipol l P + Ipol l Q" -proof (induct P Q arbitrary: l rule: add.induct) - case (6 x P y Q) - show ?case - proof (rule linorder_cases) - assume "x < y" - with 6 show ?case by (simp add: mkPinj_ci algebra_simps) - next - assume "x = y" - with 6 show ?case by (simp add: mkPinj_ci) - next - assume "x > y" - with 6 show ?case by (simp add: mkPinj_ci algebra_simps) - qed -next - case (7 x P Q y R) - have "x = 0 \ x = 1 \ x > 1" by arith - moreover - { assume "x = 0" with 7 have ?case by simp } - moreover - { assume "x = 1" with 7 have ?case by (simp add: algebra_simps) } - moreover - { assume "x > 1" from 7 have ?case by (cases x) simp_all } - ultimately show ?case by blast -next - case (8 P x R y Q) - have "y = 0 \ y = 1 \ y > 1" by arith - moreover - { assume "y = 0" with 8 have ?case by simp } - moreover - { assume "y = 1" with 8 have ?case by simp } - moreover - { assume "y > 1" with 8 have ?case by simp } - ultimately show ?case by blast -next - case (9 P1 x P2 Q1 y Q2) - show ?case - proof (rule linorder_cases) - assume a: "x < y" hence "EX d. d + x = y" by arith - with 9 a show ?case by (auto simp add: mkPX_ci power_add algebra_simps) - next - assume a: "y < x" hence "EX d. d + y = x" by arith - with 9 a show ?case by (auto simp add: power_add mkPX_ci algebra_simps) - next - assume "x = y" - with 9 show ?case by (simp add: mkPX_ci algebra_simps) - qed -qed (auto simp add: algebra_simps) - -text {* Multiplication *} -lemma mul_ci: "Ipol l (P \ Q) = Ipol l P * Ipol l Q" - by (induct P Q arbitrary: l rule: mul.induct) - (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add) - -text {* Substraction *} -lemma sub_ci: "Ipol l (P \ Q) = Ipol l P - Ipol l Q" - by (simp add: add_ci neg_ci sub_def) - -text {* Square *} -lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P" - by (induct P arbitrary: ls) - (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add) - -text {* Power *} -lemma even_pow:"even n \ pow n P = pow (n div 2) (sqr P)" - by (induct n) simp_all - -lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n" -proof (induct n arbitrary: P rule: nat_less_induct) - case (1 k) - show ?case - proof (cases k) - case 0 - then show ?thesis by simp - next - case (Suc l) - show ?thesis - proof cases - assume "even l" - then have "Suc l div 2 = l div 2" - by (simp add: nat_number even_nat_plus_one_div_two) - moreover - from Suc have "l < k" by simp - with 1 have "\P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp - moreover - note Suc `even l` even_nat_plus_one_div_two - ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow) - next - assume "odd l" - { - fix p - have "Ipol ls (sqr P) ^ (Suc l div 2) = Ipol ls P ^ Suc l" - proof (cases l) - case 0 - with `odd l` show ?thesis by simp - next - case (Suc w) - with `odd l` have "even w" by simp - have two_times: "2 * (w div 2) = w" - by (simp only: numerals even_nat_div_two_times_two [OF `even w`]) - have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)" - by (simp add: power_Suc) - then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2" - by (simp add: numerals) - with Suc show ?thesis - by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci - simp del: power_Suc) - qed - } with 1 Suc `odd l` show ?thesis by simp - qed - qed -qed - -text {* Normalization preserves semantics *} -lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)" - by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci) - -text {* Reflection lemma: Key to the (incomplete) decision procedure *} -lemma norm_eq: - assumes "norm P1 = norm P2" - shows "Ipolex l P1 = Ipolex l P2" -proof - - from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp - then show ?thesis by (simp only: norm_ci) -qed - - -use "comm_ring.ML" -setup CommRing.setup - -end diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Library/Library.thy Fri Oct 30 13:59:49 2009 +0100 @@ -11,7 +11,6 @@ Code_Char_chr Code_Integer Coinductive_List - Commutative_Ring Continuity ContNotDenum Countable diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/Library/comm_ring.ML --- a/src/HOL/Library/comm_ring.ML Fri Oct 30 01:32:06 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,109 +0,0 @@ -(* Author: Amine Chaieb - -Tactic for solving equalities over commutative rings. -*) - -signature COMM_RING = -sig - val comm_ring_tac : Proof.context -> int -> tactic - val setup : theory -> theory -end - -structure CommRing: COMM_RING = -struct - -(* The Cring exception for erronous uses of cring_tac *) -exception CRing of string; - -(* Zero and One of the commutative ring *) -fun cring_zero T = Const (@{const_name HOL.zero}, T); -fun cring_one T = Const (@{const_name HOL.one}, T); - -(* reification functions *) -(* add two polynom expressions *) -fun polT t = Type ("Commutative_Ring.pol", [t]); -fun polexT t = Type ("Commutative_Ring.polex", [t]); - -(* pol *) -fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t); -fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t); -fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t); - -(* polex *) -fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t); -fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t); -fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t); -fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t); -fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t); -fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t); - -(* reification of polynoms : primitive cring expressions *) -fun reif_pol T vs (t as Free _) = - let - val one = @{term "1::nat"}; - val i = find_index (fn t' => t' = t) vs - in if i = 0 - then pol_PX T $ (pol_Pc T $ cring_one T) - $ one $ (pol_Pc T $ cring_zero T) - else pol_Pinj T $ HOLogic.mk_nat i - $ (pol_PX T $ (pol_Pc T $ cring_one T) - $ one $ (pol_Pc T $ cring_zero T)) - end - | reif_pol T vs t = pol_Pc T $ t; - -(* reification of polynom expressions *) -fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) = - polex_add T $ reif_polex T vs a $ reif_polex T vs b - | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) = - polex_sub T $ reif_polex T vs a $ reif_polex T vs b - | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) = - polex_mul T $ reif_polex T vs a $ reif_polex T vs b - | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) = - polex_neg T $ reif_polex T vs a - | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) = - polex_pow T $ reif_polex T vs a $ n - | reif_polex T vs t = polex_pol T $ reif_pol T vs t; - -(* reification of the equation *) -val cr_sort = @{sort "comm_ring_1"}; - -fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) = - if Sign.of_sort thy (T, cr_sort) then - let - val fs = OldTerm.term_frees eq; - val cvs = cterm_of thy (HOLogic.mk_list T fs); - val clhs = cterm_of thy (reif_polex T fs lhs); - val crhs = cterm_of thy (reif_polex T fs rhs); - val ca = ctyp_of thy T; - in (ca, cvs, clhs, crhs) end - else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort) - | reif_eq _ _ = raise CRing "reif_eq: not an equation"; - -(* The cring tactic *) -(* Attention: You have to make sure that no t^0 is in the goal!! *) -(* Use simply rewriting t^0 = 1 *) -val cring_simps = - [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add}, - @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]]; - -fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) => - let - val thy = ProofContext.theory_of ctxt; - val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*) - addsimps cring_simps; - val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g) - val norm_eq_th = - simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq}) - in - cut_rules_tac [norm_eq_th] i - THEN (simp_tac cring_ss i) - THEN (simp_tac cring_ss i) - end); - -val setup = - Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac)) - "reflective decision procedure for equalities over commutative rings" #> - Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac)) - "method for proving algebraic properties (same as comm_ring)"; - -end; diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/ex/Codegenerator_Candidates.thy --- a/src/HOL/ex/Codegenerator_Candidates.thy Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Fri Oct 30 13:59:49 2009 +0100 @@ -9,7 +9,6 @@ AssocList Binomial Fset - Commutative_Ring Enum List_Prefix Nat_Infinity @@ -22,7 +21,7 @@ Tree While_Combinator Word - "~~/src/HOL/ex/Commutative_Ring_Complete" + "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete" "~~/src/HOL/ex/Records" begin diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/ex/Commutative_RingEx.thy --- a/src/HOL/ex/Commutative_RingEx.thy Fri Oct 30 01:32:06 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -(* ID: $Id$ - Author: Bernhard Haeupler -*) - -header {* Some examples demonstrating the comm-ring method *} - -theory Commutative_RingEx -imports Commutative_Ring -begin - -lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" -by comm_ring - -lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" -by comm_ring - -lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x" -by comm_ring - -lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3" -by comm_ring - -lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y" -by comm_ring - -lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c" -by comm_ring - -lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c" -by comm_ring - -lemma "(a::int)*b + a*c = a*(b+c)" -by comm_ring - -lemma "(a::int)^2 - b^2 = (a - b) * (a + b)" -by comm_ring - -lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)" -by comm_ring - -lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)" -by comm_ring - -lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)" -by comm_ring - -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 )" -by comm_ring - -end diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/ex/Commutative_Ring_Complete.thy --- a/src/HOL/ex/Commutative_Ring_Complete.thy Fri Oct 30 01:32:06 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,391 +0,0 @@ -(* Author: Bernhard Haeupler - -This theory is about of the relative completeness of method comm-ring -method. As long as the reified atomic polynomials of type 'a pol are -in normal form, the cring method is complete. -*) - -header {* Proof of the relative completeness of method comm-ring *} - -theory Commutative_Ring_Complete -imports Commutative_Ring -begin - -text {* Formalization of normal form *} -fun - isnorm :: "('a::{comm_ring}) pol \ bool" -where - "isnorm (Pc c) \ True" - | "isnorm (Pinj i (Pc c)) \ False" - | "isnorm (Pinj i (Pinj j Q)) \ False" - | "isnorm (Pinj 0 P) \ False" - | "isnorm (Pinj i (PX Q1 j Q2)) \ isnorm (PX Q1 j Q2)" - | "isnorm (PX P 0 Q) \ False" - | "isnorm (PX (Pc c) i Q) \ c \ 0 \ isnorm Q" - | "isnorm (PX (PX P1 j (Pc c)) i Q) \ c \ 0 \ isnorm (PX P1 j (Pc c)) \ isnorm Q" - | "isnorm (PX P i Q) \ isnorm P \ isnorm Q" - -(* Some helpful lemmas *) -lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False" -by(cases P, auto) - -lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False" -by(cases i, auto) - -lemma norm_Pinj:"isnorm (Pinj i Q) \ isnorm Q" -by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto - -lemma norm_PX2:"isnorm (PX P i Q) \ isnorm Q" -by(cases i, auto, cases P, auto, case_tac pol2, auto) - -lemma norm_PX1:"isnorm (PX P i Q) \ isnorm P" -by(cases i, auto, cases P, auto, case_tac pol2, auto) - -lemma mkPinj_cn:"\y~=0; isnorm Q\ \ isnorm (mkPinj y Q)" -apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split) -apply(case_tac nat, auto simp add: norm_Pinj_0_False) -by(case_tac pol, auto) (case_tac y, auto) - -lemma norm_PXtrans: - assumes A:"isnorm (PX P x Q)" and "isnorm Q2" - shows "isnorm (PX P x Q2)" -proof(cases P) - case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto) -next - case Pc from prems show ?thesis by(cases x, auto) -next - case Pinj from prems show ?thesis by(cases x, auto) -qed - -lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)" -proof(cases P) - case (PX p1 y p2) - from prems show ?thesis by(cases x, auto, cases p2, auto) -next - case Pc - from prems show ?thesis by(cases x, auto) -next - case Pinj - from prems show ?thesis by(cases x, auto) -qed - -text {* mkPX conserves normalizedness (@{text "_cn"}) *} -lemma mkPX_cn: - assumes "x \ 0" and "isnorm P" and "isnorm Q" - shows "isnorm (mkPX P x Q)" -proof(cases P) - case (Pc c) - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) -next - case (Pinj i Q) - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) -next - case (PX P1 y P2) - from prems have Y0:"y>0" by(cases y, auto) - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2]) - with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto) -qed - -text {* add conserves normalizedness *} -lemma add_cn:"isnorm P \ isnorm Q \ isnorm (P \ Q)" -proof(induct P Q rule: add.induct) - case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all) -next - case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all) -next - case (4 c P2 i Q2) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) -next - case (5 P2 i Q2 c) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) -next - case (6 x P2 y Q2) - from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False) - from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False) - have "x < y \ x = y \ x > y" by arith - moreover - { assume "xy" hence "EX d. x=d+y" by arith - then obtain d where "x=d+y".. - moreover - note prems Y0 - moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) - ultimately have ?case by (simp add: mkPinj_cn)} - ultimately show ?case by blast -next - case (7 x P2 Q2 y R) - have "x=0 \ (x = 1) \ (x > 1)" by arith - moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} - moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \ P2)" by simp - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) } - moreover - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } - ultimately show ?case by blast -next - case (8 Q2 y R x P2) - have "x = 0 \ x = 1 \ x > 1" by arith - moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} - moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \ P2)" by simp - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) } - moreover - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } - ultimately show ?case by blast -next - case (9 P1 x P2 Q1 y Q2) - from prems have Y0:"y>0" by(cases y, auto) - from prems have X0:"x>0" by(cases x, auto) - from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) - from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2]) - have "y < x \ x = y \ x < y" by arith - moreover - {assume sm1:"y < x" hence "EX d. x=d+y" by arith - then obtain d where sm2:"x=d+y".. - note prems NQ1 NP1 NP2 NQ2 sm1 sm2 - moreover - have "isnorm (PX P1 d (Pc 0))" - proof(cases P1) - case (PX p1 y p2) - with prems show ?thesis by(cases d, simp,cases p2, auto) - next case Pc from prems show ?thesis by(cases d, auto) - next case Pinj from prems show ?thesis by(cases d, auto) - qed - ultimately have "isnorm (P2 \ Q2)" "isnorm (PX P1 (x - y) (Pc 0) \ Q1)" by auto - with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)} - moreover - {assume "x=y" - from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \ Q2)" "isnorm (P1 \ Q1)" by auto - with Y0 prems have ?case by (simp add: mkPX_cn) } - moreover - {assume sm1:"x Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \ P1)" by auto - with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)} - ultimately show ?case by blast -qed simp - -text {* mul concerves normalizedness *} -lemma mul_cn :"isnorm P \ isnorm Q \ isnorm (P \ Q)" -proof(induct P Q rule: mul.induct) - case (2 c i P2) thus ?case - by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) -next - case (3 i P2 c) thus ?case - by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) -next - case (4 c P2 i Q2) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn) -next - case (5 P2 i Q2 c) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn) -next - case (6 x P2 y Q2) - have "x < y \ x = y \ x > y" by arith - moreover - { assume "x0" by (cases x, auto simp add: norm_Pinj_0_False) - moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) - ultimately have ?case by (simp add: mkPinj_cn)} - moreover - { assume "x=y" - moreover - from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) - moreover - note prems - moreover - ultimately have ?case by (simp add: mkPinj_cn) } - moreover - { assume "x>y" hence "EX d. x=d+y" by arith - then obtain d where "x=d+y".. - moreover - note prems - moreover - from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) - moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) - ultimately have ?case by (simp add: mkPinj_cn) } - ultimately show ?case by blast -next - case (7 x P2 Q2 y R) - from prems have Y0:"y>0" by(cases y, auto) - have "x=0 \ (x = 1) \ (x > 1)" by arith - moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} - moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \ P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) - with Y0 prems have ?case by (simp add: mkPX_cn)} - moreover - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) - moreover - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - moreover - from prems have "isnorm (Pinj x P2)" by(cases P2, auto) - moreover - note prems - ultimately have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" by auto - with Y0 X have ?case by (simp add: mkPX_cn)} - ultimately show ?case by blast -next - case (8 Q2 y R x P2) - from prems have Y0:"y>0" by(cases y, auto) - have "x=0 \ (x = 1) \ (x > 1)" by arith - moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} - moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \ P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) - with Y0 prems have ?case by (simp add: mkPX_cn) } - moreover - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) - moreover - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - moreover - from prems have "isnorm (Pinj x P2)" by(cases P2, auto) - moreover - note prems - ultimately have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" by auto - with Y0 X have ?case by (simp add: mkPX_cn) } - ultimately show ?case by blast -next - case (9 P1 x P2 Q1 y Q2) - from prems have X0:"x>0" by(cases x, auto) - from prems have Y0:"y>0" by(cases y, auto) - note prems - moreover - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) - moreover - from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) - ultimately have "isnorm (P1 \ Q1)" "isnorm (P2 \ Q2)" - "isnorm (P1 \ mkPinj 1 Q2)" "isnorm (Q1 \ mkPinj 1 P2)" - by (auto simp add: mkPinj_cn) - with prems X0 Y0 have - "isnorm (mkPX (P1 \ Q1) (x + y) (P2 \ Q2))" - "isnorm (mkPX (P1 \ mkPinj (Suc 0) Q2) x (Pc 0))" - "isnorm (mkPX (Q1 \ mkPinj (Suc 0) P2) y (Pc 0))" - by (auto simp add: mkPX_cn) - thus ?case by (simp add: add_cn) -qed(simp) - -text {* neg conserves normalizedness *} -lemma neg_cn: "isnorm P \ isnorm (neg P)" -proof (induct P) - case (Pinj i P2) - from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2]) - with prems show ?case by(cases P2, auto, cases i, auto) -next - case (PX P1 x P2) - from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) - with prems show ?case - proof(cases P1) - case (PX p1 y p2) - with prems show ?thesis by(cases x, auto, cases p2, auto) - next - case Pinj - with prems show ?thesis by(cases x, auto) - qed(cases x, auto) -qed(simp) - -text {* sub conserves normalizedness *} -lemma sub_cn:"isnorm p \ isnorm q \ isnorm (p \ q)" -by (simp add: sub_def add_cn neg_cn) - -text {* sqr conserves normalizizedness *} -lemma sqr_cn:"isnorm P \ isnorm (sqr P)" -proof(induct P) - case (Pinj i Q) - from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) -next - case (PX P1 x P2) - 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]) - with prems have - "isnorm (mkPX (Pc (1 + 1) \ P1 \ mkPinj (Suc 0) P2) x (Pc 0))" - and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" - by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) - thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) -qed simp - -text {* pow conserves normalizedness *} -lemma pow_cn:"isnorm P \ isnorm (pow n P)" -proof (induct n arbitrary: P rule: nat_less_induct) - case (1 k) - show ?case - proof (cases "k=0") - case False - then have K2:"k div 2 < k" by (cases k, auto) - from prems have "isnorm (sqr P)" by (simp add: sqr_cn) - with prems K2 show ?thesis - by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) - qed simp -qed - -end diff -r 37ec56ac3fd4 -r 9157d0f9f00e src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Fri Oct 30 13:59:49 2009 +0100 @@ -45,8 +45,6 @@ "Groebner_Examples", "MT", "Unification", - "Commutative_RingEx", - "Commutative_Ring_Complete", "Primrec", "Tarski", "Adder",