Quelle Groebner_Examples.thy Sprache: Isabelle

(*  Title:      HOL/Examples/Groebner_Examples.thy
    Author:     Amine Chaieb, TU Muenchen
*)

section \<open>Groebner Basis Examples\<close>

theory Groebner_Examples
imports Main
begin

subsection \<open>Basic examples\<close>

lemma
  fixes x :: int
  shows "x ^ 3 = x ^ 3"
  apply (tactic \<open>ALLGOALS (CONVERSION
    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
  by (rule refl)

lemma
  fixes x :: int
  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<^sup>2 + (80 * x + 32))))"
  apply (tactic \<open>ALLGOALS (CONVERSION
    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
  by (rule refl)

schematic_goal
  fixes x :: int
  shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X"
  apply (tactic \<open>ALLGOALS (CONVERSION
    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
  by (rule refl)

lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
  apply (simp only: power_Suc power_0)
  apply (simp only: semiring_norm)
  oops

lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \ x = z + 3 \ x = - y"
  by algebra

lemma "(4::nat) + 4 = 3 + 5"
  by algebra

lemma "(4::int) + 0 = 4"
  apply algebra?
  by simp

lemma
  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
  shows "d\<^sup>2 * c\<^sup>2 - 2 * d * c * a * f + a\<^sup>2 * f\<^sup>2 - e * d * b * c - e * b * a * f +
    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
  using assms by algebra

lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \ (x = 3 \ x = -1)"
  by algebra

theorem "x* (x\<^sup>2 - x - 5) - 3 = (0::int) \ (x = 3 \ x = -1)"
  by algebra

lemma
  fixes x::"'a::idom"
  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \ x = 1 & y = 1 | x = 0 & y = 0"
  by algebra

subsection \<open>Lemmas for Lagrange's theorem\<close>

definition
  sq :: "'a::times => 'a" where
  "sq x == x*x"

lemma
  fixes x1 :: "'a::{idom}"
  shows
  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
  by (algebra add: sq_def)

lemma
  fixes p1 :: "'a::{idom}"
  shows
  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
  by (algebra add: sq_def)

subsection \<open>Colinearity is invariant by rotation\<close>

type_synonym point = "int \ int"

definition collinear ::"point \ point \ point \ bool" where
  "collinear \ \(Ax,Ay) (Bx,By) (Cx,Cy).
    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"

lemma collinear_inv_rotation:
  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
  using assms
  by (algebra add: collinear_def split_def fst_conv snd_conv)

lemma "\(d::int). a*y - a*x = n*d \ \u v. a*u + n*v = 1 \ \e. y - x = n*e"
  by algebra

end

quality97%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.