Stream: General

Topic: nested subtype, relator

Robert Soeldner (Sep 16 2021 at 11:11):

Consider the following example of a nested subtype:

typedef 'a A = "{a :: 'a fset . True}"
  by simp

setup_lifting type_definition_A

typedef 'a B = "{a :: 'a A. True}"
  by simp

setup_lifting type_definition_B

Here, the second setup_lifting of type B highlights, the missing relator of A.

Why does 'a A does not automatically have a relator?

From my understanding, a relator in this simple case would be

lift_definition rel_A :: "('a ⇒ 'b ⇒ bool) ⇒ 'a A  ⇒ 'b A ⇒ bool" is
"rel_fset" .

But what properties do I have to prove, to make it an "official" relator for the lifting package?

Last updated: Jul 15 2022 at 23:21 UTC