From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>

Hi!

I would like to replace terms of the form `curry ?f`

by `?g`

in facts,

where `?g`

would be a curried function. I’m trying to achieve this via

the Transfer package, essentially treating non-curried functions as

representations and curried functions as abstract values.

To this end, I have written the following code:

definition

curry_relation :: "('a × 'b ⇒ 'c) ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ bool"

where

[simp]: "curry_relation f g ⟷ curry f = g"

lemma curry_relation_bi_uniqueness [transfer_rule]:

shows "bi_unique curry_relation"

by (simp add: bi_unique_def) (metis case_prod_curry)

lemma uncurry_transfer [transfer_rule]:

shows "rel_fun curry_relation (=) curry (λg. g)"

by (simp add: rel_fun_def)

As an example, I’m trying to transfer the fact stated as follows:

lemma triviality:

shows "curry f = curry f"

using refl .

I would expect `triviality [transferred]`

to yield `?g = ?g`

, but it

actually yields `curry ?f = curry ?f`

.

What am I missing?

All the best,

Wolfgang

From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>

Through further experimenting I found out the missing part: for the

`transferred`

attribute to work, it is necessary to prove right totality

of `curry_relation`

and register it as a transfer rule (and for the

`transfer`

method to work, the same is necessary for bi-totality).

Is this mentioned somewhere in the documentation? I think neither the

reference manual nor the paper by Huffman and Kunčar mentions it.

All the best,

Wolfgang

Last updated: Sep 25 2021 at 09:17 UTC