Re: [isabelle] Lifting package and state transformers

Hi Peter,

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:
Hi Andreas,

Cant you just define an abbreviation âliftâ, and define foo_state = lift foo ?


-------- Originalnachricht --------
Betreff: [isabelle] Lifting package and state transformers
Von: Andreas Lochbihler
An: isabelle-users

    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
    the following:

    setup_lifting ...
    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 MHonArc.