equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Groebner Basis Examples *} |
6 header {* Groebner Basis Examples *} |
7 |
7 |
8 theory Groebner_Examples |
8 theory Groebner_Examples |
9 imports Main |
9 imports Groebner_Basis |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Basic examples *} |
12 subsection {* Basic examples *} |
13 |
13 |
14 lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})" |
14 lemma "3 ^ 3 == (?X::'a::{number_ring,recpower})" |
96 shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s) |
96 shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s) |
97 (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)" |
97 (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)" |
98 using assms |
98 using assms |
99 by (algebra add: collinear_def split_def fst_conv snd_conv) |
99 by (algebra add: collinear_def split_def fst_conv snd_conv) |
100 |
100 |
|
101 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" |
|
102 apply algebra |
|
103 done |
|
104 |
101 end |
105 end |