Email Gateway (Oct 12 2022 at 13:16): Email Gateway (Oct 12 2022 at 13:16):From: Gunnar Teege <Gunnar.Teege@unibw.de>
Dear all,
I would like to apply the lifting and transfer packages to lift
functions from a record type to a subtype of it. My problem is the
missing relator for the record type.
Example:
record ('a, 'b) R =
f1 :: "'a"
f2 :: "'b"
type_synonym rr = "(nat, nat) R"
definition wlfR :: "rr ⇒ bool" where "wlfR r ≡ (f1 r) = 0"
typedef WlfR = "{x. wlfR x}"
proof
show "⦇R.f1 = 0, f2 = 0⦈ ∈ {x. wlfR x}" by (simp add: wlfR_def)
qed
When I now setup the lifting package using
setup_lifting type_definition_WlfR
Isabelle says
Generation of a parametrized correspondence relation failed.
Reason: No relator for the type "<theory name>.R.R_ext" found.
I understand that the record type constructor R needs a relator which
can be defined by something like
definition rel_R ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ ('e ⇒ 'f ⇒ bool) ⇒
('a,'c,'e) R_scheme ⇒ ('b,'d,'f) R_scheme ⇒ bool"
where "rel_R p1 p2 p3 r1 r2 ≡
p1 (f1 r1) (f1 r2) ∧
p2 (f2 r1) (f2 r2) ∧
p3 (R.more r1) (R.more r2)"
(do I really need to handle the more part explicitly here?)
but how can I make the relator known to the lifting package so that
setup_lifting finds it?
Regards
Gunnar Teege
smime.p7s
Email Gateway (Oct 12 2022 at 14:42):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Gunnar,
First of all, the message from setup_lifting is just a warning. Whether it is relevant depends on what you want to do after that.
You can automatically generate and register the relator for R (more precisely for R_ext) using the following command:
copy_bnf (no_warn_transfer) ('a, 'b, 'more) R_ext
This does a bit more than just adding the relator: you can read about it in the datatypes tutorial.
If you want just the relator you can define it as you did. To register it with lifting you will need to prove a couple of properties of your definition and register those theorems with corresponding attributes. See the isar-ref section on the Lifting and Transfer packages that mention the attributes relator_mono, relator_eq, relator_distr, relator_eq_onp, and quot_map and points to HOL-Library.Lifting_Set for examples — I’m not sure which subset of these attributes is strictly necessary to get rid of the warning.
Best wishes,
Dmitriy
Email Gateway (Oct 13 2022 at 12:14):From: Gunnar Teege <Gunnar.Teege@unibw.de>
Hi Dmitriy,
thanks for the answers. copy_bnf worked fine for me and removed the
warning. Actually, as you supposed, it was not even required for the
liftings I wanted do do.
Next question: When a record component has a word type, another warning
appears in setup_lifting: "No relator for the type "Numeral_Type.bit0"
found." It seems no problem either, but I would like to understand it
and how the warning can be handled. I tried
lift_bnf 'a Numeral_Type.bit0
(I am using an older Isabelle version (before 2021) where bit0 was
defined by a typedef), but Isabelle tells me "No live variables", so it
seems not so easy. And I am not sure how to define a relator at all for
bit0 or whether bit0 is a BNF.
Here is the definition of bit0 in the version I use:
typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
Cheers
Gunnar
smime.p7s
Last updated: Apr 26 2024 at 01:06 UTC