Email Gateway (Aug 18 2022 at 18:11): Email Gateway (Aug 18 2022 at 18:11):From: Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
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@ubuntu:~/test$ wget
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011_bundle_x86-linux.tar.gz
sternk@ubuntu:~/test$ tar xzf Isabelle2011_bundle_x86-linux.tar.gz
sternk@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@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
Email Gateway (Aug 18 2022 at 18:11):From: Alexander Krauss <krauss@in.tum.de>
This gets you into the internal system toplevel, which is not suitable
for most applications nowadays. Instead you want to write your ML
literally inside a theory context like this:
theory Scratch
imports Main
begin
ML {*
Datatype.get_info @{theory} @{type_name nat}
*}
end
Note the use of antiquotations @{theory} and @{type_name ...} to refer
to formal entities from the context.
See also Chapter 0 of the Implementation manual for basic examples, as
well as the Programming Tutorial (aka Cookbook).
Alex
Email Gateway (Aug 18 2022 at 18:15):From: Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
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 the
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.
Jonathan
Email Gateway (Aug 18 2022 at 18:16):From: Lukas Bulwahn <bulwahn@in.tum.de>
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
Last updated: Apr 24 2024 at 20:16 UTC