Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Handmade transfer rules not invoked


view this post on Zulip Email Gateway (Aug 23 2020 at 18:55):

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

view this post on Zulip Email Gateway (Aug 25 2020 at 17:24):

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