# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273499089 -7200
# Node ID c0ab7451b20dd1f697a439680aaf1d509be0189c
# Parent  6cb1a463952172535d75a291f4eef185750f0290
prod_rel and prod_fv eqvt and mono

diff -r 6cb1a4639521 -r c0ab7451b20d Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu May 06 14:14:30 2010 +0200
+++ b/Nominal/Abs.thy	Mon May 10 15:44:49 2010 +0200
@@ -840,5 +840,14 @@
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
+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]: "(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)
+
 end