equal
deleted
inserted
replaced
1543 by (induct xs) auto |
1543 by (induct xs) auto |
1544 |
1544 |
1545 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" |
1545 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" |
1546 by (induct xs) simp_all |
1546 by (induct xs) simp_all |
1547 |
1547 |
|
1548 lemmas empty_filter_conv = filter_empty_conv[THEN eq_iff_swap] |
|
1549 |
1548 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)" |
1550 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)" |
1549 proof (induct xs) |
1551 proof (induct xs) |
1550 case (Cons x xs) |
1552 case (Cons x xs) |
1551 then show ?case |
1553 then show ?case |
1552 using length_filter_le |
1554 using length_filter_le |