Re: [isabelle] Lifting package and state transformers



Hi Dmitriy,

It would be the point of using lift_definition to relieve the user from figuring out how to pass the state through. Unfortunately, it looks as if you were right.

No theorem of the form "type_definition Rep Abs X" will work, because it would state that the new type is isomorphic to the set X. But ('s, 'm) stateT has much more elements than 'm (unless 's is a singleton type), so there cannot be such an isomorphic subset.

For the same reason of cardinality, no theorem "Quotient R Abs Rep T" can do the job, either. Still, it feels as if some automation should be possible, as I myself found all the lifted versions of constants by "type-directed programming".

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





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