[isabelle] nested locales


I am interested in building a new outer syntax in Isabelle to support
the following kind of construction within a theory:

program Search
  situation Init
     fixes n::nat and a::"nat => 'a" and x :: 'a

  situation Loop = Init +
    fixes i::nat
    assumes "i <= n"
    assumes "j < i ==> a i \not= x"

  situation Found = Loop +
    assumes "i < n"
    assumes "a i = x"

  situation NotFound = Loop +
    assumes "i = n"

  context Loop:
    transition to_Loop:
      assumes grd1: "i < n"
      assumes grd2: "a i \not= x"
      assumes inc: "i' = i + 1"
      shows Loop n a i'
      proof ...

  ... more transitions

The situations are variations of the existing Isabelle locales, with
some additional syntax to distinguish between different kind
of variables.

The program environment should support declaring
situations (locales), definitions, theorems, possibly also
variables. So in a way the program environment should
be also almost like a locale.

The information within a program environment will be
used to automatically generate a collection of
mutually recursive functions implementing the program
(in this case the program searches for an element
in an array).

I have been able to play with the Isabelle outer syntax,
but I could not figure out how to create a nested environment
as described above.

Any hints on where I should look to get started would be

The underlying construction of this approach is explained in

Preoteasa, Back, Eriksson. Verification and code generation for
invariant diagrams in Isabelle. Journal of Logical and Algebraic
Methods in Programming. Volume 84, Issue 1.

Best regards,

Viorel Preoteasa

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