src/HOL/ex/Commutative_RingEx.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 17508 c84af7f39a6b
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
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