Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2_FSet.thy
changeset 1571 1d70813ae674
parent 1568 2311a9fc4624
child 1675 d24f59f78a86 
--- a/Nominal/Nominal2_FSet.thy	Mon Mar 22 10:20:57 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Mon Mar 22 10:21:14 2010 +0100
@@ -147,10 +147,22 @@
   apply (simp add: supp_fset_to_set)
   done
 
+lemma supp_fempty:
+  "supp {||} = {}"
+  by (simp add: supp_def eqvts)
+
 instance fset :: (at) fs
   apply (default)
   apply (induct_tac x rule: fset_induct)
-  apply (simp add: supp_def eqvts)
+  apply (simp add: supp_fempty)
+  apply (simp add: supp_at_finsert)
+  apply (simp add: supp_at_base)
+  done
+
+lemma supp_at_fset:
+  "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)"
+  apply (induct fset)
+  apply (simp add: supp_fempty)
   apply (simp add: supp_at_finsert)
   apply (simp add: supp_at_base)
   done
nominal2