[isabelle] Metalogical "spec" not resolved automatically



Hello Isabelle-users,

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?

Thanks for any insights

Nicole

PS: This is the full Isabelle output with types, sorts and brackets activated:

goal (show, 2 subgoals):
1. (\<And>(N\<Colon>nat). (\<lbrakk>((0\<Colon>nat) < N); (P N) \<rbrakk> \<Longrightarrow> (P (Suc (0\<Colon>nat))))) 2. (\<And>(N\<Colon>nat). (\<lbrakk>((0\<Colon>nat) < N); (P N); ((0 \<Colon>nat) < M)\<rbrakk> \<Longrightarrow> (P M)))
variables:
  P :: (nat \<Rightarrow> bool)
  M :: nat

Attachment: PGP.sig
Description: Signierter Teil der Nachricht



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