[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.