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.
tuned eqvt-proofs about prod_rel and prod_fv
authorChristian Urban <urbanc@in.tum.de>
Thu, 13 May 2010 15:12:34 +0100
changeset 2124 a17b25cb94a6
parent 2123 2f39ce2aba6c
child 2125 60ee289a8c63
tuned eqvt-proofs about prod_rel and prod_fv
Nominal/Abs.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Abs.thy	Thu May 13 15:12:05 2010 +0100
+++ b/Nominal/Abs.thy	Thu May 13 15:12:34 2010 +0100
@@ -843,11 +843,15 @@
 lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
   by auto
 
-lemma [eqvt]: "(p \<bullet> prod_rel A B x y) = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
-  by (simp, perm_simp) (rule refl)
+lemma [eqvt]: 
+  shows "p \<bullet> prod_rel A B x y = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  unfolding prod_rel.simps
+  by (perm_simp) (rule refl)
 
-lemma [eqvt]: "(p \<bullet> prod_fv A B (x, y)) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
-  by (simp, perm_simp) (rule refl)
+lemma [eqvt]: 
+  shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+  unfolding prod_fv.simps
+  by (perm_simp) (rule refl)
 
 end
nominal2