Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add transfer rule for set difference
authorhuffman
Sun, 22 Apr 2012 20:16:30 +0200
changeset 47680 49aa3686e566
parent 47678 c04b223d661e
child 47681 d9a1b706d569
add transfer rule for set difference
src/HOL/Library/Quotient_Set.thy file | annotate | diff | comparison | revisions 
--- 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>)"
isabelle