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"
    by (simp add: test_def_def)
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.