[isabelle] Relating class operations and corresponding locale.
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:
"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)
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and