equal
deleted
inserted
replaced
291 shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)" |
291 shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)" |
292 proof (induct pi1) |
292 proof (induct pi1) |
293 case Nil show ?case by (simp add: at1[OF at]) |
293 case Nil show ?case by (simp add: at1[OF at]) |
294 next |
294 next |
295 case (Cons x xs) |
295 case (Cons x xs) |
296 assume i: "(xs @ pi2)\<bullet>c = xs\<bullet>(pi2\<bullet>c)" |
296 have "(xs@pi2)\<bullet>c = xs\<bullet>(pi2\<bullet>c)" by fact |
297 have "(x#xs)@pi2 = x#(xs@pi2)" by simp |
297 also have "(x#xs)@pi2 = x#(xs@pi2)" by simp |
298 thus ?case using i by (cases "x", simp add: at2[OF at]) |
298 ultimately show ?case by (cases "x", simp add: at2[OF at]) |
299 qed |
299 qed |
300 |
300 |
301 lemma at_swap: |
301 lemma at_swap: |
302 fixes a :: "'x" |
302 fixes a :: "'x" |
303 and b :: "'x" |
303 and b :: "'x" |
549 assumes at: "at TYPE('x)" |
549 assumes at: "at TYPE('x)" |
550 shows "pt TYPE('x) TYPE('x)" |
550 shows "pt TYPE('x) TYPE('x)" |
551 apply(auto simp only: pt_def) |
551 apply(auto simp only: pt_def) |
552 apply(simp only: at1[OF at]) |
552 apply(simp only: at1[OF at]) |
553 apply(simp only: at_append[OF at]) |
553 apply(simp only: at_append[OF at]) |
554 apply(simp add: prm_eq_def) |
554 apply(simp only: prm_eq_def) |
555 done |
555 done |
556 |
556 |
557 section {* finite support properties *} |
557 section {* finite support properties *} |
558 (*===================================*) |
558 (*===================================*) |
559 |
559 |
893 and x :: "'a" |
893 and x :: "'a" |
894 and X :: "'a set" |
894 and X :: "'a set" |
895 assumes pt: "pt TYPE('a) TYPE('x)" |
895 assumes pt: "pt TYPE('a) TYPE('x)" |
896 and at: "at TYPE('x)" |
896 and at: "at TYPE('x)" |
897 shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)" |
897 shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)" |
898 by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at]) |
898 by (simp add: perm_set_def pt_bij[OF pt, OF at]) |
899 |
899 |
900 lemma pt_set_bij2: |
900 lemma pt_set_bij2: |
901 fixes pi :: "'x prm" |
901 fixes pi :: "'x prm" |
902 and x :: "'a" |
902 and x :: "'a" |
903 and X :: "'a set" |
903 and X :: "'a set" |
1264 lemma supports_subset: |
1264 lemma supports_subset: |
1265 fixes x :: "'a" |
1265 fixes x :: "'a" |
1266 and S1 :: "'x set" |
1266 and S1 :: "'x set" |
1267 and S2 :: "'x set" |
1267 and S2 :: "'x set" |
1268 assumes a: "S1 supports x" |
1268 assumes a: "S1 supports x" |
1269 and b: "S1\<subseteq>S2" |
1269 and b: "S1 \<subseteq> S2" |
1270 shows "S2 supports x" |
1270 shows "S2 supports x" |
1271 using a b |
1271 using a b |
1272 by (force simp add: "op supports_def") |
1272 by (force simp add: "op supports_def") |
1273 |
1273 |
1274 lemma supp_supports: |
1274 lemma supp_supports: |