author wenzelm Sat Jun 20 20:17:29 2015 +0200 (2015-06-20) changeset 60537 5398aa5a4df9 parent 60536 00db0d934a7d child 60538 b9add7665d7a
eliminated list_all;
```     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.32      then have "poly ((c # cs) +++ -- (d # ds)) = poly []"
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)