Re: [isabelle] Uniqueness quantification
On Fri, 2012-07-27 at 12:02 +0100, John Munroe wrote:
> > lemma ex_unique_from_length:
> > "length (filter P xs) = 1 ==> (EX! x : set xs. P x)"
> Right, but how come the reverse doesn't hold? If there's exactly one
> of the predicates returning true, then isn't the length of the
> filtered list one?
"(EX! x : set xs. P x) ==> length (filter P xs) = 1"
This archive was generated by a fusion of
Pipermail (Mailman edition) and