equal
deleted
inserted
replaced
412 |
412 |
413 lemma permute_fun_app_eq: |
413 lemma permute_fun_app_eq: |
414 shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)" |
414 shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)" |
415 unfolding permute_fun_def by simp |
415 unfolding permute_fun_def by simp |
416 |
416 |
417 |
|
418 subsection {* Permutations for booleans *} |
417 subsection {* Permutations for booleans *} |
419 |
418 |
420 instantiation bool :: pt |
419 instantiation bool :: pt |
421 begin |
420 begin |
422 |
421 |
480 |
479 |
481 lemma permute_set_eq_vimage: |
480 lemma permute_set_eq_vimage: |
482 shows "p \<bullet> X = permute (- p) -` X" |
481 shows "p \<bullet> X = permute (- p) -` X" |
483 unfolding permute_fun_def permute_bool_def |
482 unfolding permute_fun_def permute_bool_def |
484 unfolding vimage_def Collect_def mem_def .. |
483 unfolding vimage_def Collect_def mem_def .. |
|
484 |
|
485 lemma permute_finite [simp]: |
|
486 shows "finite (p \<bullet> X) = finite X" |
|
487 apply(simp add: permute_set_eq_image) |
|
488 apply(rule iffI) |
|
489 apply(drule finite_imageD) |
|
490 using inj_permute[where p="p"] |
|
491 apply(simp add: inj_on_def) |
|
492 apply(assumption) |
|
493 apply(rule finite_imageI) |
|
494 apply(assumption) |
|
495 done |
485 |
496 |
486 lemma swap_set_not_in: |
497 lemma swap_set_not_in: |
487 assumes a: "a \<notin> S" "b \<notin> S" |
498 assumes a: "a \<notin> S" "b \<notin> S" |
488 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
499 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
489 unfolding permute_set_eq |
500 unfolding permute_set_eq |
1160 apply default |
1171 apply default |
1161 apply (induct_tac x) |
1172 apply (induct_tac x) |
1162 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1173 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1163 done |
1174 done |
1164 |
1175 |
|
1176 lemma supp_of_atom_list: |
|
1177 fixes as::"atom list" |
|
1178 shows "supp as = set as" |
|
1179 by (induct as) |
|
1180 (simp_all add: supp_Nil supp_Cons supp_atom) |
|
1181 |
1165 |
1182 |
1166 section {* Support and Freshness for Applications *} |
1183 section {* Support and Freshness for Applications *} |
1167 |
1184 |
1168 lemma fresh_conv_MOST: |
1185 lemma fresh_conv_MOST: |
1169 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1186 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1285 fixes S::"('a::fs) set" |
1302 fixes S::"('a::fs) set" |
1286 assumes fin: "finite S" |
1303 assumes fin: "finite S" |
1287 shows "supp (insert x S) = supp x \<union> supp S" |
1304 shows "supp (insert x S) = supp x \<union> supp S" |
1288 using fin |
1305 using fin |
1289 by (simp add: supp_of_finite_sets) |
1306 by (simp add: supp_of_finite_sets) |
|
1307 |
|
1308 lemma fresh_finite_insert: |
|
1309 fixes S::"('a::fs) set" |
|
1310 assumes fin: "finite S" |
|
1311 shows "a \<sharp> (insert x S) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S" |
|
1312 using fin unfolding fresh_def |
|
1313 by (simp add: supp_of_finite_insert) |
1290 |
1314 |
1291 |
1315 |
1292 subsection {* Type @{typ "'a fset"} is finitely supported *} |
1316 subsection {* Type @{typ "'a fset"} is finitely supported *} |
1293 |
1317 |
1294 lemma fset_eqvt: |
1318 lemma fset_eqvt: |