wenzelm@23273: (* Title: HOL/ex/Groebner_Examples.thy wenzelm@23273: Author: Amine Chaieb, TU Muenchen wenzelm@23273: *) wenzelm@23273: wenzelm@23273: header {* Groebner Basis Examples *} wenzelm@23273: wenzelm@23273: theory Groebner_Examples chaieb@25255: imports Groebner_Basis wenzelm@23273: begin wenzelm@23273: wenzelm@23273: subsection {* Basic examples *} wenzelm@23273: haftmann@36700: lemma haftmann@36700: fixes x :: int haftmann@36700: shows "x ^ 3 = x ^ 3" haftmann@36700: apply (tactic {* ALLGOALS (CONVERSION haftmann@36700: (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) haftmann@36700: by (rule refl) wenzelm@23273: haftmann@36700: lemma haftmann@36700: fixes x :: int haftmann@36700: shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x² + (80 * x + 32))))" haftmann@36700: apply (tactic {* ALLGOALS (CONVERSION haftmann@36700: (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) haftmann@36700: by (rule refl) wenzelm@23273: haftmann@36700: schematic_lemma haftmann@36700: fixes x :: int haftmann@36700: shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X" haftmann@36700: apply (tactic {* ALLGOALS (CONVERSION haftmann@36700: (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) haftmann@36700: by (rule refl) wenzelm@23273: haftmann@31021: lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})" wenzelm@23273: apply (simp only: power_Suc power_0) wenzelm@23273: apply (simp only: comp_arith) wenzelm@23273: oops wenzelm@23273: wenzelm@23273: lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \ x = z + 3 \ x = - y" wenzelm@23273: by algebra wenzelm@23273: wenzelm@23273: lemma "(4::nat) + 4 = 3 + 5" wenzelm@23273: by algebra wenzelm@23273: wenzelm@23273: lemma "(4::int) + 0 = 4" wenzelm@23273: apply algebra? wenzelm@23273: by simp wenzelm@23273: wenzelm@23273: lemma wenzelm@23273: assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0" wenzelm@23273: 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" wenzelm@23273: using assms by algebra wenzelm@23273: wenzelm@23273: lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \ (x = 3 \ x = -1)" wenzelm@23273: by algebra wenzelm@23273: wenzelm@23273: theorem "x* (x\ - x - 5) - 3 = (0::int) \ (x = 3 \ x = -1)" wenzelm@23273: by algebra wenzelm@23273: wenzelm@23581: lemma haftmann@31021: fixes x::"'a::{idom,number_ring}" wenzelm@23581: shows "x^2*y = x^2 & x*y^2 = y^2 \ x=1 & y=1 | x=0 & y=0" wenzelm@23581: by algebra wenzelm@23273: wenzelm@23273: subsection {* Lemmas for Lagrange's theorem *} wenzelm@23273: wenzelm@23273: definition wenzelm@23273: sq :: "'a::times => 'a" where wenzelm@23273: "sq x == x*x" wenzelm@23273: wenzelm@23273: lemma haftmann@31021: fixes x1 :: "'a::{idom,number_ring}" wenzelm@23273: shows wenzelm@23273: "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = wenzelm@23273: sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + wenzelm@23273: sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + wenzelm@23273: sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + wenzelm@23273: sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" chaieb@23338: by (algebra add: sq_def) wenzelm@23273: wenzelm@23273: lemma haftmann@31021: fixes p1 :: "'a::{idom,number_ring}" wenzelm@23273: shows wenzelm@23273: "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * wenzelm@23273: (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) wenzelm@23273: = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + wenzelm@23273: sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + wenzelm@23273: sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) + wenzelm@23273: sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + wenzelm@23273: sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + wenzelm@23273: sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + wenzelm@23273: sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + wenzelm@23273: sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" chaieb@23338: by (algebra add: sq_def) wenzelm@23273: wenzelm@23273: wenzelm@23273: subsection {* Colinearity is invariant by rotation *} wenzelm@23273: wenzelm@23273: types point = "int \ int" wenzelm@23273: wenzelm@23273: definition collinear ::"point \ point \ point \ bool" where wenzelm@23273: "collinear \ \(Ax,Ay) (Bx,By) (Cx,Cy). wenzelm@23273: ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))" wenzelm@23273: wenzelm@23273: lemma collinear_inv_rotation: wenzelm@23273: assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\ + s\ = 1" wenzelm@23273: shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s) wenzelm@23273: (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)" chaieb@23338: using assms chaieb@23338: by (algebra add: collinear_def split_def fst_conv snd_conv) wenzelm@23273: chaieb@25255: lemma "EX (d::int). a*y - a*x = n*d \ EX u v. a*u + n*v = 1 \ EX e. y - x = n*e" wenzelm@26317: by algebra chaieb@25255: wenzelm@23273: end