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)