[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 ∼)"
  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"
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
  by (simp add: tree_equivp)

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

  Is there something I can do about this?
  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.