Email Gateway (Aug 22 2022 at 10:54): Email Gateway (Aug 22 2022 at 10:54):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Andreas,
the good news is that there is a ML interface that you could use, but it
requires some setup.
I don't know why you decided to define the transfer relation from 'a
option to 'a set and not the other way around. I would say that 'a set
is the representation type for 'a option. If we turn the direction
around, there is a quite straightforward solution since we can use
setup_lifting to set up the whole machinery for us.
definition set_option_inv :: "'a set => 'a option" where "set_option_inv
= inv set_option"
lemma td_option: "type_definition set_option set_option_inv {A . card A
≤ 1}"
sorry
setup_lifting td_option
(* setup lifting defines cr_option and pcr_option for you *)
lemma join_option_transfer: "(pcr_option (pcr_option op=) ===>
pcr_option op=) Union join_option"
sorry
(* this is the step where you have to unfortunately use the ML interface *)
ML{*
Lifting_Def.generate_parametric_transfer_rule @{context} @{thm
join_option_transfer} @{thm Union_transfer}
*}
If you insist on the other direction the things get considerably more
hackish. I would like to refine the infrastructure such that this
functionality would not be so much Lifting dependent and could be used
independently in the Transfer world, but this is nothing that would
happen in the next two months. But still hopefully before the next release.
Hope this helps.
Bests,
Ondrej
.
Email Gateway (Aug 22 2022 at 10:58):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondrej,
Thanks for the quick answer. I chose the direction from 'a option to 'a set such that I
could get a reasonable transfer rule for set_option, namely
(op = ===> cr_option_set) (%x. x) set_option
If we turn the direction around, we get
(op = ===> cr_set_option) set_option (%x. x)
and I had a bad gut feeling about registering a transfer rule with "%x. x" on the
right-hand side. I do not have any concrete example where this might cause trouble, but as
it is often cumbersome to figure out why transfer/transfer_prover in a big statement, I
try to stay away from problems. Do you know whether such a rule is safe or of a better format?
I also tried setup_lifting with another monad, say type ('a, 'b, 'c) my_monad (where 'b
and 'c are just additional type parameters which are fixed for the monad instance;
my_monad is defined with the datatype package where 'c is dead). Unfortunately,
setup_lifting refused the registration of the td lemma because the raw type has extra type
variables 'b and 'c. Can I somehow work around this as well?
Best,
Andreas
PS: And don't worry about release cycles. I am again hooked on the repository anyway.
Email Gateway (Aug 22 2022 at 11:05):From: Ondřej Kunčar <kuncar@in.tum.de>
On 08/05/2015 08:26 AM, Andreas Lochbihler wrote:
Hi Ondrej,
Thanks for the quick answer. I chose the direction from 'a option to 'a
set such that I could get a reasonable transfer rule for set_option, namely(op = ===> cr_option_set) (%x. x) set_option
If we turn the direction around, we get
(op = ===> cr_set_option) set_option (%x. x)
and I had a bad gut feeling about registering a transfer rule with "%x.
x" on the right-hand side. I do not have any concrete example where this
might cause trouble, but as it is often cumbersome to figure out why
transfer/transfer_prover in a big statement, I try to stay away from
problems. Do you know whether such a rule is safe or of a better format?
In my proposal, the setup_lifting command generates automatically the
following (fully parametrized) transfer rule for set_option:
option.rep_transfer: (pcr_option ?T ===> rel_set ?T) (λx. x) set_option
Is this rule reasonable for you as well or did I miss something?
I also tried setup_lifting with another monad, say type ('a, 'b, 'c)
my_monad (where 'b and 'c are just additional type parameters which are
fixed for the monad instance; my_monad is defined with the datatype
package where 'c is dead). Unfortunately, setup_lifting refused the
registration of the td lemma because the raw type has extra type
variables 'b and 'c. Can I somehow work around this as well?
I'm afraid most probably not since it is one of the basic invariants of
Lifting. Dead variables are not (yet) supported as well.
Ondrej
Email Gateway (Aug 22 2022 at 11:09):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of lifting and transfer,
The command lift_definition can generate parametric transfer rules from non-parametric
ones if a parametricity theorem for the raw term is given. I would like to use this
transformation also for other transfer rules between constants that are not defined with
lift_definition.
Consider, for example, the option monad can be embedded in the monad on sets. Thus, one
can define the correspondence relation and prove appropriate transfer rules for the monad
operations.
definition cr_option_set :: "'a option ⇒ 'a set ⇒ bool"
where "cr_option_set x A ⟷ A = set_option x"
lemma
"(cr_option_set ===> (op = ===> cr_option_set) ===> cr_option_set)
Option.bind Set.bind"
by(auto simp add: cr_option_set_def rel_fun_def)
Now, if I have two functions defined over the option monad and the set monad,
respectively, then transfer_prover can show that the second is an embedding of the first.
Unfortunately, this does not work for the join operation on monads, because the types are
nested: join_option :: "'a option option => 'a option" and Union :: "'a set set => 'a set".
So, I'd like to use parametrised transfer rules, but proving them directly is a pain. Can
I somehow use the magic behind lift_definition for deriving the parametrised rules?
Thanks,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC