eliminated list_all;
authorwenzelm
Sat Jun 20 20:17:29 2015 +0200 (2015-06-20)
changeset 605375398aa5a4df9
parent 60536 00db0d934a7d
child 60538 b9add7665d7a
eliminated list_all;
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jun 20 20:11:22 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jun 20 20:17:29 2015 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> list_all (\<lambda>c. c = 0) p"
     1.8 +lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> (\<forall>c \<in> set p. c = 0)"
     1.9    apply (induct p)
    1.10    apply simp
    1.11    apply (rule iffI)
    1.12 @@ -506,7 +506,7 @@
    1.13    apply auto
    1.14    done
    1.15  
    1.16 -lemma (in idom_char_0) poly_0: "list_all (\<lambda>c. c = 0) p \<Longrightarrow> poly p x = 0"
    1.17 +lemma (in idom_char_0) poly_0: "\<forall>c \<in> set p. c = 0 \<Longrightarrow> poly p x = 0"
    1.18    unfolding poly_zero[symmetric] by simp
    1.19  
    1.20  
    1.21 @@ -873,7 +873,7 @@
    1.22  
    1.23  text \<open>The degree of a polynomial.\<close>
    1.24  
    1.25 -lemma (in semiring_0) lemma_degree_zero: "list_all (\<lambda>c. c = 0) p \<longleftrightarrow> pnormalize p = []"
    1.26 +lemma (in semiring_0) lemma_degree_zero: "(\<forall>c \<in> set p. c = 0) \<longleftrightarrow> pnormalize p = []"
    1.27    by (induct p) auto
    1.28  
    1.29  lemma (in idom_char_0) degree_zero:
    1.30 @@ -916,7 +916,7 @@
    1.31        by (simp only: poly_minus poly_add algebra_simps) (simp add: algebra_simps)
    1.32      then have "poly ((c # cs) +++ -- (d # ds)) = poly []"
    1.33        by (simp add: fun_eq_iff)
    1.34 -    then have "c = d" and "list_all (\<lambda>x. x = 0) ((cs +++ -- ds))"
    1.35 +    then have "c = d" and "\<forall>x \<in> set (cs +++ -- ds). x = 0"
    1.36        unfolding poly_zero by (simp_all add: poly_minus_def algebra_simps)
    1.37      from this(2) have "poly (cs +++ -- ds) x = 0" for x
    1.38        unfolding poly_zero[symmetric] by simp
     2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:11:22 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:17:29 2015 +0200
     2.3 @@ -1217,7 +1217,7 @@
     2.4        then have "poly (polypoly' (?ts @ xs) p) = poly []"
     2.5          by auto
     2.6        then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
     2.7 -        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
     2.8 +        using poly_zero[where ?'a='a] by (simp add: polypoly'_def)
     2.9        with coefficients_head[of p, symmetric]
    2.10        have th0: "Ipoly (?ts @ xs) ?hd = 0"
    2.11          by simp