808 shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)" |
808 shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)" |
809 by (simp add: permute_bool_def) |
809 by (simp add: permute_bool_def) |
810 |
810 |
811 declare imp_eqvt[folded induct_implies_def, eqvt] |
811 declare imp_eqvt[folded induct_implies_def, eqvt] |
812 |
812 |
|
813 lemma all_eqvt [eqvt]: |
|
814 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
|
815 unfolding All_def |
|
816 by (perm_simp) (rule refl) |
|
817 |
|
818 declare all_eqvt[folded induct_forall_def, eqvt] |
|
819 |
813 lemma ex_eqvt [eqvt]: |
820 lemma ex_eqvt [eqvt]: |
814 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
821 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
815 unfolding permute_fun_def permute_bool_def |
822 unfolding Ex_def |
816 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
823 by (perm_simp) (rule refl) |
817 |
|
818 lemma all_eqvt [eqvt]: |
|
819 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
|
820 unfolding permute_fun_def permute_bool_def |
|
821 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
|
822 |
|
823 declare all_eqvt[folded induct_forall_def, eqvt] |
|
824 |
824 |
825 lemma ex1_eqvt [eqvt]: |
825 lemma ex1_eqvt [eqvt]: |
826 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
826 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
827 unfolding Ex1_def |
827 unfolding Ex1_def |
828 by (perm_simp) (rule refl) |
828 by (perm_simp) (rule refl) |
2557 apply(simp add: supp_of_finite_sets[OF a]) |
2557 apply(simp add: supp_of_finite_sets[OF a]) |
2558 apply(simp add: supp_at_base) |
2558 apply(simp add: supp_at_base) |
2559 apply(auto) |
2559 apply(auto) |
2560 done |
2560 done |
2561 |
2561 |
|
2562 (* FIXME |
|
2563 lemma supp_cofinite_set_at_base: |
|
2564 assumes a: "finite (UNIV - S)" |
|
2565 shows "supp S = atom ` (UNIV - S)" |
|
2566 apply(rule finite_supp_unique) |
|
2567 *) |
|
2568 |
2562 lemma fresh_finite_set_at_base: |
2569 lemma fresh_finite_set_at_base: |
2563 fixes a::"'a::at_base" |
2570 fixes a::"'a::at_base" |
2564 assumes a: "finite S" |
2571 assumes a: "finite S" |
2565 shows "atom a \<sharp> S \<longleftrightarrow> a \<notin> S" |
2572 shows "atom a \<sharp> S \<longleftrightarrow> a \<notin> S" |
2566 unfolding fresh_def |
2573 unfolding fresh_def |