src/HOL/ex/Groebner_Examples.thy
changeset 23273 c6d5ab154c7c
child 23331 da040caa0596
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Tue Jun 05 22:47:49 2007 +0200
     1.3 @@ -0,0 +1,97 @@
     1.4 +(*  Title:      HOL/ex/Groebner_Examples.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Groebner Basis Examples *}
    1.10 +
    1.11 +theory Groebner_Examples
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +subsection {* Basic examples *}
    1.16 +
    1.17 +lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})"
    1.18 +  by sring_norm
    1.19 +
    1.20 +lemma "(x - (-2))^5 == ?X::int"
    1.21 +  by sring_norm
    1.22 +
    1.23 +lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
    1.24 +  by sring_norm
    1.25 +
    1.26 +lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring,recpower})"
    1.27 +  apply (simp only: power_Suc power_0)
    1.28 +  apply (simp only: comp_arith)
    1.29 +  oops
    1.30 +
    1.31 +lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
    1.32 +  by algebra
    1.33 +
    1.34 +lemma "(4::nat) + 4 = 3 + 5"
    1.35 +  by algebra
    1.36 +
    1.37 +lemma "(4::int) + 0 = 4"
    1.38 +  apply algebra?
    1.39 +  by simp
    1.40 +
    1.41 +lemma
    1.42 +  assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0"
    1.43 +  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"
    1.44 +  using assms by algebra
    1.45 +
    1.46 +lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
    1.47 +  by algebra
    1.48 +
    1.49 +theorem "x* (x\<twosuperior> - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
    1.50 +  by algebra
    1.51 +
    1.52 +
    1.53 +subsection {* Lemmas for Lagrange's theorem *}
    1.54 +
    1.55 +definition
    1.56 +  sq :: "'a::times => 'a" where
    1.57 +  "sq x == x*x"
    1.58 +
    1.59 +lemma
    1.60 +  fixes x1 :: "'a::{idom,recpower,number_ring}"
    1.61 +  shows
    1.62 +  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    1.63 +    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    1.64 +    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    1.65 +    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    1.66 +    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    1.67 +  unfolding sq_def by algebra
    1.68 +
    1.69 +lemma
    1.70 +  fixes p1 :: "'a::{idom,recpower,number_ring}"
    1.71 +  shows
    1.72 +  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
    1.73 +   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
    1.74 +    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
    1.75 +      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    1.76 +      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    1.77 +      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    1.78 +      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    1.79 +      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    1.80 +      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    1.81 +      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    1.82 +  unfolding sq_def by algebra
    1.83 +
    1.84 +
    1.85 +subsection {* Colinearity is invariant by rotation *}
    1.86 +
    1.87 +types point = "int \<times> int"
    1.88 +
    1.89 +definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
    1.90 +  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
    1.91 +    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
    1.92 +
    1.93 +lemma collinear_inv_rotation:
    1.94 +  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1"
    1.95 +  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
    1.96 +    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
    1.97 +  using assms unfolding collinear_def split_def fst_conv snd_conv
    1.98 +  by algebra
    1.99 +
   1.100 +end