File AlphaClass.ML

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

- A few small lemmas concerning alpha-equivalence classes

*)

Goalw [alphaclass] "e =A= e' ==> alphaclass(e) = alphaclass(e')";
by(Auto_tac);
by(eatac rtrancl_trans 1 1);
by(rotate_tac 1 1);
by(dtac alphaeq_sym 1);
by(eatac (rtrancl_trans RS alphaeq_sym) 1 1);
qed "alphaclass_lemma_1";


Goalw[alphaclass] "x:alphaclass(e) ==> alphaclass(x) = alphaclass(e)";
by(Auto_tac);
by(eatac rtrancl_trans 1 1);
by(dtac alphaeq_sym 1);
by(eatac rtrancl_trans 1 1);
qed "alphaclass_lemma_2";


Goalw[alphaclass] "x:alphaclass(e)==> x =A= e";
by(Auto_tac);
qed "alphaclass_lemma_3";


Goalw [alphaclass] "e: alphaclass(e)";
by(Auto_tac);
qed "alphaclass_self_inclusion";