src/HOL/Library/FSet.thy
changeset 56525 b5b6ad5dc2ae
parent 56524 f4ba736040fa
child 56646 360a05d60761
equal deleted inserted replaced
56524:f4ba736040fa 56525:b5b6ad5dc2ae
   770 apply (rule ext)+
   770 apply (rule ext)+
   771 apply transfer'
   771 apply transfer'
   772 apply (subst rel_set_def[unfolded fun_eq_iff]) 
   772 apply (subst rel_set_def[unfolded fun_eq_iff]) 
   773 by blast
   773 by blast
   774 
   774 
   775 lemma rel_fset_conversep: "rel_fset (conversep R) = conversep (rel_fset R)"
       
   776   unfolding rel_fset_alt_def by auto
       
   777 
       
   778 lemmas rel_fset_eq [relator_eq] = rel_set_eq[Transfer.transferred]
       
   779 
       
   780 lemma rel_fset_mono[relator_mono]: "A \<le> B \<Longrightarrow> rel_fset A \<le> rel_fset B"
       
   781 unfolding rel_fset_alt_def by blast
       
   782 
       
   783 lemma finite_rel_set:
   775 lemma finite_rel_set:
   784   assumes fin: "finite X" "finite Z"
   776   assumes fin: "finite X" "finite Z"
   785   assumes R_S: "rel_set (R OO S) X Z"
   777   assumes R_S: "rel_set (R OO S) X Z"
   786   shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
   778   shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
   787 proof -
   779 proof -
   803   moreover have "rel_set S ?Y Z"
   795   moreover have "rel_set S ?Y Z"
   804     unfolding rel_set_def
   796     unfolding rel_set_def
   805     using f g by clarsimp blast
   797     using f g by clarsimp blast
   806   ultimately show ?thesis by metis
   798   ultimately show ?thesis by metis
   807 qed
   799 qed
   808 
       
   809 lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
       
   810 apply (rule ext)+
       
   811 by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
       
   812 
       
   813 lemma Domainp_fset[relator_domain]: "Domainp (rel_fset T) = (\<lambda>A. fBall A (Domainp T))"
       
   814 proof -
       
   815   obtain f where f: "\<forall>x\<in>Collect (Domainp T). T x (f x)"
       
   816     unfolding Domainp_iff[abs_def]
       
   817     apply atomize_elim
       
   818     by (subst bchoice_iff[symmetric]) (auto iff: bchoice_iff[symmetric])
       
   819   from f show ?thesis
       
   820     unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
       
   821     apply clarify
       
   822     apply (rule iffI)
       
   823       apply blast
       
   824     by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
       
   825 qed
       
   826 
       
   827 lemma right_total_rel_fset[transfer_rule]: "right_total A \<Longrightarrow> right_total (rel_fset A)"
       
   828 unfolding right_total_def 
       
   829 apply transfer
       
   830 apply (subst(asm) choice_iff)
       
   831 apply clarsimp
       
   832 apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
       
   833 by (auto simp add: rel_set_def)
       
   834 
       
   835 lemma left_total_rel_fset[transfer_rule]: "left_total A \<Longrightarrow> left_total (rel_fset A)"
       
   836 unfolding left_total_def 
       
   837 apply transfer
       
   838 apply (subst(asm) choice_iff)
       
   839 apply clarsimp
       
   840 apply (rename_tac A f y, rule_tac x = "f ` y" in exI)
       
   841 by (auto simp add: rel_set_def)
       
   842 
       
   843 lemmas right_unique_rel_fset[transfer_rule] = right_unique_rel_set[Transfer.transferred]
       
   844 lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
       
   845 
       
   846 thm right_unique_rel_fset left_unique_rel_fset
       
   847 
       
   848 lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
       
   849 by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def)
       
   850 
       
   851 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
       
   852 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def)
       
   853 
       
   854 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
       
   855 
       
   856 
       
   857 subsubsection {* Quotient theorem for the Lifting package *}
       
   858 
       
   859 lemma Quotient_fset_map[quot_map]:
       
   860   assumes "Quotient R Abs Rep T"
       
   861   shows "Quotient (rel_fset R) (fimage Abs) (fimage Rep) (rel_fset T)"
       
   862   using assms unfolding Quotient_alt_def4
       
   863   by (simp add: rel_fset_OO[symmetric] rel_fset_conversep) (simp add: rel_fset_alt_def, blast)
       
   864 
       
   865 
   800 
   866 subsubsection {* Transfer rules for the Transfer package *}
   801 subsubsection {* Transfer rules for the Transfer package *}
   867 
   802 
   868 text {* Unconditional transfer rules *}
   803 text {* Unconditional transfer rules *}
   869 
   804