src/HOL/ex/Groebner_Examples.thy
author haftmann
Thu, 06 May 2010 23:37:07 +0200
changeset 36724 5779d9fbedd0
parent 36714 ae84ddf03c58
child 36753 5cf4e9128f22
permissions -rw-r--r--
xsymbolized
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/Groebner_Examples.thy
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     3
*)
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     4
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     5
header {* Groebner Basis Examples *}
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     6
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     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
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
     9
begin
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    10
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    11
subsection {* Basic examples *}
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    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
9b85b9d74b83 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents: 36319
diff changeset
    17
    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
9b85b9d74b83 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents: 36319
diff changeset
    18
  by (rule refl)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    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
5779d9fbedd0 xsymbolized
haftmann
parents: 36714
diff changeset
    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
9b85b9d74b83 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents: 36319
diff changeset
    24
    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
9b85b9d74b83 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents: 36319
diff changeset
    25
  by (rule refl)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    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
9b85b9d74b83 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents: 36319
diff changeset
    31
    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
9b85b9d74b83 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents: 36319
diff changeset
    32
  by (rule refl)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    33
31021
53642251a04f farewell to class recpower
haftmann
parents: 26317
diff changeset
    34
lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    35
  apply (simp only: power_Suc power_0)
36714
ae84ddf03c58 dropped duplicate comp_arith
haftmann
parents: 36700
diff changeset
    36
  apply (simp only: semiring_norm)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    37
  oops
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    38
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    39
lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    40
  by algebra
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    41
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    42
lemma "(4::nat) + 4 = 3 + 5"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    43
  by algebra
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    44
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    45
lemma "(4::int) + 0 = 4"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    46
  apply algebra?
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    47
  by simp
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    48
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    49
lemma
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    50
  assumes "a * x^2 + b * x + c = (0::int)" and "d * x^2 + e * x + f = 0"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    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"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    52
  using assms by algebra
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    53
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    54
lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    55
  by algebra
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    56
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    57
theorem "x* (x\<twosuperior> - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    58
  by algebra
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    59
23581
wenzelm
parents: 23338
diff changeset
    60
lemma
31021
53642251a04f farewell to class recpower
haftmann
parents: 26317
diff changeset
    61
  fixes x::"'a::{idom,number_ring}"
23581
wenzelm
parents: 23338
diff changeset
    62
  shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
wenzelm
parents: 23338
diff changeset
    63
  by algebra
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    64
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    65
subsection {* Lemmas for Lagrange's theorem *}
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    66
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    67
definition
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    68
  sq :: "'a::times => 'a" where
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    69
  "sq x == x*x"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    70
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    71
lemma
31021
53642251a04f farewell to class recpower
haftmann
parents: 26317
diff changeset
    72
  fixes x1 :: "'a::{idom,number_ring}"
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    73
  shows
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    74
  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    75
    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    76
    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    77
    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    78
    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
23338
3f1a453cb538 Tuned proofs : now use 'algebra ad: ...'
chaieb
parents: 23331
diff changeset
    79
  by (algebra add: sq_def)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    80
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    81
lemma
31021
53642251a04f farewell to class recpower
haftmann
parents: 26317
diff changeset
    82
  fixes p1 :: "'a::{idom,number_ring}"
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    83
  shows
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    84
  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    85
   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    86
    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    87
      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    88
      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    89
      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    90
      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    91
      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    92
      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    93
      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
23338
3f1a453cb538 Tuned proofs : now use 'algebra ad: ...'
chaieb
parents: 23331
diff changeset
    94
  by (algebra add: sq_def)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    95
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    96
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    97
subsection {* Colinearity is invariant by rotation *}
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    98
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
    99
types point = "int \<times> int"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   100
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   101
definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   102
  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   103
    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   104
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   105
lemma collinear_inv_rotation:
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   106
  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1"
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   107
  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   108
    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
23338
3f1a453cb538 Tuned proofs : now use 'algebra ad: ...'
chaieb
parents: 23331
diff changeset
   109
  using assms 
3f1a453cb538 Tuned proofs : now use 'algebra ad: ...'
chaieb
parents: 23331
diff changeset
   110
  by (algebra add: collinear_def split_def fst_conv snd_conv)
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   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
01a98fd72eae tuned proof;
wenzelm
parents: 25255
diff changeset
   113
  by algebra
25255
66ee31849d13 Added example for the ideal membership problem solved by algebra
chaieb
parents: 23581
diff changeset
   114
23273
c6d5ab154c7c Groebner Basis Examples.
wenzelm
parents:
diff changeset
   115
end