src/HOL/BNF_Util.thy
changeset 55084 8ee9aabb2bca
parent 55066 4e5ddf3162ac
child 55803 74d3fe9031d8
     1.1 --- a/src/HOL/BNF_Util.thy	Mon Jan 20 20:21:12 2014 +0100
     1.2 +++ b/src/HOL/BNF_Util.thy	Mon Jan 20 20:42:43 2014 +0100
     1.3 @@ -10,9 +10,23 @@
     1.4  
     1.5  theory BNF_Util
     1.6  imports BNF_Cardinal_Arithmetic
     1.7 -  Transfer (*FIXME: define fun_rel here, reuse in Transfer once this theory is in HOL*)
     1.8  begin
     1.9  
    1.10 +definition
    1.11 +  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    1.12 +where
    1.13 +  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    1.14 +
    1.15 +lemma fun_relI [intro]:
    1.16 +  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    1.17 +  shows "fun_rel A B f g"
    1.18 +  using assms by (simp add: fun_rel_def)
    1.19 +
    1.20 +lemma fun_relD:
    1.21 +  assumes "fun_rel A B f g" and "A x y"
    1.22 +  shows "B (f x) (g y)"
    1.23 +  using assms by (simp add: fun_rel_def)
    1.24 +
    1.25  definition collect where
    1.26  "collect F x = (\<Union>f \<in> F. f x)"
    1.27