*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Lifting package and state transformers*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Tue, 17 May 2016 09:22:56 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <573AA3A5.7070101@inf.ethz.ch>*References*: <573AA3A5.7070101@inf.ethz.ch>

Hi Andreas, > On 17 May 2016, at 06:52, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > > 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? This obviously does not work, since with the above type_definition lift_definition expects you to tell what to do with the state âs. The following works. datatype ('s, 'm) stateT = StateT (run_state: "'s => 'm") context fixes foo :: "('a => 'm) => 'm" begin lemma typedef_stateT: "type_definition run_state StateT UNIV" by unfold_locales auto setup_lifting typedef_stateT lift_definition foo_state :: "('a => ('s, 'm) stateT) => ('s, 'm) stateT" is "Îf s. foo (Îa. f a s)" . end So you can automatically insert the morphisms StateT and run_state, but I donât think you can come up with a type_definition that hides the threading through of the state âs from the user. Dmitriy

**Follow-Ups**:**Re: [isabelle] Lifting package and state transformers***From:*Andreas Lochbihler

**References**:**[isabelle] Lifting package and state transformers***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Lifting package and state transformers
- Next by Date: Re: [isabelle] Inclusion-minimal sets
- Previous by Thread: [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