*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Relating class operations and corresponding locale.*From*: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Thu, 28 Jun 2018 12:59:49 +0200*Reply-to*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*User-agent*: Mutt/1.10.0 (2018-05-17)

Hi, I'm wondering how to best convert between the typeclass and the locale versions of operations. For example, the ordered tree property for red-black trees can be written as rbt_sorted or ord.rbt_sorted (op <), and the two can be shown to be equivalent: theory Test imports "HOL-Library.RBT_Impl" begin lemma rbt_sorted_conv: "ord.rbt_sorted (op <) = rbt_sorted" by (auto simp: rbt_sorted_def ord.rbt_sorted_def rbt_less_prop ord.rbt_less_prop rbt_greater_prop ord.rbt_greater_prop) end However, the way I'm proving this is horrible -- basically I'm unfolding the definitions down to the elementary class operations, which does not scale very well. Is there a better way to obtain such conversions? Cheers, Bertram

**Follow-Ups**:**Re: [isabelle] Relating class operations and corresponding locale.***From:*Bertram Felgenhauer via Cl-isabelle-users

- Previous by Date: Re: [isabelle] to automatically generate all the 16 lemmas corresponding to all the possible cases just from the definition of the function
- Next by Date: Re: [isabelle] Relating class operations and corresponding locale.
- Previous by Thread: Re: [isabelle] to automatically generate all the 16 lemmas corresponding to all the possible cases just from the definition of the function
- Next by Thread: Re: [isabelle] Relating class operations and corresponding locale.
- Cl-isabelle-users June 2018 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