[isabelle] Recursive datatypes



Hi all,

I am wondering if is there a natural way of encoding in Isabelle a grammar
like this:

 Value = VInt int | ...
 Cmd = Skip | NonDeterministicChoice "Cmd set" | ...

The motivation would be to give definition a few specification commands in
terms of Non deterministic choice, e.g.:

 Magic == NonDeterministicChoice {}
 Rely c r z = Defined using set compreehension and NonDeterministicChoice

Isabelle complains about the recursive occurrence of type "Cmd" in "Cmd
set" when I try to represent the grammar through a datatype, i.e.:

Unsupported recursive occurrence of type "Cmd" via type constructor
"Set.set" in type expression "Cmd set". Use the "bnf" command to register
"Set.set" as a bounded natural functor to allow nested (co)recursion
through it

Looking the Isabelle error message when I use set, I couldn't figure out
how to register the bounded natural functor for the type 'set' in this
context, so I decided to try two speculative solutions.

*Speculative solution*

*Option 1*

Instead of use set, if I use an inductively defined datatype such as list,
Isabelle does not complain e.g.

datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...

Lists are not the right abstraction here, but I give it a go to see if it
would work or not. The immediate effect of using lists is that, instead of
use set comprehension I need to use sequence filtering, and the problem
then become to come up with two lists: one containing all elements of *Cmd*,
and other containing all elements of *Value*.

I declared two uninterpreted constants:

consts Values :: "Value list"
consts Programs :: "Cmd list"

Because lists are finite, it makes more sense to explain the constants as
"all elements (of interest) of Cmd" and "all values (of interest)". Say,
all elements of interest are those that can be represented in the memory of
a computer.

*Option 2*

If I need to use consts, then I could just declare
NonDeterministicChoiceSet as

consts NonDeterministicChoiceSet :: "Cmd set â Cmd"

and explain it (informally) as a function that receives a set of Cmd, and
returns the correspondent NonDeterministicChoice fed with the list
containing all the elements of the set given as argument, ordered by some
criteria, say lexicographic order. Then, rather than use
"NonDeterministicChoice" when giving a semantics, I would give a semantics
for "NonDeterministicChoiceSet" and only use "NonDeterministicChoiceSet" in
the theory.

*Questions*

   1. Do these modelling make sense if my intention is to capture the
   grammar of Cmd and give an operational semantics to the constructors of Cmd?
   2. Is there a better way of represent that grammar?
   3. Is Isabelle the appropriated theorem-prover if I want to represent
   that grammar? I experimented define this grammar in Z/Eves using free
   types, and it raised no complains.


Thanks in advance for any suggestions,

Diego Dias



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