equal
deleted
inserted
replaced
145 apply (simp add: supp_finite_atom_set) |
145 apply (simp add: supp_finite_atom_set) |
146 apply (simp add: supp_at_insert[OF fin_fset_to_set]) |
146 apply (simp add: supp_at_insert[OF fin_fset_to_set]) |
147 apply (simp add: supp_fset_to_set) |
147 apply (simp add: supp_fset_to_set) |
148 done |
148 done |
149 |
149 |
|
150 lemma supp_fempty: |
|
151 "supp {||} = {}" |
|
152 by (simp add: supp_def eqvts) |
|
153 |
150 instance fset :: (at) fs |
154 instance fset :: (at) fs |
151 apply (default) |
155 apply (default) |
152 apply (induct_tac x rule: fset_induct) |
156 apply (induct_tac x rule: fset_induct) |
153 apply (simp add: supp_def eqvts) |
157 apply (simp add: supp_fempty) |
|
158 apply (simp add: supp_at_finsert) |
|
159 apply (simp add: supp_at_base) |
|
160 done |
|
161 |
|
162 lemma supp_at_fset: |
|
163 "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)" |
|
164 apply (induct fset) |
|
165 apply (simp add: supp_fempty) |
154 apply (simp add: supp_at_finsert) |
166 apply (simp add: supp_at_finsert) |
155 apply (simp add: supp_at_base) |
167 apply (simp add: supp_at_base) |
156 done |
168 done |
157 |
169 |
158 end |
170 end |