(*  Title:      NSet.ML
    Date:       2002/10/26 modified 2003/10/31 
    Author:     Jan-Georg Smaus, Universitaet Freiburg
    Copyright   2003  Universitaet Freiburg
*)

Goal "(P(t)) \\<Longrightarrow> (t : { x. P(x) })";
br iffD2 1;
br Collect 1;
ba 1;
qed "inI";

(*an elimination rule as usual in logic*)
Goal "(t : { x. P(x) }) \\<Longrightarrow> P(t)";
br iffD1 1;
br Collect 1;
ba 1;
qed "inElimination";

(*an elimination rule that works with etac*)
val [p1,p2] = Goal "\\<lbrakk> (t : { x. P(x) }); P(t) \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R";
br p2 1;
br inElimination 1;
br p1 1;
qed "inE";


Goal "(ALL x. x:A \\<longleftrightarrow> x:B) \\<Longrightarrow> A = B";
br iffD2 1;
br ext 1;
ba 1;
qed "equalsI";

(*an elimination rule as usual in logic*)
Goal "A = B \\<Longrightarrow> (ALL x. x:A \\<longleftrightarrow> x:B)";
br iffD1 1;
br ext 1;
ba 1;
qed "equalsElimination";

(*an elimination rule that works with etac*)
val [p1,p2] = Goal "\\<lbrakk> A = B; (ALL x. x:A \\<longleftrightarrow> x:B) \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R";
br p2 1;
br equalsElimination 1;
br p1 1;
qed "equalsE";