added covariant relator set_rel, with transfer rules for set operations
authorhuffman
Sat Apr 21 11:02:01 2012 +0200 (2012-04-21)
changeset 476486b9d20a095ae
parent 47647 ec29cc09599d
child 47649 df687f0797fb
added covariant relator set_rel, with transfer rules for set operations
src/HOL/Library/Quotient_Set.thy
     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