--- a/src/HOL/Library/Quotient_Set.thy Sat Apr 21 10:59:52 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Sat Apr 21 11:02:01 2012 +0200
@@ -8,7 +8,198 @@
imports Main Quotient_Syntax
begin
-subsection {* set map (vimage) and set relation *}
+subsection {* Relator for set type *}
+
+definition set_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
+ where "set_rel R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
+
+lemma set_relI:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
+ assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
+ shows "set_rel R A B"
+ using assms unfolding set_rel_def by simp
+
+lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
+ unfolding set_rel_def by auto
+
+lemma set_rel_OO: "set_rel (R OO S) = set_rel R OO set_rel S"
+ apply (intro ext, rename_tac X Z)
+ apply (rule iffI)
+ apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
+ apply (simp add: set_rel_def, fast)
+ apply (simp add: set_rel_def, fast)
+ apply (simp add: set_rel_def, fast)
+ done
+
+lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
+ unfolding set_rel_def fun_eq_iff by auto
+
+lemma reflp_set_rel: "reflp R \<Longrightarrow> reflp (set_rel R)"
+ unfolding reflp_def set_rel_def by fast
+
+lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
+ unfolding symp_def set_rel_def by fast
+
+lemma transp_set_rel: "transp R \<Longrightarrow> transp (set_rel R)"
+ unfolding transp_def set_rel_def by fast
+
+lemma equivp_set_rel: "equivp R \<Longrightarrow> equivp (set_rel R)"
+ by (blast intro: equivpI reflp_set_rel symp_set_rel transp_set_rel
+ elim: equivpE)
+
+lemma right_total_set_rel [transfer_rule]:
+ "right_total A \<Longrightarrow> right_total (set_rel A)"
+ unfolding right_total_def set_rel_def
+ by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
+
+lemma right_unique_set_rel [transfer_rule]:
+ "right_unique A \<Longrightarrow> right_unique (set_rel A)"
+ unfolding right_unique_def set_rel_def by fast
+
+lemma bi_total_set_rel [transfer_rule]:
+ "bi_total A \<Longrightarrow> bi_total (set_rel A)"
+ unfolding bi_total_def set_rel_def
+ apply safe
+ apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
+ apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
+ done
+
+lemma bi_unique_set_rel [transfer_rule]:
+ "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
+ unfolding bi_unique_def set_rel_def by fast
+
+subsection {* Transfer rules for transfer package *}
+
+subsubsection {* Unconditional transfer rules *}
+
+lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}"
+ unfolding set_rel_def by simp
+
+lemma insert_transfer [transfer_rule]:
+ "(A ===> set_rel A ===> set_rel A) insert insert"
+ unfolding fun_rel_def set_rel_def by auto
+
+lemma union_transfer [transfer_rule]:
+ "(set_rel A ===> set_rel A ===> set_rel A) union union"
+ unfolding fun_rel_def set_rel_def by auto
+
+lemma Union_transfer [transfer_rule]:
+ "(set_rel (set_rel A) ===> set_rel A) Union Union"
+ unfolding fun_rel_def set_rel_def by simp fast
+
+lemma image_transfer [transfer_rule]:
+ "((A ===> B) ===> set_rel A ===> set_rel B) image image"
+ unfolding fun_rel_def set_rel_def by simp fast
+
+lemma Ball_transfer [transfer_rule]:
+ "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
+ unfolding set_rel_def fun_rel_def by fast
+
+lemma Bex_transfer [transfer_rule]:
+ "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex"
+ unfolding set_rel_def fun_rel_def by fast
+
+lemma Pow_transfer [transfer_rule]:
+ "(set_rel A ===> set_rel (set_rel A)) Pow Pow"
+ apply (rule fun_relI, rename_tac X Y, rule set_relI)
+ apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
+ apply (simp add: set_rel_def, fast)
+ apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
+ apply (simp add: set_rel_def, fast)
+ done
+
+subsubsection {* Rules requiring bi-unique or bi-total relations *}
+
+lemma member_transfer [transfer_rule]:
+ assumes "bi_unique A"
+ shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
+ using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
+
+lemma Collect_transfer [transfer_rule]:
+ assumes "bi_total A"
+ shows "((A ===> op =) ===> set_rel A) Collect Collect"
+ using assms unfolding fun_rel_def set_rel_def bi_total_def by fast
+
+lemma inter_transfer [transfer_rule]:
+ assumes "bi_unique A"
+ 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 subset_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
+ unfolding subset_eq [abs_def] by transfer_prover
+
+lemma UNIV_transfer [transfer_rule]:
+ assumes "bi_total A"
+ shows "(set_rel A) UNIV UNIV"
+ using assms unfolding set_rel_def bi_total_def by simp
+
+lemma Compl_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
+ shows "(set_rel A ===> set_rel A) uminus uminus"
+ unfolding Compl_eq [abs_def] by transfer_prover
+
+lemma Inter_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
+ shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
+ unfolding Inter_eq [abs_def] by transfer_prover
+
+lemma finite_transfer [transfer_rule]:
+ assumes "bi_unique A"
+ shows "(set_rel A ===> op =) finite finite"
+ apply (rule fun_relI, rename_tac X Y)
+ apply (rule iffI)
+ apply (subgoal_tac "Y \<subseteq> (\<lambda>x. THE y. A x y) ` X")
+ apply (erule finite_subset, erule finite_imageI)
+ apply (rule subsetI, rename_tac y)
+ apply (clarsimp simp add: set_rel_def)
+ apply (drule (1) bspec, clarify)
+ apply (rule image_eqI)
+ apply (rule the_equality [symmetric])
+ apply assumption
+ apply (simp add: assms [unfolded bi_unique_def])
+ apply assumption
+ apply (subgoal_tac "X \<subseteq> (\<lambda>y. THE x. A x y) ` Y")
+ apply (erule finite_subset, erule finite_imageI)
+ apply (rule subsetI, rename_tac x)
+ apply (clarsimp simp add: set_rel_def)
+ apply (drule (1) bspec, clarify)
+ apply (rule image_eqI)
+ apply (rule the_equality [symmetric])
+ apply assumption
+ apply (simp add: assms [unfolded bi_unique_def])
+ apply assumption
+ done
+
+subsection {* Setup for lifting package *}
+
+lemma Quotient_alt_def3:
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
+ (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
+ unfolding Quotient_alt_def2 by (safe, metis+)
+
+lemma Quotient_alt_def4:
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
+ unfolding Quotient_alt_def3 fun_eq_iff by auto
+
+lemma Quotient_set:
+ assumes "Quotient R Abs Rep T"
+ shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
+ using assms unfolding Quotient_alt_def4
+ apply (simp add: set_rel_OO set_rel_conversep)
+ apply (simp add: set_rel_def, fast)
+ done
+
+declare [[map set = (set_rel, Quotient_set)]]
+
+lemma set_invariant_commute [invariant_commute]:
+ "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
+ unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast
+
+subsection {* Contravariant set map (vimage) and set relator *}
definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"