--- a/src/HOL/Transfer.thy Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Transfer.thy Tue Aug 13 15:59:22 2013 +0200
@@ -12,10 +12,20 @@
subsection {* Relator for function space *}
definition
- 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)
+ fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
where
"fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+locale lifting_syntax
+begin
+ notation fun_rel (infixr "===>" 55)
+ notation map_fun (infixr "--->" 55)
+end
+
+context
+begin
+interpretation lifting_syntax .
+
lemma fun_relI [intro]:
assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
shows "(A ===> B) f g"
@@ -112,6 +122,8 @@
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
using assms unfolding Rel_def fun_rel_def by fast
+end
+
ML_file "Tools/transfer.ML"
setup Transfer.setup
@@ -121,6 +133,10 @@
hide_const (open) Rel
+context
+begin
+interpretation lifting_syntax .
+
text {* Handling of domains *}
lemma Domaimp_refl[transfer_domain_rule]:
@@ -358,3 +374,5 @@
unfolding transfer_forall_def by (rule All_transfer)
end
+
+end