# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273145137 -7200
# Node ID 79b733010bc5dc03d4cf30ae06830d3415e5c928
# Parent  ace7775cbd04d357ae08b37f3f0280db70098fc8
prod_fv and its respectfullness and preservation.

diff -r ace7775cbd04 -r 79b733010bc5 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu May 06 10:43:41 2010 +0200
+++ b/Nominal/Abs.thy	Thu May 06 13:25:37 2010 +0200
@@ -825,6 +825,20 @@
   apply (simp)
   done
 
+fun
+  prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+where
+  "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
+
+lemma [quot_respect]:
+  "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  by auto
+
+lemma [quot_preserve]:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  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])
 
 end