Email Gateway (Jun 14 2021 at 09:28): Email Gateway (Jun 14 2021 at 09:28):From: "Stüber, Sebastian" <stueber@se-rwth.de>
Dear all,
I am trying to use a "typedef" datatype for code execution.
When I am executing the definition, it fails with an "Abstraction violation".
Can I add code-lemmata so that the definition "conv" (see below) is executable?
The theory:
typedef evenNat = "{x::nat | x. even x}"
by auto
setup_lifting type_definition_evenNat
definition conv::"nat list ⇒ evenNat list" where
"conv = map Abs_evenNat o filter even"
value "conv [1::nat, 2::nat]" (* Fails with: "Abstraction violation" *)
Sincerely,
Sebastian
Sebastian Stüber, M.Sc.RWTH | Software Engineering
Lehrstuhl für Software Engineering | RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany | https://www.se-rwth.de
Phone ++49 241 80-21352
Scratch.thy
Email Gateway (Jun 14 2021 at 10:35):From: "C.A. Watt" <caw77@cam.ac.uk>
Dear Sebastian
My understanding is that you must define conv by way of
"lift_definition". Intuitively, in your current setup you have not
proven that you are applying Abs_evenNat to only elements of nat that
are within the evenNat set. So instead of your current definition, you
should state:
lift_definition(code_dt) conv :: "nat list => evenNat list" is "filter
even"
by (simp add: list_all_def)
The proof obligation is exactly the fact that the result of "filter
even" is always within the set that defines evenNat. Note that the
"code_dt" parameter is necessary to allow extraction/execution of conv,
because the abstract type evenNat occuring in the return type has a type
constructor applied to it. I don't understand all the technical details
of this parameter, but it's documented in isar-ref.
Best wishes
Conrad
Last updated: Jul 15 2022 at 23:21 UTC