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))"
    1.56    by (simp add: fun_rel_def)
    1.57  
    1.58