File Congruence.ML


(*** Restrictedness ***)

Goal "P .~ Q ==> rstr P & rstr Q";
by (etac PiCon.induct 1);
by (auto_tac (claset() addEs RSTR.elims addSIs RSTR.intrs addIs RSTRA.intrs @
    [rstra_rstr,rstr_rstra], simpset()));
qed "lemma";

Goal "P .~ Q ==> rstr P";
by (fast_tac (claset() addDs [lemma]) 1);
qed "PiCon_rstr1";

Goal "P .~ Q ==> rstr Q";
by (fast_tac (claset() addDs [lemma]) 1);
qed "PiCon_rstr2";

Goal "P .> Q ==> rstr P & rstr Q";
by (etac AxExp.induct 1);
by (etac WFNA.elim 6);
by (force_tac (claset() addEs RSTR.elims addSIs RSTR.intrs @ RSTRA.intrs
    @ [PiCon_rstr1,PiCon_rstr2,rstra_rstra], simpset()) 7);
by (auto_tac (claset() addEs RSTR.elims addIs RSTR.intrs @ RSTRA.intrs
    @ [PiCon_rstr1,PiCon_rstr2,rstra_rstra], simpset()));
qed "lemma";

Goal "P .> Q ==> rstr P";
by (fast_tac (claset() addDs [lemma]) 1);
qed "AxExp_rstr1";

Goal "P .> Q ==> rstr Q";
by (fast_tac (claset() addDs [lemma]) 1);
qed "AxExp_rstr2";


(* Examples: transitivity has to be explicitely instantiated *)

Goal "rstr P ==> .#x. (P .+ .0) .~ P";
by (res_inst_tac [("Q", "P .+ .0")] PiCon.trans 1);
by (auto_tac (claset() addIs PiCon.intrs @ RSTR.intrs, simpset()));
qed "n_res_ch_null";

Goal "rstr P ==> .#x. (P .| .0) .~ P";
by (res_inst_tac [("Q", "P .| .0")] PiCon.trans 1);
by (auto_tac (claset() addIs PiCon.intrs @ RSTR.intrs, simpset()));
qed "n_res_par_null";