File Subst.ML


(************************************************************)
(*** Renamings                                            ***)
(************************************************************)

Addsimps [nren_def];

Goal "n{x<->x}a = a";
by (Simp_tac 1);
qed "nren_id";

Goal "p{x<->x}P = P";
by (induct_tac "P" 1);
by (Auto_tac);
qed "pren_id";

Addsimps [pren_id];

Goal "n{x<->y}a = n{y<->x}a";
by (Simp_tac 1);
qed "nren_sym";

Goal "p{x<->y}P = p{y<->x}P";
by (induct_tac "P" 1);
by (Auto_tac);
qed "pren_sym";

Goal "a ~: {y, z} ==> n{y<->z}n{z<->x}a = n{y<->x}a";
by (Auto_tac);
qed "nren_trans";

Goal "{y, z} Int n P = {} --> p{y<->z}p{z<->x}P = p{y<->x}P";
by (induct_tac "P" 1);
by (auto_tac (claset() addIs [nren_trans],
              simpset() delsimps [nren_def]));
qed "lemma";

Goal "[| y ~: n P ; z ~: n P |] ==> p{y<->z}p{z<->x}P = p{y<->x}P";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "pren_trans";


Goal "a ~: {x, y} ==> n{x<->y}a = a";
by (Auto_tac);
qed "nren_vain";

Goal "x ~: n P & y ~: n P --> p{y<->x}P = P";
by (induct_tac "P" 1);
by (Auto_tac);
qed "lemma";

Goal "[| x ~: n P ; y ~: n P |] ==> p{y<->x}P = P";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "pren_vain";

Addsimps [pren_vain];

Goal "n{n{x<->y}x'<->n{x<->y}y'}n{x<->y}a = n{x<->y}n{x'<->y'}a";
by (Auto_tac);
qed "nren_swap";

Goal "n{x'<->y'}n{n{x'<->y'}x<->n{x'<->y'}y}a = n{x<->y}n{x'<->y'}a";
by (Auto_tac);
qed "nren_swap_alt";

Goal "p{n{x<->y}x'<->n{x<->y}y'}p{x<->y}P = p{x<->y}p{x'<->y'}P";
by (induct_tac "P" 1);
by (auto_tac (claset() addIs [nren_swap],
              simpset() delsimps [nren_def]));
qed "pren_swap";

Goal "p{x'<->y'}p{n{x'<->y'}x<->n{x'<->y'}y}P = p{x<->y}p{x'<->y'}P";
by (induct_tac "P" 1);
by (auto_tac (claset() addIs [nren_swap_alt],
              simpset() delsimps [nren_def]));
qed "pren_swap_alt";

Goal "x' ~: {x, y} \
  \ ==> p{x'<->n{x<->y}y'}p{x<->y}P = p{x<->y}p{x'<->y'}P";
by (dtac nren_vain 1);
by (cut_inst_tac [("x", "x"), ("y", "y"),
                  ("x'", "x'"), ("y'", "y'")] pren_swap 1);
by (Auto_tac);
qed "pren_swap1";

Goal "y' ~: {x, y} \
  \ ==> p{n{x<->y}x'<->y'}p{x<->y}P = p{x<->y}p{x'<->y'}P";
by (dtac nren_vain 1);
by (cut_inst_tac [("x", "x"), ("y", "y"),
                  ("x'", "x'"), ("y'", "y'")] pren_swap 1);
by (Auto_tac);
qed "pren_swap2";

Goal "x ~: n P --> \
 \ (if b : n P then n (p{x<->b}P) = insert x (n P) - {b} \
 \             else n (p{x<->b}P) = n P)";
by (induct_tac "P" 1);
by (ALLGOALS Clarify_tac);

(* Inaction *)
by (Force_tac 1);

(* Silent prefix *)
by (Force_tac 1);

(* Output *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs" 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);

(* Input *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs" 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);

(* Restriction *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs" 1);
by (Force_tac 1);
by (Force_tac 1);

(* Choice *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs1" 1);
by (EVERY [(case_tac "b : n procs2" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "b : n procs2" 1),
           (Force_tac 1),
           (Force_tac 1)]);

(* Parallel Composition *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs1" 1);
by (EVERY [(case_tac "b : n procs2" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "b : n procs2" 1),
           (Force_tac 1),
           (Force_tac 1)]);

(* Matching *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs" 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);

(* Mismatching *)
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (case_tac "b : n procs" 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);

(* Replication *)
by (Force_tac 1);

qed "lemma";

Goal "x ~: n P ==> \
 \ if b : n P then n (p{x<->b}P) = insert x (n P) - {b} \
 \            else n (p{x<->b}P) = n P";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "n_pren";

Goal "[| x ~: n P ; b ~: n P |] ==> n (p{x<->b}P) = n P";
by (dres_inst_tac [("b", "b")] n_pren 1);
by (Auto_tac);
qed "n_pren1";

Goal "[| x ~: n P ; b : n P |] \
 \ ==> n (p{x<->b}P) = insert x (n P) - {b}";
by (dres_inst_tac [("b", "b")] n_pren 1);
by (Auto_tac);
qed "n_pren2";

Goal "x ~: n P ==> b ~: n (p{x<->b}P)";
by (dres_inst_tac [("b", "b")] n_pren 1);
by (case_tac "b : n P" 1);
by (Auto_tac);
qed "pren_del";

Goal "x : n P & b : n P --> n (p{x<->b}P) = n P";
by (induct_tac "P" 1);
by (ALLGOALS Clarify_tac);
(* Inaction, silent prefix *)
by (Force_tac 1);
by (Force_tac 1);
(* Output *)
by (case_tac "b : n procs" 1);
by (case_tac "x : n procs" 1);
by (etac impE 1);
by (Fast_tac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "x"), ("b", "b")] n_pren2 1);
by (atac 1);
by (EVERY [(case_tac "a1=x" 1),
           (Force_tac 1),
           (case_tac "a2=x" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (case_tac "x : n procs" 1);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren2 1);
by (atac 1);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs")] pren_sym 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren1 1);
by (atac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
(* Input *)
by (case_tac "b : n procs" 1);
by (case_tac "x : n procs" 1);
by (etac impE 1);
by (Fast_tac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "x"), ("b", "b")] n_pren2 1);
by (atac 1);
by (EVERY [(case_tac "a1=x" 1),
           (Force_tac 1),
           (case_tac "a2=x" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (case_tac "x : n procs" 1);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren2 1);
by (atac 1);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs")] pren_sym 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren1 1);
by (atac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
(* Restriction *)
by (case_tac "b : n procs" 1);
by (case_tac "x : n procs" 1);
by (etac impE 1);
by (Fast_tac 1);
by (Force_tac 1);
by (forw_inst_tac [("x", "x"), ("b", "b")] n_pren2 1);
by (atac 1);
by (Force_tac 1);
by (case_tac "x : n procs" 1);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren2 1);
by (atac 1);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs")] pren_sym 1);
by (Force_tac 1);
by (forw_inst_tac [("x", "x"), ("b", "b")] n_pren1 1);
by (atac 1);
by (Force_tac 1);
(* Plus *)
by (case_tac "b : n procs1" 1);
by (case_tac "x : n procs1" 1);
by (etac impE 1);
by (Fast_tac 1);
by (dtac n_pren2 2);
by (atac 2);
by (case_tac "x : n procs1" 3);
by (dtac n_pren2 3);
by (atac 3);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs1")] pren_sym 3);
by (dtac n_pren1 4);
by (atac 4);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (Force_tac 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren1], simpset()) 1);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (Force_tac 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren1], simpset()) 1);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (Force_tac 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren1], simpset()) 1);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset(), simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
(* Parallel composition *)
by (case_tac "b : n procs1" 1);
by (case_tac "x : n procs1" 1);
by (etac impE 1);
by (Fast_tac 1);
by (dtac n_pren2 2);
by (atac 2);
by (case_tac "x : n procs1" 3);
by (dtac n_pren2 3);
by (atac 3);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs1")] pren_sym 3);
by (dtac n_pren1 4);
by (atac 4);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (Force_tac 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren1], simpset()) 1);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (Force_tac 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren1], simpset()) 1);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (Force_tac 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren1], simpset()) 1);
by (case_tac "b : n procs2" 1);
by (case_tac "x : n procs2" 1);
by (force_tac (claset(), simpset() addsimps [pren_sym]) 1);
by (force_tac (claset() addDs [n_pren2], simpset()) 1);
by (force_tac (claset() addDs [n_pren2], simpset() addsimps [pren_sym]) 1);
(* Matching *)
by (case_tac "b : n procs" 1);
by (case_tac "x : n procs" 1);
by (etac impE 1);
by (Fast_tac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "x"), ("b", "b")] n_pren2 1);
by (atac 1);
by (EVERY [(case_tac "a1=x" 1),
           (Force_tac 1),
           (case_tac "a2=x" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (case_tac "x : n procs" 1);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren2 1);
by (atac 1);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs")] pren_sym 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren1 1);
by (atac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
(* Mismatching *)
by (case_tac "b : n procs" 1);
by (case_tac "x : n procs" 1);
by (etac impE 1);
by (Fast_tac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "x"), ("b", "b")] n_pren2 1);
by (atac 1);
by (EVERY [(case_tac "a1=x" 1),
           (Force_tac 1),
           (case_tac "a2=x" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (case_tac "x : n procs" 1);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren2 1);
by (atac 1);
by (cut_inst_tac [("x", "x"), ("y", "b"), ("P", "procs")] pren_sym 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (forw_inst_tac [("x", "b"), ("b", "x")] n_pren1 1);
by (atac 1);
by (EVERY [(case_tac "a1=b" 1),
           (Force_tac 1),
           (case_tac "a2=b" 1),
           (Force_tac 1),
           (Force_tac 1)]);
(* Replication *)
by (Force_tac 1);
qed "lemma";

Goal "[| x : n P ; b : n P |] ==> n (p{x<->b}P) = n P";
by (rtac (lemma RS mp) 1);
by (Fast_tac 1);
qed "n_pren3";


(************************************************************)
(*** Substitutions                                        ***)
(************************************************************)

Goalw [dom_def] "dom [] = {}";
by (Simp_tac 1);
qed "dom_empty";

Goalw [dom_def] "dom (x#xs) = insert (fst x) (insert (snd x) (dom xs))";
by (Auto_tac);
qed "dom_cons";

Goalw [dom_def] "dom (xs@ys) = (dom xs) Un (dom ys)";
by (Auto_tac);
qed "dom_app";

Addsimps [dom_empty, dom_cons, dom_app];

Goal "finite (dom xs)";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "dom_finite";

Addsimps [dom_finite];

Goal "p{xs@ys}P = p{ys}p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_app";

Addsimps [psubst_app];

Goal "p{xs}.0 = .0";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Null";

Goal "p{xs}(.t.P) = .t.p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Tau";

Goal "p{xs}(a<b>.P) = n{xs}a<n{xs}b>.p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (res_inst_tac [("x", "b")] spec 1);
by (res_inst_tac [("x", "a")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Out";

Goal "p{xs}(a[b].P) = n{xs}a[n{xs}b].p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (res_inst_tac [("x", "b")] spec 1);
by (res_inst_tac [("x", "a")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_In";

Goal "p{xs}(.#b P) = .#n{xs}b p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (res_inst_tac [("x", "b")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Res";

Goal "p{xs}(P .+ Q) = p{xs}P .+ p{xs}Q";
by (res_inst_tac [("x", "Q")] spec 1);
by (res_inst_tac [("x", "P")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Plus";

Goal "p{xs}(P .| Q) = p{xs}P .| p{xs}Q";
by (res_inst_tac [("x", "Q")] spec 1);
by (res_inst_tac [("x", "P")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Par";

Goal "p{xs}(.[a.=b]P) = .[n{xs}a.=n{xs}b]p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (res_inst_tac [("x", "b")] spec 1);
by (res_inst_tac [("x", "a")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Mt";

Goal "p{xs}(.[a.~=b]P) = .[n{xs}a.~=n{xs}b]p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (res_inst_tac [("x", "b")] spec 1);
by (res_inst_tac [("x", "a")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Mmt";

Goal "p{xs}(.!P) = .!p{xs}P";
by (res_inst_tac [("x", "P")] spec 1);
by (induct_tac "xs" 1);
by (Auto_tac);
qed "psubst_Repl";

val psubst_simp = [psubst_Null, psubst_Tau, psubst_Out, psubst_In,
                   psubst_Res, psubst_Plus, psubst_Par, psubst_Mt,
                   psubst_Mmt, psubst_Repl];

Addsimps psubst_simp;

Delsimps [nren_def];


(************************************************************)
(*** Equalities, inequalities                             ***)
(************************************************************)

Goalw [nren_def] "[| b ~: {x,y} ; b ~= a |] ==> b ~= n{x<->y}a";
by (Auto_tac);
qed "nren_ineq";

Goal "b ~: dom xs & b ~= a --> b ~= n{xs}a";
by (res_inst_tac [("x", "a")] spec 1);
by (induct_tac "xs" 1);
by (Asm_simp_tac 1);
by (strip_tac 1);
by (eres_inst_tac [("x", "n{fst a<->snd a}x")] allE 1);
by (etac impE 1);
by (rtac conjI 1);
by (rtac nren_ineq 2);
by (ALLGOALS Asm_full_simp_tac);
qed "lemma";

Goal "[| b ~: dom xs ; b ~= a |] ==> b ~= n{xs}a";
by (fast_tac (claset() addSIs [lemma RS mp]) 1);
qed "pren_ineq";


(************************************************************)
(*** Cases                                                ***)
(************************************************************)

Goal ".0 = p{xs}Q --> Q = .0";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal ".0 = p{xs}Q ==> Q = .0";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Null";

Goal ".t.P = p{xs}Q --> (EX R. Q = .t.R & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal ".t.P = p{xs}Q ==> EX R. Q = .t.R & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Tau";

Goal "a<b>.P = p{xs}Q --> (EX c d R. Q = c<d>.R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal "a<b>.P = p{xs}Q ==> EX c d R. Q = c<d>.R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Out";

Goal "a[b].P = p{xs}Q --> (EX c d R. Q = c[d].R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal "a[b].P = p{xs}Q ==> EX c d R. Q = c[d].R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_In";

Goal ".#b P = p{xs}Q --> (EX d R. Q = .#d R & \
  \ b = n{xs}d & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal ".#b P = p{xs}Q ==> EX d R. Q = .#d R & \
  \ b = n{xs}d & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Res";

Goal "P .+ P' = p{xs}Q --> (EX R S. Q = R .+ S & \
  \ P = p{xs}R & P' = p{xs}S)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal "P .+ P' = p{xs}Q ==> EX R S. Q = R .+ S & \
  \ P = p{xs}R & P' = p{xs}S";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Plus";

Goal "P .| P' = p{xs}Q --> (EX R S. Q = R .| S & \
  \ P = p{xs}R & P' = p{xs}S)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal "P .| P' = p{xs}Q ==> EX R S. Q = R .| S & \
  \ P = p{xs}R & P' = p{xs}S";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Par";

Goal ".[a.=b]P = p{xs}Q --> (EX c d R. Q = .[c.=d]R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal ".[a.=b]P = p{xs}Q ==> EX c d R. Q = .[c.=d]R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Mt";

Goal ".[a.~=b]P = p{xs}Q --> (EX c d R. Q = .[c.~=d]R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal ".[a.~=b]P = p{xs}Q ==> EX c d R. Q = .[c.~=d]R & \
  \ a = n{xs}c & b = n{xs}d & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Mmt";

Goal ".!P = p{xs}Q --> (EX R. Q = .!R & P = p{xs}R)";
by (induct_tac "Q" 1);
by (Auto_tac);
qed "lemma";

Goal ".!P = p{xs}Q ==> EX R. Q = .!R & P = p{xs}R";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "psubst_cases_Repl";

val psubst_cases = [psubst_cases_Null, psubst_cases_Tau,
                    psubst_cases_Out,  psubst_cases_In,
                    psubst_cases_Res, psubst_cases_Plus,
                    psubst_cases_Par, psubst_cases_Mt,
                    psubst_cases_Mmt, psubst_cases_Repl];