[isabelle] Relating class operations and corresponding locale.



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




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