543 subsection {* Renaming of bodies of abstractions *}

   544 

   545 

   546 lemma Abs_rename_set:

   547   fixes x::"'a::fs"

   548   assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 

   549   and     b: "finite bs"

   550   shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"

   551 proof -

   552   from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   

   553   with set_renaming_perm 

   554   obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis

   555   have "[bs]set. x =  q \<bullet> ([bs]set. x)"

   556     apply(rule perm_supp_eq[symmetric])

   557     using a **

   558     unfolding fresh_star_Pair

   559     unfolding Abs_fresh_star_iff

   560     unfolding fresh_star_def

   561     by auto

   562   also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp

   563   also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp

   564   finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .

   565   then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast

   566 qed

   567 

   568 lemma Abs_rename_res:

   569   fixes x::"'a::fs"

   570   assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 

   571   and     b: "finite bs"

   572   shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"

   573 proof -

   574   from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 

   575   with set_renaming_perm 

   576   obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis

   577   have "[bs]res. x =  q \<bullet> ([bs]res. x)"

   578     apply(rule perm_supp_eq[symmetric])

   579     using a **

   580     unfolding fresh_star_Pair

   581     unfolding Abs_fresh_star_iff

   582     unfolding fresh_star_def

   583     by auto

   584   also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp

   585   also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp

   586   finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .

   587   then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast

   588 qed

   589 

   590 lemma Abs_rename_list:

   591   fixes x::"'a::fs"

   592   assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 

   593   shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"

   594 proof -

   595   from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 

   596     by (simp add: fresh_star_Pair fresh_star_set)

   597   with list_renaming_perm 

   598   obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 

   599   have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"

   600     apply(rule perm_supp_eq[symmetric])

   601     using a **

   602     unfolding fresh_star_Pair

   603     unfolding Abs_fresh_star_iff

   604     unfolding fresh_star_def

   605     by auto

   606   also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp

   607   also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp

   608   finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .

   609   then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast

   610 qed

   611 

   612 

   613