Email Gateway (Aug 22 2022 at 15:58): Email Gateway (Aug 22 2022 at 15:58):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
I implemented an “assert” top-level command; it is similar to “value",
but requires the expression to be boolean and to evaluate to true.
Otherwise the command fails.
I was surprised not to find something similar in the rich code-base of
Isabelle and found it dead useful when developing / debugging design-level
models.
Its not a big thing; If integrated into the Isabelle sources, it could after
refactoring probably be reduced to 5 - 10 additional lines. In the meantime,
users might just include my little theory in the annex.
Best regards,
bu
Assert.thy
Email Gateway (Aug 22 2022 at 16:01):From: Manuel Eberl <eberlm@in.tum.de>
For the sake of completeness, there is something like this for the
"values" command in the predicate compiler:
values [expected "{}" pred] "{x. False'}"
Manuel
Email Gateway (Aug 22 2022 at 16:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Burkhart,
There are already plenty of ways to do this if you are willing to commit to a specific
evaluator. Here are a few:
notepad begin have "proposition" by eval end
generates the code in SML, compiles and runs it in the running PolyML process
same as (1), but "by normalization" or "by code_simp" use evaluation by NBE or with the
simplifier.
The theory HOL/Library/Code_Test implements a command test_code for testing code
generator setups. The command test_code takes a boolean expression and a non-empty list of
names for the executable of the target language (PolyML, SMLNJ, mlton, GHC, OCaml, Scala).
It then generates the code for the boolean expression and evaluates it in an external
process. For example:
test_code "5 = (7 :: int)" in PolyML Scala
This is slower than the other options because it starts up an external process. But it has
a few heuristics to pretty-print the result of subexpressions (such as the two sides of an
equality).
All the best,
Andreas
Email Gateway (Aug 22 2022 at 16:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A quite idiomatic way to express assertions by evaluation is something like
theory Foo
imports Main
begin
text ‹
@{lemma "sorted [1, 2, 3::nat]" by eval}
›
text ‹
@{lemma "sorted [1, 3, 2::nat]" by eval}
›
end
where assertions are treated as formal text within the theory.
In Isar, there is a tendency to be more explicit and verbose concerning
evaluation techniques the more formal its particular application is.
The deeper reason is that executability in Isabelle/HOL is no inherent
property of the calculus but rather a certain interpretation of
ingredients of the calculus.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 08:19 UTC