equal
deleted
inserted
replaced
|
1 (* $Id$ *) |
|
2 theory Commutative_RingEx |
|
3 imports Main |
|
4 begin |
|
5 |
|
6 (* Some examples demonstrating the comm_ring method *) |
|
7 |
|
8 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
|
9 by comm_ring |
|
10 |
|
11 lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" |
|
12 by comm_ring |
|
13 |
|
14 lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x" |
|
15 by comm_ring |
|
16 |
|
17 lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3" |
|
18 by comm_ring |
|
19 |
|
20 lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y" |
|
21 by comm_ring |
|
22 |
|
23 lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c" |
|
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 + a*c = a*(b+c)" |
|
30 by comm_ring |
|
31 |
|
32 lemma "(a::int)^2 - b^2 = (a - b) * (a + b)" |
|
33 by comm_ring |
|
34 |
|
35 lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)" |
|
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)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)" |
|
42 by comm_ring |
|
43 |
|
44 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 by comm_ring |
|
46 |
|
47 end |