src/HOL/Transfer.thy
changeset 53011 aeee0a4be6cf
parent 52358 f4c4bcb0d564
child 53927 abe2b313f0e5
     1.1 --- a/src/HOL/Transfer.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -12,10 +12,20 @@
     1.4  subsection {* Relator for function space *}
     1.5  
     1.6  definition
     1.7 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
     1.8 +  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
     1.9  where
    1.10    "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    1.11  
    1.12 +locale lifting_syntax
    1.13 +begin
    1.14 +  notation fun_rel (infixr "===>" 55)
    1.15 +  notation map_fun (infixr "--->" 55)
    1.16 +end
    1.17 +
    1.18 +context
    1.19 +begin
    1.20 +interpretation lifting_syntax .
    1.21 +
    1.22  lemma fun_relI [intro]:
    1.23    assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    1.24    shows "(A ===> B) f g"
    1.25 @@ -112,6 +122,8 @@
    1.26    shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
    1.27    using assms unfolding Rel_def fun_rel_def by fast
    1.28  
    1.29 +end
    1.30 +
    1.31  ML_file "Tools/transfer.ML"
    1.32  setup Transfer.setup
    1.33  
    1.34 @@ -121,6 +133,10 @@
    1.35  
    1.36  hide_const (open) Rel
    1.37  
    1.38 +context
    1.39 +begin
    1.40 +interpretation lifting_syntax .
    1.41 +
    1.42  text {* Handling of domains *}
    1.43  
    1.44  lemma Domaimp_refl[transfer_domain_rule]:
    1.45 @@ -358,3 +374,5 @@
    1.46    unfolding transfer_forall_def by (rule All_transfer)
    1.47  
    1.48  end
    1.49 +
    1.50 +end