Email Gateway (Aug 18 2022 at 10:21): Email Gateway (Aug 18 2022 at 10:21):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
IN the attached theory file, (also copied below),
I get an error at
lemmas bin_nth_simps = bin_nth_0 bin_nth_Suc ;
the error being
*** Unknown theorem(s) "bin_nth_0"
*** At command "lemmas" (line 40 of
"/home/users/jeremy/isabelle/l4/bg.thy").
However when I delete the earlier line
lemmas fs = funpow_Suc ;
then this error does not occur.
Does anyone know why this might be?
Thanks for any help
Jeremy
PS this is with Isabelle_11-Feb-2007
file bg.thy follows
theory bg imports Main
begin
consts
(* corresponding operations analysing bins *)
bin_nth :: "int => nat => bool"
primrec
Z : "bin_nth w 0 = True"
Suc : "bin_nth w (Suc n) = False"
ML {*
use_legacy_bindings (the_context()) ;
*}
ML {*
val _ = ListPair.app bind_thm (["funpow_0", "funpow_Suc"],
thms "funpow.simps") ;
*}
(* if this is deleted then bin_nth_0 below is recognised
*)
lemmas fs = funpow_Suc ;
ML {*
val _ = ListPair.app bind_thm (["bin_nth_0", "bin_nth_Suc"],
bin_nth.simps) ;
*}
lemmas bin_nth_simps = bin_nth_0 bin_nth_Suc ;
end
bg.thy
Email Gateway (Aug 18 2022 at 10:22):From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
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
Email Gateway (Aug 18 2022 at 10:23):From: Makarius <makarius@sketis.net>
A general note to anybody working with recent development snapshots: with
the advent of ML antiquotations, the need for various legacy ML bindings
has disappeared altogether. See the NEWS file within the sources for
typical examples. This works uniformly for any kind of ML text
incorporated into an Isar theory. For example:
apply (tactic "ALLGOALS (force_tac @{clasimpset}")
No need to worry about changing dynamic contexts etc. Everything is
statically scoped (at compile-time) as expected.
Makarius
Last updated: May 03 2024 at 04:19 UTC