src/HOL/ex/Groebner_Examples.thy
 changeset 36700 9b85b9d74b83 parent 36319 8feb2c4bef1a child 36714 ae84ddf03c58
```     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Wed May 05 16:53:21 2010 +0200
1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Thu May 06 16:32:20 2010 +0200
1.3 @@ -10,14 +10,26 @@
1.4
1.5  subsection {* Basic examples *}
1.6
1.7 -schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
1.8 -  by sring_norm
1.9 +lemma
1.10 +  fixes x :: int
1.11 +  shows "x ^ 3 = x ^ 3"
1.12 +  apply (tactic {* ALLGOALS (CONVERSION
1.13 +    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
1.14 +  by (rule refl)
1.15
1.16 -schematic_lemma "(x - (-2))^5 == ?X::int"
1.17 -  by sring_norm
1.18 +lemma
1.19 +  fixes x :: int
1.20 +  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x² + (80 * x + 32))))"
1.21 +  apply (tactic {* ALLGOALS (CONVERSION
1.22 +    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
1.23 +  by (rule refl)
1.24
1.25 -schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
1.26 -  by sring_norm
1.27 +schematic_lemma
1.28 +  fixes x :: int
1.29 +  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X"
1.30 +  apply (tactic {* ALLGOALS (CONVERSION
1.31 +    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
1.32 +  by (rule refl)
1.33
1.34  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
1.35    apply (simp only: power_Suc power_0)
```