[isabelle] Lifting package and state transformers



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




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