78 apply (simp add: supp_atom_insert[OF fin_fset_to_set]) |
78 apply (simp add: supp_atom_insert[OF fin_fset_to_set]) |
79 apply (simp add: supp_fset_to_set) |
79 apply (simp add: supp_fset_to_set) |
80 done |
80 done |
81 |
81 |
82 lemma supp_at_finsert: |
82 lemma supp_at_finsert: |
83 fixes S::"('a::at) fset" |
83 fixes a::"'a::at_base" |
84 shows "supp (finsert x S) = supp x \<union> supp S" |
84 shows "supp (finsert a S) = supp a \<union> supp S" |
85 apply (subst supp_fset_to_set[symmetric]) |
85 apply (subst supp_fset_to_set[symmetric]) |
86 apply (simp add: supp_finite_atom_set) |
86 apply (simp add: supp_finite_atom_set) |
87 apply (simp add: supp_at_insert[OF fin_fset_to_set]) |
87 apply (simp add: supp_at_base_insert[OF fin_fset_to_set]) |
88 apply (simp add: supp_fset_to_set) |
88 apply (simp add: supp_fset_to_set) |
89 done |
89 done |
90 |
90 |
91 lemma supp_fempty: |
91 lemma supp_fempty: |
92 "supp {||} = {}" |
92 "supp {||} = {}" |
93 by (simp add: supp_def eqvts) |
93 by (simp add: supp_def eqvts) |
94 |
94 |
95 instance fset :: (at) fs |
95 instance fset :: (at_base) fs |
96 apply (default) |
96 apply (default) |
97 apply (induct_tac x rule: fset_induct) |
97 apply (induct_tac x rule: fset_induct) |
98 apply (simp add: supp_fempty) |
98 apply (simp add: supp_fempty) |
99 apply (simp add: supp_at_finsert) |
99 apply (simp add: supp_at_finsert) |
100 apply (simp add: supp_at_base) |
100 apply (simp add: supp_at_base) |
101 done |
101 done |
102 |
102 |
103 lemma supp_at_fset: |
103 lemma supp_at_fset: |
104 "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)" |
104 fixes S::"('a::at_base) fset" |
105 apply (induct fset) |
105 shows "supp S = fset_to_set (fmap atom S)" |
|
106 apply (induct S) |
106 apply (simp add: supp_fempty) |
107 apply (simp add: supp_fempty) |
107 apply (simp add: supp_at_finsert) |
108 apply (simp add: supp_at_finsert) |
108 apply (simp add: supp_at_base) |
109 apply (simp add: supp_at_base) |
109 done |
110 done |
110 |
111 |