Dear Larry,
at least I'm under the impression that the representatives are needed ;).
Let me elaborate: I am formalizing a proof as part of IsaFoR (mainly
first-order term rewriting). In the remainder of IsaFoR (which is
already quite huge) term rewrite systems (TRS) are just represented as
sets of pairs of terms. This is a well-supported type and easy to use.
But in the new proof a crucial property is that at a certain point a TRS
does not contain variants (i.e., variable renamed versions of rules).
Since I want to reuse all the existing lemmas about TRSs but for the
current proof I need a TRS without variants, I defined the operation of
removing variants from TRSs (via first building the equivalence classes
w.r.t. variable renaming and then projecting, using SOME, to a system of
representatives).
Please let me know what you think about this setup or if you have any
suggestions for improvements.
cheers
chris
Post by Lawrence PaulsonAre specific representatives actually needed? It might be better to use the equivalence classes themselves. That is the point of this construction.
--lcp
Post by Christian SternagelThanks Dimitriy,
That looks similar to the construction I'm currently using ;), i.e.,
"repsys A R = {(SOME x. x ∈ X) | X. X ∈ A // R}"
I was hoping that some properties are already proved about it. E.g., that two non-equal elements of "repsys A R" are not in relation w.r.t. "R", "repsys A R" is a subset of "A", ...
But it should be easy to do anyway. Would this be interesting for anybody else?
cheers
chris
btw: I could not find the constant "proj" in Equiv_Relations.
Post by Dmitriy TraytelHi Chris,
Post by Christian SternagelDear fellow Isabellers,
I am wondering whether there is already a way in the Isabelle/HOL
library (or the AFP, for that matter) to obtain a system of
representatives (I'm not sure whether this is the correct term, in
German it is called "Repräsentantensystem") for a given equivalence
relation, i.e., a set containing one representative of each
equivalence class?
Something like this: "(λX. SOME x. x ∈ X) ` Equiv_Relations.proj r `
Field r"
The function Equiv_Relations.proj gives you the (non-empty) equivalence
class of an element.
Dmitriy