69 unfolding supp_def |
69 unfolding supp_def |
70 apply (perm_simp) |
70 apply (perm_simp) |
71 apply (simp add: atom_fmap_cong) |
71 apply (simp add: atom_fmap_cong) |
72 done |
72 done |
73 |
73 |
74 lemma supp_atom_insert: |
|
75 "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs" |
|
76 apply (simp add: supp_finite_atom_set) |
|
77 apply (simp add: supp_atom) |
|
78 done |
|
79 |
|
80 lemma atom_image_cong: |
|
81 shows "(atom ` X = atom ` Y) = (X = Y)" |
|
82 apply(rule inj_image_eq_iff) |
|
83 apply(simp add: inj_on_def) |
|
84 done |
|
85 |
|
86 lemma atom_eqvt_raw: |
|
87 fixes p::"perm" |
|
88 shows "(p \<bullet> atom) = atom" |
|
89 apply(perm_simp) |
|
90 apply(simp) |
|
91 done |
|
92 |
|
93 lemma supp_finite_at_set: |
|
94 fixes S::"('a :: at) set" |
|
95 assumes a: "finite S" |
|
96 shows "supp S = atom ` S" |
|
97 apply(rule finite_supp_unique) |
|
98 apply(simp add: supports_def) |
|
99 apply (rule finite_induct[OF a]) |
|
100 apply (simp add: eqvts) |
|
101 apply (simp) |
|
102 apply clarify |
|
103 apply (subst atom_image_cong[symmetric]) |
|
104 apply (subst atom_eqvt_raw[symmetric]) |
|
105 apply (subst eqvts[symmetric]) |
|
106 apply (rule swap_set_not_in) |
|
107 apply simp_all |
|
108 apply(rule finite_imageI) |
|
109 apply(rule a) |
|
110 apply (subst atom_image_cong[symmetric]) |
|
111 apply (subst atom_eqvt_raw[symmetric]) |
|
112 apply (subst eqvts[symmetric]) |
|
113 apply (rule swap_set_in) |
|
114 apply simp_all |
|
115 done |
|
116 |
|
117 lemma supp_at_insert: |
|
118 "finite (xs :: ('a :: at) set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs" |
|
119 apply (simp add: supp_finite_at_set) |
|
120 apply (simp add: supp_at_base) |
|
121 done |
|
122 |
|
123 lemma supp_atom_finsert: |
74 lemma supp_atom_finsert: |
124 "supp (finsert (x :: atom) S) = supp x \<union> supp S" |
75 "supp (finsert (x :: atom) S) = supp x \<union> supp S" |
125 apply (subst supp_fset_to_set[symmetric]) |
76 apply (subst supp_fset_to_set[symmetric]) |
126 apply (simp add: supp_finite_atom_set) |
77 apply (simp add: supp_finite_atom_set) |
127 apply (simp add: supp_atom_insert[OF fin_fset_to_set]) |
78 apply (simp add: supp_atom_insert[OF fin_fset_to_set]) |
128 apply (simp add: supp_fset_to_set) |
79 apply (simp add: supp_fset_to_set) |
129 done |
80 done |
130 |
81 |
131 lemma supp_at_finsert: |
82 lemma supp_at_finsert: |
132 "supp (finsert (x :: 'a :: at) S) = supp x \<union> supp S" |
83 fixes S::"('a::at) fset" |
|
84 shows "supp (finsert x S) = supp x \<union> supp S" |
133 apply (subst supp_fset_to_set[symmetric]) |
85 apply (subst supp_fset_to_set[symmetric]) |
134 apply (simp add: supp_finite_atom_set) |
86 apply (simp add: supp_finite_atom_set) |
135 apply (simp add: supp_at_insert[OF fin_fset_to_set]) |
87 apply (simp add: supp_at_insert[OF fin_fset_to_set]) |
136 apply (simp add: supp_fset_to_set) |
88 apply (simp add: supp_fset_to_set) |
137 done |
89 done |