src/HOL/Lifting_Set.thy
 changeset 53945 4191acef9d0e parent 53927 abe2b313f0e5 child 53952 b2781a3ce958
equal inserted replaced
53944:50c8f7f21327 53945:4191acef9d0e
`    21 `
`    21 `
`    22 lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"`
`    22 lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"`
`    23   and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"`
`    23   and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"`
`    24 by(simp_all add: set_rel_def)`
`    24 by(simp_all add: set_rel_def)`
`    25 `
`    25 `
`    26 lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"`
`    26 lemma set_rel_conversep [simp]: "set_rel A\<inverse>\<inverse> = (set_rel A)\<inverse>\<inverse>"`
`    27   unfolding set_rel_def by auto`
`    27   unfolding set_rel_def by auto`
`    28 `
`    28 `
`    29 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"`
`    29 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"`
`    30   unfolding set_rel_def fun_eq_iff by auto`
`    30   unfolding set_rel_def fun_eq_iff by auto`
`    31 `
`    31 `
`    69   unfolding left_unique_def set_rel_def`
`    69   unfolding left_unique_def set_rel_def`
`    70   by fast`
`    70   by fast`
`    71 `
`    71 `
`    72 lemma right_total_set_rel [transfer_rule]:`
`    72 lemma right_total_set_rel [transfer_rule]:`
`    73   "right_total A \<Longrightarrow> right_total (set_rel A)"`
`    73   "right_total A \<Longrightarrow> right_total (set_rel A)"`
`    74   unfolding right_total_def set_rel_def`
`    74 using left_total_set_rel[of "A\<inverse>\<inverse>"] by simp`
`    75   by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)`
`       `
`    76 `
`    75 `
`    77 lemma right_unique_set_rel [transfer_rule]:`
`    76 lemma right_unique_set_rel [transfer_rule]:`
`    78   "right_unique A \<Longrightarrow> right_unique (set_rel A)"`
`    77   "right_unique A \<Longrightarrow> right_unique (set_rel A)"`
`    79   unfolding right_unique_def set_rel_def by fast`
`    78   unfolding right_unique_def set_rel_def by fast`
`    80 `
`    79 `
`    81 lemma bi_total_set_rel [transfer_rule]:`
`    80 lemma bi_total_set_rel [transfer_rule]:`
`    82   "bi_total A \<Longrightarrow> bi_total (set_rel A)"`
`    81   "bi_total A \<Longrightarrow> bi_total (set_rel A)"`
`    83   unfolding bi_total_def set_rel_def`
`    82 by(simp add: bi_total_conv_left_right left_total_set_rel right_total_set_rel)`
`    84   apply safe`
`       `
`    85   apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)`
`       `
`    86   apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)`
`       `
`    87   done`
`       `
`    88 `
`    83 `
`    89 lemma bi_unique_set_rel [transfer_rule]:`
`    84 lemma bi_unique_set_rel [transfer_rule]:`
`    90   "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"`
`    85   "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"`
`    91   unfolding bi_unique_def set_rel_def by fast`
`    86   unfolding bi_unique_def set_rel_def by fast`
`    92 `
`    87 `
`    98 `
`    93 `
`    99 lemma Quotient_set[quot_map]:`
`    94 lemma Quotient_set[quot_map]:`
`   100   assumes "Quotient R Abs Rep T"`
`    95   assumes "Quotient R Abs Rep T"`
`   101   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"`
`    96   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"`
`   102   using assms unfolding Quotient_alt_def4`
`    97   using assms unfolding Quotient_alt_def4`
`   103   apply (simp add: set_rel_OO[symmetric] set_rel_conversep)`
`    98   apply (simp add: set_rel_OO[symmetric])`
`   104   apply (simp add: set_rel_def, fast)`
`    99   apply (simp add: set_rel_def, fast)`
`   105   done`
`   100   done`
`   106 `
`   101 `
`   107 subsection {* Transfer rules for the Transfer package *}`
`   102 subsection {* Transfer rules for the Transfer package *}`
`   108 `
`   103 `