Re: [isabelle] Get an ML value from a theory context



Hi Lukas,
thanks for your response. It seems like I'm doing something wrong in "setting
up" the Isabelle/ML level or maybe I'm not "within the HOL image"? - Anyways
this is what I'm currently doing. Maybe someone can point out the mistake(s) I'm
making:
 
sternk at ubuntu:~/test$ wget
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011_bundle_x86-linux.tar.gz
 sternk at ubuntu:~/test$ tar xzf Isabelle2011_bundle_x86-linux.tar.gz
 sternk at ubuntu:~/test$ ./Isabelle2011/bin/isabelle-process HOL
 > val it = (): unit
 val commit = fn: unit -> bool
 ML> Datatype_Data;
 Error-Value or constructor (Datatype_Data) has not been declared
 Found near Datatype_Data
 Static Errors
 
Jonathan
 

 Lukas Bulwahn <bulwahn at in.tum.de> hat am 4. August 2011 um 13:50 geschrieben:

 > On 08/03/2011 12:57 PM, Jonathan von Schroeder wrote:
 > > Hello all,
 > >   I'm currently working on a way to export Isabelle/HOL type definitions
 > >and
 > > their attached (user defined) axioms/theorems from a given theory in
 > > Isabelle. I
 > > have already managed to get this workign by simply going through all the
 > > constants, axioms and theorems present in the theories' context. But
 > > unluckily I
 > > currently get more axioms / theorems than I'm interested in, because thep,
 > > theorems automatically generated by
 > > http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/
 > > are not really "user generated" and thus do not foll within the scope of
 > > theorems I wish to export.
 > >
 > >   Thus I'd really like to have (in the top-level raw ML loop) access to the
 > > structure
 > > http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML
 > > (which lives in the context of
 > > http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Datatype.thy
 > > from what i can tell) to be able to figure out which theorems were
 > > generated by
 > > the Datatype-Tool. Does anybody have any suggestions on how to do this,
 > > because
 > > the Manual http://isabelle.in.tum.de/doc/implementation.pdf only mentions
 > > on
 > > page 11 that "... [the function factorial] is not yet accessible in the
 > > preceding paragraph, nor in a different theory that is independent from the
 > > current one in the import hierarchy", but I wasn't able to find any
 > > information
 > > on how to "get" access to it (or for that matter to any ml functions /
 > > structures defined within a theory). I'd greatly appreciate any information
 > > anybody can provide on this matter.
 > >
 > If you work properly on the Isabelle/ML level, within the HOL image, the
 > datatype package is loaded and set up.
 > Hence, you can then access the structure simply by its name "Datatype_Data".
 >
 >
 >
 > Lukas
 > >   Jonathan
 > >
 >




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