diff -r 50c8f7f21327 -r 4191acef9d0e src/HOL/Lifting_Set.thy --- 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: "\ set_rel R A B; y \ B \ \ \x \ A. R x y" by(simp_all add: set_rel_def) -lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)" +lemma set_rel_conversep [simp]: "set_rel A\\ = (set_rel A)\\" 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 \ right_total (set_rel A)" - unfolding right_total_def set_rel_def - by (rule allI, rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) +using left_total_set_rel[of "A\\"] by simp lemma right_unique_set_rel [transfer_rule]: "right_unique A \ right_unique (set_rel A)" @@ -80,11 +79,7 @@ lemma bi_total_set_rel [transfer_rule]: "bi_total A \ bi_total (set_rel A)" - unfolding bi_total_def set_rel_def - apply safe - apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) - apply (rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) - done +by(simp add: bi_total_conv_left_right left_total_set_rel right_total_set_rel) lemma bi_unique_set_rel [transfer_rule]: "bi_unique A \ bi_unique (set_rel A)" @@ -100,7 +95,7 @@ assumes "Quotient R Abs Rep T" shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" using assms unfolding Quotient_alt_def4 - apply (simp add: set_rel_OO[symmetric] set_rel_conversep) + apply (simp add: set_rel_OO[symmetric]) apply (simp add: set_rel_def, fast) done