Quotient Package: added respectfulness and preservation lemmas for mem.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon Aug 30 15:44:33 2010 +0900 (2010-08-30)
changeset 3886127c7b620758c
parent 38860 749d09f52fde
child 38862 2795499a20bd
Quotient Package: added respectfulness and preservation lemmas for mem.
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Sat Aug 28 21:17:25 2010 +0800
     1.2 +++ b/src/HOL/Quotient.thy	Mon Aug 30 15:44:33 2010 +0900
     1.3 @@ -651,6 +651,16 @@
     1.4    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
     1.5    by auto
     1.6  
     1.7 +lemma mem_rsp:
     1.8 +  shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
     1.9 +  by (simp add: mem_def)
    1.10 +
    1.11 +lemma mem_prs:
    1.12 +  assumes a1: "Quotient R1 Abs1 Rep1"
    1.13 +  and     a2: "Quotient R2 Abs2 Rep2"
    1.14 +  shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
    1.15 +  by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
    1.16 +
    1.17  locale quot_type =
    1.18    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.19    and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
    1.20 @@ -721,8 +731,8 @@
    1.21  declare [[map "fun" = (fun_map, fun_rel)]]
    1.22  
    1.23  lemmas [quot_thm] = fun_quotient
    1.24 -lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp
    1.25 -lemmas [quot_preserve] = if_prs o_prs let_prs
    1.26 +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp
    1.27 +lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs
    1.28  lemmas [quot_equiv] = identity_equivp
    1.29  
    1.30