equal
deleted
inserted
replaced
17 (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
17 (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
18 by (rule refl) |
18 by (rule refl) |
19 |
19 |
20 lemma |
20 lemma |
21 fixes x :: int |
21 fixes x :: int |
22 shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))" |
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 |
23 apply (tactic {* ALLGOALS (CONVERSION |
24 (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
24 (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *}) |
25 by (rule refl) |
25 by (rule refl) |
26 |
26 |
27 schematic_lemma |
27 schematic_lemma |
52 using assms by algebra |
52 using assms by algebra |
53 |
53 |
54 lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)" |
54 lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)" |
55 by algebra |
55 by algebra |
56 |
56 |
57 theorem "x* (x\<twosuperior> - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
57 theorem "x* (x\<^sup>2 - x - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)" |
58 by algebra |
58 by algebra |
59 |
59 |
60 lemma |
60 lemma |
61 fixes x::"'a::{idom}" |
61 fixes x::"'a::{idom}" |
62 shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
62 shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow> x=1 & y=1 | x=0 & y=0" |
101 definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where |
101 definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where |
102 "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy). |
102 "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy). |
103 ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))" |
103 ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))" |
104 |
104 |
105 lemma collinear_inv_rotation: |
105 lemma collinear_inv_rotation: |
106 assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1" |
106 assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1" |
107 shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s) |
107 shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s) |
108 (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)" |
108 (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)" |
109 using assms |
109 using assms |
110 by (algebra add: collinear_def split_def fst_conv snd_conv) |
110 by (algebra add: collinear_def split_def fst_conv snd_conv) |
111 |
111 |