Quotient Package: some infrastructure for lifting inside sets

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_Set.thy	Tue Aug 23 03:34:17 2011 +0900
@@ -0,0 +1,77 @@
+(*  Title:      HOL/Library/Quotient_Set.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+*)
+
+header {* Quotient infrastructure for the set type *}
+
+theory Quotient_Set
+imports Main Quotient_Syntax
+begin
+
+lemma set_quotient [quot_thm]:
+  assumes "Quotient R Abs Rep"
+  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
+proof (rule QuotientI)
+  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+  then show "\<And>xs. Rep -` (Abs -` xs) = xs"
+    unfolding vimage_def by auto
+next
+  show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
+    unfolding set_rel_def vimage_def
+    by auto (metis Quotient_rel_abs[OF assms])+
+next
+  fix r s
+  show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
+    unfolding set_rel_def vimage_def set_eq_iff
+    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
+qed
+
+lemma empty_set_rsp[quot_respect]:
+  "set_rel R {} {}"
+  unfolding set_rel_def by simp
+
+lemma collect_rsp[quot_respect]:
+  assumes "Quotient R Abs Rep"
+  shows "((R ===> op =) ===> set_rel R) Collect Collect"
+  by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
+
+lemma collect_prs[quot_preserve]:
+  assumes "Quotient R Abs Rep"
+  shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
+  unfolding fun_eq_iff
+  by (simp add: Quotient_abs_rep[OF assms])
+
+lemma union_rsp[quot_respect]:
+  assumes "Quotient R Abs Rep"
+  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
+  by (intro fun_relI) (auto simp add: set_rel_def)
+
+lemma union_prs[quot_preserve]:
+  assumes "Quotient R Abs Rep"
+  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
+  unfolding fun_eq_iff
+  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+
+lemma diff_rsp[quot_respect]:
+  assumes "Quotient R Abs Rep"
+  shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
+  by (intro fun_relI) (auto simp add: set_rel_def)
+
+lemma diff_prs[quot_preserve]:
+  assumes "Quotient R Abs Rep"
+  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
+  unfolding fun_eq_iff
+  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
+
+lemma inter_rsp[quot_respect]:
+  assumes "Quotient R Abs Rep"
+  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
+  by (intro fun_relI) (auto simp add: set_rel_def)
+
+lemma inter_prs[quot_preserve]:
+  assumes "Quotient R Abs Rep"
+  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
+  unfolding fun_eq_iff
+  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+
+end

--- a/src/HOL/Quotient.thy	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Quotient.thy	Tue Aug 23 03:34:17 2011 +0900
@@ -69,6 +69,24 @@
   shows "((op =) ===> (op =)) = (op =)"
   by (auto simp add: fun_eq_iff elim: fun_relE)
 
+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"
+
+lemma vimage_id:
+  "vimage id = id"
+  unfolding vimage_def fun_eq_iff by auto
+
+lemma set_rel_eq:
+  "set_rel op = = op ="
+  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
+
+lemma set_rel_equivp:
+  assumes e: "equivp R"
+  shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
+  unfolding set_rel_def
+  using equivp_reflp[OF e]
+  by auto (metis equivp_symp[OF e])+
 
 subsection {* Quotient Predicate *}
 
@@ -665,6 +683,7 @@
 setup Quotient_Info.setup
 
 declare [[map "fun" = (map_fun, fun_rel)]]
+declare [[map set = (vimage, set_rel)]]
 
 lemmas [quot_thm] = fun_quotient
 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
@@ -680,6 +699,8 @@
   id_o
   o_id
   eq_comp_r
+  set_rel_eq
+  vimage_id
 
 text {* Translation functions for the lifting process. *}
 use "Tools/Quotient/quotient_term.ML"

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Aug 23 03:34:17 2011 +0900
@@ -208,6 +208,13 @@
         in
           list_comb (get_mapfun ctxt "fun", [arg1, arg2])
         end
+(* FIXME: use type_name antiquotation if set type becomes explicit *)
+    | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) =>
+        let
+          val arg = absrep_fun (negF flag) ctxt (ty, ty')
+        in
+          get_mapfun ctxt "Set.set" $ arg
+        end
     | (Type (s, tys), Type (s', tys')) =>
         if s = s'
         then