Re: [isabelle] Recursive datatypes

See also the answer by Manuel on Stack Overflow:

Le 19 juin 2015 11:57:07 GMT+02:00, Diego Machado Dias <diegodias.m at> a Ãcrit :
>Hi all,
>I am wondering if is there a natural way of encoding in Isabelle a
>like this:
> Value = VInt int | ...
> Cmd = Skip | NonDeterministicChoice "Cmd set" | ...
>The motivation would be to give definition a few specification commands
>terms of Non deterministic choice, e.g.:
> Magic == NonDeterministicChoice {}
>Rely c r z = Defined using set compreehension and
>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
>"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
>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
>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
>would work or not. The immediate effect of using lists is that, instead
>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
>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
>"all elements (of interest) of Cmd" and "all values (of interest)".
>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,
>returns the correspondent NonDeterministicChoice fed with the list
>containing all the elements of the set given as argument, ordered by
>criteria, say lexicographic order. Then, rather than use
>"NonDeterministicChoice" when giving a semantics, I would give a
>for "NonDeterministicChoiceSet" and only use
>"NonDeterministicChoiceSet" in
>the theory.
>   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
>   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.