# HG changeset patch
# User huffman
# Date 1335118590 -7200
# Node ID 49aa3686e566a8c034251dcf75b660dfd072aa2b
# Parent  c04b223d661e4c79c7d76a25b90f2e321bd48080
add transfer rule for set difference

diff -r c04b223d661e -r 49aa3686e566 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Sun Apr 22 19:44:40 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Sun Apr 22 20:16:30 2012 +0200
@@ -129,6 +129,13 @@
   shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
   using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
 
+lemma Diff_transfer [transfer_rule]:
+  assumes "bi_unique A"
+  shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)"
+  using assms unfolding fun_rel_def set_rel_def bi_unique_def
+  unfolding Ball_def Bex_def Diff_eq
+  by (safe, simp, metis, simp, metis)
+
 lemma subset_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"