Re: [isabelle] Quantifying over conditions



>
>  lemma "EX Q. Q --> p = 0"
>
> However, the lemma trivially holds (independently of rule1):  Q can be
> instantiated to False, or to "p = 0".

Hi Tjark,

Yes, quantifying over Q was the first thing that came to my mind. But
like you said, it trivially holds. So is there a way to formulate it
such that it isn't trivial? I want to check that if there is such a
precondition such that "p = 0". If there isn't, then the statement
should be evaluated to False.

Thanks
John

>
> Kind regards,
> Tjark
>
>





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