[isabelle] Quantifying over conditions


If I have a theory containing something like:

rule1: "a = 1 --> p = 0"

where a and p are naturals. Is there a good way to express that
whether there exists a condition such that if it is satisfied, then "p
= 0"? We know that there is because "a = 1" by rule1.

Thank you in advance.


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