File StTrans.ML


Goal "P -a<b>-> P' ==> rstr P";
by (etac StFOut.induct 1);
by (auto_tac (claset() addEs RSTR.elims addIs RSTR.intrs, simpset()));
qed "StFOut_rstr1";

Goal "P -a<b>-> P' ==> wfp P";
by (auto_tac (claset() addIs [StFOut_rstr1, rstr_wfp], simpset()));
qed "StFOut_wfp1";

Goal "P -a<b>-> P' ==> rstr P'";
by (etac StFOut.induct 1);
by (auto_tac (claset() addIs RSTR.intrs, simpset()));
qed "StFOut_rstr2";

Goal "P -a<b>-> P' ==> wfp P'";
by (auto_tac (claset() addIs [StFOut_rstr2, rstr_wfp], simpset()));
qed "StFOut_wfp2";

Goal "P -a<>-> fP' ==> rstr P";
by (etac StBOut.induct 1);
by (auto_tac (claset() addEs RSTR.elims addIs RSTR.intrs, simpset()));
qed "StBOut_rstr1";

Goal "P -a<>-> fP' ==> wfp P";
by (auto_tac (claset() addIs [StBOut_rstr1, rstr_wfp], simpset()));
qed "StBOut_wfp1";

Goal "P -a<>-> fP' ==> rstra fP'";
by (etac StBOut.induct 1);
by (auto_tac (claset() addIs RSTRA.intrs addIs [rstr_rstra], simpset()));
qed "StBOut_rstra2";

Goal "P -a<>-> fP' ==> wfpa fP'";
by (auto_tac (claset() addIs [StBOut_rstra2, rstra_wfpa], simpset()));
qed "StBOut_wfpa2";

Goal "P -a[]-> fP' ==> rstr P";
by (etac StIn.induct 1);
by (auto_tac (claset() addEs RSTR.elims addIs RSTR.intrs, simpset()));
qed "StIn_rstr1";

Goal "P -a[]-> fP' ==> wfp P";
by (auto_tac (claset() addIs [StIn_rstr1, rstr_wfp], simpset()));
qed "StIn_wfp1";

Goal "P -a[]-> fP' ==> rstra fP'";
by (etac StIn.induct 1);
by (auto_tac (claset() addSIs RSTRA.intrs @ WFNA.intrs
              addIs [rstr_rstra,rstra_rstra], simpset()));
qed "StIn_rstra2";

Goal "P -a[]-> fP' ==> wfpa fP'";
by (auto_tac (claset() addIs [StIn_rstra2, rstra_wfpa], simpset()));
qed "StIn_wfpa2";

Goal "P -tau-> P' ==> rstr P";
by (etac StTau.induct 1);
by (auto_tac (claset() addIs RSTR.intrs @
              [StFOut_rstr1,StBOut_rstr1,StIn_rstr1], simpset()));
qed "StTau_rstr1";

Goal "P -tau-> P' ==> wfp P";
by (auto_tac (claset() addIs [StTau_rstr1, rstr_wfp], simpset()));
qed "StTau_wfp1";

Goal "P -tau-> P' ==> rstr P'";
by (etac StTau.induct 1);
by (auto_tac (claset() addSIs RSTR.intrs @ RSTRA.intrs @ [rstra_rstr] addIs
             [StFOut_rstr2,StBOut_rstra2,StIn_rstra2,rstr_rstra], simpset()));
qed "StTau_rstr2";

Goal "P -tau-> P' ==> wfp P'";
by (auto_tac (claset() addIs [StTau_rstr2, rstr_wfp], simpset()));
qed "StTau_wfp2";

val StTrans_rstr1 = [StFOut_rstr1,StBOut_rstr1,StIn_rstr1,StTau_rstr1];
val StTrans_rstr2 = [StFOut_rstr2,StBOut_rstra2,StIn_rstra2,StTau_rstr2];


(*** Cases of transitions ***)

val StIn_In = StIn.mk_cases "a[x].fP x -m[]-> fP'";
val StIn_Ch = StIn.mk_cases "P .+ Q -m[]-> fP'";
val StIn_Pr = StIn.mk_cases "P .| Q -m[]-> fP'";
val StIn_Rs = StIn.mk_cases ".#x. fP x -m[]-> fP'";
val StIn_Rp = StIn.mk_cases ".!P -m[]-> fP'";

val StFOut_Ot = StFOut.mk_cases "a<b>.P -m<n>-> P'";
val StFOut_Ch = StFOut.mk_cases "P .+ Q -m<n>-> P'";
val StFOut_Pr = StFOut.mk_cases "P .| Q -m<n>-> P'";
val StFOut_Rs = StFOut.mk_cases ".#x. fP x -m<n>-> P'";
val StFOut_Rp = StFOut.mk_cases ".!P -m<n>-> P'";

val StBOut_Ot = StBOut.mk_cases "a<b>.P -m<>-> P'";
val StBOut_Ch = StBOut.mk_cases "P .+ Q -m<>-> P'";
val StBOut_Pr = StBOut.mk_cases "P .| Q -m<>-> P'";
val StBOut_Rs = StBOut.mk_cases ".#x. fP x -m<>-> P'";
val StBOut_Rp = StBOut.mk_cases ".!P -m<>-> P'";


(*** Renaming ***)
(*
Goal "P -a[]-> fP' ==> ALL fP ffP' c b. \
 \ fP c -a[]-> ffP' c & rstra fP & (ALL b. rstra ffP' b) & \
 \ (ALL b. rstra (%x. ffP' x b)) & fresha c fP & freshaa c ffP' & c ~= a & \
 \ P = fP c & fP' = ffP' c --> fP b -a[]-> ffP' b";
by (etac StIn.induct 1);
by (ALLGOALS Clarify_tac);
by (dresolve_tac rstra_cases 1);
by (atac 1);
by (Clarify_tac 1);
by (etac WFNA.elim 1);
by (Clarify_tac 1);
by (force_tac (claset() addEs [StIn_In], simpset()) 1);
by (Clarify_tac 1);
by (etac StIn_In 1);
by (Clarify_tac 1);
by (dtac ext_paa_rstra 1);
by (asm_full_simp_tac (simpset() addsimps [freshaa_def,fresha_def,fna_def,fnaa_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [freshaa_def,fresha_def,fna_def,fnaa_def]) 1);
by (REPEAT (atac 1));
by (force_tac (claset() addIs StIn.intrs, simpset()) 1);
(* restriction *)
by (dresolve_tac rstra_cases 1);
by (atac 1);
by (Clarify_tac 1);
by (etac StIn_Rs 1);
by (Clarify_tac 1);
*)