[isabelle] lift_definition: op OO in proof obligation



Dear experts of the lifting package,

Normally, the lifting package nicely preprocesses the proof obligation before they are presented to the user. This usually works even if lifting is nested, as for example in

lift_definition dconcat :: "'a dlist dlist => 'a dlist"
is "... :: 'a list list => 'a list"

for dlist from ~~/src/HOL/Library/Dlist. However, in my application, I now came across a case where the internal construction is not simplified away. Here's the reduces example:

datatype_new ('a, 's) step = Done | Skip 's | Yield 'a 's
type_synonym ('a, 's) raw = "'s ⇒ ('a,'s) step"
consts wf :: "('a, 's) raw ⇒ bool"
typedef ('a,'s) wf = "{g :: ('a,'s) raw. wf g}" sorry
setup_lifting type_definition_wf

consts raw :: "('a ⇒ ('b, 'sg) raw × 'sg) ⇒ ('a, 's) raw ⇒ ('b, 's × (('b, 'sg) raw × 'sg) option) raw" lift_definition foo :: "('a ⇒ ('b, 'sg) wf × 'sg) ⇒ ('a, 's) wf ⇒ ('b, 's × (('b, 'sg) wf × 'sg) option) wf"
is "raw"

Now, I wonder whether I am missing some setup for lifting or whether I just have to crunch my way through this proof obligation:

⋀fun1 fun2 fun3.
⟦⋀x. rel_prod (λx y. wf x ∧ x = y) op = (fun1 x) (fun2 x); wf fun3⟧
⟹ (rel_fun (rel_prod op = (rel_option (rel_prod (pcr_wf op = op =) op =)))
      (rel_step op = (rel_prod op = (rel_option (rel_prod (pcr_wf op = op =) op =)))) OO
     (λx y. wf x ∧ x = y) OO
     (rel_fun (rel_prod op = (rel_option (rel_prod (pcr_wf op = op =) op =)))
       (rel_step op = (rel_prod op = (rel_option (rel_prod (pcr_wf op = op =) op =)))))¯¯)
     (raw fun1 fun3) (raw fun2 fun3)

If I miss some setup, I'd also be interested in how I could have found out what was missing.

Thanks,
Andreas




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