src/HOL/Transfer.thy
changeset 47523 1bf0e92c1ca0
parent 47503 cb44d09d9d22
child 47612 bc9c7b5c26fd
     1.1 --- a/src/HOL/Transfer.thy	Tue Apr 17 20:48:07 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Tue Apr 17 14:00:09 2012 +0200
     1.3 @@ -84,22 +84,22 @@
     1.4  lemma Rel_eq_refl: "Rel (op =) x x"
     1.5    unfolding Rel_def ..
     1.6  
     1.7 +lemma Rel_App:
     1.8 +  assumes "Rel (A ===> B) f g" and "Rel A x y"
     1.9 +  shows "Rel B (App f x) (App g y)"
    1.10 +  using assms unfolding Rel_def App_def fun_rel_def by fast
    1.11 +
    1.12 +lemma Rel_Abs:
    1.13 +  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
    1.14 +  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
    1.15 +  using assms unfolding Rel_def Abs_def fun_rel_def by fast
    1.16 +
    1.17  use "Tools/transfer.ML"
    1.18  
    1.19  setup Transfer.setup
    1.20  
    1.21  declare fun_rel_eq [relator_eq]
    1.22  
    1.23 -lemma Rel_App [transfer_raw]:
    1.24 -  assumes "Rel (A ===> B) f g" and "Rel A x y"
    1.25 -  shows "Rel B (App f x) (App g y)"
    1.26 -  using assms unfolding Rel_def App_def fun_rel_def by fast
    1.27 -
    1.28 -lemma Rel_Abs [transfer_raw]:
    1.29 -  assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
    1.30 -  shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
    1.31 -  using assms unfolding Rel_def Abs_def fun_rel_def by fast
    1.32 -
    1.33  hide_const (open) App Abs Rel
    1.34  
    1.35