Email Gateway (Aug 23 2020 at 18:55): 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
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: Apr 18 2024 at 16:19 UTC