src/HOL/Lifting_Set.thy
 changeset 53945 4191acef9d0e parent 53927 abe2b313f0e5 child 53952 b2781a3ce958
```--- a/src/HOL/Lifting_Set.thy	Fri Sep 27 09:07:45 2013 +0200
+++ b/src/HOL/Lifting_Set.thy	Fri Sep 27 09:15:40 2013 +0200
@@ -23,7 +23,7 @@
and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"

-lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
+lemma set_rel_conversep [simp]: "set_rel A\<inverse>\<inverse> = (set_rel A)\<inverse>\<inverse>"
unfolding set_rel_def by auto

lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
@@ -71,8 +71,7 @@

lemma right_total_set_rel [transfer_rule]:
"right_total A \<Longrightarrow> right_total (set_rel A)"
-  unfolding right_total_def set_rel_def
-  by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
+using left_total_set_rel[of "A\<inverse>\<inverse>"] by simp

lemma right_unique_set_rel [transfer_rule]:
"right_unique A \<Longrightarrow> right_unique (set_rel A)"
@@ -80,11 +79,7 @@

lemma bi_total_set_rel [transfer_rule]:
"bi_total A \<Longrightarrow> bi_total (set_rel A)"
-  unfolding bi_total_def set_rel_def
-  apply safe
-  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
-  apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
-  done