src/HOL/ex/Groebner_Examples.thy
author wenzelm
Tue Mar 18 20:33:33 2008 +0100 (2008-03-18)
changeset 26317 01a98fd72eae
parent 25255 66ee31849d13
child 31021 53642251a04f
permissions -rw-r--r--
tuned proof;
     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 Groebner_Basis
    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 
    49 lemma
    50   fixes x::"'a::{idom,recpower,number_ring}"
    51   shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
    52   by algebra
    53 
    54 subsection {* Lemmas for Lagrange's theorem *}
    55 
    56 definition
    57   sq :: "'a::times => 'a" where
    58   "sq x == x*x"
    59 
    60 lemma
    61   fixes x1 :: "'a::{idom,recpower,number_ring}"
    62   shows
    63   "(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)  +
    65     sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    66     sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    67     sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    68   by (algebra add: sq_def)
    69 
    70 lemma
    71   fixes p1 :: "'a::{idom,recpower,number_ring}"
    72   shows
    73   "(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)
    75     = 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) +
    77       sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    78       sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    79       sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    80       sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    81       sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    82       sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    83   by (algebra add: sq_def)
    84 
    85 
    86 subsection {* Colinearity is invariant by rotation *}
    87 
    88 types point = "int \<times> int"
    89 
    90 definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
    91   "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
    92     ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
    93 
    94 lemma collinear_inv_rotation:
    95   assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1"
    96   shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
    97     (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
    98   using assms 
    99   by (algebra add: collinear_def split_def fst_conv snd_conv)
   100 
   101 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"
   102   by algebra
   103 
   104 end