File Receptive.ML


(*** Restrictedness ***)

Goal "rr{m}P ==> rstr P";
by (etac RR.induct 1);
by (auto_tac (claset() addIs RSTR.intrs, simpset()));
qed "rr_rstr";

Goal "ee{m}P ==> rstr P";
by (etac EE.induct 1);
by (auto_tac (claset() addIs RSTR.intrs, simpset()));
qed "ee_rstr";

Goal "ur{m}P ==> rstr P";
by (etac UR.induct 1);
by (auto_tac (claset() addIs RSTR.intrs, simpset()));
qed "ur_rstr";

Goal "ue{m}P ==> rstr P";
by (etac UE.induct 1);
by (auto_tac (claset() addIs RSTR.intrs, simpset()));
qed "ue_rstr";


(*** Relationships ***)

Goal "ur{m}P ==> rr{m}P";
by (etac UR.induct 1);
by (auto_tac (claset() addIs RR.intrs, simpset()));
qed "ur_rr";

Goal "ue{m}P ==> ee{m}P";
by (etac UE.induct 1);
by (auto_tac (claset() addIs EE.intrs, simpset()));
qed "ue_ee";


(*** Possibility of Transitions ***)

Goal "rr{m}P ==> EX fP. P -m[]-> fP";
by (etac RR.induct 1);
(* input prefix, choice *)
by (force_tac (claset() addIs StIn.intrs, simpset()) 1);
by (force_tac (claset() addIs StIn.intrs @ RSTRA.intrs, simpset()) 1);
by (force_tac (claset() addIs StIn.intrs @ RSTRA.intrs, simpset()) 1);
(* parallel composition *)
by (force_tac (claset() addIs StIn.intrs @ RSTRA.intrs @ [rstr_rstra],
               simpset()) 1);
by (force_tac (claset() addIs StIn.intrs @ RSTRA.intrs @ [rstr_rstra],
               simpset()) 1);
(* restriction *)
by (Clarify_tac 1);
by (forward_tac [StIn_rstra2] 1);
by (dres_inst_tac [("fP", "fPa"), ("a", "n")] beta_expa_rstra 1);
by (Clarify_tac 1);
by (res_inst_tac [("x", "%x. .#y. ffP y x")] exI 1);
by (fast_tac (claset() addIs StIn.intrs) 1);
(* matching, replication *)
by (force_tac (claset() addIs StIn.intrs @ RSTRA.intrs, simpset()) 1);
by (force_tac (claset() addIs StIn.intrs, simpset()) 1);
qed "rr_StIn";

Goal "ee{m}P ==> (EX b P'. P -m<b>-> P') | (EX fP. P -m<>-> fP)";
by (etac EE.induct 1);
(* output prefix, choice *)
by (force_tac (claset() addIs StFOut.intrs, simpset()) 1);
by (force_tac (claset() addIs StFOut.intrs @ StBOut.intrs @
    RSTRA.intrs, simpset()) 1);
by (force_tac (claset() addIs StFOut.intrs @ StBOut.intrs @
    RSTRA.intrs, simpset()) 1);
(* parallel composition *)
by (force_tac (claset() addIs StFOut.intrs  @ StBOut.intrs @
    RSTRA.intrs @ [rstr_rstra], simpset()) 1);
by (force_tac (claset() addIs StFOut.intrs  @ StBOut.intrs @
    RSTRA.intrs @ [rstr_rstra], simpset()) 1);
(* restriction *)
by (etac disjE 1);
 (* free output *)
 by (REPEAT (etac exE 1));
 by (forward_tac [StFOut_rstr2] 1);
 by (dres_inst_tac [("P", "P'"), ("a", "n")] beta_exp_rstr 1);
 by (REPEAT (eresolve_tac [exE,conjE] 1));
 by (case_tac "n=b" 1);
  (* bound case *)
  by (rtac disjI2 1);
  by (res_inst_tac [("x", "fPa")] exI 1);
  by (fast_tac (claset() addIs StBOut.intrs) 1);
  (* free case *)
  by (rtac disjI1 1);
  by (res_inst_tac [("x", "b")] exI 1);
  by (res_inst_tac [("x", ".#x. fPa x")] exI 1);
  by (fast_tac (claset() addIs StFOut.intrs) 1);
 (* bound output *)
 by (rtac disjI2 1);
 by (Clarify_tac 1);
 by (forward_tac [StBOut_rstra2] 1);
 by (dres_inst_tac [("fP", "fPa"), ("a", "n")] beta_expa_rstra 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "%x. .#y. ffP y x")] exI 1);
 by (fast_tac (claset() addIs StBOut.intrs) 1);
(* matching *)
by (force_tac (claset() addIs StFOut.intrs @ StBOut.intrs @
    RSTRA.intrs, simpset()) 1);
qed "ee_StOut";

Goal "ur{m}P ==> EX fP. P -m[]-> fP";
by (auto_tac (claset() addDs [rr_StIn,ur_rr], simpset()));
qed "ur_StIn";

Goal "ue{m}P ==> (EX b P'. P -m<b>-> P') | (EX fP. P -m<>-> fP)";
by (auto_tac (claset() addDs [ee_StOut,ue_ee], simpset()));
qed "ue_StOut";


(*** Transitions yield inclusion ***)

Goal "P -m[]-> fP ==> rr{m}P";
by (etac StIn.induct 1);
by (auto_tac (claset() addIs RR.intrs, simpset()));
qed "StIn_rr";

Goal "P -m<b>-> P' ==> ee{m}P";
by (etac StFOut.induct 1);
by (auto_tac (claset() addIs EE.intrs, simpset()));
qed "StFOut_ee";

Goal "P -m<>-> fP ==> ee{m}P";
by (etac StBOut.induct 1);
by (auto_tac (claset() addIs EE.intrs @ [StFOut_ee] addEs StFOut.elims, simpset()));
qed "StBOut_ee";


(*** Impossibility of transitions ***)

Goal "[| ~ rr{m}P ; P -m[]-> fP |] ==> Pr";
by (auto_tac (claset() addIs [StIn_rr], simpset()));
qed "not_rr_not_StIn";

Goal "[| ~ ee{m}P ; P -m<b>-> P' |] ==> Pr";
by (auto_tac (claset() addIs [StFOut_ee], simpset()));
qed "not_ee_not_StFOut";

Goal "[| ~ ee{m}P ; P -m<>-> fP |] ==> Pr";
by (auto_tac (claset() addIs [StBOut_ee], simpset()));
qed "not_ee_not_StBOut";


(*** Uniqueness of transitions ***)

Goal "ur{m}P ==> ALL fP fP'. P -m[]-> fP & P -m[]-> fP' --> fP = fP'";
by (etac UR.induct 1);
by (auto_tac (claset() addSEs [StIn_In,StIn_Ch,StIn_Pr,StIn_Rp]
    addDs [not_rr_not_StIn], simpset()));
qed "lemma";

Goal "[| ur{m}P ;  P -m[]-> fP ; P -m[]-> fP' |] ==> fP = fP'";
by (fast_tac (claset() addDs [lemma]) 1);
qed "ur_unique";

Goal "ue{m}P ==> ALL a b P' P''. P -m<a>-> P' & P -m<b>-> P'' \
 \ --> a=b & P'=P''";
by (etac UE.induct 1);
by (auto_tac (claset() addSEs [StFOut_Ot,StFOut_Ch,StFOut_Pr]
     addDs [not_ee_not_StFOut], simpset()));
qed "lemma";

Goal "[| ue{m}P ; P -m<a>-> P' ; P -m<b>-> P'' |] ==> a=b & P'=P''";
by (fast_tac (claset() addDs [lemma]) 1);
qed "ue_unique_FOut_FOut";

Goal "ue{m}P ==> ALL a b fP fP'. P -m<>-> fP & P -m<>-> fP' \
 \ --> fP=fP'";
by (etac UE.induct 1);
by (auto_tac (claset() addSEs [StBOut_Ot,StBOut_Ch,StBOut_Pr]
     addDs [not_ee_not_StBOut], simpset()));
qed "lemma";

Goal "[| ue{m}P ; P -m<>-> fP ; P -m<>-> fP' |] ==> fP = fP'";
by (fast_tac (claset() addDs [lemma]) 1);
qed "ue_unique_BOut_BOut";

Goal "ue{m}P ==> ALL a P' fP'. P -m<a>-> P' & P -m<>-> fP' \
 \ --> Pr";
by (etac UE.induct 1);
by (auto_tac (claset() addSEs
     [StFOut_Ot,StFOut_Ch,StFOut_Pr,StBOut_Ot,StBOut_Ch,StBOut_Pr]
     addDs [not_ee_not_StFOut,not_ee_not_StBOut], simpset()));
qed "lemma";

Goal "[| ue{m}P ; P -m<a>-> P' ; P -m<>-> fP' |] ==> Pr";
by (auto_tac (claset() addDs [lemma], simpset()));
qed "ue_unique_FOut_BOut";

val ue_uniques = [ue_unique_FOut_FOut,ue_unique_BOut_BOut,ue_unique_FOut_BOut];