Re: [isabelle] can anyone explain this?



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.