Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "lift_definition" to perform two liftings

view this post on Zulip Email Gateway (Aug 22 2022 at 21:08):

From: "Stüber, Sebastian" <stueber@se-rwth.de>
Dear all,
I use “lift_definition” to create definitions. For the normal case it works without problems, but now I want to perform two liftings at once.
For example:

(* imports HOLCF *)

setup_lifting type_definition_cfun

lift_definition complicated:: "tr → tr → tr"

is "λb c. trand⋅b⋅c"

sorry (* Complicated Proof *)

The resulting subgoal is:

goal (1 subgoal):

  1. (rel_fun (=) (pcr_cfun (=) (=)) OO

    (λx y. x ∈ cfun ∧ x = y) OO (rel_fun (=) (pcr_cfun (=) (=)))¯¯)

    andalso_syn andalso_syn

I was unable to prove the subgoal, is there a special trick to show it?

Sincerely,
Sebastian Stüber

Sebastian Stüber, M.Sc.RWTH | Software Engineering
Lehrstuhl für Software Engineering | RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany | http://www.se-rwth.de<http://www.se-rwth.de/>
Phone ++49 241 80-21352 |

Last updated: Apr 25 2024 at 08:20 UTC