equal
deleted
inserted
replaced
430 |
430 |
431 lemma permute_set_eq_vimage: |
431 lemma permute_set_eq_vimage: |
432 shows "p \<bullet> X = permute (- p) -` X" |
432 shows "p \<bullet> X = permute (- p) -` X" |
433 unfolding permute_fun_def permute_bool_def |
433 unfolding permute_fun_def permute_bool_def |
434 unfolding vimage_def Collect_def mem_def .. |
434 unfolding vimage_def Collect_def mem_def .. |
|
435 |
|
436 lemma swap_set_not_in: |
|
437 assumes a: "a \<notin> S" "b \<notin> S" |
|
438 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
|
439 using a by (auto simp add: permute_set_eq swap_atom) |
|
440 |
|
441 lemma swap_set_in: |
|
442 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
|
443 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
|
444 using a by (auto simp add: permute_set_eq swap_atom) |
|
445 |
435 |
446 |
436 subsection {* Permutations for units *} |
447 subsection {* Permutations for units *} |
437 |
448 |
438 instantiation unit :: pt |
449 instantiation unit :: pt |
439 begin |
450 begin |
952 apply default |
963 apply default |
953 apply (induct_tac x) |
964 apply (induct_tac x) |
954 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
965 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
955 done |
966 done |
956 |
967 |
957 |
968 section {* Support and freshness for applications *} |
958 section {* support and freshness for applications *} |
|
959 |
969 |
960 lemma supp_fun_app: |
970 lemma supp_fun_app: |
961 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
971 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
962 proof (rule subsetCI) |
972 proof (rule subsetCI) |
963 fix a::"atom" |
973 fix a::"atom" |