546 by (simp add: permute_fun_def permute_bool_def) |
546 by (simp add: permute_fun_def permute_bool_def) |
547 |
547 |
548 lemma insert_eqvt: |
548 lemma insert_eqvt: |
549 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
549 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
550 unfolding permute_set_eq_image image_insert .. |
550 unfolding permute_set_eq_image image_insert .. |
|
551 |
|
552 lemma Collect_eqvt: |
|
553 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
|
554 unfolding Collect_def permute_fun_def .. |
|
555 |
|
556 lemma inter_eqvt: |
|
557 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
|
558 unfolding Int_def |
|
559 apply(simp add: Collect_eqvt) |
|
560 apply(simp add: permute_fun_def) |
|
561 apply(simp add: conj_eqvt) |
|
562 apply(simp add: mem_eqvt) |
|
563 apply(simp add: permute_fun_def) |
|
564 done |
|
565 |
551 |
566 |
552 |
567 |
553 subsection {* Permutations for units *} |
568 subsection {* Permutations for units *} |
554 |
569 |
555 instantiation unit :: pt |
570 instantiation unit :: pt |
1995 } |
2010 } |
1996 ultimately show "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2011 ultimately show "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
1997 by blast |
2012 by blast |
1998 qed |
2013 qed |
1999 |
2014 |
2000 |
2015 lemma set_renaming_perm2: |
|
2016 shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
|
2017 proof - |
|
2018 have "finite (bs \<inter> supp p)" by (simp add: finite_supp) |
|
2019 then obtain q |
|
2020 where *: "\<forall>b \<in> bs \<inter> supp p. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> (bs \<inter> supp p) \<union> (p \<bullet> (bs \<inter> supp p))" |
|
2021 using set_renaming_perm by blast |
|
2022 from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp add: inter_eqvt) |
|
2023 moreover |
|
2024 have "\<forall>b \<in> bs - supp p. q \<bullet> b = p \<bullet> b" |
|
2025 apply(auto) |
|
2026 apply(subgoal_tac "b \<notin> supp q") |
|
2027 apply(simp add: fresh_def[symmetric]) |
|
2028 apply(simp add: fresh_perm) |
|
2029 apply(clarify) |
|
2030 apply(rotate_tac 2) |
|
2031 apply(drule subsetD[OF **]) |
|
2032 apply(simp add: inter_eqvt supp_eqvt permute_self) |
|
2033 done |
|
2034 ultimately have "(\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" using * by auto |
|
2035 then show "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
|
2036 qed |
|
2037 |
2001 lemma list_renaming_perm: |
2038 lemma list_renaming_perm: |
2002 shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" |
2039 shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" |
2003 proof (induct bs) |
2040 proof (induct bs) |
2004 case Nil |
2041 case Nil |
2005 have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
2042 have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |