Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added eqvt-lemma for Image
authorChristian Urban <urbanc@in.tum.de>
Sat, 26 Nov 2011 09:24:19 +0000
changeset 3050 7519ebb41145
parent 3049 83744806b660
child 3051 a06de111c70e
added eqvt-lemma for Image
Nominal/Nominal2_Base.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Nominal2_Base.thy	Thu Nov 10 01:15:19 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Nov 26 09:24:19 2011 +0000
@@ -906,6 +906,11 @@
   unfolding image_def
   by (perm_simp) (rule refl)
 
+lemma Image_eqvt [eqvt]:
+  shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)"
+  unfolding Image_def
+  by (perm_simp) (rule refl)
+
 lemma UNIV_eqvt [eqvt]:
   shows "p \<bullet> UNIV = UNIV"
   unfolding UNIV_def
nominal2