src/HOL/ex/Commutative_RingEx.thy
 author wenzelm Tue Sep 20 14:03:37 2005 +0200 (2005-09-20) changeset 17508 c84af7f39a6b parent 17388 495c799df31d permissions -rw-r--r--
tuned theory dependencies;
 wenzelm@17388 1 (* ID: \$Id\$ wenzelm@17388 2 Author: Bernhard Haeupler wenzelm@17388 3 *) wenzelm@17388 4 wenzelm@17388 5 header {* Some examples demonstrating the comm-ring method *} wenzelm@17388 6 chaieb@17378 7 theory Commutative_RingEx wenzelm@17508 8 imports Commutative_Ring chaieb@17378 9 begin chaieb@17378 10 chaieb@17378 11 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" chaieb@17378 12 by comm_ring chaieb@17378 13 chaieb@17378 14 lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" chaieb@17378 15 by comm_ring chaieb@17378 16 chaieb@17378 17 lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x" chaieb@17378 18 by comm_ring chaieb@17378 19 chaieb@17378 20 lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3" chaieb@17378 21 by comm_ring chaieb@17378 22 chaieb@17378 23 lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y" chaieb@17378 24 by comm_ring chaieb@17378 25 chaieb@17378 26 lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c" chaieb@17378 27 by comm_ring chaieb@17378 28 chaieb@17378 29 lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c" chaieb@17378 30 by comm_ring chaieb@17378 31 chaieb@17378 32 lemma "(a::int)*b + a*c = a*(b+c)" chaieb@17378 33 by comm_ring chaieb@17378 34 chaieb@17378 35 lemma "(a::int)^2 - b^2 = (a - b) * (a + b)" chaieb@17378 36 by comm_ring chaieb@17378 37 chaieb@17378 38 lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)" chaieb@17378 39 by comm_ring chaieb@17378 40 chaieb@17378 41 lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)" chaieb@17378 42 by comm_ring chaieb@17378 43 chaieb@17378 44 lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)" chaieb@17378 45 by comm_ring chaieb@17378 46 chaieb@17378 47 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 )" chaieb@17378 48 by comm_ring chaieb@17378 49 wenzelm@17388 50 end