# [isabelle] Isar polymorphism problem

Hi all,
I'm trying to write a fairly simple proof in Isar, but I'm getting
stuck on a weird problem relating to polymorphism. Here's a minimized
example:
fun test_fun :: "'a \<Rightarrow> bool"
where
"test_fun a = True"
fun nat_fun :: "nat \<Rightarrow> bool"
where
"nat_fun a = True"
definition test_def :: "'a \<Rightarrow> bool"
where
"test_def \<equiv> \<lambda>a. True"
lemma one:
shows "\<exists>a. test_fun a"
(* fails *)
(* proof *)
(* show "test_fun a" *)
sorry
lemma two:
shows "\<exists>a. test_def a"
(* fails *)
(* proof *)
(* show "test_def a" *)
sorry
lemma three:
shows "\<exists>a. nat_fun a"
(* works *)
proof
show "nat_fun a" by simp
qed
On lemma one and two, I get errors like:
*** Failed to refine any pending goal
*** At command "show" (line 82 of "file.thy")
*** Local statement fails to refine any pending goal
*** Failed attempt to solve goal by exported rule:
*** test_fun a
*** At command "show" (line 82 of "file.thy")
Lemma three goes through fine.
Can someone help me understand what is going on? I would like to
prove lemma one or two. The problem is obviously related to
polymorphism, since lemma three goes through fine, but other than that
I am not sure what the problem is.
Thanks,
Edward

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