Re: [isabelle] Define records in ML?



* Thomas Bleher <bleher at informatik.uni-muenchen.de> [2006-11-10 10:19]:
> Greetings!
> Right now I'm looking at the ISM package (=Interacting State Machines) in
> order to make them work with Isabelle2005.
> This package defines its own syntax extensions and parses them into
> records (among lots of other things).
> 
> Now the CVS commit on "Mon May 3 21:22:17 2004 +0000", commit message
> > reimplementation of HOL records; only one type is created for
> > each record extension, instead of one type for each field. See NEWS.
> completely breaks this ML code.
> 
> I looked through the code and it seems like I have to reimplement most
> of it. I tried to figure out how to create and manipulate records in ML,
> but failed (HOL/Tools/record_package.ML is not very light reading).
> 
> Could someone give me some hints how to
> * create an Isabelle record in ML?
> * look up a field in a record by name and determine its type?
> 
> Or alternatively point me to some modules from which I could borrow
> code; I'd also welcome any documentation - I didn't find anything
> relevant.

OK, I continued to search for a solution for this, but I'm stuck.
I looked at
https://cgi.cse.unsw.edu.au/~formalmethods/wiki/isabelle/index.cgi/ProgrammingIsabelle
and came up with the following code to add a simple typedef:

ML {*
Context.>> (TypedefPackage.add_typedecls ([("test_type":bstring,[],NoSyn)]));
*}

However, the next command then fails with
  "exception TERM raised: Stale theory encountered: {<long list of theories>}"

Which magic incantation do I have to use to add a typedecl (or anything
else) to the current theory?
Any tips greatly appreciated!

While I'm at it, two other questions:
* There are a lot of seemingly definitions like add_inductive and
  add_inductive_i. What's the difference between them?
* Where should I post bugs and corrections I found?

Thanks for your time!
Thomas






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