# HG changeset patch
# User huffman
# Date 1334756912 -7200
# Node ID e455cdaac4790b0315db8fd761cc11ac7f500f20
# Parent  1f0ec5b8135a21911a63aa8e959151234b2ff589
move constant 'Respects' into Lifting.thy;
add quantifier transfer rules for quotients

diff -r 1f0ec5b8135a -r e455cdaac479 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Apr 18 15:09:07 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed Apr 18 15:48:32 2012 +0200
@@ -201,6 +201,14 @@
   "equivp R \<Longrightarrow> reflp R"
   by (erule equivpE)
 
+subsection {* Respects predicate *}
+
+definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
+  where "Respects R = {x. R x x}"
+
+lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
+  unfolding Respects_def by simp
+
 subsection {* Invariant *}
 
 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
@@ -300,6 +308,22 @@
   assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
   using 1 assms unfolding Quotient_def by metis
 
+lemma Quotient_All_transfer:
+  "((T ===> op =) ===> op =) (Ball (Respects R)) All"
+  unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
+  by (auto, metis Quotient_abs_induct)
+
+lemma Quotient_Ex_transfer:
+  "((T ===> op =) ===> op =) (Bex (Respects R)) Ex"
+  unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
+  by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1])
+
+lemma Quotient_forall_transfer:
+  "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall"
+  using Quotient_All_transfer
+  unfolding transfer_forall_def transfer_bforall_def
+    Ball_def [abs_def] in_respects .
+
 end
 
 text {* Generating transfer rules for total quotients. *}
diff -r 1f0ec5b8135a -r e455cdaac479 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Wed Apr 18 15:09:07 2012 +0200
+++ b/src/HOL/Quotient.thy	Wed Apr 18 15:48:32 2012 +0200
@@ -34,17 +34,6 @@
   shows "((op =) OOO R) = R"
   by (auto simp add: fun_eq_iff)
 
-subsection {* Respects predicate *}
-
-definition
-  Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
-where
-  "Respects R = {x. R x x}"
-
-lemma in_respects:
-  shows "x \<in> Respects R \<longleftrightarrow> R x x"
-  unfolding Respects_def by simp
-
 subsection {* set map (vimage) and set relation *}
 
 definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"