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?

No. Try

  lemma length_from_ex_unique:
    "(EX! x : set xs. P x) ==> length (filter P xs) = 1"
  nitpick

Best regards,
Tjark







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.