Email Gateway (Aug 23 2022 at 09:18): Email Gateway (Aug 23 2022 at 09:18):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Dear Isabelle Users,
Let me apologize in advance if this question reflects some fundamental
misunderstandings about Isabelle's Lifting and Transfer facilities. I am
still new to them and, while I've read the documentation about them, I
still feel shaky about my intuitions.
My mental model of the Lifting package is the following: if for some types
typeb and typea I can prove
"type_definition Rep Abs A" (for Rep :: typeb => typea, Abs : typea =>
typeb, A :: typea set)
then I can feed this theorem to the Lifting tool to lift definitions that
talks about the concrete type A to definitions that talk about the abstract
type B. (And I can use Transfer to assist in proving theorems about the
functions I derive this way).
My question is whether Isabelle contains any support for automated lifting
when the relationship is reversed. That is, suppose I have a suite of
definitions for the "abstract" type B and I want to "lower" them to
definitions on type A (where we know the same type_definition fact
indicated above).
It seemed to me that there probably wasn't a way to do this in general.
Although in some concrete cases it does seem that there is something sane
you can do - for instance, we could prove "type_definition Some
(case_option undefined id) {x . ∃ y . x = Some y}". And then map_option
would seem to be the "lowering" function we'd be looking for.
However, I saw the description of the "Transfer.transferred" attribute in
isar-ref, and, while I did not fully understand it, it seemed like it might
be something akin to what I was looking for. It at least made me question
whether there is something sane that can be done in the "reverse" direction
in the general case.
So my question is basically
Is there anything sane that can be done in general when it comes to this
sort of "lowering"?
Does Isabelle have any automation that supports such "lowering" in a
similar way to its support for Lifting?
Regardless of the answers to 1 and 2, what exactly does
"Transfer.transferred" do?
Thanks,
Mario
Email Gateway (Aug 23 2022 at 09:18):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Mario,
I’m not an export on transfer on my own, but merely a user.
From my experience transfer-lifting mostly works uni-directional.
However, there is an attribute “untransferred” that permits to go in
the other direction. Example:
typedef large_nat = "{ x :: nat. x ≥ 5 }" by auto
setup_lifting type_definition_large_nat
lift_definition sq_large_nat :: "large_nat ⇒ large_nat" is "λ x. x * x"
by (meson leD leI le_less_trans le_square)
lift_definition get_nat :: "large_nat ⇒ nat" is "λ x. x" .
lemma sq_20: "get_nat (sq_large_nat x) ≥ 20"
proof (transfer)
(* this is the standard direction *)
fix x :: nat
assume "5 ≤ x"
hence "5 * 5 ≤ x * x"
using mult_le_mono by blast
thus "20 ≤ x * x" by auto
qed
(* and now we can go in the other direction *)
thm sq_20[untransferred] (* results in 5 ≤ x ⟹ 20 ≤ x * x *)
Best,
René
Email Gateway (Aug 23 2022 at 09:19):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Hi René,
Thanks for your help. I guess perhaps I was confused about the difference
between "transferred" and "untransferred" (although I have to admit I'm
still not clear on what "untransferred" does, since I had thought that it
did more or less what you described "transferred" as doing in your example.)
I'd still appreciate it if anyone could help me out with an intuition for
what "untransferred" does, but I think I've gotten the main thing I wanted
to know from René's reply; namely, that I can only lift definitions one way
(using Lifting) but that (at least under some circumstances) I can transfer
facts about my lifted constants in the reverse direction.
Thanks,
Mario
Last updated: Apr 23 2024 at 08:19 UTC