Re: [isabelle] Lifting package and state transformers



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.