Re: [isabelle] Metalogical "spec" not resolved automatically


On Wednesday 19 October 2005 08:20, Nicole Rauch wrote:
> I'm stuck with a logical problem and I don't see why it is not
> trivial to Isabelle. These are my two subgoals:
> 1. !! N. [| 0 < N; P N |] ==> P (Suc 0)
> 2. !! N. [| 0 < N; P N; 0 < M |] ==> P M

when Isabelle can't prove your goal, it may be able to disprove it:  both 
"quickcheck" and "refute" find simple counterexamples to your conjectures.

(As Larry already explained, the reason why these are not theorems is that the 
quantifier !! extends over the whole statement, not just over the premises of 
the implication).

Best regards,

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