*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] transfer / lifting / quotient - questions*From*: Salomon Sickert <sickert at in.tum.de>*Date*: Mon, 23 Jun 2014 14:41:13 +0200*User-agent*: Roundcube Webmail/0.8.1

Dear transfer / lifting / quotient-experts,

(hopefully easy to solve) problems.

from the raw to the abstract type. --------------------------------------------------------------------------------------------------- theory QuotientTypeTests imports Main begin datatype tree = leaf "nat" | node "tree" "tree" (* Question 1:

Generation of a parametrized correspondence relation failed. Reason: No relator for the type "QuotientTypeTests.tree" found.

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 ∼)"

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

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

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

**Follow-Ups**:**Re: [isabelle] transfer / lifting / quotient - questions***From:*Ondřej Kunčar

**Re: [isabelle] transfer / lifting / quotient - questions***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Simple
- Next by Date: Re: [isabelle] transfer / lifting / quotient - questions
- Previous by Thread: [isabelle] Instance
- Next by Thread: Re: [isabelle] transfer / lifting / quotient - questions
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list