9 imports Groebner_Basis |
8 imports Groebner_Basis |
10 begin |
9 begin |
11 |
10 |
12 subsection {* Basic examples *} |
11 subsection {* Basic examples *} |
13 |
12 |
14 lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})" |
13 lemma "3 ^ 3 == (?X::'a::{number_ring})" |
15 by sring_norm |
14 by sring_norm |
16 |
15 |
17 lemma "(x - (-2))^5 == ?X::int" |
16 lemma "(x - (-2))^5 == ?X::int" |
18 by sring_norm |
17 by sring_norm |
19 |
18 |
20 lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int" |
19 lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int" |
21 by sring_norm |
20 by sring_norm |
22 |
21 |
23 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring,recpower})" |
22 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})" |
24 apply (simp only: power_Suc power_0) |
23 apply (simp only: power_Suc power_0) |
25 apply (simp only: comp_arith) |
24 apply (simp only: comp_arith) |
26 oops |
25 oops |
27 |
26 |
28 lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y" |
27 lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y" |
45 |
44 |
46 theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
45 theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
47 by algebra |
46 by algebra |
48 |
47 |
49 lemma |
48 lemma |
50 fixes x::"'a::{idom,recpower,number_ring}" |
49 fixes x::"'a::{idom,number_ring}" |
51 shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
50 shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
52 by algebra |
51 by algebra |
53 |
52 |
54 subsection {* Lemmas for Lagrange's theorem *} |
53 subsection {* Lemmas for Lagrange's theorem *} |
55 |
54 |
56 definition |
55 definition |
57 sq :: "'a::times => 'a" where |
56 sq :: "'a::times => 'a" where |
58 "sq x == x*x" |
57 "sq x == x*x" |
59 |
58 |
60 lemma |
59 lemma |
61 fixes x1 :: "'a::{idom,recpower,number_ring}" |
60 fixes x1 :: "'a::{idom,number_ring}" |
62 shows |
61 shows |
63 "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
62 "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
64 sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
63 sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
65 sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
64 sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
66 sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
65 sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
67 sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
66 sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
68 by (algebra add: sq_def) |
67 by (algebra add: sq_def) |
69 |
68 |
70 lemma |
69 lemma |
71 fixes p1 :: "'a::{idom,recpower,number_ring}" |
70 fixes p1 :: "'a::{idom,number_ring}" |
72 shows |
71 shows |
73 "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * |
72 "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * |
74 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) |
73 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) |
75 = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + |
74 = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + |
76 sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + |
75 sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + |