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_Abs.thy
changeset 2591 35c570891a3a
parent 2584 1eac050a36f4
child 2592 98236fbd8aa6 
--- a/Nominal/Nominal2_Abs.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -523,6 +523,14 @@
   unfolding supp_Abs
   by auto
 
+lemma Abs_fresh_star_iff:
+  fixes x::"'a::fs"
+  shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x"
+  unfolding fresh_star_def
+  by (auto simp add: Abs_fresh_iff)
+
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
   shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"
nominal2