src/HOL/Decision_Procs/Polynomial_List.thy
changeset 36350 bc7982c54e37
parent 35028 108662d50512
child 37598 893dcabf0c04
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Apr 26 11:34:17 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Apr 26 11:34:19 2010 +0200
     1.3 @@ -283,11 +283,11 @@
     1.4  apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
     1.5  apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
     1.6  apply (drule_tac x = "Suc (length q)" in spec)
     1.7 -apply (auto simp add: ring_simps)
     1.8 +apply (auto simp add: field_simps)
     1.9  apply (drule_tac x = xa in spec)
    1.10 -apply (clarsimp simp add: ring_simps)
    1.11 +apply (clarsimp simp add: field_simps)
    1.12  apply (drule_tac x = m in spec)
    1.13 -apply (auto simp add:ring_simps)
    1.14 +apply (auto simp add:field_simps)
    1.15  done
    1.16  lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard]
    1.17  
    1.18 @@ -327,7 +327,7 @@
    1.19  apply (drule_tac x = "a#i" in spec)
    1.20  apply (auto simp only: poly_mult List.list.size)
    1.21  apply (drule_tac x = xa in spec)
    1.22 -apply (clarsimp simp add: ring_simps)
    1.23 +apply (clarsimp simp add: field_simps)
    1.24  done
    1.25  
    1.26  lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
    1.27 @@ -413,7 +413,7 @@
    1.28  by (auto intro!: ext)
    1.29  
    1.30  lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
    1.31 -by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult)
    1.32 +by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
    1.33  
    1.34  lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
    1.35  by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)