[isabelle] can anyone explain this?




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


(* 
    ID:         $Id: BinGeneral.thy 2667 2006-09-26 07:15:00Z gklein $
    Author:     Jeremy Dawson, NICTA

*) 

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




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