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