Email Gateway (Sep 15 2025 at 13:22): Email Gateway (Sep 15 2025 at 13:22):From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
I am working on a tool to export a locale to PVL. PVL is a specification language [pvl] supported by the
deductive verifier VerCors. The outcome of this tool is to replace trusted axiomatic data types [axiomatic data types]
with equivalent that are automatically generated.
Consider this example of a Tuple ADT in PVL. The constructor cons and selectors left and right
must satisfy the axioms listed after the names are declared.
adt MyTuple {
pure MyTuple cons(int l, int r);
pure int left(MyTuple t);
pure int right(MyTuple t);
axiom (\forall int l, int r; left(cons(l, r)) == l);
axiom (\forall int l, int r; right(cons(l, r)) == r);
axiom (\forall int l1, int l2, int r1, int r2; (cons(l1, r1) == cons(l2, r2)) ==> (l1 == l2 && r1 == r2));
}
This ADT can be generated from the following locale definition.
locale MyPair =
fixes cons :: "'a ⇒ 'b ⇒ 'pair"
and left :: "'pair ⇒ 'a"
and right :: "'pair ⇒ 'b"
assumes L [simp]: "left (cons a b) = a"
assumes R: "right (cons a b) = b"
assumes "cons l1 r1 = cons l2 r2 ==> l1 = l2 && r1 = r2"
begin
lemma test: "cons (left (cons a b)) b = cons a b" by (simp add: L R)
end
The locale API allows me to access the names used in fixes and assumes as well as the terms
associated with the assumptions.
I cannot access the test lemma from the locale API. What is the appropriate way to list
all theorems in a locale? If this is not possible what are the alternatives that I can use?
Thanks for the help
[pvl]: https://github.com/utwente-fmt/vercors/wiki/PVL-Syntax-Reference
[axiomatic data types]: https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types
Last updated: Sep 16 2025 at 12:42 UTC