src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
changeset 49070 f00fee6d21d4
parent 48480 cb03acfae211
child 58889 5b7a9633cfa8
equal deleted inserted replaced
49069:c0e298d05026 49070:f00fee6d21d4
     5 theory Commutative_Ring_Ex
     5 theory Commutative_Ring_Ex
     6 imports "../Commutative_Ring"
     6 imports "../Commutative_Ring"
     7 begin
     7 begin
     8 
     8 
     9 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
     9 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
    10 by comm_ring
    10   by comm_ring
    11 
    11 
    12 lemma "((x::int) + y)^2  = x^2 + y^2 + 2*x*y"
    12 lemma "((x::int) + y)^2  = x^2 + y^2 + 2*x*y"
    13 by comm_ring
    13   by comm_ring
    14 
    14 
    15 lemma "((x::int) + y)^3  = x^3 + y^3 + 3*x^2*y + 3*y^2*x"
    15 lemma "((x::int) + y)^3  = x^3 + y^3 + 3*x^2*y + 3*y^2*x"
    16 by comm_ring
    16   by comm_ring
    17 
    17 
    18 lemma "((x::int) - y)^3  = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3"
    18 lemma "((x::int) - y)^3  = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3"
    19 by comm_ring
    19   by comm_ring
    20 
    20 
    21 lemma "((x::int) - y)^2  = x^2 + y^2 - 2*x*y"
    21 lemma "((x::int) - y)^2  = x^2 + y^2 - 2*x*y"
    22 by comm_ring
    22   by comm_ring
    23 
    23 
    24 lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c"
    24 lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c"
    25 by comm_ring
    25   by comm_ring
    26 
    26 
    27 lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c"
    27 lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c"
    28 by comm_ring
    28   by comm_ring
    29 
    29 
    30 lemma "(a::int)*b + a*c = a*(b+c)"
    30 lemma "(a::int)*b + a*c = a*(b+c)"
    31 by comm_ring
    31   by comm_ring
    32 
    32 
    33 lemma "(a::int)^2 - b^2 = (a - b) * (a + b)"
    33 lemma "(a::int)^2 - b^2 = (a - b) * (a + b)"
    34 by comm_ring
    34   by comm_ring
    35 
    35 
    36 lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)"
    36 lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)"
    37 by comm_ring
    37   by comm_ring
    38 
    38 
    39 lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)"
    39 lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)"
    40 by comm_ring
    40   by comm_ring
    41 
    41 
    42 lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)"
    42 lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)"
    43 by comm_ring
    43   by comm_ring
    44 
    44 
    45 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 )"
    45 lemma "(a::int)^10 - b^10 =
    46 by comm_ring
    46   (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)"
       
    47   by comm_ring
    47 
    48 
    48 end
    49 end