Re: [isabelle] Lifting package and state transformers
- To: Peter Lammich <lammich at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] Lifting package and state transformers
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Tue, 17 May 2016 08:51:07 +0200
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.7.2
The function foo is just an example. I want to do this for several other functions, each
of which has its own type. So I'd need a new abbreviation of each of them?
(And I would also like to do this for a bunch of other transformers, not just state, but
I'm hoping that I get enough insights from this example to generalise it to the others.)
On 17/05/16 08:47, Peter Lammich wrote:
Cant you just define an abbreviation âliftâ, and define foo_state = lift foo ?
-------- Originalnachricht --------
Betreff: [isabelle] Lifting package and state transformers
Von: Andreas Lochbihler
Dear experts of the lifting package,
I wonder whether I can automate certain liftings with the Lifting package. Concretely,
suppose I have a function foo and I want to lift it to a type of state transformers:
datatype ('s, 'm) stateT = StateT (run_state: "'s => 'm")
context fixes foo :: "('a => 'm) => 'm" begin
definition foo_state :: "('a => ('s, 'm) stateT) => ('s, 'm) stateT"
where "foo_state f = StateT (%s. foo (%a. run_state (f a) s))"
Can I (somehow) use lift_definition to define foo_state? I am thinking of something like
lift_definition foo_state :: "('a => ('s, 'm) stateT) => ('s, 'm) stateT" is foo
Unfortunately, I have no idea what theorem provide to setup_lifting to make this work. I
tried with the obvious one
type_definition run_state StateT UNIV
but that did not work. Any ideas?
This archive was generated by a fusion of
Pipermail (Mailman edition) and