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