[isabelle] nested locales



Hello,

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

program Search
begin
  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:
  begin
    transition to_Loop:
      assumes grd1: "i < n"
      assumes grd2: "a i \not= x"
      assumes inc: "i' = i + 1"
      shows Loop n a i'
      proof ...
  end

  ... more transitions
end

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
appreciated.

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.