summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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: