--- a/src/HOL/BNF_Def.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Def.thy Thu Sep 25 16:35:53 2014 +0200
@@ -19,6 +19,14 @@
by auto
definition
+ rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+where
+ "rel_sum R1 R2 x y =
+ (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+ | (Inr x, Inr y) \<Rightarrow> R2 x y
+ | _ \<Rightarrow> False)"
+
+definition
rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
where
"rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"