[isabelle] nested locales
I am interested in building a new outer syntax in Isabelle to support
the following kind of construction within a theory:
fixes n::nat and a::"nat => 'a" and x :: 'a
situation Loop = Init +
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"
assumes grd1: "i < n"
assumes grd2: "a i \not= x"
assumes inc: "i' = i + 1"
shows Loop n a i'
... more transitions
The situations are variations of the existing Isabelle locales, with
some additional syntax to distinguish between different kind
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and