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";