23273
|
1 |
(* Title: HOL/ex/Groebner_Examples.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Amine Chaieb, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Groebner Basis Examples *}
|
|
7 |
|
|
8 |
theory Groebner_Examples
|
|
9 |
imports Main
|
|
10 |
begin
|
|
11 |
|
|
12 |
subsection {* Basic examples *}
|
|
13 |
|
|
14 |
lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})"
|
|
15 |
by sring_norm
|
|
16 |
|
|
17 |
lemma "(x - (-2))^5 == ?X::int"
|
|
18 |
by sring_norm
|
|
19 |
|
|
20 |
lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int"
|
|
21 |
by sring_norm
|
|
22 |
|
|
23 |
lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring,recpower})"
|
|
24 |
apply (simp only: power_Suc power_0)
|
|
25 |
apply (simp only: comp_arith)
|
|
26 |
oops
|
|
27 |
|
|
28 |
lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
|
|
29 |
by algebra
|
|
30 |
|
|
31 |
lemma "(4::nat) + 4 = 3 + 5"
|
|
32 |
by algebra
|
|
33 |
|
|
34 |
lemma "(4::int) + 0 = 4"
|
|
35 |
apply algebra?
|
|
36 |
by simp
|
|
37 |
|
|
38 |
lemma
|
|
39 |
assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0"
|
|
40 |
shows "d^2*c^2 - 2*d*c*a*f + a^2*f^2 - e*d*b*c - e*b*a*f + a*e^2*c + f*d*b^2 = 0"
|
|
41 |
using assms by algebra
|
|
42 |
|
|
43 |
lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
|
|
44 |
by algebra
|
|
45 |
|
|
46 |
theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
|
|
47 |
by algebra
|
|
48 |
|
23331
|
49 |
lemma fixes x::"'a::{idom,recpower,number_ring}"
|
|
50 |
shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0"
|
|
51 |
by algebra
|
23273
|
52 |
|
|
53 |
subsection {* Lemmas for Lagrange's theorem *}
|
|
54 |
|
|
55 |
definition
|
|
56 |
sq :: "'a::times => 'a" where
|
|
57 |
"sq x == x*x"
|
|
58 |
|
|
59 |
lemma
|
|
60 |
fixes x1 :: "'a::{idom,recpower,number_ring}"
|
|
61 |
shows
|
|
62 |
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
|
|
63 |
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
|
|
64 |
sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) +
|
|
65 |
sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) +
|
|
66 |
sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
|
23338
|
67 |
by (algebra add: sq_def)
|
23273
|
68 |
|
|
69 |
lemma
|
|
70 |
fixes p1 :: "'a::{idom,recpower,number_ring}"
|
|
71 |
shows
|
|
72 |
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
|
|
73 |
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
|
|
74 |
= sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
|
|
75 |
sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
|
|
76 |
sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
|
|
77 |
sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
|
|
78 |
sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
|
|
79 |
sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
|
|
80 |
sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
|
|
81 |
sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
|
23338
|
82 |
by (algebra add: sq_def)
|
23273
|
83 |
|
|
84 |
|
|
85 |
subsection {* Colinearity is invariant by rotation *}
|
|
86 |
|
|
87 |
types point = "int \<times> int"
|
|
88 |
|
|
89 |
definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
|
|
90 |
"collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
|
|
91 |
((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
|
|
92 |
|
|
93 |
lemma collinear_inv_rotation:
|
|
94 |
assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1"
|
|
95 |
shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
|
|
96 |
(Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
|
23338
|
97 |
using assms
|
|
98 |
by (algebra add: collinear_def split_def fst_conv snd_conv)
|
23273
|
99 |
|
|
100 |
end
|