File Alpha.ML


(************************************************************)
(*** Alpha-equivalence wrt. "forbidden" names             ***)
(************************************************************)

Goal "P =a[S] P' ==> P =a[S Un T] P'";
by (etac Al.induct 1);
by (auto_tac (claset() addSIs Al.intrs, simpset()));
qed "Al_un1";

Goal "P =a[T] P' ==> P =a[S Un T] P'";
by (etac Al.induct 1);
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Al_un2";

Goal "P =a[S] P' ==> P =a[insert x S] P'";
by (dres_inst_tac [("S", "{x}")] Al_un2 1);
by (Auto_tac);
qed "Al_insert";

Goal "T <= S ==> T Un S = S";
by (Auto_tac);
qed "lemma";

Goal "[| P =a[T] P' ; T <= S |] ==> P =a[S] P'";
by (dres_inst_tac [("T", "S")] Al_un1 1);
by (asm_full_simp_tac (simpset() addsimps [lemma]) 1);
qed "Al_subset";

Goal "p{xs}P =a[S] p{xs}P";
by (res_inst_tac [("x", "xs")] spec 1);
by (induct_tac "P" 1);
by (auto_tac (claset() addSIs Al.intrs, simpset()));
by (eres_inst_tac [("x", "x@[(xa, n{x}a2)]")] allE 1);
by (eres_inst_tac [("x", "x@[(xa, n{x}a)]")] allE 2);
by (auto_tac (claset() addIs [Al_insert], simpset()));
qed "Al_refl_subst";

Goal "P =a[S] P";
by (cut_inst_tac [("xs", "[]")] Al_refl_subst 1);
by (Auto_tac);
qed "Al_refl";

Goal "P =a[S] P' ==> P' =a[S] P";
by (etac Al.induct 1);
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Al_sym";

Goal "P =a[S] P' ==> ALL P''. P' =a[S] P'' --> P =a[S] P''";
by (etac Al.induct 1);
by (REPEAT (force_tac (claset() addEs Al.elims addIs Al.intrs,
            simpset()) 1));
qed "lemma";

Goal "[| P =a[S] P' ; P' =a[S] P'' |] ==> P =a[S] P''";
by (fast_tac (claset() addDs [lemma]) 1);
qed "Al_trans";

Goal "p{y<->z}P =a[S] p{y<->z}P' ==> p{z<->y}P =a[S] p{z<->y}P'";
by (auto_tac (claset(), simpset() addsimps [pren_sym]));
qed "Al_pren_sym";

Goal "P =a[S] P' ==> ALL Q Q' xs xs' . \
 \ P = p{xs}Q & P' = p{xs'}Q' & \
 \ y ~: insert z ((dom xs) Un (dom xs') Un n Q Un n Q') --> \
 \ p{y<->z}P =a[{y, z} Un S] p{y<->z}P'";

by (etac Al.induct 1);
by (ALLGOALS strip_tac);

(* Null, Tau, Out *)
by (force_tac (claset() addSDs psubst_cases addSIs Al.intrs,
               simpset()) 1);
by (force_tac (claset() addSDs psubst_cases addSIs Al.intrs,
               simpset()) 1);
by (force_tac (claset() addSDs psubst_cases addSIs Al.intrs,
               simpset()) 1);

(* In *)
by (REPEAT (etac conjE 1));
by (dresolve_tac psubst_cases 1);
by (dresolve_tac psubst_cases 1);
by (REPEAT (etac exE 1));
by (Asm_simp_tac 1);
by (resolve_tac Al.intrs 1);
by (strip_tac 1);
by (EVERY [(eres_inst_tac [("x", "x")] allE 1),
           (etac impE 1),
           (Force_tac 1),
           (REPEAT (etac conjE 1))]);
by (eres_inst_tac [("x", "R")] allE 1);
by (eres_inst_tac [("x", "Ra")] allE 1);
by (eres_inst_tac [("x", "xs@[(x,b)]")] allE 1);
by (eres_inst_tac [("x", "xs'@[(x,b')]")] allE 1);
by (etac impE 1);
by (REPEAT ((rtac conjI 1) THEN (Force_tac 1)));
by (Asm_full_simp_tac 1);
by ((rtac conjI 1) THEN (Force_tac 1));
by ((rtac conjI 1) THEN (EVERY
     [(rtac pren_ineq 1),
      (Asm_simp_tac 1),
      (Force_tac 1)]));
by ((rtac conjI 1) THEN (Force_tac 1));
by (EVERY
     [(rtac pren_ineq 1),
      (Asm_simp_tac 1),
      (Force_tac 1)]);
by (asm_full_simp_tac (simpset() addsimps [pren_swap1]) 1);

(* Res *)
by (REPEAT (etac conjE 1));
by (dresolve_tac psubst_cases 1);
by (dresolve_tac psubst_cases 1);
by (REPEAT (etac exE 1));
by (Asm_simp_tac 1);
by (resolve_tac Al.intrs 1);
by (strip_tac 1);
by (EVERY [(eres_inst_tac [("x", "x")] allE 1),
           (etac impE 1),
           (Force_tac 1),
           (REPEAT (etac conjE 1))]);
by (eres_inst_tac [("x", "R")] allE 1);
by (eres_inst_tac [("x", "Ra")] allE 1);
by (eres_inst_tac [("x", "xs@[(x,b)]")] allE 1);
by (eres_inst_tac [("x", "xs'@[(x,b')]")] allE 1);
by (etac impE 1);
by (REPEAT ((rtac conjI 1) THEN (Force_tac 1)));
by (Asm_full_simp_tac 1);
by ((rtac conjI 1) THEN (Force_tac 1));
by ((rtac conjI 1) THEN (EVERY
     [(rtac pren_ineq 1),
      (Asm_simp_tac 1),
      (Force_tac 1)]));
by ((rtac conjI 1) THEN (Force_tac 1));
by (EVERY
     [(rtac pren_ineq 1),
      (Asm_simp_tac 1),
      (Force_tac 1)]);
by (asm_full_simp_tac (simpset() addsimps [pren_swap1]) 1);

(* Plus, Par, Mt, Mmt, Repl *)
by (REPEAT (force_tac
    (claset() addSDs psubst_cases addSIs Al.intrs, simpset()) 1));
qed "lemma";

Goal "[| P =a[S] P' ; y ~: (n P Un n P') |] \
 \ ==> p{y<->z}P =a[{y, z} Un S] p{y<->z}P'";
by (case_tac "y=z" 1);
by (force_tac (claset() addIs [Al_insert], simpset()) 1);
by (dres_inst_tac [("y", "y"), ("z", "z")] lemma 1);
by (eres_inst_tac [("x", "P")] allE 1);
by (eres_inst_tac [("x", "P'")] allE 1);
by (eres_inst_tac [("x", "[]")] allE 1);
by (eres_inst_tac [("x", "[]")] allE 1);
by (Force_tac 1);
qed "Al_pren_cong1";

Goal "{x, y} Un A = {y, x} Un A";
by (Auto_tac);
qed "lemma";

Goal "[| P =a[S] P' ; z ~: (n P Un n P') |] \
 \ ==> p{y<->z}P =a[{y, z} Un S] p{y<->z}P'";
by (rtac Al_pren_sym 1);
by (dres_inst_tac [("y", "z"), ("z", "y")] Al_pren_cong1 1);
by (cut_inst_tac [("x", "y"), ("y", "z"), ("A", "S")] lemma 2);
by (Auto_tac);
qed "Al_pren_cong2";

Goal "[| p{x<->b}P =a[S] p{x<->b'}P' ; {x, y} Int (n P Un n P') = {} |] \
 \ ==> p{y<->b}P =a[{y, x} Un S] p{y<->b'}P'";
by (case_tac "x=y" 1);
by (force_tac (claset() addIs [Al_insert], simpset()) 1);
by (dres_inst_tac [("y", "y"), ("z", "x")] Al_pren_cong1 1);
by (cut_inst_tac [("x", "x"), ("b", "b"), ("P", "P")] n_pren 1);
by (Force_tac 1);
by (cut_inst_tac [("x", "x"), ("b", "b'"), ("P", "P'")] n_pren 1);
by (Force_tac 1);
by (case_tac "b : n P" 1);
by (EVERY [(case_tac "b' : n P'" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "b' : n P'" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (cut_inst_tac [("y", "y"), ("z", "x"),
    ("x", "b"), ("P", "P")] pren_trans 1);
by ((Force_tac 1) THEN (Force_tac 1));
by (cut_inst_tac [("y", "y"), ("z", "x"),
    ("x", "b'"), ("P", "P'")] pren_trans 1);
by ((Force_tac 1) THEN (Force_tac 1));
by (Asm_full_simp_tac 1);
qed "Al_pren_choose";


(************************************************************)
(*** Alpha-equivalence                                    ***)
(************************************************************)

Goalw [Alpha_def] "[| finite S ; P =a[S] P' |] ==> P =a P'";
by (Auto_tac);
qed "AlphaI";

Goalw [Alpha_def] "P =a P' ==> EX S. finite S & P =a[S] P'";
by (Auto_tac);
qed "AlphaD";

Goalw [Alpha_def] "P =a P";
by (auto_tac (claset(), simpset() addsimps [Al_refl]));
qed "Alpha_refl";

Goalw [Alpha_def] "P =a P' ==> P' =a P";
by (auto_tac (claset() addIs [Al_sym], simpset()));
qed "Alpha_sym";

Goalw [Alpha_def] "[| P =a P' ; P' =a P'' |] ==> P =a P''";
by (Clarify_tac 1);
by (res_inst_tac [("x", "S Un Sa")] exI 1);
by (dres_inst_tac [("T", "Sa")] Al_un1 1);
by (dres_inst_tac [("S", "S")] Al_un2 1);
by (auto_tac (claset() addIs [Al_trans], simpset()));
qed "Alpha_trans";

Goalw [Alpha_def] "[| P =a P' ; y ~: (n P Un n P') |] \
 \ ==> p{y<->z}P =a p{y<->z}P'";
by (Clarify_tac 1);
by (res_inst_tac [("x", "{y, z} Un S")] exI 1);
by (auto_tac (claset() addDs [Al_pren_cong1], simpset()));
qed "Alpha_pren_cong1";

Goalw [Alpha_def] "[| P =a P' ; z ~: (n P Un n P') |] \
 \ ==> p{y<->z}P =a p{y<->z}P'";
by (Clarify_tac 1);
by (res_inst_tac [("x", "{y, z} Un S")] exI 1);
by (auto_tac (claset() addDs [Al_pren_cong2], simpset()));
qed "Alpha_pren_cong2";

Goal "[| p{x<->b}P =a p{x<->b'}P' ; {x, y} Int (n P Un n P') = {} |] \
 \ ==> p{y<->b}P =a p{y<->b'}P'";
by (case_tac "x=y" 1);
by (Asm_full_simp_tac 1);
by (dres_inst_tac [("y", "y"), ("z", "x")] Alpha_pren_cong1 1);
by (cut_inst_tac [("x", "x"), ("b", "b"), ("P", "P")] n_pren 1);
by (Force_tac 1);
by (cut_inst_tac [("x", "x"), ("b", "b'"), ("P", "P'")] n_pren 1);
by (Force_tac 1);
by (case_tac "b : n P" 1);
by (EVERY [(case_tac "b' : n P'" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (EVERY [(case_tac "b' : n P'" 1),
           (Force_tac 1),
           (Force_tac 1)]);
by (cut_inst_tac [("y", "y"), ("z", "x"),
    ("x", "b"), ("P", "P")] pren_trans 1);
by ((Force_tac 1) THEN (Force_tac 1));
by (cut_inst_tac [("y", "y"), ("z", "x"),
    ("x", "b'"), ("P", "P'")] pren_trans 1);
by ((Force_tac 1) THEN (Force_tac 1));
by (Asm_full_simp_tac 1);
qed "Alpha_pren_choose";

Goalw [Alpha_def] ".0 =a .0";
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Alpha_Null";

Goalw [Alpha_def] "P =a P' ==> .t.P =a .t.P'";
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Alpha_Tau";

Goalw [Alpha_def] "P =a P' ==> a<b>.P =a a<b>.P'";
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Alpha_Out";

Goalw [Alpha_def] "[| finite S ; ALL x. x ~: S --> \
  \ p{x<->b}P =a[insert x S] p{x<->b'}P' |] ==> a[b].P =a a[b'].P'";
by (auto_tac (claset() addSIs Al.intrs, simpset()));
qed "lemma";

Goal "[| p{x<->b}P =a p{x<->b'}P' ; x ~: n P Un n P' |] \
  \ ==> a[b].P =a a[b'].P'";
by (dtac AlphaD 1);
by ((etac exE 1) THEN (etac conjE 1));
by (res_inst_tac [("S", "{b, x} Un n P Un n P' Un S")] lemma 1);
by (Force_tac 1);
by (strip_tac 1);
by (dres_inst_tac [("y", "xa")] Al_pren_choose 1);
by (Force_tac 1);
by (res_inst_tac [("T", "{xa, x} Un S")] Al_subset 1);
by (Auto_tac);
qed "Alpha_In";

Goal "P =a P' ==> a[b].P =a a[b].P'";
by (dtac AlphaD 1);
by (Clarify_tac 1);
by (res_inst_tac [("S", "insert b (n P Un n P' Un S)")] lemma 1);
by (Force_tac 1);
by (strip_tac 1);
by (dres_inst_tac [("y", "x"), ("z", "b")] Al_pren_cong1 1);
by (Force_tac 1);
by (res_inst_tac [("T", "{x, b} Un S")] Al_subset 1);
by (Auto_tac);
qed "Alpha_In_eq";

Goalw [Alpha_def] "[| finite S ; ALL x. x ~: S --> \
  \ p{x<->b}P =a[insert x S] p{x<->b'}P' |] ==> .#b P =a .#b' P'";
by (auto_tac (claset() addSIs Al.intrs, simpset()));
qed "lemma";

Goal "[| p{x<->b}P =a p{x<->b'}P' ; x ~: n P Un n P' |] \
  \ ==> .#b P =a .#b' P'";
by (dtac AlphaD 1);
by ((etac exE 1) THEN (etac conjE 1));
by (res_inst_tac [("S", "{b, x} Un n P Un n P' Un S")] lemma 1);
by (Force_tac 1);
by (strip_tac 1);
by (dres_inst_tac [("y", "xa")] Al_pren_choose 1);
by (Force_tac 1);
by (res_inst_tac [("T", "{xa, x} Un S")] Al_subset 1);
by (Auto_tac);
qed "Alpha_Res";

Goal "P =a P' ==> .#b P =a .#b P'";
by (dtac AlphaD 1);
by (Clarify_tac 1);
by (res_inst_tac [("S", "insert b (n P Un n P' Un S)")] lemma 1);
by (Force_tac 1);
by (strip_tac 1);
by (dres_inst_tac [("y", "x"), ("z", "b")] Al_pren_cong1 1);
by (Force_tac 1);
by (res_inst_tac [("T", "{x, b} Un S")] Al_subset 1);
by (Auto_tac);
qed "Alpha_Res_eq";

Goalw [Alpha_def] "[| P =a P' ; Q =a Q' |] ==> P .+ Q =a P' .+ Q'";
by (Clarify_tac 1);
by (res_inst_tac [("x", "S Un Sa")] exI 1);
by (fast_tac (claset() addSIs Al.intrs addIs [Al_un1,Al_un2]) 1);
qed "Alpha_Plus";

Goalw [Alpha_def] "[| P =a P' ; Q =a Q' |] ==> P .| Q =a P' .| Q'";
by (Clarify_tac 1);
by (res_inst_tac [("x", "S Un Sa")] exI 1);
by (fast_tac (claset() addSIs Al.intrs addIs [Al_un1,Al_un2]) 1);
qed "Alpha_Par";

Goalw [Alpha_def] "P =a P' ==> .[a.=b]P =a .[a.=b]P'";
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Alpha_Mt";

Goalw [Alpha_def] "P =a P' ==> .[a.~=b]P =a .[a.~=b]P'";
by (auto_tac (claset() addIs Al.intrs, simpset()));
qed "Alpha_Mmt";

Goalw [Alpha_def] "P =a P' ==> .!P =a .!P'";
by (auto_tac (claset() addSIs Al.intrs, simpset()));
qed "Alpha_Repl";

val Alpha_intrs = [Alpha_Null, Alpha_Tau, Alpha_Out, Alpha_In,
                   Alpha_Res, Alpha_Plus, Alpha_Par, Alpha_Mt,
                   Alpha_Mmt, Alpha_Repl];


(************************************************************)
(*** Alpha-conversion                                     ***)
(************************************************************)

Goalw [Alpha_def] "x ~: n P ==> a[x].p{x<->b}P =a a[b].P";
by (Clarify_tac 1);
by (res_inst_tac [("x", "insert x (n P)")] exI 1);
by (rtac conjI 1);
by (Asm_simp_tac 1);
by (resolve_tac Al.intrs 1);
by (asm_full_simp_tac (simpset() addsimps [pren_trans, Al_refl]) 1);
qed "Alpha_In_conv";

Goalw [Alpha_def] "x ~: n P ==> .#x p{x<->b}P =a .#b P";
by (Clarify_tac 1);
by (res_inst_tac [("x", "insert x (n P)")] exI 1);
by (rtac conjI 1);
by (Asm_simp_tac 1);
by (resolve_tac Al.intrs 1);
by (asm_full_simp_tac (simpset() addsimps [pren_trans, Al_refl]) 1);
qed "Alpha_Res_conv";

Goal "x ~: n P --> b ~: bn (c{x<-b}P)";
by (induct_tac "P" 1);
by (Force_tac 1);
by (Force_tac 1);
by (Force_tac 1);

(* Input *)
by (strip_tac 1);
by (case_tac "a2=b" 1);
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (Force_tac 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac conjE 1));
by (dres_inst_tac [("b", "b")] pren_del 1);
by (force_tac (claset(), simpset() addsimps [n_def]) 1);
by (Force_tac 1);

(* Restriction *)
by (strip_tac 1);
by (case_tac "a=b" 1);
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (Force_tac 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac conjE 1));
by (dres_inst_tac [("b", "b")] pren_del 1);
by (force_tac (claset(), simpset() addsimps [n_def]) 1);
by (Force_tac 1);

by (REPEAT (Force_tac 1));
qed "lemma";

Goal "x ~: n P ==> b ~: bn (c{x<-b}P)";
by (fast_tac (claset() addSIs [lemma RS mp]) 1);
qed "Conv_del";

Goal "x ~: n P --> c{x<-b}P =a P";
by (induct_tac "P" 1);

(* Inaction, silent prefix, output prefix *)
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);

(* Input *)
by (strip_tac 1);
by (case_tac "a2=b" 1);
by (case_tac "b=x" 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (rtac Alpha_In_conv 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (force_tac (claset() addIs [Alpha_In_eq], simpset()) 1);

(* Restriction *)
by (strip_tac 1);
by (case_tac "a=b" 1);
by (case_tac "b=x" 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (rtac Alpha_Res_conv 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [nren_def]) 1);
by (force_tac (claset() addIs [Alpha_Res_eq], simpset()) 1);

(* Choice, parallel composition, matching, mismatching, replication *)
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
by (force_tac (claset() addIs Alpha_intrs, simpset()) 1);
qed "lemma";

Goal "x ~: n P ==> c{x<-b}P =a P";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "Conv_eq";

Goal "EX P'. P =a P' & b ~: bn P'";
by (cut_inst_tac [("A", "n P")] ex_dist_set 1);
by (Simp_tac 1);
by (etac exE 1);
by (res_inst_tac [("x", "c{ba<-b}P")] exI 1);
by (auto_tac (claset() addIs [Conv_eq, Alpha_sym],
              simpset() addsimps [Conv_del]));
qed "Alpha_conv";