src/HOL/Lifting_Set.thy
changeset 53945 4191acef9d0e
parent 53927 abe2b313f0e5
child 53952 b2781a3ce958
     1.1 --- a/src/HOL/Lifting_Set.thy	Fri Sep 27 09:07:45 2013 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Fri Sep 27 09:15:40 2013 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
     1.5  by(simp_all add: set_rel_def)
     1.6  
     1.7 -lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
     1.8 +lemma set_rel_conversep [simp]: "set_rel A\<inverse>\<inverse> = (set_rel A)\<inverse>\<inverse>"
     1.9    unfolding set_rel_def by auto
    1.10  
    1.11  lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
    1.12 @@ -71,8 +71,7 @@
    1.13  
    1.14  lemma right_total_set_rel [transfer_rule]:
    1.15    "right_total A \<Longrightarrow> right_total (set_rel A)"
    1.16 -  unfolding right_total_def set_rel_def
    1.17 -  by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
    1.18 +using left_total_set_rel[of "A\<inverse>\<inverse>"] by simp
    1.19  
    1.20  lemma right_unique_set_rel [transfer_rule]:
    1.21    "right_unique A \<Longrightarrow> right_unique (set_rel A)"
    1.22 @@ -80,11 +79,7 @@
    1.23  
    1.24  lemma bi_total_set_rel [transfer_rule]:
    1.25    "bi_total A \<Longrightarrow> bi_total (set_rel A)"
    1.26 -  unfolding bi_total_def set_rel_def
    1.27 -  apply safe
    1.28 -  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    1.29 -  apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
    1.30 -  done
    1.31 +by(simp add: bi_total_conv_left_right left_total_set_rel right_total_set_rel)
    1.32  
    1.33  lemma bi_unique_set_rel [transfer_rule]:
    1.34    "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
    1.35 @@ -100,7 +95,7 @@
    1.36    assumes "Quotient R Abs Rep T"
    1.37    shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
    1.38    using assms unfolding Quotient_alt_def4
    1.39 -  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
    1.40 +  apply (simp add: set_rel_OO[symmetric])
    1.41    apply (simp add: set_rel_def, fast)
    1.42    done
    1.43