src/HOL/ex/Groebner_Examples.thy
author wenzelm
Fri Aug 18 20:47:47 2017 +0200 (23 months ago)
changeset 66453 cc19f7ca2ed6
parent 61343 5b5656a63bd6
child 67006 b1278ed3cd46
permissions -rw-r--r--
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm@23273
     1
(*  Title:      HOL/ex/Groebner_Examples.thy
wenzelm@23273
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@23273
     3
*)
wenzelm@23273
     4
wenzelm@61343
     5
section \<open>Groebner Basis Examples\<close>
wenzelm@23273
     6
wenzelm@23273
     7
theory Groebner_Examples
wenzelm@66453
     8
imports HOL.Groebner_Basis
wenzelm@23273
     9
begin
wenzelm@23273
    10
wenzelm@61343
    11
subsection \<open>Basic examples\<close>
wenzelm@23273
    12
haftmann@36700
    13
lemma
haftmann@36700
    14
  fixes x :: int
traytel@55092
    15
  shows "x ^ 3 = x ^ 3"
wenzelm@61343
    16
  apply (tactic \<open>ALLGOALS (CONVERSION
wenzelm@61343
    17
    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context}))))\<close>)
haftmann@36700
    18
  by (rule refl)
wenzelm@23273
    19
haftmann@36700
    20
lemma
haftmann@36700
    21
  fixes x :: int
wenzelm@53015
    22
  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<^sup>2 + (80 * x + 32))))" 
wenzelm@61343
    23
  apply (tactic \<open>ALLGOALS (CONVERSION
wenzelm@61343
    24
    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context}))))\<close>)
haftmann@36700
    25
  by (rule refl)
wenzelm@23273
    26
wenzelm@61337
    27
schematic_goal
haftmann@36700
    28
  fixes x :: int
haftmann@36700
    29
  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
wenzelm@61343
    30
  apply (tactic \<open>ALLGOALS (CONVERSION
wenzelm@61343
    31
    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context}))))\<close>)
haftmann@36700
    32
  by (rule refl)
wenzelm@23273
    33
huffman@47108
    34
lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
wenzelm@23273
    35
  apply (simp only: power_Suc power_0)
haftmann@36714
    36
  apply (simp only: semiring_norm)
wenzelm@23273
    37
  oops
wenzelm@23273
    38
wenzelm@23273
    39
lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
wenzelm@23273
    40
  by algebra
wenzelm@23273
    41
wenzelm@23273
    42
lemma "(4::nat) + 4 = 3 + 5"
wenzelm@23273
    43
  by algebra
wenzelm@23273
    44
wenzelm@23273
    45
lemma "(4::int) + 0 = 4"
wenzelm@23273
    46
  apply algebra?
wenzelm@23273
    47
  by simp
wenzelm@55115
    48
wenzelm@23273
    49
lemma
wenzelm@53077
    50
  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
traytel@55092
    51
  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 +
traytel@55092
    52
    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
wenzelm@23273
    53
  using assms by algebra
wenzelm@23273
    54
wenzelm@23273
    55
lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
wenzelm@23273
    56
  by algebra
wenzelm@23273
    57
wenzelm@53015
    58
theorem "x* (x\<^sup>2 - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
wenzelm@23273
    59
  by algebra
wenzelm@23273
    60
wenzelm@23581
    61
lemma
wenzelm@53077
    62
  fixes x::"'a::idom"
wenzelm@53077
    63
  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
wenzelm@23581
    64
  by algebra
wenzelm@23273
    65
wenzelm@61343
    66
subsection \<open>Lemmas for Lagrange's theorem\<close>
wenzelm@23273
    67
wenzelm@23273
    68
definition
wenzelm@23273
    69
  sq :: "'a::times => 'a" where
wenzelm@23273
    70
  "sq x == x*x"
wenzelm@23273
    71
wenzelm@23273
    72
lemma
huffman@47108
    73
  fixes x1 :: "'a::{idom}"
wenzelm@23273
    74
  shows
wenzelm@23273
    75
  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
wenzelm@23273
    76
    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
wenzelm@23273
    77
    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
wenzelm@23273
    78
    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
wenzelm@23273
    79
    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
chaieb@23338
    80
  by (algebra add: sq_def)
wenzelm@23273
    81
wenzelm@23273
    82
lemma
huffman@47108
    83
  fixes p1 :: "'a::{idom}"
wenzelm@23273
    84
  shows
wenzelm@23273
    85
  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
wenzelm@23273
    86
   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
wenzelm@23273
    87
    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
wenzelm@23273
    88
      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
wenzelm@23273
    89
      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
wenzelm@23273
    90
      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
wenzelm@23273
    91
      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
wenzelm@23273
    92
      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
wenzelm@23273
    93
      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
wenzelm@23273
    94
      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
chaieb@23338
    95
  by (algebra add: sq_def)
wenzelm@23273
    96
wenzelm@23273
    97
wenzelm@61343
    98
subsection \<open>Colinearity is invariant by rotation\<close>
wenzelm@23273
    99
wenzelm@42463
   100
type_synonym point = "int \<times> int"
wenzelm@23273
   101
wenzelm@23273
   102
definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
wenzelm@23273
   103
  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
wenzelm@23273
   104
    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
wenzelm@23273
   105
wenzelm@23273
   106
lemma collinear_inv_rotation:
wenzelm@53015
   107
  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
wenzelm@23273
   108
  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
wenzelm@23273
   109
    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
chaieb@23338
   110
  using assms 
chaieb@23338
   111
  by (algebra add: collinear_def split_def fst_conv snd_conv)
wenzelm@23273
   112
chaieb@25255
   113
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"
wenzelm@26317
   114
  by algebra
chaieb@25255
   115
wenzelm@23273
   116
end