File ProcExt.ML


(* names abstractions *)

Goal "[| wfna fa ; wfna fb ; fa a = fb a ; \
  \ a ~: fnna fa ; a ~: fnna fb |] ==> fa = fb";
by (auto_tac (claset() addSEs WFNA.elims,
              simpset() addsimps [fnna_def]));
qed "ext_na";


(* process abstractions *)

Goal "finite ({a, c} Un (fnaa ffP) Un (fnaa ffQ))";
by (asm_simp_tac (simpset() addsimps [finite_fnaa]) 1);
qed "lemma";

Goal "EX d. d ~= a & d ~= c & d ~: fnaa ffP & d ~: fnaa ffQ";
by (cut_inst_tac
    [("a", "a"), ("c", "c"), ("ffP", "ffP"), ("ffQ", "ffQ")]
    lemma 1);
by (fast_tac (claset() addSDs [ex_dist_set]) 1);
qed "fresh_ext";

Goal "[| ALL b fQ a. wfpa fQ & ffP b a = fQ a & \
  \ a ~: fna (ffP b) & a ~: fna fQ --> ffP b = fQ ; \
  \ ALL b fQ a. wfpa fQ & ffP a b = fQ a & \
  \ a ~: fna (%x. ffP x b) & a ~: fna fQ --> (%x. ffP x b) = fQ ; \
  \ ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
  \ ALL b. wfpa (ffQ b) ; ALL b. wfpa (%x. ffQ x b) ; \
  \ a ~: fnaa ffP ; a ~: fnaa ffQ ; \
  \ (%x. ffP x a) = (%x. ffQ x a) |] \
  \ ==> (%x. ffP x c) = (%x. ffQ x c)";

(* introduce a fresh name, d *)
by (cut_inst_tac
    [("a", "a"), ("c", "c"), ("ffP", "ffP"), ("ffQ", "ffQ")]
    fresh_ext 1);
by (Clarify_tac 1);

(* instantiate first hypothesis: b -> d, fQ -> ffQ d, a -> a *)
by (eres_inst_tac [("x", "d")] allE 1);
by (eres_inst_tac [("x", "ffQ d")] allE 1);
by (rotate_tac 12 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (rtac conjI 1);
by (Fast_tac 1);
by (rtac conjI 1);
by (fast_tac (claset() addDs [inst_fun_eq]) 1);
by (rtac conjI 1);
by (rtac not_fnaa_fna 1);
by (REPEAT (atac 1));
by (Fast_tac 1);
by (rtac not_fnaa_fna 1);
by (REPEAT (atac 1));
by (Fast_tac 1);

(* instantiate second hypothesis: b -> c, fQ -> %x. ffQ x c, a -> d *)
by (eres_inst_tac [("x", "c")] allE 1);
by (eres_inst_tac [("x", "%x. ffQ x c")] allE 1);
by (rotate_tac 12 1);
by (eres_inst_tac [("x", "d")] allE 1);
by (etac impE 1);
by (rtac conjI 1);
by (Fast_tac 1);
by (rtac conjI 1);
by (fast_tac (claset() addDs [inst_fun_eq]) 1);
by (rtac conjI 1);
by (rtac not_fnaa_fna 1);
by (REPEAT (atac 1));
by (cut_inst_tac [("ffP", "ffP")] fnaa_sym 1);
by (Force_tac 1);
by (Fast_tac 1);
by (rtac not_fnaa_fna 1);
by (REPEAT (atac 1));
by (cut_inst_tac [("ffP", "ffQ")] fnaa_sym 1);
by (Force_tac 1);
by (Fast_tac 1);
by (Fast_tac 1);
qed "inst_hyp";

Goal "wfpa fP ==> ALL fQ a. wfpa fQ & fP a = fQ a & \
  \ a ~: fna fP & a ~: fna fQ --> fP = fQ";
by (etac WFPA.induct 1);
by (ALLGOALS Clarify_tac);

(* inaction *)
by (fast_tac (claset() addDs [wfpa_cases0]) 1);

(* silent prefix *)
by (forward_tac [wfpa_cases1] 1);
by (atac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna1], simpset()) 1);
by (Fast_tac 1);

(* output *)
by (forward_tac [wfpa_cases2] 1);
by (atac 1);
by (Clarify_tac 1);
by (dres_inst_tac [("fa", "fa"), ("fb", "fba")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna2a], simpset()) 1);
by (force_tac (claset() addDs [not_fna2a], simpset()) 1);
by (dres_inst_tac [("fa", "fb"), ("fb", "fc")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna2b], simpset()) 1);
by (force_tac (claset() addDs [not_fna2b], simpset()) 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna2c], simpset()) 1);
by (Fast_tac 1);

(* input *)
by (forward_tac [wfpa_cases3] 1);
by (atac 1);
by (Clarify_tac 1);
by (dres_inst_tac [("fa", "fa"), ("fb", "fb")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna3a], simpset()) 1);
by (force_tac (claset() addDs [not_fna3a], simpset()) 1);
by (rtac ext 1);
by (Asm_simp_tac 1);
by (REPEAT (etac all_conjE 1));
by (res_inst_tac [("a", "a")] inst_hyp 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna3b], simpset()) 1);
by (force_tac (claset() addDs [not_fna3b], simpset()) 1);
by (atac 1);

(* restriction *)
by (forward_tac [wfpa_cases4] 1);
by (atac 1);
by (Clarify_tac 1);
by (rtac ext 1);
by (Asm_simp_tac 1);
by (REPEAT (etac all_conjE 1));
by (res_inst_tac [("a", "a")] inst_hyp 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna4], simpset()) 1);
by (force_tac (claset() addDs [not_fna4], simpset()) 1);
by (atac 1);

(* choice *)
by (forward_tac [wfpa_cases5] 1);
by (atac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna5a], simpset()) 1);
by (eres_inst_tac [("x", "fQb")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna5b], simpset()) 1);
by (Fast_tac 1);

(* parallel composition *)
by (forward_tac [wfpa_cases6] 1);
by (atac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna6a], simpset()) 1);
by (eres_inst_tac [("x", "fQb")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna6b], simpset()) 1);
by (Fast_tac 1);

(* matching *)
by (forward_tac [wfpa_cases7] 1);
by (atac 1);
by (Clarify_tac 1);
by (dres_inst_tac [("fa", "fa"), ("fb", "fba")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna7a], simpset()) 1);
by (force_tac (claset() addDs [not_fna7a], simpset()) 1);
by (dres_inst_tac [("fa", "fb"), ("fb", "fc")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna7b], simpset()) 1);
by (force_tac (claset() addDs [not_fna7b], simpset()) 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna7c], simpset()) 1);
by (Fast_tac 1);

(* mismatching *)
by (forward_tac [wfpa_cases8] 1);
by (atac 1);
by (Clarify_tac 1);
by (dres_inst_tac [("fa", "fa"), ("fb", "fba")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna8a], simpset()) 1);
by (force_tac (claset() addDs [not_fna8a], simpset()) 1);
by (dres_inst_tac [("fa", "fb"), ("fb", "fc")] ext_na 1);
by (REPEAT (atac 1));
by (force_tac (claset() addDs [not_fna8b], simpset()) 1);
by (force_tac (claset() addDs [not_fna8b], simpset()) 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna8c], simpset()) 1);
by (Fast_tac 1);

(* replication *)
by (forward_tac [wfpa_cases9] 1);
by (atac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "fP'")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (etac impE 1);
by (force_tac (claset() addDs [not_fna9], simpset()) 1);
by (Fast_tac 1);
qed "lemma";

Goal "[| wfpa fP ; wfpa fQ ; fP a = fQ a ; \
  \ fresha a fP ; fresha a fQ |] ==> fP = fQ";
by (auto_tac (claset() addDs [lemma],
              simpset() addsimps [fresha_def]));
qed "ext_pa";

Goalw [freshaa_def]
 "[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
  \ ALL b. wfpa (ffQ b) ; ALL b. wfpa (%x. ffQ x b) ; \
  \ ffP a = ffQ a ; freshaa a ffP ; freshaa a ffQ |] \
  \ ==> ffP = ffQ";
by (rtac ext 1);
by (cut_inst_tac [("ffP", "ffP")] fnaa_sym 1);
by (cut_inst_tac [("ffP", "ffQ")] fnaa_sym 1);

(* introduce a fresh name, d *)
by (cut_inst_tac
    [("a", "a"), ("c", "x"), ("ffP", "ffP"), ("ffQ", "ffQ")]
    fresh_ext 1);
by (Clarify_tac 1);

(* apply ext_pa to (ffP x) and (ffQ x) with fresh name d *)
by (res_inst_tac [("a", "d")] ext_pa 1);
by (Fast_tac 1);
by (Fast_tac 1);
by (asm_simp_tac (simpset() addsimps [fresha_def]) 2);
by (rtac not_fnaa_fna 2);
by (REPEAT (atac 2));
by (asm_simp_tac (simpset() addsimps [fresha_def]) 2);
by (rtac not_fnaa_fna 2);
by (REPEAT (atac 2));

(* apply ext_pa to (%x. ffP x d) and (%x. ffQ x d) with fresh name a *)
by (dres_inst_tac [("x", "d")] inst_fun_eq 1);
by (dres_inst_tac
    [("a", "a"), ("fP", "%x. ffP x d"), ("fQ", "%x. ffQ x d")]
    (rotate_prems 2 ext_pa) 1);
by (asm_simp_tac (simpset() addsimps [fresha_def]) 1);
by (rtac not_fnaa_fna 1);
by (REPEAT (atac 1));
by (Force_tac 1);
by (Fast_tac 1);
by (asm_simp_tac (simpset() addsimps [fresha_def]) 1);
by (rtac not_fnaa_fna 1);
by (REPEAT (atac 1));
by (Force_tac 1);
by (REPEAT (fast_tac (claset() addDs [inst_fun_eq]) 1));
qed "ext_paa";