src/HOL/Lifting.thy
 changeset 47325 ec6187036495 parent 47308 9caab698dbe4 child 47351 0193e663a19e child 47435 e1b761c216ac
--- a/src/HOL/Lifting.thy	Tue Apr 03 22:04:50 2012 +0200
+++ b/src/HOL/Lifting.thy	Tue Apr 03 22:31:00 2012 +0200
@@ -6,7 +6,7 @@

theory Lifting
-imports Plain Equiv_Relations
+imports Plain Equiv_Relations Transfer
keywords
"print_quotmaps" "print_quotients" :: diag and
"lift_definition" :: thy_goal and
@@ -18,7 +18,7 @@
("Tools/Lifting/lifting_setup.ML")
begin

-subsection {* Function map and function relation *}
+subsection {* Function map *}

notation map_fun (infixr "--->" 55)

@@ -26,29 +26,6 @@
"(id ---> id) = id"

-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)
-where
-  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
-
-lemma fun_relI [intro]:
-  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  shows "(R1 ===> R2) f g"
-  using assms by (simp add: fun_rel_def)
-
-lemma fun_relE:
-  assumes "(R1 ===> R2) f g" and "R1 x y"
-  obtains "R2 (f x) (g y)"
-  using assms by (simp add: fun_rel_def)
-
-lemma fun_rel_eq:
-  shows "((op =) ===> (op =)) = (op =)"
-  by (auto simp add: fun_eq_iff elim: fun_relE)
-
-lemma fun_rel_eq_rel:
-  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"