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".

Kind regards,

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