*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Lifting package and state transformers*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 17 May 2016 08:47:46 +0200

Hi Andreas,

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

Peter

-------- Originalnachricht --------

Betreff: [isabelle] Lifting package and state transformers

Von: Andreas Lochbihler

An: isabelle-users

Cc:

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))"

end

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?

Best,

Andreas

- Previous by Date: [isabelle] Lifting package and state transformers
- Next by Date: Re: [isabelle] Lifting package and state transformers
- Previous by Thread: Re: [isabelle] Lifting package and state transformers
- Next by Thread: Re: [isabelle] Lifting package and state transformers
- Cl-isabelle-users May 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list