*To*: Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] Lifting package and state transformers*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 17 May 2016 13:38:12 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <3E77413C-C0C7-48DF-BE91-B9F08FF06102@inf.ethz.ch>*References*: <573AA3A5.7070101@inf.ethz.ch> <3E77413C-C0C7-48DF-BE91-B9F08FF06102@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.7.2

Hi Dmitriy,

Andreas On 17/05/16 09:22, Dmitriy Traytel wrote:

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:*Ognjen Maric

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

**Re: [isabelle] Lifting package and state transformers***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Inclusion-minimal sets
- 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