*To*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Subject*: Re: [isabelle] can anyone explain this?*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Tue, 27 Mar 2007 15:33:03 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4608C388.6050203@rsise.anu.edu.au>*Organization*: Technische Universität München*References*: <044933B9-73BD-4075-8B6D-60DEFCC44D29@klebermass.de> <Pine.LNX.4.63.0701181922380.20738@atbroy100.informatik.tu-muenchen.de> <46087872.30008@rsise.anu.edu.au> <4608C388.6050203@rsise.anu.edu.au>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20050920

Jeremy Dawson wrote:

*** Unknown theorem(s) "bin_nth_0" *** At command "lemmas" (line 40 of "/home/users/jeremy/isabelle/l4/bg.thy"). [...] Does anyone know why this might be?

Dear Jeremy, the bind_thm function is legacy - it was intended for use in *.ML files attached to old-style theories. It relies on some imperative features of the theory datatype, which we unfortunately could not yet completely get rid of. More precisely, it destructively updates the theorem database, which is part of the theory associated with the theorem you want to store. If you interactively step through a new-style theory, Isabelle creates an intermediate theory for each command you execute (to be able to undo the command). If you now use bind_thm inside such a theory, the theory associated with the theorem to be stored is usually not the current one, but some older theory, so the result of this operation is (as you have noticed) completely random. Instead of using store_thm, you could rename the theorems in bin_nth.simps by lemmas bin_nth_0 = bin_nth.simps(1) lemmas bin_nth_Suc = bin_nth.simps(2) and then add the corresponding legacy ML bindings later by ML {* val bin_nth_0 = thm "bin_nth_0"; val bin_nth_Suc = thm "bin_nth_Suc"; *} Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**References**:**[isabelle] Isar and theories***From:*Jeremy Dawson

**[isabelle] can anyone explain this?***From:*Jeremy Dawson

- Previous by Date: [isabelle] Question to "lemmas" - instruction
- Next by Date: Re: [isabelle] malformed dependency
- Previous by Thread: [isabelle] can anyone explain this?
- Next by Thread: [isabelle] Question to "lemmas" - instruction
- Cl-isabelle-users March 2007 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