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
```