Quotient Package: add mem_rsp, mem_prs, tune proofs.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed Aug 24 10:59:22 2011 +0900 (2011-08-24)
changeset 44459079ccfb074d9
parent 44458 f8c2def19f84
child 44460 5d0754cf994a
Quotient Package: add mem_rsp, mem_prs, tune proofs.
src/HOL/Library/Quotient_Set.thy
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Tue Aug 23 15:46:53 2011 -0700
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Wed Aug 24 10:59:22 2011 +0900
     1.3 @@ -33,7 +33,7 @@
     1.4  lemma collect_rsp[quot_respect]:
     1.5    assumes "Quotient R Abs Rep"
     1.6    shows "((R ===> op =) ===> set_rel R) Collect Collect"
     1.7 -  by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
     1.8 +  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
     1.9  
    1.10  lemma collect_prs[quot_preserve]:
    1.11    assumes "Quotient R Abs Rep"
    1.12 @@ -44,7 +44,7 @@
    1.13  lemma union_rsp[quot_respect]:
    1.14    assumes "Quotient R Abs Rep"
    1.15    shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
    1.16 -  by (intro fun_relI) (auto simp add: set_rel_def)
    1.17 +  by (intro fun_relI) (simp add: set_rel_def)
    1.18  
    1.19  lemma union_prs[quot_preserve]:
    1.20    assumes "Quotient R Abs Rep"
    1.21 @@ -55,7 +55,7 @@
    1.22  lemma diff_rsp[quot_respect]:
    1.23    assumes "Quotient R Abs Rep"
    1.24    shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
    1.25 -  by (intro fun_relI) (auto simp add: set_rel_def)
    1.26 +  by (intro fun_relI) (simp add: set_rel_def)
    1.27  
    1.28  lemma diff_prs[quot_preserve]:
    1.29    assumes "Quotient R Abs Rep"
    1.30 @@ -74,4 +74,13 @@
    1.31    unfolding fun_eq_iff
    1.32    by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    1.33  
    1.34 +lemma mem_prs[quot_preserve]:
    1.35 +  assumes "Quotient R Abs Rep"
    1.36 +  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    1.37 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
    1.38 +
    1.39 +lemma mem_rsp[quot_respect]:
    1.40 +  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
    1.41 +  by (intro fun_relI) (simp add: set_rel_def)
    1.42 +
    1.43  end