src/HOL/ex/Commutative_RingEx.thy
 author wenzelm Wed Sep 14 22:08:08 2005 +0200 (2005-09-14) changeset 17388 495c799df31d parent 17378 105519771c67 child 17508 c84af7f39a6b permissions -rw-r--r--
 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 ``` chaieb@17378 ` 8` ```imports Main ``` 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 ```