File WkTrans.ML


(*** Restrictedness ***)

Goalw [WkTau_def] "P =tau=> P' ==> rstr P & rstr P'";
by (etac trancl_trans_induct 1);
by (auto_tac (claset() addIs [StTau_rstr1,StTau_rstr2], simpset()));
qed "lemma";

Goal "P =tau=> P' ==> rstr P";
by (fast_tac (claset() addDs [lemma]) 1);
qed "WkTau_rstr1";

Goal "P =tau=> P' ==> rstr P'";
by (fast_tac (claset() addDs [lemma]) 1);
qed "WkTau_rstr2";

Goalw [WkEps_def,RstrId_def] "P =eps=> P' ==> rstr P";
by (auto_tac (claset() addIs [WkTau_rstr1], simpset()));
qed "WkEps_rstr1";

Goalw [WkEps_def,RstrId_def] "P =eps=> P' ==> rstr P'";
by (auto_tac (claset() addIs [WkTau_rstr2], simpset()));
qed "WkEps_rstr2";

Goalw [WkFOut_def] "P =a<b>=> P' ==> rstr P";
by (auto_tac (claset() addIs [WkEps_rstr1], simpset()));
qed "WkFOut_rstr1";

Goalw [WkFOut_def] "P =a<b>=> P' ==> rstr P'";
by (auto_tac (claset() addIs [StFOut_rstr2], simpset()));
qed "WkFOut_rstr2";

Goalw [WkBOut_def] "P =a<>=> fP' ==> rstr P";
by (auto_tac (claset() addIs [WkEps_rstr1], simpset()));
qed "WkBOut_rstr1";

Goalw [WkBOut_def] "P =a<>=> fP' ==> rstra fP'";
by (auto_tac (claset() addIs [StBOut_rstra2], simpset()));
qed "WkBOut_rstra2";

Goalw [WkIn_def] "P =a[]=> fP' ==> rstr P";
by (auto_tac (claset() addIs [WkEps_rstr1], simpset()));
qed "WkIn_rstr1";

Goalw [WkIn_def] "P =a[]=> fP' ==> rstra fP'";
by (auto_tac (claset() addIs [StIn_rstra2], simpset()));
qed "WkIn_rstra2";

val WkTrans_rstr1 = [WkFOut_rstr1,WkBOut_rstr1,WkIn_rstr1,WkEps_rstr1];
val WkTrans_rstr2 = [WkFOut_rstr2,WkBOut_rstra2,WkIn_rstra2,WkEps_rstr2];


(*** Well-formedness ***)

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

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

Goal "P =eps=> P' ==> wfp P";
by (auto_tac (claset() addIs [WkEps_rstr1,rstr_wfp], simpset()));
qed "WkEps_wfp1";

Goal "P =eps=> P' ==> wfp P'";
by (auto_tac (claset() addIs [WkEps_rstr2,rstr_wfp], simpset()));
qed "WkTau_wfp2";

Goalw [WkFOut_def] "P =a<b>=> P' ==> wfp P";
by (auto_tac (claset() addIs [WkEps_wfp1], simpset()));
qed "WkFOut_wfp1";

Goalw [WkFOut_def] "P =a<b>=> P' ==> wfp P'";
by (auto_tac (claset() addIs [StFOut_wfp2], simpset()));
qed "WkFOut_wfp2";

Goalw [WkBOut_def] "P =a<>=> fP' ==> wfp P";
by (auto_tac (claset() addIs [WkEps_wfp1], simpset()));
qed "WkBOut_wfp1";

Goalw [WkBOut_def] "P =a<>=> fP' ==> wfpa fP'";
by (auto_tac (claset() addIs [StBOut_wfpa2], simpset()));
qed "WkBOut_wfpa2";

Goalw [WkIn_def] "P =a[]=> fP' ==> wfp P";
by (auto_tac (claset() addIs [WkEps_wfp1], simpset()));
qed "WkIn_wfp1";

Goalw [WkIn_def] "P =a[]=> fP' ==> wfpa fP'";
by (auto_tac (claset() addIs [StIn_wfpa2], simpset()));
qed "WkIn_wfpa2";

Goalw [WkIn_def] "P =a[]=> fP' ==> wfpa fP'";
by (auto_tac (claset() addIs [StIn_wfpa2], simpset()));
qed "WkIn_wfp2";


(*** Rules for WkTau ***)

Goalw [WkTau_def] "P -tau-> P' ==> P =tau=> P'";
by (auto_tac (claset() addIs [r_into_trancl], simpset()));
qed "StTau_WkTau";

Goalw [WkTau_def] "[| P =tau=> P' ; P' =tau=> P'' |] ==> P =tau=> P''";
by (auto_tac (claset() addIs [trancl_trans], simpset()));
qed "WkTau_trans";

val prems = Goalw [WkTau_def]
 "[| P =tau=> P' ; !!P'. P -tau-> P' ==> Pr P' ; \
   \ !!P' P''. [| P =tau=> P' ; P' -tau-> P'' ; Pr P' |] \
   \ ==> Pr P'' |] ==> Pr P'";
by (auto_tac (claset() addIs prems @ [trancl_induct], simpset()));
qed "WkTau_induct";

val prems = Goalw [WkTau_def]
 "[| P =tau=> P' ; !!P P'. P -tau-> P' ==> Pr P P' ; \
   \ !!P P' P''. [| P =tau=> P' ; Pr P P' ; P' =tau=> P'' ; Pr P' P'' |] \
   \ ==> Pr P P'' |] ==> Pr P P'";
by (auto_tac (claset() addIs prems @ [trancl_trans_induct], simpset()));
qed "WkTau_trans_induct";


(*** Rules for WkEps ***)

Goalw [WkEps_def,RstrId_def]
 "P =eps=> P' ==> (P, P') : RstrId | P =tau=> P'";
by (Auto_tac);
qed "WkEpsD";

Goalw [WkEps_def,WkTau_def] "P -tau-> P' ==> P =eps=> P'";
by (Auto_tac);
qed "StTau_WkEps";

Goalw [WkEps_def] "P =tau=> P' ==> P =eps=> P'";
by (Auto_tac);
qed "WkTau_WkEps";

Goal "[| P =eps=> P' ; P ~= P' |] ==> P =tau=> P'";
by (auto_tac (claset() addDs [WkEpsD], simpset() addsimps [RstrId_def]));
qed "WkEps_WkTau";

Goalw [WkEps_def,WkTau_def,RstrId_def]
 "[| (P, P') : StTau^* ; rstr P ; rstr P' |] ==> P =eps=> P'";
by (auto_tac (claset() addSDs [rtranclD], simpset()));
qed "StTau_rtrancl_WkEps";

Goalw [WkEps_def,RstrId_def] "rstr P ==> P =eps=> P";
by (Auto_tac);
qed "WkEps_refl";

Goal "[| P =eps=> P' ; P' =eps=> P'' |] ==> P =eps=> P''";
by (auto_tac (claset() addSDs [WkEpsD]
              addIs [WkTau_WkEps,WkTau_trans,WkEps_refl],
              simpset() addsimps [RstrId_def]));
qed "WkEps_trans";

Goal "[| P =eps=> P' ; P' -tau-> P'' |] ==> P =eps=> P''";
by (auto_tac (claset() addIs [WkEps_trans,StTau_WkEps], simpset()));
qed "WkEps_StTau_trans";

val prems = Goal
 "[| P =eps=> P' ; !!P. rstr P ==> Pr P ; \
   \ !!P' P''. [| P =eps=> P' ; P' -tau-> P'' ; Pr P' |] \
   \ ==> Pr P'' |] ==> rstr P' --> Pr P'";
by (auto_tac (claset() addIs prems @ [rtrancl_induct], simpset()));
qed "lemma";

val prems = Goal
 "[| P =eps=> P' ; !!P. rstr P ==> Pr P ; \
   \ !!P' P''. [| P =eps=> P' ; P' -tau-> P'' ; Pr P' |] \
   \ ==> Pr P'' |] ==> Pr P'";
by (rtac (lemma RS mp) 1);
by (auto_tac (claset() addIs prems @ [WkEps_rstr2], simpset()));
qed "WkEps_induct";

val prems = Goal
 "[| P =eps=> P' ; !!P. rstr P ==> Pr P P ; \
   \ !!P P' P''. [| Pr P P' ; P =eps=> P' ; P' -tau-> P'' |] \
   \ ==> Pr P P'' |] ==> rstr P & rstr P' --> Pr P P'";
by (cut_inst_tac [("r", "StTau"), ("a", "P"), ("b", "P'"),
    ("P", "%(P,P').  rstr P & rstr P' --> Pr P P'")]
    rtrancl_full_induct 1);
(* P (-tau->)^* P' *)
by (cut_facts_tac prems 1);
by (force_tac (claset() addDs [WkEpsD,rtrancl_refl]
               addIs [trancl_into_rtrancl],
               simpset() addsimps [WkTau_def,RstrId_def]) 1);
(* base case *)
by (force_tac (claset() addIs prems, simpset()) 1);
(* induction case *)
by (forward_tac [StTau_rstr1] 1);
by (auto_tac (claset() addIs prems addSDs [StTau_rtrancl_WkEps], simpset()));
qed "lemma";

val prems = Goal
 "[| P =eps=> P' ; !!P. rstr P ==> Pr P P ; \
   \ !!P P' P''. [| Pr P P' ; P =eps=> P' ; P' -tau-> P'' |] \
   \ ==> Pr P P'' |] ==> Pr P P'";
by (rtac (lemma RS mp) 1);
by (auto_tac (claset() addIs prems @ [WkEps_rstr1,WkEps_rstr2], simpset()));
qed "WkEps_full_induct";

val prems = Goal
 "[| P =eps=> P' ; !!P. rstr P ==> rstr f P ; \
   \ !!P P'. P -tau-> P' ==> f P -tau-> f P' |] ==> f P =eps=> f P'";
by (cut_facts_tac prems 1);
by (etac WkEps_full_induct 1);
by (res_inst_tac [("P'", "f P'")] WkEps_trans 2);
by (auto_tac (claset() addIs prems @ [WkEps_refl,StTau_WkEps], simpset()));
qed "WkEps_trans_induct";


(*** General introduction and destruction rules ***)

Goalw [WkFOut_def]
 "[| P =eps=> P' ; P' -a<b>-> P'' |] ==> P =a<b>=> P''";
by (Auto_tac);
qed "WkFOutI";

Goalw [WkBOut_def]
 "[| P =eps=> P' ; P' -a<>-> P'' |] ==> P =a<>=> P''";
by (Auto_tac);
qed "WkBOutI";

Goalw [WkIn_def]
 "[| P =eps=> P' ; P' -a[]-> P'' |] ==> P =a[]=> P''";
by (Auto_tac);
qed "WkInI";

Goal "[| P =eps=> P' ; P' -tau-> P'' |] ==> P =tau=> P''";
by (auto_tac (claset() addIs [WkTau_trans] addSDs [WkEpsD,StTau_WkTau],
              simpset() addsimps [RstrId_def]));
qed "WkTauI";

Goalw [WkFOut_def]
 "P =a<b>=> P' ==> EX P''. P =eps=> P'' & P'' -a<b>-> P'";
by (Auto_tac);
qed "WkFOutD";

Goalw [WkBOut_def]
 "P =a<>=> fP' ==> EX P''. P =eps=> P'' & P'' -a<>-> fP'";
by (Auto_tac);
qed "WkBOutD";

Goalw [WkIn_def]
 "P =a[]=> fP' ==> EX P''. P =eps=> P'' & P'' -a[]-> fP'";
by (Auto_tac);
qed "WkInD";

Goalw [WkTau_def,WkEps_def]
 "P =tau=> P' ==>  EX P''. P =eps=> P'' & P'' -tau-> P'";
by (etac tranclE 1);
by (auto_tac (claset() addIs [StTau_rstr1],
              simpset() addsimps [RstrId_def]));
qed "WkTauD";


(*** Introduction rules for WkEps ***)

Goal "rstr P ==> .t.P =eps=> P";
by (auto_tac (claset() addIs StTau.intrs @ [StTau_WkEps], simpset()));
qed "WkEps_ta0";

Goal "P =eps=> P' ==> ALL fP fP'. P = fP c & P' = fP' c & \
 \ rstra fP & rstra fP' & fresha c fP & fresha c fP' \
 \ --> .#x. fP x =eps=> .#x. fP' x";
by (etac WkEps_full_induct 1);
by (force_tac (claset() addSDs [ext_pa_rstra]
    addIs RSTR.intrs @ [WkEps_refl], simpset()) 1);
by (forward_tac [StTau_rstr1] 1);
by (dres_inst_tac [("a", "c")] beta_exp_rstr 1);
by (auto_tac (claset() addIs StTau.intrs @ [WkEps_StTau_trans],
              simpset()));
qed "lemma";

Goal "[| P =eps=> P' ; fresha c fP ; fresha c fP' ; \
       \ rstra fP ; rstra fP' ; P = fP c ; P' = fP' c |] \
       \ ==> .#x. fP x =eps=> .#x. fP' x";
by (fast_tac (claset() addDs [lemma]) 1);
qed "WkEps_ta1";

Goal "[| P =eps=> P' ; rstr Q |] ==> P .| Q =eps=> P' .| Q";
by (eres_inst_tac [("f", "%x. x .| Q")] WkEps_trans_induct 1);
by (auto_tac (claset() addIs StTau.intrs @ RSTR.intrs, simpset()));
qed "WkEps_ta3a";

Goal "[| Q =eps=> Q' ; rstr P |] ==> P .| Q =eps=> P .| Q'";
by (eres_inst_tac [("f", "%x. P .| x")] WkEps_trans_induct 1);
by (auto_tac (claset() addIs StTau.intrs @ RSTR.intrs, simpset()));
qed "WkEps_ta3b";

Goal "[| P =a<b>=> P' ; Q =a[]=> fQ' |] \
       \ ==> P .| Q =eps=> P' .| fQ' b";
by (dtac WkFOutD 1);
by (dtac WkInD 1);
by (Clarify_tac 1);
by (res_inst_tac [("P'", "P'' .| P''a")] WkEps_trans 1);
by (res_inst_tac [("P'", "P'' .| Q")] WkEps_trans 1);
by (rtac StTau_WkEps 3);
by (auto_tac (claset() addIs StTau.intrs @
              [WkEps_ta3a,WkEps_ta3b,WkEps_rstr1,WkEps_rstr2],
              simpset()));
qed "WkEps_ta4a";

Goal "[| P =a[]=> fP' ; Q =a<b>=> Q' |] \
       \ ==> P .| Q =eps=> fP' b .| Q'";
by (dtac WkInD 1);
by (dtac WkFOutD 1);
by (Clarify_tac 1);
by (res_inst_tac [("P'", "P'' .| P''a")] WkEps_trans 1);
by (res_inst_tac [("P'", "P'' .| Q")] WkEps_trans 1);
by (rtac StTau_WkEps 3);
by (auto_tac (claset() addIs StTau.intrs @
              [WkEps_ta3a,WkEps_ta3b,WkEps_rstr1,WkEps_rstr2],
              simpset()));
qed "WkEps_ta4b";

Goal "[| P =a<>=> fP' ; Q =a[]=> fQ' |] \
       \ ==> P .| Q =eps=> .#x. (fP' x .| fQ' x)";
by (dtac WkBOutD 1);
by (dtac WkInD 1);
by (Clarify_tac 1);
by (res_inst_tac [("P'", "P'' .| P''a")] WkEps_trans 1);
by (res_inst_tac [("P'", "P'' .| Q")] WkEps_trans 1);
by (rtac StTau_WkEps 3);
by (auto_tac (claset() addIs StTau.intrs @
              [WkEps_ta3a,WkEps_ta3b,WkEps_rstr1,WkEps_rstr2],
              simpset()));
qed "WkEps_ta5a";

Goal "[| P =a[]=> fP' ; Q =a<>=> fQ' |] \
       \ ==> P .| Q =eps=>  .#x. (fP' x .| fQ' x)";
by (dtac WkInD 1);
by (dtac WkBOutD 1);
by (Clarify_tac 1);
by (res_inst_tac [("P'", "P'' .| P''a")] WkEps_trans 1);
by (res_inst_tac [("P'", "P'' .| Q")] WkEps_trans 1);
by (rtac StTau_WkEps 3);
by (auto_tac (claset() addIs StTau.intrs @
              [WkEps_ta3a,WkEps_ta3b,WkEps_rstr1,WkEps_rstr2],
              simpset()));
qed "WkEps_ta5b";

val WkEps_intrs = [WkEps_ta0,WkEps_ta1,WkEps_ta3a,WkEps_ta3b,
                   WkEps_ta4a,WkEps_ta4b,WkEps_ta5a,WkEps_ta5b];


Goal "[| P =eps=> P' ; Q =eps=> Q' |] ==> P .| Q =eps=> P' .| Q'";
by (res_inst_tac [("P'", "P' .| Q")] WkEps_trans 1);
by (auto_tac (claset() addIs WkEps_intrs @ [WkEps_rstr1,WkEps_rstr2],
              simpset()));
qed "WkEps_par_trans";


(*** Introduction rules for WkFOut ***)

Goalw [WkFOut_def] "P -a<b>-> P' ==> P =a<b>=> P'";
by (auto_tac (claset() addIs [WkEps_refl] addDs [StFOut_rstr1], simpset()));
qed "StFOut_WkFOut";

Goal "rstr P ==> a<b>.P =a<b>=> P";
by (auto_tac (claset() addIs [StFOut_WkFOut] @ StFOut.intrs, simpset()));
qed "WkFOut_fo0";

Goal "[| fP c =a<b>=> fP' c ; fresha c fP ; fresha c fP' ; \
       \ c ~: {a, b} ; rstra fP ; rstra fP' |] \
       \ ==> Res fP =a<b>=> Res fP'";
by (dtac WkFOutD 1);
by (etac exE 1);
by (etac conjE 1);
by (forward_tac [StFOut_rstr1] 1);
by (dres_inst_tac [("a", "c")] beta_exp_rstr 1);
by (force_tac (claset() addIs WkEps_intrs @ StFOut.intrs @ [WkFOutI],
               simpset()) 1);
qed "WkFOut_fo1";

Goal "[| P =a<b>=> P' ; rstr Q |] ==> P .| Q =a<b>=> P' .| Q";
by (auto_tac (claset() addSDs [WkFOutD]
    addIs StFOut.intrs @ WkEps_intrs @ [WkFOutI], simpset()));
qed "WkFOut_fo3a";

Goal "[| Q =a<b>=> Q' ; rstr P |] ==> P .| Q =a<b>=> P .| Q'";
by (auto_tac (claset() addSDs [WkFOutD]
    addIs StFOut.intrs @ WkEps_intrs @ [WkFOutI], simpset()));
qed "WkFOut_fo3b";

val WkFOut_intrs = [WkFOut_fo0,WkFOut_fo1,WkFOut_fo3a,WkFOut_fo3b];


(*** Introduction rules for WkBOut ***)

Goalw [WkBOut_def] "P -a<>-> P' ==> P =a<>=> P'";
by (auto_tac (claset() addIs [WkEps_refl] addDs [StBOut_rstr1], simpset()));
qed "StBOut_WkBOut";

Goal "[| fP c =a<c>=> fP' c ; fresha c fP ; fresha c fP' ; \
           \ a ~= c ; rstra fP ; rstra fP' |] \
           \ ==> Res fP =a<>=> fP'";
by (dtac WkFOutD 1);
by (Clarify_tac 1);
by (forward_tac [StFOut_rstr1] 1);
by (dres_inst_tac [("a", "c")] beta_exp_rstr 1);
by (force_tac (claset() addIs WkEps_intrs @ StBOut.intrs @ [WkBOutI],
               simpset()) 1);
qed "WkBOut_bo0";

Goal "[| fP c =a<>=> ffP' c ; fresha c fP ; freshaa c ffP' ; \
       \ a ~= c ; rstra fP ; ALL b. rstra ffP' b ; \
       \ ALL b. rstra (%x. ffP' x b) |] \
       \ ==> .#y. fP y =a<>=> (%x. .#y. ffP' y x)";
by (dtac WkBOutD 1);
by (etac exE 1);
by (etac conjE 1);
by (forward_tac [StBOut_rstr1] 1);
by (dres_inst_tac [("a", "c")] beta_exp_rstr 1);
by (force_tac (claset() addIs WkEps_intrs @ StBOut.intrs @ [WkBOutI],
               simpset()) 1);
qed "WkBOut_bo1";

Goal "[| P =a<>=> fP' ; rstr Q |] ==> P .| Q =a<>=> (%x. fP' x .| Q)";
by (auto_tac (claset() addSDs [WkBOutD]
    addIs StBOut.intrs @ WkEps_intrs @ [WkBOutI], simpset()));
qed "WkBOut_bo3a";

Goal "[| Q =a<>=> fQ' ; rstr P |] ==> P .| Q =a<>=> (%x. P .| fQ' x)";
by (auto_tac (claset() addSDs [WkBOutD]
    addIs StBOut.intrs @ WkEps_intrs @ [WkBOutI], simpset()));
qed "WkBOut_bo3b";

val WkBOut_intrs = [WkBOut_bo0,WkBOut_bo1,WkBOut_bo3a,WkBOut_bo3b];


(*** Introduction rules for WkIn ***)

Goalw [WkIn_def] "P -a[]-> P' ==> P =a[]=> P'";
by (auto_tac (claset() addIs [WkEps_refl] addDs [StIn_rstr1], simpset()));
qed "StIn_WkIn";

Goal "rstra fP ==> a[x].fP x =a[]=> fP";
by (auto_tac (claset() addIs StIn.intrs @ [StIn_WkIn], simpset()));
qed "WkIn_in0";

Goal "[| fP c =a[]=> ffP' c ; fresha c fP ; freshaa c ffP' ; \
       \ a ~= c ; rstra fP ; ALL b. rstra ffP' b ; \
       \ ALL b. rstra (%x. ffP' x b) |] \
       \ ==> .#y. fP y =a[]=> (%x. .#y. ffP' y x)";
by (dtac WkInD 1);
by (etac exE 1);
by (etac conjE 1);
by (forward_tac [StIn_rstr1] 1);
by (dres_inst_tac [("a", "c")] beta_exp_rstr 1);
by (force_tac (claset() addIs WkEps_intrs @ StIn.intrs @ [WkInI],
               simpset()) 1);
qed "WkIn_in1";

Goal "[| P =a[]=> fP' ; rstr Q |] ==> P .| Q =a[]=> (%x. fP' x .| Q)";
by (auto_tac (claset() addSDs [WkInD]
    addIs StIn.intrs @ WkEps_intrs @ [WkInI], simpset()));
qed "WkIn_in3a";


Goal "[| Q =a[]=> fQ' ; rstr P |] ==> P .| Q =a[]=> (%x. P .| fQ' x)";
by (auto_tac (claset() addSDs [WkInD]
    addIs StIn.intrs @ WkEps_intrs @ [WkInI], simpset()));
qed "WkIn_in3b";

val WkIn_intrs = [WkIn_in0,WkIn_in1,WkIn_in3a,WkIn_in3b];


(*** Introduction rules for WkTau ***)

Goal "rstr P ==> .t.P =tau=> P";
by (auto_tac (claset() addIs StTau.intrs @ [StTau_WkTau], simpset()));
qed "WkTau_ta0";

Goal "[| fP c =tau=> fP' c ; fresha c fP ; fresha c fP' ; \
       \ rstra fP ; rstra fP' |] \
       \ ==> Res fP =tau=> Res fP'";
by (dtac WkTauD 1);
by (etac exE 1);
by (etac conjE 1);
by (forward_tac [StTau_rstr1] 1);
by (dres_inst_tac [("a", "c")] beta_exp_rstr 1);
by (force_tac (claset() addIs WkEps_intrs @ StTau.intrs @ [WkTauI],
               simpset()) 1);
qed "WkTau_ta1";

Goal "[| P =tau=> P' ; rstr Q |] ==> P .| Q =tau=> P' .| Q";
by (auto_tac (claset() addSDs [WkTauD]
    addIs StTau.intrs @ WkEps_intrs @ [WkTauI], simpset()));
qed "WkTau_ta3a";

Goal "[| Q =tau=> Q' ; rstr P |] ==> P .| Q =tau=> P .| Q'";
by (auto_tac (claset() addSDs [WkTauD]
    addIs StTau.intrs @ WkEps_intrs @ [WkTauI], simpset()));
qed "WkTau_ta3b";

Goal "[| P =a<b>=> P' ; Q =a[]=> fQ' |] \
       \ ==> P .| Q =tau=> P' .| fQ' b";
by (auto_tac (claset() addSDs [WkFOutD,WkInD]
    addIs StTau.intrs @ [WkEps_par_trans] @ [WkTauI], simpset()));
qed "WkTau_ta4a";

Goal "[| P =a[]=> fP' ; Q =a<b>=> Q' |] \
       \ ==> P .| Q =tau=> fP' b .| Q'";
by (auto_tac (claset() addSDs [WkFOutD,WkInD]
    addIs StTau.intrs @ [WkEps_par_trans] @ [WkTauI], simpset()));
qed "WkTau_ta4b";

Goal "[| P =a<>=> fP' ; Q =a[]=> fQ' |] \
       \ ==> P .| Q =tau=> .#x. (fP' x .| fQ' x)";
by (auto_tac (claset() addSDs [WkBOutD,WkInD]
    addIs StTau.intrs @ [WkEps_par_trans] @ [WkTauI], simpset()));
qed "WkTau_ta5a";

Goal "[| P =a[]=> fP' ; Q =a<>=> fQ' |] \
       \ ==> P .| Q =tau=>  .#x. (fP' x .| fQ' x)";
by (auto_tac (claset() addSDs [WkBOutD,WkInD]
    addIs StTau.intrs @ [WkEps_par_trans] @ [WkTauI], simpset()));
qed "WkTau_ta5b";

val WkTau_intrs = [WkTau_ta0,WkTau_ta1,WkTau_ta3a,WkTau_ta3b,
                   WkTau_ta4a,WkTau_ta4b,WkTau_ta5a,WkTau_ta5b];

val StTrans_WkTrans = [StFOut_WkFOut,StBOut_WkBOut,StIn_WkIn,StTau_WkEps];