52 lemma set_renaming_perm:

    52 

    53   assumes a: "p \<bullet> bs \<inter> bs = {}" 

    53 text {* *}

    54   and     b: "finite bs"

    54 

    55   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"

    56 using b a

    57 proof (induct)

    58   case empty

    59   have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"

    60     by (simp add: permute_set_eq supp_perm)

    61   then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast

    62 next

    63   case (insert a bs)

    64   then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" 

    65     by (perm_simp) (auto)

    66   then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 

    67   { assume 1: "q \<bullet> a = p \<bullet> a"

    68     have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)

    69     moreover 

    70     have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 

    71       using ** by (auto simp add: insert_eqvt)

    72     ultimately 

    73     have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast

    74   }

    75   moreover

    76   { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"

    77     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"

    78     { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)

    79       moreover 

    80       have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)

    81       ultimately 

    82       have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def 

    83         by (simp add: insert_eqvt  swap_set_not_in) 

    84     }

    85     moreover 

    86     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"

    87 	using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`

    88 	by (auto simp add: supp_perm insert_eqvt)

    89       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)

    90       moreover

    91       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 

    92 	using ** by (auto simp add: insert_eqvt)

    93       ultimately 

    94       have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 

    95         unfolding q'_def using supp_plus_perm by blast

    96     }

    97     ultimately 

    98     have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast

    99   }

   100   ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"

   101     by blast

   102 qed

   103 

   104 

   105 lemma Abs_rename_set:

   106   fixes x::"'a::fs"

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

   108   and     b: "finite bs"

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

   110 proof -

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

   112   with set_renaming_perm 

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

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

   115     apply(rule perm_supp_eq[symmetric])

   116     using a **

   117     unfolding fresh_star_Pair

   118     unfolding Abs_fresh_star_iff

   119     unfolding fresh_star_def

   120     by auto

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

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

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

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

   125 qed

   126 

   127 lemma Abs_rename_res:

   128   fixes x::"'a::fs"

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

   130   and     b: "finite bs"

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

   132 proof -

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

   134   with set_renaming_perm 

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

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

   137     apply(rule perm_supp_eq[symmetric])

   138     using a **

   139     unfolding fresh_star_Pair

   140     unfolding Abs_fresh_star_iff

   141     unfolding fresh_star_def

   142     by auto

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

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

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

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

   147 qed

   148 

   149 lemma list_renaming_perm:

   150   fixes bs::"atom list"

   151   assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"

   152   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"

   153 using a

   154 proof (induct bs)

   155   case Nil

   156   have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"

   157     by (simp add: permute_set_eq supp_perm)

   158   then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast

   159 next

   160   case (Cons a bs)

   161   then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" 

   162     by (perm_simp) (auto)

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

   164   { assume 1: "a \<in> set bs"

   165     have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)

   166     then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp 

   167     moreover 

   168     have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)

   169     ultimately 

   170     have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast

   171   }

   172   moreover

   173   { assume 2: "a \<notin> set bs"

   174     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"

   175     { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] 

   176 	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)

   177       moreover 

   178       have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` 

   179 	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)

   180       ultimately 

   181       have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def 

   182         by (simp add: swap_fresh_fresh) 

   183     }

   184     moreover 

   185     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"

   186 	using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`

   187 	by (auto simp add: supp_perm insert_eqvt)

   188       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)

   189       moreover

   190       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 

   191 	using ** by (auto simp add: insert_eqvt)

   192       ultimately 

   193       have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 

   194         unfolding q'_def using supp_plus_perm by blast

   195     }

   196     ultimately 

   197     have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast

   198   }

   199   ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"

   200     by blast

   201 qed

   202 

   203 

   204 lemma Abs_rename_list:

   205   fixes x::"'a::fs"

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

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

   208 proof -

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

   210     by (simp add: fresh_star_Pair fresh_star_set)

   211   with list_renaming_perm 

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

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

   214     apply(rule perm_supp_eq[symmetric])

   215     using a **

   216     unfolding fresh_star_Pair

   217     unfolding Abs_fresh_star_iff

   218     unfolding fresh_star_def

   219     by auto

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

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

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

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

   224 qed