File Procs.ML


Addsimps [n_def];

Goal "finite (fn P)";
by (induct_tac "P" 1);
by (Auto_tac);
qed "fn_finite";

Goal "finite (bn P)";
by (induct_tac "P" 1);
by (Auto_tac);
qed "bn_finite";

Addsimps [fn_finite,bn_finite];

Goal "finite (n P)";
by (Auto_tac);
qed "n_finite";

Addsimps [n_finite];

Goal "n (.0) = {}";
by (Auto_tac);
qed "n_Null";

Goal "n (.t.P) = n P";
by (Auto_tac);
qed "n_Tau";

Goal "n (a<b>.P) = {a, b} Un n P";
by (Auto_tac);
qed "n_Out";

Goal "n (a[b].P) = {a, b} Un n P";
by (Auto_tac);
qed "n_In";

Goal "n (.#b P) = insert b (n P)";
by (Auto_tac);
qed "n_Res";

Goal "n (P .+ Q) = n P Un n Q";
by (Auto_tac);
qed "n_Plus";

Goal "n (P .| Q) = n P Un n Q";
by (Auto_tac);
qed "n_Par";

Goal "n (.[a.=b]P) = {a, b} Un n P";
by (Auto_tac);
qed "n_Mt";

Goal "n (.[a.~=b]P) = {a, b} Un n P";
by (Auto_tac);
qed "n_Mmt";

Goal "n (.!P) = n P";
by (Auto_tac);
qed "n_Repl";

val n_simps = [n_Null, n_Tau, n_Out, n_In, n_Res, n_Plus,
               n_Par, n_Mt, n_Mmt, n_Repl];

Delsimps [n_def];

Addsimps n_simps;