138 lemma sort_of_Rep_perm: "sort_of (Rep_perm p a) = sort_of a" |
138 lemma sort_of_Rep_perm: "sort_of (Rep_perm p a) = sort_of a" |
139 using Rep_perm [of p] unfolding perm_def by simp |
139 using Rep_perm [of p] unfolding perm_def by simp |
140 |
140 |
141 lemma Rep_perm_ext: |
141 lemma Rep_perm_ext: |
142 "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2" |
142 "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2" |
143 by (simp add: expand_fun_eq Rep_perm_inject [symmetric]) |
143 by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) |
144 |
144 |
145 |
145 |
146 subsection {* Permutations form a group *} |
146 subsection {* Permutations form a group *} |
147 |
147 |
148 instantiation perm :: group_add |
148 instantiation perm :: group_add |
222 by (rule Rep_perm_ext) (simp add: Rep_perm_simps) |
222 by (rule Rep_perm_ext) (simp add: Rep_perm_simps) |
223 |
223 |
224 lemma swap_cancel: |
224 lemma swap_cancel: |
225 "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0" |
225 "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0" |
226 by (rule Rep_perm_ext) |
226 by (rule Rep_perm_ext) |
227 (simp add: Rep_perm_simps expand_fun_eq) |
227 (simp add: Rep_perm_simps fun_eq_iff) |
228 |
228 |
229 lemma swap_self [simp]: |
229 lemma swap_self [simp]: |
230 "(a \<rightleftharpoons> a) = 0" |
230 "(a \<rightleftharpoons> a) = 0" |
231 by (rule Rep_perm_ext, simp add: Rep_perm_simps expand_fun_eq) |
231 by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff) |
232 |
232 |
233 lemma minus_swap [simp]: |
233 lemma minus_swap [simp]: |
234 "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)" |
234 "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)" |
235 by (rule minus_unique [OF swap_cancel]) |
235 by (rule minus_unique [OF swap_cancel]) |
236 |
236 |
237 lemma swap_commute: |
237 lemma swap_commute: |
238 "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)" |
238 "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)" |
239 by (rule Rep_perm_ext) |
239 by (rule Rep_perm_ext) |
240 (simp add: Rep_perm_swap expand_fun_eq) |
240 (simp add: Rep_perm_swap fun_eq_iff) |
241 |
241 |
242 lemma swap_triple: |
242 lemma swap_triple: |
243 assumes "a \<noteq> b" and "c \<noteq> b" |
243 assumes "a \<noteq> b" and "c \<noteq> b" |
244 assumes "sort_of a = sort_of b" "sort_of b = sort_of c" |
244 assumes "sort_of a = sort_of b" "sort_of b = sort_of c" |
245 shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)" |
245 shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)" |
246 using assms |
246 using assms |
247 by (rule_tac Rep_perm_ext) |
247 by (rule_tac Rep_perm_ext) |
248 (auto simp add: Rep_perm_simps expand_fun_eq) |
248 (auto simp add: Rep_perm_simps fun_eq_iff) |
249 |
249 |
250 |
250 |
251 section {* Permutation Types *} |
251 section {* Permutation Types *} |
252 |
252 |
253 text {* |
253 text {* |
1870 show "(FRESH x. f (P x)) = f (FRESH x. P x)" |
1870 show "(FRESH x. f (P x)) = f (FRESH x. P x)" |
1871 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
1871 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
1872 apply (cut_tac `atom a \<sharp> P`) |
1872 apply (cut_tac `atom a \<sharp> P`) |
1873 apply (simp add: fresh_conv_MOST) |
1873 apply (simp add: fresh_conv_MOST) |
1874 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
1874 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
1875 apply (simp add: permute_fun_def permute_pure expand_fun_eq) |
1875 apply (simp add: permute_fun_def permute_pure fun_eq_iff) |
1876 apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh]) |
1876 apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh]) |
1877 apply (rule refl) |
1877 apply (rule refl) |
1878 done |
1878 done |
1879 qed |
1879 qed |
1880 |
1880 |
1894 show ?thesis |
1894 show ?thesis |
1895 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
1895 apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) |
1896 apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`) |
1896 apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`) |
1897 apply (simp add: fresh_conv_MOST) |
1897 apply (simp add: fresh_conv_MOST) |
1898 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
1898 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
1899 apply (simp add: permute_fun_def permute_pure expand_fun_eq) |
1899 apply (simp add: permute_fun_def permute_pure fun_eq_iff) |
1900 apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh]) |
1900 apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh]) |
1901 apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh]) |
1901 apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh]) |
1902 apply (rule refl) |
1902 apply (rule refl) |
1903 done |
1903 done |
1904 qed |
1904 qed |