author huffman Sat Apr 21 11:02:01 2012 +0200 (2012-04-21) changeset 47648 6b9d20a095ae parent 47647 ec29cc09599d child 47649 df687f0797fb
added covariant relator set_rel, with transfer rules for set operations
```     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 10:59:52 2012 +0200
1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 11:02:01 2012 +0200
1.3 @@ -8,7 +8,198 @@
1.4  imports Main Quotient_Syntax
1.5  begin
1.6
1.7 -subsection {* set map (vimage) and set relation *}
1.8 +subsection {* Relator for set type *}
1.9 +
1.10 +definition set_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
1.11 +  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))"
1.12 +
1.13 +lemma set_relI:
1.14 +  assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
1.15 +  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
1.16 +  shows "set_rel R A B"
1.17 +  using assms unfolding set_rel_def by simp
1.18 +
1.19 +lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
1.20 +  unfolding set_rel_def by auto
1.21 +
1.22 +lemma set_rel_OO: "set_rel (R OO S) = set_rel R OO set_rel S"
1.23 +  apply (intro ext, rename_tac X Z)
1.24 +  apply (rule iffI)
1.25 +  apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
1.26 +  apply (simp add: set_rel_def, fast)
1.27 +  apply (simp add: set_rel_def, fast)
1.28 +  apply (simp add: set_rel_def, fast)
1.29 +  done
1.30 +
1.31 +lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
1.32 +  unfolding set_rel_def fun_eq_iff by auto
1.33 +
1.34 +lemma reflp_set_rel: "reflp R \<Longrightarrow> reflp (set_rel R)"
1.35 +  unfolding reflp_def set_rel_def by fast
1.36 +
1.37 +lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
1.38 +  unfolding symp_def set_rel_def by fast
1.39 +
1.40 +lemma transp_set_rel: "transp R \<Longrightarrow> transp (set_rel R)"
1.41 +  unfolding transp_def set_rel_def by fast
1.42 +
1.43 +lemma equivp_set_rel: "equivp R \<Longrightarrow> equivp (set_rel R)"
1.44 +  by (blast intro: equivpI reflp_set_rel symp_set_rel transp_set_rel
1.45 +    elim: equivpE)
1.46 +
1.47 +lemma right_total_set_rel [transfer_rule]:
1.48 +  "right_total A \<Longrightarrow> right_total (set_rel A)"
1.49 +  unfolding right_total_def set_rel_def
1.50 +  by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
1.51 +
1.52 +lemma right_unique_set_rel [transfer_rule]:
1.53 +  "right_unique A \<Longrightarrow> right_unique (set_rel A)"
1.54 +  unfolding right_unique_def set_rel_def by fast
1.55 +
1.56 +lemma bi_total_set_rel [transfer_rule]:
1.57 +  "bi_total A \<Longrightarrow> bi_total (set_rel A)"
1.58 +  unfolding bi_total_def set_rel_def
1.59 +  apply safe
1.60 +  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
1.61 +  apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
1.62 +  done
1.63 +
1.64 +lemma bi_unique_set_rel [transfer_rule]:
1.65 +  "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
1.66 +  unfolding bi_unique_def set_rel_def by fast
1.67 +
1.68 +subsection {* Transfer rules for transfer package *}
1.69 +
1.70 +subsubsection {* Unconditional transfer rules *}
1.71 +
1.72 +lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}"
1.73 +  unfolding set_rel_def by simp
1.74 +
1.75 +lemma insert_transfer [transfer_rule]:
1.76 +  "(A ===> set_rel A ===> set_rel A) insert insert"
1.77 +  unfolding fun_rel_def set_rel_def by auto
1.78 +
1.79 +lemma union_transfer [transfer_rule]:
1.80 +  "(set_rel A ===> set_rel A ===> set_rel A) union union"
1.81 +  unfolding fun_rel_def set_rel_def by auto
1.82 +
1.83 +lemma Union_transfer [transfer_rule]:
1.84 +  "(set_rel (set_rel A) ===> set_rel A) Union Union"
1.85 +  unfolding fun_rel_def set_rel_def by simp fast
1.86 +
1.87 +lemma image_transfer [transfer_rule]:
1.88 +  "((A ===> B) ===> set_rel A ===> set_rel B) image image"
1.89 +  unfolding fun_rel_def set_rel_def by simp fast
1.90 +
1.91 +lemma Ball_transfer [transfer_rule]:
1.92 +  "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
1.93 +  unfolding set_rel_def fun_rel_def by fast
1.94 +
1.95 +lemma Bex_transfer [transfer_rule]:
1.96 +  "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex"
1.97 +  unfolding set_rel_def fun_rel_def by fast
1.98 +
1.99 +lemma Pow_transfer [transfer_rule]:
1.100 +  "(set_rel A ===> set_rel (set_rel A)) Pow Pow"
1.101 +  apply (rule fun_relI, rename_tac X Y, rule set_relI)
1.102 +  apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
1.103 +  apply (simp add: set_rel_def, fast)
1.104 +  apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
1.105 +  apply (simp add: set_rel_def, fast)
1.106 +  done
1.107 +
1.108 +subsubsection {* Rules requiring bi-unique or bi-total relations *}
1.109 +
1.110 +lemma member_transfer [transfer_rule]:
1.111 +  assumes "bi_unique A"
1.112 +  shows "(A ===> set_rel A ===> op =) (op \<in>) (op \<in>)"
1.113 +  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
1.114 +
1.115 +lemma Collect_transfer [transfer_rule]:
1.116 +  assumes "bi_total A"
1.117 +  shows "((A ===> op =) ===> set_rel A) Collect Collect"
1.118 +  using assms unfolding fun_rel_def set_rel_def bi_total_def by fast
1.119 +
1.120 +lemma inter_transfer [transfer_rule]:
1.121 +  assumes "bi_unique A"
1.122 +  shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter"
1.123 +  using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast
1.124 +
1.125 +lemma subset_transfer [transfer_rule]:
1.126 +  assumes [transfer_rule]: "bi_unique A"
1.127 +  shows "(set_rel A ===> set_rel A ===> op =) (op \<subseteq>) (op \<subseteq>)"
1.128 +  unfolding subset_eq [abs_def] by transfer_prover
1.129 +
1.130 +lemma UNIV_transfer [transfer_rule]:
1.131 +  assumes "bi_total A"
1.132 +  shows "(set_rel A) UNIV UNIV"
1.133 +  using assms unfolding set_rel_def bi_total_def by simp
1.134 +
1.135 +lemma Compl_transfer [transfer_rule]:
1.136 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
1.137 +  shows "(set_rel A ===> set_rel A) uminus uminus"
1.138 +  unfolding Compl_eq [abs_def] by transfer_prover
1.139 +
1.140 +lemma Inter_transfer [transfer_rule]:
1.141 +  assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
1.142 +  shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter"
1.143 +  unfolding Inter_eq [abs_def] by transfer_prover
1.144 +
1.145 +lemma finite_transfer [transfer_rule]:
1.146 +  assumes "bi_unique A"
1.147 +  shows "(set_rel A ===> op =) finite finite"
1.148 +  apply (rule fun_relI, rename_tac X Y)
1.149 +  apply (rule iffI)
1.150 +  apply (subgoal_tac "Y \<subseteq> (\<lambda>x. THE y. A x y) ` X")
1.151 +  apply (erule finite_subset, erule finite_imageI)
1.152 +  apply (rule subsetI, rename_tac y)
1.153 +  apply (clarsimp simp add: set_rel_def)
1.154 +  apply (drule (1) bspec, clarify)
1.155 +  apply (rule image_eqI)
1.156 +  apply (rule the_equality [symmetric])
1.157 +  apply assumption
1.158 +  apply (simp add: assms [unfolded bi_unique_def])
1.159 +  apply assumption
1.160 +  apply (subgoal_tac "X \<subseteq> (\<lambda>y. THE x. A x y) ` Y")
1.161 +  apply (erule finite_subset, erule finite_imageI)
1.162 +  apply (rule subsetI, rename_tac x)
1.163 +  apply (clarsimp simp add: set_rel_def)
1.164 +  apply (drule (1) bspec, clarify)
1.165 +  apply (rule image_eqI)
1.166 +  apply (rule the_equality [symmetric])
1.167 +  apply assumption
1.168 +  apply (simp add: assms [unfolded bi_unique_def])
1.169 +  apply assumption
1.170 +  done
1.171 +
1.172 +subsection {* Setup for lifting package *}
1.173 +
1.174 +lemma Quotient_alt_def3:
1.175 +  "Quotient R Abs Rep T \<longleftrightarrow>
1.176 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
1.177 +    (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
1.178 +  unfolding Quotient_alt_def2 by (safe, metis+)
1.179 +
1.180 +lemma Quotient_alt_def4:
1.181 +  "Quotient R Abs Rep T \<longleftrightarrow>
1.182 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
1.183 +  unfolding Quotient_alt_def3 fun_eq_iff by auto
1.184 +
1.185 +lemma Quotient_set:
1.186 +  assumes "Quotient R Abs Rep T"
1.187 +  shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
1.188 +  using assms unfolding Quotient_alt_def4
1.189 +  apply (simp add: set_rel_OO set_rel_conversep)
1.190 +  apply (simp add: set_rel_def, fast)
1.191 +  done
1.192 +
1.193 +declare [[map set = (set_rel, Quotient_set)]]
1.194 +
1.195 +lemma set_invariant_commute [invariant_commute]:
1.196 +  "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
1.197 +  unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast
1.198 +
1.199 +subsection {* Contravariant set map (vimage) and set relator *}
1.200
1.201  definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
1.202
```