*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isar polymorphism problem*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 28 Apr 2014 14:38:32 +0200*In-reply-to*: <CAHPz_Mr8KgKU4966DTROET1AgtJs-gDfU-YQ=AVNZUzcDRxz6Q@mail.gmail.com>*References*: <CAHPz_Mr8KgKU4966DTROET1AgtJs-gDfU-YQ=AVNZUzcDRxz6Q@mail.gmail.com>

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 >

**References**:**[isabelle] Isar polymorphism problem***From:*Edward Schwartz

- Previous by Date: [isabelle] Excluding theories from the session_graph output
- Next by Date: [isabelle] ISABELLE WORKSHOP 2014 Call for submissions (Reminder)
- Previous by Thread: [isabelle] Isar polymorphism problem
- Next by Thread: Re: [isabelle] Isar polymorphism problem
- Cl-isabelle-users April 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list