Email Gateway (Aug 22 2022 at 10:30): Email Gateway (Aug 22 2022 at 10:30):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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
Last updated: Nov 21 2024 at 12:39 UTC