Dear Isabelle Community, I would like to better understand the 'setup_lifting' command and have spelled out a detailed question about this command here: https://stackoverflow.com/questions/72392804/how-to-setup-lifitng-with-custom-types-aka-how-to-define-a-relator

I would much appreciate your help!

Hi Marco,

The setup_lifting is only useful if you intend to use the lifting-and-transfer framework, for the details of which you can read Huffman and Kuncar's CPP paper. Some recent progress in this framework is mostly related to bounded natural functors, for which you can have a look at this paper.

Proposing suitable relators requires insight of the data type. Here `setup_lifting`

gives us some relatively easy relator theorems for free.

I appreciate the reference to the theory behind this framework (an interesting glimpse into Isabelle history), but I care about using this framework for a specific example in formalizing mathematics — polynomials —, where two `typedef`

s build on top of each other. Unfortunately, neither of two links above seems to be of much help to learn how to use the framework.

In the CPP paper, there are two examples of quotient theorems for relators — apparently the type of theorem I should care about — at the beginning of section 3.2. However, the next paragraph immediately states

Users generally will not prove the Quotient theorem manually for new types, as special commands exist to automate the process. The command quotient type defines a new quotient type, internally proves the corresponding Quotient theorem and registers it with setup lifting.

We also support types defined by the command typedef.The theorem type_definition Rep Abs {x. P x}, which axiomatizes the newly defined subtype,can be supplied to setup_lifting.*

(emphasis mine)

As explained on StackOverflow, I am working with the `typedef`

command. How can I supply this "Quotient theorem" about my monom type to setup_lifting?

Then I guess you are running into the problem of proposing a relator for some concrete types, which again can be ** highly non-trivial** and sometimes even impossible... I have been working on the relator for the topology type and asked a similar question in the mailing list -- not sure if you can find the discussions online.

For a starting point of self-proposing a relator, you can have a look at the relator for sets and that for filters. Essentially, you need to propose a relation `rel_monom`

of type `('a => 'b => bool) => 'a mono => 'b monom => bool`

and then prove properties like

```
lemma rel_monom_eq[relator_eq]: "rel_monom (=) = (=)"
lemma rel_monom_mono[relator_mono]: "rel_monom R ≤ rel_monom S" if "R ≤ S"
lemma rel_monom_distr [relator_distr]: "rel_monom A OO rel_monom B = rel_monom (A OO B)"
lemma Quotient_monom [quot_map]:
"Quotient R Abs Rep T ⟹ Quotient (rel_monom R) (monom_map Abs) (monom_map Rep) (rel_monom T)"
```

Thank you for the concrete pointers and lemma statements, that looks very useful! It is surprising that quotient types and subtypes of lists, sets etc work so seamlessly but as soon as you stack type definitions, it becomes much more complicated suddenly.

Last updated: Sep 25 2022 at 23:25 UTC