# Re: [isabelle] Isar polymorphism problem

```Hi.

Looks like Isabelle does not like the dangling free variable a that you
introduce. Using something else, e.g., undefined, does the job:

lemma one:
shows "\<exists>a. test_fun a"
proof
show "test_fun undefined"
by simp
qed

lemma two:
shows "\<exists>a. test_def a"
proof
show "test_def undefined"
qed

Cheers,
Peter

On So, 2014-04-27 at 12:01 -0400, Edward Schwartz wrote:
> 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.