# [isabelle] transfer / lifting / quotient - questions

```Dear transfer / lifting / quotient-experts,

```
for my project I've started to work with the new quotient package and now I'm stuck with some
```(hopefully easy to solve) problems.

```
To keep everything small and compact I created a little example to illustrate my problems. In this example, all trees are grouped by their size and then the "increase" function is lifted
```from the raw to the abstract type.

---------------------------------------------------------------------------------------------------

theory QuotientTypeTests
imports Main
begin

datatype tree = leaf "nat"
| node "tree" "tree"

(*
Question 1:

```
If I try to generalize nat to 'a, I get the following error from the quotient_type command:
```
Generation of a parametrized correspondence relation failed.
Reason:
No relator for the type "QuotientTypeTests.tree"
found.

```
Looking at the quotient examples didn't help me to figure out, what to prove or define to fix this.
```  What do I have to do? Or can I simply ignore it?
*)

definition tree_equivp :: "tree ⇒ tree ⇒ bool" (infix "∼" 60)
where
"t⇩1 ∼ t⇩2 ≡ size t⇩1 = size t⇩2"

lemma tree_equiv_reflp:
"reflp (op ∼)"

lemma tree_equiv_symp:
"symp (op ∼)"

lemma tree_equiv_transp:
"transp (op ∼)"

lemma tree_equivp:
"equivp (op ∼)"
```
by (auto intro: equivpI simp add: tree_equiv_reflp tree_equiv_symp tree_equiv_transp)
```
fun increase :: "tree ⇒ tree"
where
"increase (leaf a) = node (leaf a) (leaf 0)"
| "increase (node t1 t2) = node (node t1 t2) (leaf 0)"

lemma increase_correct:
"size (increase t) = (Suc (size t))"
by (induction t) simp+

lemma increase_respects_tree_equivp:
"t1 ∼ t2 ⟹ increase t1 ∼ increase t2"
unfolding tree_equivp_def using increase_correct by simp

quotient_type same_size_tree = "tree" / "op ∼"
morphisms Rep Abs

lemma "size (leaf 1) = 0"
by eval

lemma "size (Rep (Abs (leaf 1))) = 0"
nitpick
```
by (metis Quotient3_rep_abs Quotient3_same_size_tree tree.size(3) tree_equivp_def)
```
(*
Question 2:

Why does nitpick report a counterexample (Empty assignment),
while sledgehammer finds a proof?
*)

```
lift_definition increase_abs :: "same_size_tree ⇒ same_size_tree" is increase
```  by (simp add: increase_respects_tree_equivp)

value "increase_abs (Abs (leaf 3))"

(* Great, this works! *)

value "Abs (leaf 0) = Abs (leaf 1)"

(*
Question 3:

The command fails with:

Wellsortedness error:
Type same_size_tree not of sort equal
No type arity same_size_tree :: equal

Will this cause issues, if I want to generate code?
*)

---------------------------------------------------------------------------------------------------

Best,
Salomon

```

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