Re: [isabelle] Code generation for typedefs with an invariant

NB: if I wrap the conjunction in the typedef of mynat into another definition, everything works fine. So there seems to be some problem with the conjunction.


On 15/10/2021 18:34, Manuel Eberl wrote:
Interesting, thanks!

Unfortunately, there seems to be a problem with the implementation. Consider e.g. this example:

typedef mynat = "{n::nat. n > 0 ∧ even n}"
  by (rule exI[of _ 2]) auto

typedef foo = "{(a :: nat,bs :: (nat × nat) list). ∀b∈set bs. fst b > 0 ∧ even (fst b)}"
  by (rule exI[of _ "(0, [])"]) auto

setup_lifting type_definition_foo
setup_lifting type_definition_mynat

lift_definition (code_dt) bar :: "foo ⇒ (mynat × nat) list" is snd
  by (force simp: list.pred_set)

This gives me a "tactic failed".


On 15/10/2021 18:11, Dmitriy Traytel wrote:
Hi Manuel,

lift_definition already implements your workaround. Try:

context notes[[typedef_overloaded]] begin
lift_definition (code_dt) my_complicated_computation' :: "nat ⇒ good_nat list" is my_complicated_computation
   using my_complicated_computation_good by (auto simp: list.pred_set)

(The context is only needed because your typedef is overloaded. If you have a concrete non-overloaded definition for good you can drop it.)

This is documented in Ondra's PhD thesis (, Section 6.4) and in isar-ref (page 282 for the Isabelle2021 edition).

IIRC, Ondra had also considered extending the code generator but decided against as it would significantly increase the trusted code base (which now would need to take map functions into account).


On 15 Oct 2021, at 16:52, Manuel Eberl <manuel at> wrote:

Small addition: another application of this is to make a "safe"
constructor for types with invariants that returns "None" if the given
value does not fulfil the invariant, e.g.:

mk_pos_nat :: nat ⇒ good_nat option
mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None)

One can do this with an auxiliary function that returns a default value
instead of None, but then you have to check the condition twice.

The best possible solution I see here is if "code abstype" could handle
not only equations of the form "projection (fun_with_invariant x y z) =
…" but relations involving "canonical" relators on types. In the above
case, one would then not have a code equation but a code relation:

rel_fun (=) (rel_option pcr_good_nat)
     (λn. if good n then Some n else None) mk_good_nat

Similarly, the function in my last email have the following relations:

rel_fun (=) (list_all2 pcr_good_nat)
     my_complicated_computation my_complicated_computation'

The actual generated code should of course be:

mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None

my_complicated_computation' xs = map Abs_good_nat
(my_complicated_computation xs)

Which is exactly the m_complicated_computation' that comes out of the
lift_definition anyway (and I imagine there's a one-to-one
correspondence between the map operations in the def lemma and the
relators in the transfer lemma).

So, not sure – is there some fundamental problem with implementation
something like this in the code generator?


On 14/10/2021 21:31, Manuel Eberl wrote:

I have a typedef of the form

typedef good_nat = "{n::nat. good n}"

and I have an executable function that produces a "nat list" where I
have proven that all entries are good.

How can I lift that to an *executable* function that produces a
"good_nat list" instead?

The way I see it, the usual approach of doing a "code abstype" and
specifying the code equation in terms of some projection out of the
"type with invariant" to "type without invariant" doesn't work here
because I have lists of these things.

I do have a workaround involving a second typedef for intermediate
results, but it is very boilerplatey and I'd be happy to know if there
is something easier.

See attachment for all the details.



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