Theory AlphaClass

Up to index of Isabelle/HOL/raw-confluence-lambda

(*  Title:      AlphaClass.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    15th January, 2001

- Definition of alpha-equivalence class

*)

AlphaClass = Alpha +

consts  alphaclass :: "lterm => lterm set"

defs
  alphaclass "alphaclass(e) == {e'. e' =A= e}"

end

theorem alphaclass_lemma_1:

  e =A= e' ==> alphaclass e = alphaclass e'

theorem alphaclass_lemma_2:

  x : alphaclass e ==> alphaclass x = alphaclass e

theorem alphaclass_lemma_3:

  x : alphaclass e ==> x =A= e

theorem alphaclass_self_inclusion:

  e : alphaclass e