diff -r 0a689157e3ce -r 8ee9aabb2bca src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Mon Jan 20 20:21:12 2014 +0100 +++ b/src/HOL/Transfer.thy Mon Jan 20 20:42:43 2014 +0100 @@ -6,16 +6,11 @@ header {* Generic theorem transfer using relations *} theory Transfer -imports Hilbert_Choice +imports Hilbert_Choice Basic_BNFs begin subsection {* Relator for function space *} -definition - fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" -where - "fun_rel A B = (\f g. \x y. A x y \ B (f x) (g y))" - locale lifting_syntax begin notation fun_rel (infixr "===>" 55) @@ -26,32 +21,20 @@ begin interpretation lifting_syntax . -lemma fun_relI [intro]: - assumes "\x y. A x y \ B (f x) (g y)" - shows "(A ===> B) f g" - using assms by (simp add: fun_rel_def) - -lemma fun_relD: - assumes "(A ===> B) f g" and "A x y" - shows "B (f x) (g y)" - using assms by (simp add: fun_rel_def) - lemma fun_relD2: - assumes "(A ===> B) f g" and "A x x" + assumes "fun_rel A B f g" and "A x x" shows "B (f x) (g x)" - using assms unfolding fun_rel_def by auto + using assms by (rule fun_relD) lemma fun_relE: - assumes "(A ===> B) f g" and "A x y" + assumes "fun_rel A B f g" and "A x y" obtains "B (f x) (g y)" using assms by (simp add: fun_rel_def) -lemma fun_rel_eq: - shows "((op =) ===> (op =)) = (op =)" - by (auto simp add: fun_eq_iff elim: fun_relE) +lemmas fun_rel_eq = fun.rel_eq lemma fun_rel_eq_rel: - shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" +shows "fun_rel (op =) R = (\f g. \x. R (f x) (g x))" by (simp add: fun_rel_def)