File Restricted.ML


(*** Cases ***)

Goal "[| .t.P' = P ; rstr P |] ==> rstr P'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases1";

Goal "[| a<b>.P' = P ; rstr P |] ==> rstr P'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases2";

Goal "[| a[y].fP' y = P ; rstr P |] ==> rstra fP'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases3";

Goal "[| .#x. fP' x = P ; rstr P |] ==> rstra fP'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases4";

Goal "[| P' .+ Q' = P ; rstr P |] ==> rstr P' & rstr Q'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases5";

Goal "[| P' .| Q' = P ; rstr P |] ==> rstr P' & rstr Q'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases6";


Goal "[| .[a.=b]P' = P ; rstr P |] ==> rstr P'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases7";

Goal "[| .!a[y].fP' y = P ; rstr P |] ==> rstra fP'";
by (auto_tac (claset() addEs RSTR.elims, simpset()));
qed "rstr_cases9";

val rstr_cases = [rstr_cases1,rstr_cases2,rstr_cases3,rstr_cases4,
                  rstr_cases5,rstr_cases6,rstr_cases7,rstr_cases9];

Goal "[| .0 = fP a ; rstra fP |] ==> fP = (%x. .0)";
by (auto_tac (claset() addEs RSTRA.elims, simpset()));
qed "rstra_cases0";

Goal "[| .t.P = fP a ; rstra fP |] ==> EX fP'. \
  \ rstra fP' & fP = (%x. .t.fP' x)";
by (auto_tac (claset() addEs RSTRA.elims, simpset()));
qed "rstra_cases1";

Goal "[| b<c>.P = fP a ; rstra fP |] ==> EX fb fc fP'. \
  \ wfna fb & wfna fc & rstra fP' & \
  \ fP = (%x. fb x<fc x>.fP' x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases2";

Goal "[| b[y].fP' y = fP a ; rstra fP |] ==> EX fb ffP. \
  \ wfna fb & (ALL b. rstra ffP b) & (ALL b. rstra (%x. ffP x b)) & \
  \ fP = (%x. fb x[y]. ffP y x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases3";

Goal "[| .#y. fP' y = fP a ; rstra fP |] ==> EX ffP. \
  \ (ALL b. rstra ffP b) & (ALL b. rstra (%x. ffP x b)) & \
  \ fP = (%x. .#y. ffP y x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases4";

Goal "[| P .+ Q = fP a ; rstra fP |] ==> EX fP' fQ. \
  \ rstra fP' & rstra fQ & fP = (%x. fP' x .+ fQ x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases5";

Goal "[| P .| Q = fP a ; rstra fP |] ==> EX fP' fQ. \
  \ rstra fP' & rstra fQ & fP = (%x. fP' x .| fQ x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases6";

Goal "[| .[b.=c]P = fP a ; rstra fP |] ==> EX fb fc fP'. \
  \ wfna fb & wfna fc & rstra fP' & \
  \ fP = (%x. .[fb x.=fc x]fP' x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases7";

Goal "[| .[b.~=c]P = fP a ; rstra fP |] ==> Pr";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases8";

Goal "[| .!P = fP a ; rstra fP |] ==> EX fb ffP'. \
  \ (ALL b. rstra ffP' b) & (ALL b. rstra (%x. ffP' x b)) & \
  \  fP = (%x. .!fb x[y].ffP' y x)";
by (eresolve_tac RSTRA.elims 1);
by (Auto_tac);
qed "rstra_cases9";

val rstra_cases = [rstra_cases0, rstra_cases1, rstra_cases2,
                   rstra_cases3, rstra_cases4, rstra_cases5,
                   rstra_cases6, rstra_cases7, rstra_cases8,
                   rstra_cases9];

Goal "rstr fa c[y].ffP y c ==> rstra (%x. ffP x c)";
by (eresolve_tac RSTR.elims 1);
by (Auto_tac);
qed "rstr_In_rstra2";

Goal "rstr .#y. ffP y c ==> rstra (%x. ffP x c)";
by (eresolve_tac RSTR.elims 1);
by (Auto_tac);
qed "rstr_Res_rstra2";

Goal "rstr (P .+ Q) ==> rstr P";
by (etac RSTR.elim 1);
by (Auto_tac);
qed "rstr_Plus1";

Goal "rstr (P .+ Q) ==> rstr Q";
by (etac RSTR.elim 1);
by (Auto_tac);
qed "rstr_Plus2";

Goal "rstr (P .| Q) ==> rstr P";
by (etac RSTR.elim 1);
by (Auto_tac);
qed "rstr_Par1";

Goal "rstr (P .| Q) ==> rstr Q";
by (etac RSTR.elim 1);
by (Auto_tac);
qed "rstr_Par2";

Goal "rstr (.[a.~=b]P) ==> Pr";
by (etac RSTR.elim 1);
by (Auto_tac);
qed "rstr_Mmt";

Goal "rstr (.!P) ==> EX a fP. P = a[x].fP x & rstra fP";
by (etac RSTR.elim 1);
by (Auto_tac);
qed "rstr_Repl";

Goal "f = g ==> f x = g x";
by (Auto_tac);
qed "fun_eq_inst";

Goal "ALL x. f x = g x ==> f = g";
by (rtac ext 1);
by (Auto_tac);
qed "fun_eq_ext";

Goal "(%x. fa x[y].ffP y x) = (%x. fb x[y].ffQ y x) \
 \ ==> fa = fb";
by (rtac ext 1);
by (auto_tac (claset() addDs [fun_eq_inst], simpset()));
qed "In_eq1";

Goal "(%x. fa x[y].ffP y x) = (%x. fb x[y].ffQ y x) \
 \ ==> ffP = ffQ";
by (rtac ext 1);
by (rtac ext 1);
by (auto_tac (claset() addDs [fun_eq_inst], simpset()));
qed "In_eq2";

Goal "rstra (%x. fb x[y].ffP y x) ==> rstra ffP b";
by (etac RSTRA.elim 1);
by (force_tac (claset() addSDs [fun_eq_inst], simpset()) 1);
by (force_tac (claset() addSDs [fun_eq_inst], simpset()) 1);
by (force_tac (claset() addSDs [fun_eq_inst], simpset()) 1);
by (REPEAT
 (force_tac (claset() addSDs [fun_eq_inst], simpset()) 2));
by (dtac In_eq2 1);
by (Auto_tac);
qed "rstra_In_rstra1";

Goal "rstra (%x. fb x[y].ffP y x) ==> rstra (%x. ffP x b)";
by (etac RSTRA.elim 1);
by (force_tac (claset() addSDs [fun_eq_inst], simpset()) 1);
by (force_tac (claset() addSDs [fun_eq_inst], simpset()) 1);
by (force_tac (claset() addSDs [fun_eq_inst], simpset()) 1);
by (REPEAT
 (force_tac (claset() addSDs [fun_eq_inst], simpset()) 2));
by (dtac In_eq2 1);
by (Auto_tac);
qed "rstra_In_rstra2";


(*** Relating well-formedness and restrictedness ***)

Goal "rstra fP ==> wfpa fP";
by (etac RSTRA.induct 1);
by (auto_tac (claset() addSIs WFPA.intrs, simpset()));
qed "rstra_wfpa";

Goal "rstr P ==> wfp P";
by (etac RSTR.induct 1);
by (auto_tac (claset() addSIs WFP.intrs addIs [rstra_wfpa], simpset()));
qed "rstr_wfp";

Goal "rstra fP ==> rstra (%x. fP b)";
by (etac RSTRA.induct 1);
by (auto_tac (claset() addSIs RSTRA.intrs @ WFNA.intrs, simpset()));
qed "rstra_rstra";

Goal "rstr P ==> rstra (%x. P)";
by (etac RSTR.induct 1);
by (auto_tac (claset() addSIs RSTRA.intrs @ WFNA.intrs
              addIs [rstra_rstra], simpset()));
qed "rstr_rstra";

Goal "rstra fP ==> rstr fP b";
by (etac RSTRA.induct 1);
by (auto_tac (claset() addSIs RSTR.intrs, simpset()));
qed "rstra_rstr";

Goal "wfpa fP ==> ALL c. rstr fP c --> rstra fP";
by (etac WFPA.induct 1);
(* Inaction, silent prefix, output *)
by (force_tac (claset() addIs RSTRA.intrs addEs RSTR.elims, simpset()) 1);
by (force_tac (claset() addIs RSTRA.intrs addEs RSTR.elims, simpset()) 1);
by (force_tac (claset() addIs RSTRA.intrs addEs RSTR.elims, simpset()) 1);
(* Input *)
by (Clarify_tac 1);
by (dtac rstr_In_rstra2 1);
by (resolve_tac RSTRA.intrs 1);
by (force_tac (claset() addDs [rstra_rstr], simpset()) 1);
by (dres_inst_tac [("b", "d")] rstra_rstr 1);
by (eres_inst_tac [("x", "d")] allE 1);
by (force_tac (claset() addDs [rstra_rstr], simpset()) 1);
by (atac 1);
(* Restriction *)
by (Clarify_tac 1);
by (dtac rstr_Res_rstra2 1);
by (resolve_tac RSTRA.intrs 1);
by (force_tac (claset() addDs [rstra_rstr], simpset()) 1);
by (dres_inst_tac [("b", "d")] rstra_rstr 1);
by (eres_inst_tac [("x", "d")] allE 1);
by (force_tac (claset() addDs [rstra_rstr], simpset()) 1);
(* Choice, parallel composition *)
by (force_tac (claset() addSIs RSTRA.intrs addDs [rstr_Plus1,rstr_Plus2],
               simpset()) 1);
by (force_tac (claset() addSIs RSTRA.intrs addDs [rstr_Par1,rstr_Par2],
               simpset()) 1);
(* Match, mismatch *)
by (force_tac (claset() addSIs RSTRA.intrs addEs RSTR.elims,
               simpset()) 1);
by (force_tac (claset() addSIs RSTRA.intrs addDs [rstr_Mmt],
               simpset()) 1);
(* Replication *)
by (Clarify_tac 1);
by (dtac rstr_Repl 1);
by (Clarify_tac 1);
by ((dres_inst_tac [("a", "c"), ("b", "a")]
     (rotate_prems 1 wfpa_cases3) 1)
     THEN (Asm_simp_tac 1));
by (Clarify_tac 1);
by (resolve_tac RSTRA.intrs 1);
by (ALLGOALS (eres_inst_tac [("x", "c")] allE));
by (auto_tac (claset() addIs RSTR.intrs @ [rstra_In_rstra1,rstra_In_rstra2],
              simpset()));
qed "lemma";

Goal "[| wfpa fP ; rstr fP c |] ==> rstra fP";
by (fast_tac (claset() addDs [lemma]) 1);
qed "wfpa_rstra";

Goal "[| fP a = fQ a ; fresha a fP ; fresha a fQ ; rstra fP ; rstra fQ |] \
 \ ==> fP = fQ";
by (fast_tac (claset() addIs [ext_pa,rstra_wfpa]) 1);
qed "ext_pa_rstra";

Goal "[| ffP a = ffQ a ; freshaa a ffP ; freshaa a ffQ ; ALL b. rstra ffP b ; \
 \ ALL b. rstra (%x. ffP x b) ; ALL b. rstra ffQ b ; ALL b. rstra (%x. ffQ x b) |] \
 \ ==> ffP = ffQ";
by (res_inst_tac [("a", "a")] ext_paa 1);
by (auto_tac (claset() addIs [rstra_wfpa], simpset()));
qed "ext_paa_rstra";

Goal "rstr P ==> EX fP. rstra fP & fresha a fP & P = fP a";
by (forward_tac [rstr_wfp] 1);
by (auto_tac (claset() addIs [wfpa_rstra] addSDs [beta_exp],
              simpset()));
qed "beta_exp_rstr";

Goal "rstra fP ==> EX ffP. (ALL b. rstra ffP b) & (ALL b. rstra (%x. ffP x b)) & \
 \ freshaa a ffP & fP = ffP a";
by (dres_inst_tac [("a", "a")] (RSTR.Res RS beta_exp_rstr) 1);
by (Clarify_tac 1);
by ((forward_tac [rstra_cases4] 1) THEN (atac 1));
by (Clarify_tac 1);
by (res_inst_tac [("x", "%x y. ffP y x")] exI 1);
by (auto_tac (claset(), simpset() addsimps
    [freshaa_def,fresha_def,fnaa_def,fna_def]));
qed "beta_expa_rstra";

Goal "rstra fP ==> (ALL P. fP = (%x. P) --> rstr P)";
by (etac RSTRA.induct 1);
by (ALLGOALS Clarify_tac);
(* inaction *)
by (dtac inst_fun_eq 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* silent prefix *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* output prefix *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* input prefix *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (rotate_tac 1 1);
by (eres_inst_tac [("x", "x")] allE 1);
by (etac conjE 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* restriction *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (rotate_tac 1 1);
by (eres_inst_tac [("x", "x")] allE 1);
by (etac conjE 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* Choice *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* Parallel composition *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* Matching *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (dres_inst_tac [("b", "x")] rstra_rstr 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
(* replication *)
by (dres_inst_tac [("x", "x")] inst_fun_eq 1);
by (rotate_tac 1 1);
by (eres_inst_tac [("x", "x")] allE 1);
by (etac conjE 1);
by (force_tac (claset() addIs RSTR.intrs, simpset()) 1);
qed "lemma";

Goal "rstra (%x. P) ==> rstr P";
by (fast_tac (claset() addDs [lemma]) 1);
qed "simp_rstra_rstr";

Goal "rstr (.#x. P) ==> rstr P";
by (auto_tac (claset() addEs RSTR.elims addDs [simp_rstra_rstr], simpset()));
qed "res_rstr_rstr";

Goal "rstr P --> rstr Q ==> rstr (.#x. P) --> rstr (.#x. Q)";
by (auto_tac (claset() addIs RSTR.intrs @ [rstr_rstra,res_rstr_rstr], simpset()));
qed "rstr_mono_res";

Goal "rstra fP --> rstra fQ ==> rstr (.#x. fP x) --> rstr (.#x. fQ x)";
by (auto_tac (claset() addIs RSTR.intrs addEs RSTR.elims, simpset()));
qed "rstra_mono_res";

val rstr_monos = [rstr_mono_res,rstra_mono_res];