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
```