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 MIf 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 NicolePS: 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
Description: Signierter Teil der Nachricht