Email Gateway (Aug 19 2022 at 16:19): Email Gateway (Aug 19 2022 at 16:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 20 2024 at 12:26 UTC