author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 47108 | 2a1953f0d20d |
child 53015 | a1119cf551e8 |
permissions | -rw-r--r-- |
23273 | 1 |
(* Title: HOL/ex/Groebner_Examples.thy |
2 |
Author: Amine Chaieb, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Groebner Basis Examples *} |
|
6 |
||
7 |
theory Groebner_Examples |
|
25255
66ee31849d13
Added example for the ideal membership problem solved by algebra
chaieb
parents:
23581
diff
changeset
|
8 |
imports Groebner_Basis |
23273 | 9 |
begin |
10 |
||
11 |
subsection {* Basic examples *} |
|
12 |
||
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
13 |
lemma |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
14 |
fixes x :: int |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
15 |
shows "x ^ 3 = x ^ 3" |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
16 |
apply (tactic {* ALLGOALS (CONVERSION |
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36724
diff
changeset
|
17 |
(Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
18 |
by (rule refl) |
23273 | 19 |
|
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
20 |
lemma |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
21 |
fixes x :: int |
36724 | 22 |
shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))" |
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
23 |
apply (tactic {* ALLGOALS (CONVERSION |
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36724
diff
changeset
|
24 |
(Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
25 |
by (rule refl) |
23273 | 26 |
|
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
27 |
schematic_lemma |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
28 |
fixes x :: int |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
29 |
shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X" |
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
30 |
apply (tactic {* ALLGOALS (CONVERSION |
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36724
diff
changeset
|
31 |
(Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
36319
diff
changeset
|
32 |
by (rule refl) |
23273 | 33 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
42463
diff
changeset
|
34 |
lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})" |
23273 | 35 |
apply (simp only: power_Suc power_0) |
36714 | 36 |
apply (simp only: semiring_norm) |
23273 | 37 |
oops |
38 |
||
39 |
lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y" |
|
40 |
by algebra |
|
41 |
||
42 |
lemma "(4::nat) + 4 = 3 + 5" |
|
43 |
by algebra |
|
44 |
||
45 |
lemma "(4::int) + 0 = 4" |
|
46 |
apply algebra? |
|
47 |
by simp |
|
48 |
||
49 |
lemma |
|
50 |
assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0" |
|
51 |
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" |
|
52 |
using assms by algebra |
|
53 |
||
54 |
lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)" |
|
55 |
by algebra |
|
56 |
||
57 |
theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
|
58 |
by algebra |
|
59 |
||
23581 | 60 |
lemma |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
42463
diff
changeset
|
61 |
fixes x::"'a::{idom}" |
23581 | 62 |
shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
63 |
by algebra |
|
23273 | 64 |
|
65 |
subsection {* Lemmas for Lagrange's theorem *} |
|
66 |
||
67 |
definition |
|
68 |
sq :: "'a::times => 'a" where |
|
69 |
"sq x == x*x" |
|
70 |
||
71 |
lemma |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
42463
diff
changeset
|
72 |
fixes x1 :: "'a::{idom}" |
23273 | 73 |
shows |
74 |
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
|
75 |
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
|
76 |
sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
|
77 |
sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
|
78 |
sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
|
23338 | 79 |
by (algebra add: sq_def) |
23273 | 80 |
|
81 |
lemma |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
42463
diff
changeset
|
82 |
fixes p1 :: "'a::{idom}" |
23273 | 83 |
shows |
84 |
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * |
|
85 |
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) |
|
86 |
= sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + |
|
87 |
sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + |
|
88 |
sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) + |
|
89 |
sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + |
|
90 |
sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + |
|
91 |
sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + |
|
92 |
sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + |
|
93 |
sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" |
|
23338 | 94 |
by (algebra add: sq_def) |
23273 | 95 |
|
96 |
||
97 |
subsection {* Colinearity is invariant by rotation *} |
|
98 |
||
42463 | 99 |
type_synonym point = "int \<times> int" |
23273 | 100 |
|
101 |
definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where |
|
102 |
"collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy). |
|
103 |
((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))" |
|
104 |
||
105 |
lemma collinear_inv_rotation: |
|
106 |
assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1" |
|
107 |
shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s) |
|
108 |
(Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)" |
|
23338 | 109 |
using assms |
110 |
by (algebra add: collinear_def split_def fst_conv snd_conv) |
|
23273 | 111 |
|
25255
66ee31849d13
Added example for the ideal membership problem solved by algebra
chaieb
parents:
23581
diff
changeset
|
112 |
lemma "EX (d::int). a*y - a*x = n*d \<Longrightarrow> EX u v. a*u + n*v = 1 \<Longrightarrow> EX e. y - x = n*e" |
26317 | 113 |
by algebra |
25255
66ee31849d13
Added example for the ideal membership problem solved by algebra
chaieb
parents:
23581
diff
changeset
|
114 |
|
23273 | 115 |
end |