src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 58710 7216a10d69ba
parent 58310 91ea607a34d8
child 58776 95e58e04e534
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Oct 19 18:05:26 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Oct 20 07:45:58 2014 +0200
     1.3 @@ -789,20 +789,18 @@
     1.4        by (simp only: power_add power_one_right) simp
     1.5      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
     1.6        by (simp only: th)
     1.7 -    finally have ?case
     1.8 -    using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp
     1.9 +    finally have ?case unfolding numeral_2_eq_2 [symmetric]
    1.10 +    using odd_two_times_div_two_Suc [OF odd] by simp
    1.11    }
    1.12    moreover
    1.13    {
    1.14      assume even: "even (Suc n)"
    1.15 -    have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2"
    1.16 -      by arith
    1.17      from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
    1.18        by (simp add: Let_def)
    1.19 -    also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
    1.20 -      using "2.hyps" by (simp only: power_add) simp
    1.21 -    finally have ?case using even_nat_div_two_times_two[OF even]
    1.22 -      by (simp only: th)
    1.23 +    also have "\<dots> = (Ipoly bs p) ^ (2 * (Suc n div 2))"
    1.24 +      using "2.hyps" by (simp only: mult_2 power_add) simp
    1.25 +    finally have ?case using even_two_times_div_two [OF even]
    1.26 +      by simp
    1.27    }
    1.28    ultimately show ?case by blast
    1.29  qed
    1.30 @@ -823,8 +821,8 @@
    1.31      by simp
    1.32    from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n"
    1.33      by simp
    1.34 -  from dn on show ?case
    1.35 -    by (simp add: Let_def)
    1.36 +  from dn on show ?case by (simp, unfold Let_def) auto
    1.37 +    
    1.38  qed
    1.39  
    1.40  lemma polypow_norm: