Re: [isabelle] Quantifying over conditions
On Mon, 2011-02-07 at 07:37 +0000, John Munroe wrote:
> 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.
I am not sure I understand your question. Working in higher-order
logic, you can quantify over truth values/predicates:
lemma "EX Q. Q --> p = 0"
However, the lemma trivially holds (independently of rule1): Q can be
instantiated to False, or to "p = 0".
This archive was generated by a fusion of
Pipermail (Mailman edition) and