Re: [isabelle] Execute typedef Definition



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

On 2021-06-14 10:27, Stüber wrote:
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 [1]
Phone ++49 241 80-21352



Links:
------
[1] https://www.se-rwth.de




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.