1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Tue Aug 23 03:34:17 2011 +0900
     1.3 @@ -0,0 +1,77 @@
     1.4 +(*  Title:      HOL/Library/Quotient_Set.thy
     1.5 +    Author:     Cezary Kaliszyk and Christian Urban
     1.6 +*)
     1.7 +
     1.8 +header {* Quotient infrastructure for the set type *}
     1.9 +
    1.10 +theory Quotient_Set
    1.11 +imports Main Quotient_Syntax
    1.12 +begin
    1.13 +
    1.14 +lemma set_quotient [quot_thm]:
    1.15 +  assumes "Quotient R Abs Rep"
    1.16 +  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
    1.17 +proof (rule QuotientI)
    1.18 +  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
    1.19 +  then show "\<And>xs. Rep -` (Abs -` xs) = xs"
    1.20 +    unfolding vimage_def by auto
    1.21 +next
    1.22 +  show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
    1.23 +    unfolding set_rel_def vimage_def
    1.24 +    by auto (metis Quotient_rel_abs[OF assms])+
    1.25 +next
    1.26 +  fix r s
    1.27 +  show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
    1.28 +    unfolding set_rel_def vimage_def set_eq_iff
    1.29 +    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
    1.30 +qed
    1.31 +
    1.32 +lemma empty_set_rsp[quot_respect]:
    1.33 +  "set_rel R {} {}"
    1.34 +  unfolding set_rel_def by simp
    1.35 +
    1.36 +lemma collect_rsp[quot_respect]:
    1.37 +  assumes "Quotient R Abs Rep"
    1.38 +  shows "((R ===> op =) ===> set_rel R) Collect Collect"
    1.39 +  by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
    1.40 +
    1.41 +lemma collect_prs[quot_preserve]:
    1.42 +  assumes "Quotient R Abs Rep"
    1.43 +  shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
    1.44 +  unfolding fun_eq_iff
    1.45 +  by (simp add: Quotient_abs_rep[OF assms])
    1.46 +
    1.47 +lemma union_rsp[quot_respect]:
    1.48 +  assumes "Quotient R Abs Rep"
    1.49 +  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
    1.50 +  by (intro fun_relI) (auto simp add: set_rel_def)
    1.51 +
    1.52 +lemma union_prs[quot_preserve]:
    1.53 +  assumes "Quotient R Abs Rep"
    1.54 +  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
    1.55 +  unfolding fun_eq_iff
    1.56 +  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    1.57 +
    1.58 +lemma diff_rsp[quot_respect]:
    1.59 +  assumes "Quotient R Abs Rep"
    1.60 +  shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
    1.61 +  by (intro fun_relI) (auto simp add: set_rel_def)
    1.62 +
    1.63 +lemma diff_prs[quot_preserve]:
    1.64 +  assumes "Quotient R Abs Rep"
    1.65 +  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
    1.66 +  unfolding fun_eq_iff
    1.67 +  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    1.68 +
    1.69 +lemma inter_rsp[quot_respect]:
    1.70 +  assumes "Quotient R Abs Rep"
    1.71 +  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
    1.72 +  by (intro fun_relI) (auto simp add: set_rel_def)
    1.73 +
    1.74 +lemma inter_prs[quot_preserve]:
    1.75 +  assumes "Quotient R Abs Rep"
    1.76 +  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
    1.77 +  unfolding fun_eq_iff
    1.78 +  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    1.79 +
    1.80 +end

     2.1 --- a/src/HOL/Quotient.thy	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Tue Aug 23 03:34:17 2011 +0900
     2.3 @@ -69,6 +69,24 @@
     2.4    shows "((op =) ===> (op =)) = (op =)"
     2.5    by (auto simp add: fun_eq_iff elim: fun_relE)
     2.6  
     2.7 +subsection {* set map (vimage) and set relation *}
     2.8 +
     2.9 +definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
    2.10 +
    2.11 +lemma vimage_id:
    2.12 +  "vimage id = id"
    2.13 +  unfolding vimage_def fun_eq_iff by auto
    2.14 +
    2.15 +lemma set_rel_eq:
    2.16 +  "set_rel op = = op ="
    2.17 +  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
    2.18 +
    2.19 +lemma set_rel_equivp:
    2.20 +  assumes e: "equivp R"
    2.21 +  shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    2.22 +  unfolding set_rel_def
    2.23 +  using equivp_reflp[OF e]
    2.24 +  by auto (metis equivp_symp[OF e])+
    2.25  
    2.26  subsection {* Quotient Predicate *}
    2.27  
    2.28 @@ -665,6 +683,7 @@
    2.29  setup Quotient_Info.setup
    2.30  
    2.31  declare [[map "fun" = (map_fun, fun_rel)]]
    2.32 +declare [[map set = (vimage, set_rel)]]
    2.33  
    2.34  lemmas [quot_thm] = fun_quotient
    2.35  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
    2.36 @@ -680,6 +699,8 @@
    2.37    id_o
    2.38    o_id
    2.39    eq_comp_r
    2.40 +  set_rel_eq
    2.41 +  vimage_id
    2.42  
    2.43  text {* Translation functions for the lifting process. *}
    2.44  use "Tools/Quotient/quotient_term.ML"

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