equal
deleted
inserted
replaced
812 done |
812 done |
813 |
813 |
814 |
814 |
815 lemma nForall_HDFilter: |
815 lemma nForall_HDFilter: |
816 "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)" |
816 "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)" |
817 (* Pay attention: is only admissible with chain-finite package to be added to |
817 unfolding not_Undef_is_Def [symmetric] |
818 adm test *) |
818 apply (induct y rule: Seq_induct) |
819 apply (rule_tac x="y" in Seq_induct) |
|
820 apply (simp add: Forall_def sforall_def) |
819 apply (simp add: Forall_def sforall_def) |
821 apply simp_all |
820 apply simp_all |
822 done |
821 done |
823 |
822 |
824 |
823 |