src/HOL/Transfer.thy
 changeset 55084 8ee9aabb2bca parent 53952 b2781a3ce958 child 55415 05f5fdb8d093
```     1.1 --- a/src/HOL/Transfer.thy	Mon Jan 20 20:21:12 2014 +0100
1.2 +++ b/src/HOL/Transfer.thy	Mon Jan 20 20:42:43 2014 +0100
1.3 @@ -6,16 +6,11 @@
1.4  header {* Generic theorem transfer using relations *}
1.5
1.6  theory Transfer
1.7 -imports Hilbert_Choice
1.8 +imports Hilbert_Choice Basic_BNFs
1.9  begin
1.10
1.11  subsection {* Relator for function space *}
1.12
1.13 -definition
1.14 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
1.15 -where
1.16 -  "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
1.17 -
1.18  locale lifting_syntax
1.19  begin
1.20    notation fun_rel (infixr "===>" 55)
1.21 @@ -26,32 +21,20 @@
1.22  begin
1.23  interpretation lifting_syntax .
1.24
1.25 -lemma fun_relI [intro]:
1.26 -  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
1.27 -  shows "(A ===> B) f g"
1.28 -  using assms by (simp add: fun_rel_def)
1.29 -
1.30 -lemma fun_relD:
1.31 -  assumes "(A ===> B) f g" and "A x y"
1.32 -  shows "B (f x) (g y)"
1.33 -  using assms by (simp add: fun_rel_def)
1.34 -
1.35  lemma fun_relD2:
1.36 -  assumes "(A ===> B) f g" and "A x x"
1.37 +  assumes "fun_rel A B f g" and "A x x"
1.38    shows "B (f x) (g x)"
1.39 -  using assms unfolding fun_rel_def by auto
1.40 +  using assms by (rule fun_relD)
1.41
1.42  lemma fun_relE:
1.43 -  assumes "(A ===> B) f g" and "A x y"
1.44 +  assumes "fun_rel A B f g" and "A x y"
1.45    obtains "B (f x) (g y)"
1.46    using assms by (simp add: fun_rel_def)
1.47
1.48 -lemma fun_rel_eq:
1.49 -  shows "((op =) ===> (op =)) = (op =)"
1.50 -  by (auto simp add: fun_eq_iff elim: fun_relE)
1.51 +lemmas fun_rel_eq = fun.rel_eq
1.52
1.53  lemma fun_rel_eq_rel:
1.54 -  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
1.55 +shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"