File ProcExp.ML


Goalw [doba_def] "dob (In a fP) c = Suc (doba fP c)";
by (Auto_tac);
qed "dob3'";

Goalw [doba_def] "dob (Res fP) c = Suc (doba fP c)";
by (Auto_tac);
qed "dob4'";

Delsimps [dob3,dob4];
Addsimps [dob3',dob4'];

(* creating the transformation list *)

Goal "a ~: set (map fst (mk_trl xs a))";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "a_not_in_trl";

Goal "set xs <= insert a (set (map fst (mk_trl xs a)))";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "mk_trl_contain";

Goal "set (map fst (mk_trl xs a)) <= set xs";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "lemma";

Goal "insert a (set (map fst (mk_trl xs a))) = insert a (set xs)";
by (rtac subset_antisym 1);
by (fast_tac (claset() addSIs [subset_insert_mono, lemma]) 1);
by (fast_tac (claset() addSIs [subset_insert_mono1, mk_trl_contain]) 1);
qed "mk_trl_map_fst";

Goal "ALL x:set (mk_trl xs a). wfna snd x";
by (induct_tac "xs" 1);
by (auto_tac (claset() addIs WFNA.intrs,
              simpset()));
qed "mk_trl_wfna";

Goal "b ~: insert a (set xs) \
  \ --> (ALL x: set (mk_trl xs a). a ~= snd x b)";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "lemma";

Goal "b ~: insert a (set xs) \
  \ ==> (ALL x: set (mk_trl xs a). a ~= snd x b)";
by (fast_tac (claset() addSIs [lemma RS mp]) 1);
qed "mk_trl_ineq";

Goal "ALL x:set (mk_trl xs a). snd x = (%y. fst x)";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "mk_trl_const";


(* transformation lists with well-formed items *)

Goal "(ALL x:set xs. wfna snd x) --> wfna trn a xs";
by (induct_tac "xs" 1);
by (auto_tac (claset() addIs WFNA.intrs,
              simpset()));
qed "lemma";

Goal "ALL x:set xs. wfna snd x ==> wfna trn a xs";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "wfna_trn";

Goal "ALL x:set xs. snd x = (%y. fst x) ==> ALL x:set xs. wfna snd x";
by (auto_tac (claset() addIs WFNA.intrs,
              simpset()));
qed "const_trl_wfna_trl";

Goal "(ALL x:set xs. snd x = (%y. fst x)) & \
  \ b:insert a (set (map fst xs)) --> (trn b xs) a = b";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "lemma";

Goal "[| ALL x:set xs. snd x = (%y. fst x) ; \
  \ b:insert a (set (map fst xs)) |] ==> (trn b xs) a = b";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "const_trn";


(* well-formed abstractions over transformation lists *)

Goal "(ALL x:set xs. wfna snd x) --> wftrl (%x. xs)";
by (induct_tac "xs" 1);
by (auto_tac (claset() addSIs WFTRL.intrs
                       addSEs WFNA.elims addIs WFNAA.intrs,
              simpset()));
qed "lemma";

Goal "ALL x:set xs. wfna snd x ==> wftrl (%x. xs)";
by (fast_tac (claset() addIs [lemma RS mp]) 1);
qed "wfna_wftrl";

Goal "wftrl fxs ==> ALL x:set (fxs a). wfna snd x";
by (etac WFTRL.induct 1);
by (auto_tac (claset() addSEs WFNAA.elims addIs WFNA.intrs,
              simpset()));
qed "wftrl_wfna";

Goal "wftrl fxs ==> wftrl (%x. (a, (%y. b))#fxs c)";
by (auto_tac (claset() addSIs WFTRL.intrs
                       addIs WFNAA.intrs
                       addSIs [wfna_wftrl, wftrl_wfna],
              simpset()));
qed "wftrl_cons1";

Goal "wftrl fxs ==> wftrl (%x. (a, (%y. x))#fxs c)";
by (auto_tac (claset() addSIs WFTRL.intrs
                       addIs WFNAA.intrs
                       addSIs [wfna_wftrl, wftrl_wfna],
              simpset()));
qed "wftrl_cons2";

Goal "wftrl fxs ==> wftrl (%x. (a, (%y. b))#fxs x)";
by (auto_tac (claset() addSIs WFTRL.intrs
                       addIs WFNAA.intrs,
              simpset()));
qed "wftrl_cons3";

Goal "wftrl fxs ==> wftrl (%x. (a, (%y. x))#fxs x)";
by (auto_tac (claset() addSIs WFTRL.intrs
                       addIs WFNAA.intrs,
              simpset()));
qed "wftrl_cons4";

Goal "wftrl fxs ==> wfna trn a (fxs b)";
by (etac WFTRL.induct 1);
by (auto_tac (claset() addSIs WFTRL.intrs
                       addEs WFNAA.elims addIs WFNA.intrs,
              simpset()));
qed "wftrl_wfna_trn1";

Goal "wftrl fxs ==> wfna (%x. trn a (fxs x) b)";
by (etac WFTRL.induct 1);
by (case_tac "a=aa" 2);
by (auto_tac (claset() addSIs WFTRL.intrs
                       addEs WFNAA.elims addIs WFNA.intrs,
              simpset()));
qed "wftrl_wfna_trn2";


(* freshness *)

Goal "(ALL x:set xs. a ~= snd x b) & a ~= b \
  \ --> a ~= (trn c xs) b";
by (induct_tac "xs" 1);
by (Auto_tac);
qed "lemma";

Goal "[| ALL x:set xs. a ~= snd x b ; a ~= b |] \
  \ ==> a ~= (trn c xs) b";
by (fast_tac (claset() addSIs [lemma RS mp]) 1);
qed "trn_fresh";

Goal "wfpa fP ==> ALL xs ys. \
  \ (ALL x:set xs. a ~= snd x b) & a ~= b \
  \  --> a ~: fn (tr (fP c) xs ys b)";
by (etac WFPA.induct 1);
by (ALLGOALS strip_tac);

(* inaction, silent prefix, output prefix *)
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addDs [trn_fresh]
                       addSss simpset()) 1);

(* input prefix *)
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (fast_tac (claset() addDs [trn_fresh]) 1);
by (res_inst_tac [("b", "b")] not_fn_fna 1);
by (Force_tac 1);

(* restriction *)
by (Asm_simp_tac 1);
by (res_inst_tac [("b", "b")] not_fn_fna 1);
by (Force_tac 1);

(* choice, parallel composition, matching, mismatching, replication *)
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addDs [trn_fresh]
                       addSss simpset()) 1);
by (fast_tac (claset() addDs [trn_fresh]
                       addSss simpset()) 1);
by (Asm_simp_tac 1);
qed "lemma";

Goal "[| wfpa fP ; ALL x:(set xs). a ~= (snd x) b ; a ~= b |] \
  \ ==> a ~: fn ((tr (fP c) xs ys) b)";
by (fast_tac (claset() addDs [lemma]) 1);
qed "tr_not_fn_abs";

Goal "wfp P ==> (ALL x:(set xs). a ~= (snd x) b) & a ~= b \
  \ --> a ~: fn ((tr P xs ys) b)";
by (etac WFP.induct 1);
by (ALLGOALS strip_tac);

(* inaction, silent prefix, output prefix *)
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addDs [trn_fresh]
                       addSss simpset()) 1);

(* input prefix *)
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (fast_tac (claset() addDs [trn_fresh]) 1);
by (res_inst_tac [("b", "b")] not_fn_fna 1);
by (rtac tr_not_fn_abs 1);
by (atac 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);

(* restriction *)
by (Asm_simp_tac 1);
by (res_inst_tac [("b", "b")] not_fn_fna 1);
by (rtac tr_not_fn_abs 1);
by (atac 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);

(* choice, parallel composition, matching, mismatching, replication *)
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addDs [trn_fresh]
                       addSss simpset()) 1);
by (fast_tac (claset() addDs [trn_fresh]
                       addSss simpset()) 1);
by (Asm_simp_tac 1);
qed "lemma";

Goal "[| wfp P ; ALL x:set xs. a ~= snd x b ; a ~= b |] \
  \ ==> a ~: fn (tr P xs ys b)";
by (fast_tac (claset() addDs [lemma]) 1);
qed "tr_not_fn";

Goal "[| wfpa fP ; ALL x:(set xs). a ~= (snd x) b ; a ~= b |] \
  \ ==> fresh a ((tr (fP c) xs ys) b)";
by (fast_tac (claset() addDs [tr_not_fn_abs] addSss
              (simpset() addsimps [fresh_def])) 1);
qed "tr_fresh_abs";

Goal "[| wfp P ; ALL x:(set xs). a ~= (snd x) b ; a ~= b |] \
  \ ==> fresh a ((tr P xs ys) b)";
by (fast_tac (claset() addDs [tr_not_fn] addSss
              (simpset() addsimps [fresh_def])) 1);
qed "tr_fresh";


(* well-formedness *)

Goal "[| ALL b fxs ys d. wftrl fxs --> \
  \ wfpa tr (ffP b c) (fxs d) ys & \
  \ wfpa (%x. tr (ffP b c) (fxs x) ys d) ; wftrl fxs |] \
  \ ==> wfpa tr (ffP e c) ((e, (%y. b))#fxs d) ys";
by (auto_tac (claset() addIs [wftrl_cons1], simpset()));
qed "inst_hyp1";

Goal "[| ALL b fxs ys d. wftrl fxs --> \
  \ wfpa tr (ffP b c) (fxs d) ys & \
  \ wfpa (%x. tr (ffP b c) (fxs x) ys d) ; wftrl fxs |] \
  \ ==> wfpa (%x. tr (ffP e c) ((e, (%y. x))#fxs d) ys b)";
by (auto_tac (claset() addIs [wftrl_cons2], simpset()));
qed "inst_hyp2";

Goal "[| ALL b fxs ys d. wftrl fxs --> \
  \ wfpa tr (ffP b c) (fxs d) ys & \
  \ wfpa (%x. tr (ffP b c) (fxs x) ys d) ; wftrl fxs |] \
  \ ==> wfpa (%x. tr (ffP e c) ((e, (%y. d))#fxs x) ys b)";
by (auto_tac (claset() addIs [wftrl_cons3], simpset()));
qed "inst_hyp3";

Goal "wfpa fP ==> ALL fxs ys d. wftrl fxs --> \
  \ wfpa tr (fP c) (fxs d) ys & \
  \ wfpa (%x. tr (fP c) (fxs x) ys d)";
by (etac WFPA.induct 1);

(* inaction, silent prefix, output prefix *)
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [wftrl_wfna_trn1, wftrl_wfna_trn2]
                       addSss simpset()) 1);

(* input prefix, restriction *)
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [inst_hyp1, inst_hyp2, inst_hyp3]
                       addSIs [wftrl_wfna_trn1, wftrl_wfna_trn2]
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [inst_hyp1, inst_hyp2, inst_hyp3]
                       addSss simpset()) 1);

(* choice, parallel composition, matching, mismatching, replication *)
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [wftrl_wfna_trn1, wftrl_wfna_trn2]
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [wftrl_wfna_trn1, wftrl_wfna_trn2]
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
qed "lemma";

Goal "[| wfpa fP ; wftrl fxs |] \
  \ ==> wfpa (tr (fP c) (fxs b) ys)";
by (fast_tac (claset() addDs [lemma]) 1);
qed "tr_wfpa_abs1";

Goal "[| wfpa fP ; wftrl fxs |] \
  \ ==> wfpa (%x. (tr (fP c) (fxs x) ys) b)";
by (fast_tac (claset() addDs [lemma]) 1);
qed "tr_wfpa_abs2";

Goal "wfp P ==> (ALL x:set(xs). wfna (snd x)) \
  \ --> wfpa (tr P xs ys)";
by (etac WFP.induct 1);
by (ALLGOALS Clarify_tac);

(* inaction, silent prefix, output prefix *)
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [wfna_trn]
                       addSss simpset()) 1);

(* input prefix *)
by (Asm_simp_tac 1);
by (resolve_tac WFPA.intrs 1);
by (fast_tac (claset() addSIs WFTRL.intrs
                       addSIs WFNAA.intrs
                       addSIs [tr_wfpa_abs1]
                       addSIs [wfna_wftrl]) 1);
by (fast_tac (claset() addSIs WFTRL.intrs
                       addSIs WFNAA.intrs
                       addSIs [tr_wfpa_abs2]
                       addSIs [wfna_wftrl]) 1);
by (fast_tac (claset() addSIs [wfna_trn]) 1);

(* restriction *)
by (Asm_simp_tac 1);
by (resolve_tac WFPA.intrs 1);
by (fast_tac (claset() addSIs WFTRL.intrs
                       addSIs WFNAA.intrs
                       addSIs [tr_wfpa_abs1]
                       addSIs [wfna_wftrl]) 1);
by (fast_tac (claset() addSIs WFTRL.intrs
                       addSIs WFNAA.intrs
                       addSIs [tr_wfpa_abs2]
                       addSIs [wfna_wftrl]) 1);

(* choice, parallel composition, matching, mismatching, replication *)
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [wfna_trn]
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSIs [wfna_trn]
                       addSss simpset()) 1);
by (fast_tac (claset() addSIs WFPA.intrs
                       addSss simpset()) 1);
qed "lemma";

Goal "[| wfp P ; ALL x:set xs. wfna snd x |] \
  \ ==> wfpa tr P xs ys";
by (fast_tac (claset() addDs [lemma]) 1);
qed "tr_wfpa";


(* equality *)

Goal "[| ALL b xs ys. (ALL x:set xs. snd x = (%y. fst x)) & \
  \ doba (ffP b) c <= length ys & \
  \ fna (ffP b) <= insert a (set (map fst xs)) & \
  \ a ~: set (map fst xs) & d : set (map fst xs) & \
  \ nodups ys & \
  \ set ys Int insert a (set (map fst xs)) = {} \
  \ --> tr (ffP b d) xs ys a = ffP b d ; \
  \ ALL b. wfpa ffP b ; ALL b. wfpa (%x. ffP x b) ; \
  \ ALL x:set xs. snd x = (%y. fst x) ; \
  \ Suc (doba (ffP c) c) <= length ys ; \
  \ fnaa ffP <= insert a (set (map fst xs)) ; \
  \ a ~: set (map fst xs) ; d : set (map fst xs) ; \
  \ nodups ys ; \
  \ set ys Int insert a (set (map fst xs)) = {} |] \
  \ ==> (%y. tr (ffP (hd ys) d) ((hd ys, (%x. y))#xs) (tl ys) a) = \
  \ (%y. ffP y d)";
by (res_inst_tac [("a", "hd ys")] ext_pa 1);

(* well-formedness *)
by (rtac tr_wfpa_abs2 1);
by (Fast_tac 1);
by (resolve_tac WFTRL.intrs 1);
by (fast_tac (claset() addIs WFNAA.intrs) 1);
by (fast_tac (claset() addSIs [wfna_wftrl, const_trl_wfna_trl]) 1);
by (Fast_tac 1);

(* equality *)
by (eres_inst_tac [("x", "hd ys")] allE 1);
by (eres_inst_tac [("x", "(hd ys, (%x. hd ys))#xs")] allE 1);
by (eres_inst_tac [("x", "tl ys")] allE 1);
by (etac impE 1);
by (dtac Suc_le_lengthD 1);
by (rtac conjI 1);
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rtac conjI 1);
by (dres_inst_tac [("a", "c"), ("b", "c"), ("c", "hd ys"), ("d", "c")]
    doba_varaa 1);
by (atac 1);
by (Force_tac 1);
by (rtac conjI 1);
by (dres_inst_tac
    [("a", "hd ys"), ("A", "insert a (set (map fst xs))")]
    fnaa_fna_subset 1);
by (REPEAT (atac 1));
by (full_simp_tac (simpset() addsimps [insert_swap]) 1);
by (rtac conjI 1);
by (Asm_full_simp_tac 1);
by (fast_tac (claset() addSDs [Int_empty_ineq_hd]) 1);
by (rtac conjI 1);
by (dtac Int_empty_Int_tl_empty 1);
by (REPEAT (atac 1));
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
by (fast_tac (claset() addIs [nodups_tl]) 1);
by (dtac Int_empty_sort 1);
by (REPEAT (atac 1));
by (Asm_full_simp_tac 1);
by (atac 1);

(* freshness *)
by (dtac Suc_le_lengthD 1);
by (Clarify_tac 1);
by (res_inst_tac [("b", "a")] fresh_mono 1);
by (rtac tr_fresh_abs 1);
by (Fast_tac 1);
by (forward_tac [Int_empty_ineq_hd] 1);
by (atac 1);
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (Fast_tac 1);
by (dtac Int_empty_not_cont_hd 1);
by (atac 1);
by (atac 1);
by (fast_tac (claset() addSIs [not_in_not_fst]) 1);
by (fast_tac (claset() addSDs [Int_empty_ineq_hd]) 1);
by (dtac Suc_le_lengthD 1);
by (Clarify_tac 1);
by (rtac freshaa_fresha 1);
by (atac 1);
by (atac 1);
by (asm_simp_tac (simpset() addsimps [freshaa_def]) 1);
by (cut_inst_tac [("ffP", "ffP")] fnaa_sym 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("B", "insert a (set (map fst xs))")]
    rev_contra_subsetD 1);
by (Asm_simp_tac 1);
by (rtac Int_empty_not_cont_hd_ins 1);
by (Asm_simp_tac 1);
by (atac 1);
by (atac 1);
by (fast_tac (claset() addSDs [Int_empty_ineq_mem]) 1);
qed "inst_hyp";

Goal "wfpa fP ==> ALL xs ys. \
  \ (ALL x:set xs. snd x = (%y. fst x)) & (doba fP c) <= length ys & \
  \ fna fP <= insert a (set (map fst xs)) & a ~: set (map fst xs) & \
  \ d : set (map fst xs) & nodups ys & \
  \ set ys Int insert a (set (map fst xs)) = {} \
  \ --> (tr (fP d) xs ys) a = fP d";
by (etac WFPA.induct 1);
by (ALLGOALS Clarify_tac);

(* inaction, silent prefix *)
by (Asm_simp_tac 1);
by (fast_tac (claset() addSDs [fna_subset1, doba_leq1]
                       addSss simpset()) 1);

(* output prefix *)
by (Asm_simp_tac 1);
by (clarify_tac (claset() addSDs [fna_subset2, doba_leq2]) 1);
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fa")] (rotate_prems 2
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fb")] (rotate_prems 2 
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (Force_tac 1);

(* input prefix *)
by (Asm_simp_tac 1);
by (clarify_tac (claset() addSEs [all_conjE] 
                          addSDs [fna_subset3, doba_leq3]) 1);
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fa")] (rotate_prems 2
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (res_inst_tac [("c", "c")] inst_hyp 1);
by (REPEAT (atac 1));

(* restriction *)
by (Asm_simp_tac 1);
by (clarify_tac (claset() addSEs [all_conjE] 
                          addSDs [fna_subset4, doba_leq4]) 1);
by (res_inst_tac [("c", "c")] inst_hyp 1);
by (REPEAT (atac 1));

(* choice, parallel composition *)
by (force_tac (claset() addSDs [fna_subset5, doba_leq5],
               simpset()) 1);
by (force_tac (claset() addSDs [fna_subset6, doba_leq6],
               simpset()) 1);

(* matching *)
by (Asm_simp_tac 1);
by (clarify_tac (claset() addSDs [fna_subset7, doba_leq7]) 1);
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fa")] (rotate_prems 2
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fb")] (rotate_prems 2 
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (Force_tac 1);

(* mismatching *)
by (Asm_simp_tac 1);
by (clarify_tac (claset() addSDs [fna_subset8, doba_leq8]) 1);
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fa")] (rotate_prems 2
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
by (res_inst_tac [("fa1", "fb")] (rotate_prems 2 
    (fnna_subset RS (rotate_prems 1 const_trn))) 1);
by (Fast_tac 1);
by (REPEAT (atac 1));
by (Force_tac 1);

(* replication *)
by (fast_tac (claset() addSDs [fna_subset9, doba_leq9]
                       addSss simpset()) 1);
qed "lemma";

Goal "[| wfpa fP ; ALL x:set xs. snd x = (%y. fst x) ; \
  \ doba fP c <= length ys ; fna fP <= insert a (set (map fst xs)) ; \
  \ a ~: set (map fst xs) ; d : set (map fst xs) ; nodups ys ; \
  \ set ys Int insert a (set (map fst xs)) = {} |] \
  \ ==> (tr (fP d) xs ys) a = fP d";
by (dres_inst_tac [("a", "a"), ("c", "c"), ("d", "d")] lemma 1);
by (Auto_tac);
qed "tr_eq_abs";

Goal "[| wfpa fP ; ALL x:set xs. snd x = (%y. fst x) ; \
  \ Suc (doba fP c) <= length ys ; \
  \ fna fP <= insert a (set (map fst xs)) ; a ~: set (map fst xs) ; \
  \ nodups ys ; set ys Int insert a (set (map fst xs)) = {} |] \
  \ ==> (%y. tr (fP (hd ys)) ((hd ys, (%x. y))#xs) (tl ys) a) = fP";
by (res_inst_tac [("a", "hd ys")] ext_pa 1);

(* well-formedness *)
by (rtac tr_wfpa_abs2 1);
by (atac 1);
by (resolve_tac WFTRL.intrs 1);
by (fast_tac (claset() addIs WFNAA.intrs) 1);
by (fast_tac (claset() addSIs [wfna_wftrl, const_trl_wfna_trl]) 1);
by (atac 1);

(* equality *)
by (clarify_tac (claset() addSDs [Suc_le_lengthD]) 1);
by (rtac tr_eq_abs 1);
by (atac 1);
by (Asm_simp_tac 1);
by (atac 1);
by (rtac subset_trans 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (fast_tac (claset() addSDs [Int_empty_ineq_hd]) 1);
by (Asm_full_simp_tac 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addSIs [nodups_tl]) 1);
by (dtac Int_empty_sort 1);
by (REPEAT (atac 1));
by (Asm_full_simp_tac 1);

(* freshness *)
by (clarify_tac (claset() addSDs [Suc_le_lengthD]) 1);
by (res_inst_tac [("b", "a")] fresh_mono 1);
by (rtac tr_fresh_abs 1);
by (atac 1);
by (forward_tac [Int_empty_ineq_hd] 1);
by (atac 1);
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (Fast_tac 1);
by (dtac Int_empty_not_cont_hd 1);
by (atac 1);
by (atac 1);
by (fast_tac (claset() addSIs [not_in_not_fst]) 1);
by (fast_tac (claset() addSDs [Int_empty_ineq_hd]) 1);
by (clarify_tac (claset() addSDs [Suc_le_lengthD]) 1);
by (asm_simp_tac (simpset() addsimps [fresha_def]) 1);
by (res_inst_tac [("B", "insert a (set (map fst xs))")]
    rev_contra_subsetD 1);
by (atac 1);
by (rtac Int_empty_not_cont_hd_ins 1);
by (REPEAT (atac 1));
qed "inst_hyp";

Goal "wfp P ==> ALL xs ys. \
  \ (ALL x:set xs. snd x = (%y. fst x)) & dob P c <= length ys & \
  \ fn P <= insert a (set (map fst xs)) & a ~: set (map fst xs) & \
  \ nodups ys & set ys Int insert a (set (map fst xs)) = {} \
  \ --> (tr P xs ys) a = P";
by (etac WFP.induct 1);
by (ALLGOALS Clarify_tac);

(* inaction, silent prefix *)
by (Asm_simp_tac 1);
by (fast_tac (claset() addSss simpset()) 1);

(* output prefix *)
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (fast_tac (claset() addSss simpset()) 1);

(* input prefix *)
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (res_inst_tac [("c", "c")] inst_hyp 1);
by (REPEAT (atac 1));
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (REPEAT (atac 1));

(* restriction *)
by (Asm_simp_tac 1);
by (res_inst_tac [("c", "c")] inst_hyp 1);
by (REPEAT (atac 1));
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (REPEAT (atac 1));

(* choice, parallel composition *)
by (force_tac (claset() addSDs [Un_subset_conj], simpset()) 1);
by (force_tac (claset() addSDs [Un_subset_conj], simpset()) 1);

(* matching *)
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (fast_tac (claset() addSss simpset()) 1);

(* mismatching *)
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (rtac conjI 1);
by (rtac const_trn 1);
by (atac 1);
by (fast_tac (claset() addSss simpset()) 1);
by (fast_tac (claset() addSss simpset()) 1);

(* replication *)
by (fast_tac (claset() addSss simpset()) 1);
qed "lemma";

Goal "[| wfp P ; ALL x:set xs. snd x = (%y. fst x) ; \
  \ dob P c <= length ys ; fn P <= insert a (set (map fst xs)) ; \
  \ a ~: set (map fst xs) ; nodups ys ; \
  \ set ys Int insert a (set (map fst xs)) = {} |] \
  \ ==> (tr P xs ys) a = P";
by (dres_inst_tac [("a", "a"), ("c", "c")] lemma 1);
by (Auto_tac);
qed "tr_eq";


(* beta-expansion *)

Goal "finite (insert a (fn P))";
by (cut_inst_tac [("P", "P")] finite_fn 1);
by (Auto_tac);
qed "finite_insert_fn";

Goal "wfp P ==> EX fP. wfpa fP & fresha a fP & P = fP a";

(* create transformation list and store of names *)
by (cut_inst_tac [("a", "a"), ("P", "P")] finite_insert_fn 1);
by (dres_inst_tac [("n", "dob P c")] ex_n_dist_set 1);
by (cut_inst_tac [("P", "P")] finite_fn 1);
by (clarify_tac (claset() addSDs [set_list_transform]) 1);

(* instantiate fP *)
by (res_inst_tac [("x", "tr P (mk_trl xs a) xsa")] exI 1);

(* well-formedness *)
by (rtac conjI 1);
by (fast_tac (claset() addSIs [tr_wfpa, mk_trl_wfna]) 1);

(* freshness *)
by (rtac conjI 1);
by (cut_inst_tac [("A", "insert a (set xs)")] ex_dist_set 1);
by (asm_simp_tac (simpset() addsimps [finite_fn]) 1);
by (etac exE 1);
by (res_inst_tac [("b", "b")] fresh_mono 1);
by (fast_tac (claset() addSIs [tr_fresh, mk_trl_ineq]) 1);

(* equality *)
by (rtac (tr_eq RS sym) 1);
by (atac 1);
by (fast_tac (claset() addSIs [mk_trl_const]) 1);
by (Force_tac 1);
by (cut_inst_tac [("xs", "xs"), ("a", "a")] mk_trl_contain 1);
by (Force_tac 1);
by (fast_tac (claset() addSIs [a_not_in_trl]) 1);
by (atac 1);
by (cut_inst_tac [("xs", "xs"), ("a", "a")] mk_trl_contain 1);
by (rewrite_goals_tac [mk_meta_eq mk_trl_map_fst]);
by (Auto_tac);
qed "beta_exp";

Goal "wfpa fP ==> EX ffP. (ALL b. wfpa ffP b) & (ALL b. wfpa (%x. ffP x b)) & \
 \ freshaa a ffP & fP = ffP a";
by (dres_inst_tac [("a", "a")] (WFP.Res RS beta_exp) 1);
by (Clarify_tac 1);
by ((forward_tac [wfpa_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";