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:
```