[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

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.
      No relator for the type "QuotientTypeTests.tree"

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)
  "t⇩1 ∼ t⇩2 ≡ size t⇩1 = size t⇩2"

lemma tree_equiv_reflp:
  "reflp (op ∼)"
  by (simp add: tree_equivp_def reflp_def)

lemma tree_equiv_symp:
  "symp (op ∼)"
  by (simp add: tree_equivp_def symp_def)

lemma tree_equiv_transp:
  "transp (op ∼)"
  by (simp add: tree_equivp_def transp_def)

lemma tree_equivp:
  "equivp (op ∼)"
by (auto intro: equivpI simp add: tree_equiv_reflp tree_equiv_symp tree_equiv_transp)

fun increase :: "tree ⇒ tree"
  "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
  by (simp add: tree_equivp)

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

lemma "size (Rep (Abs (leaf 1))) = 0"
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

  Is there something I can do about this?
  Will this cause issues, if I want to generate code?



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