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



I think you are interpreting the formulas incorrectly. The first subgoal requires showing that if P(N) holds for some positive integer N, then P(1) holds. The second requires showing that if P(N) holds for some positive integer N, and M is also a positive integer, then P (M).

Larry Paulson


On 19 Oct 2005, at 09: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

If P holds for all arguments greater than zero, then it should hold for a fixed argument which is greater than zero. This is basically HOL's spec lemma, just with metalogical quantification instead of HOL quantification. But Isabelle refuses to accept this. What am I overlooking here?






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