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".
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.
> Kind regards,
This archive was generated by a fusion of
Pipermail (Mailman edition) and