src/HOL/Library/FSet.thy
changeset 56524 f4ba736040fa
parent 56520 3373f5d1e074
child 56525 b5b6ad5dc2ae
equal deleted inserted replaced
56523:2ae16e3d8b6d 56524:f4ba736040fa
   844 lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
   844 lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred]
   845 
   845 
   846 thm right_unique_rel_fset left_unique_rel_fset
   846 thm right_unique_rel_fset left_unique_rel_fset
   847 
   847 
   848 lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)"
   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_iff)
   849 by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def)
   850 
   850 
   851 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
   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_iff)
   852 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def)
   853 
   853 
   854 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
   854 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
   855 
   855 
   856 
   856 
   857 subsubsection {* Quotient theorem for the Lifting package *}
   857 subsubsection {* Quotient theorem for the Lifting package *}