src/HOL/ex/Groebner_Examples.thy
 changeset 36700 9b85b9d74b83 parent 36319 8feb2c4bef1a child 36714 ae84ddf03c58
```--- a/src/HOL/ex/Groebner_Examples.thy	Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Thu May 06 16:32:20 2010 +0200
@@ -10,14 +10,26 @@

subsection {* Basic examples *}

-schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})"
-  by sring_norm
+lemma
+  fixes x :: int
+  shows "x ^ 3 = x ^ 3"
+  apply (tactic {* ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+  by (rule refl)

-schematic_lemma "(x - (-2))^5 == ?X::int"
-  by sring_norm
+lemma
+  fixes x :: int
+  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x² + (80 * x + 32))))"
+  apply (tactic {* ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+  by (rule refl)

-schematic_lemma "(x - (-2))^5  * (y - 78) ^ 8 == ?X::int"
-  by sring_norm
+schematic_lemma
+  fixes x :: int
+  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X"
+  apply (tactic {* ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
+  by (rule refl)

lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
apply (simp only: power_Suc power_0)```