respectfullness and preservation of function composition
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue Apr 20 14:56:20 2010 +0200 (2010-04-20)
changeset 3621588ff48884d26
parent 36214 ff2580df7ccc
child 36216 8fb6cc6f3b94
respectfullness and preservation of function composition
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Tue Apr 20 14:55:53 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Tue Apr 20 14:56:20 2010 +0200
     1.3 @@ -585,19 +585,15 @@
     1.4    assumes q1: "Quotient R1 Abs1 Rep1"
     1.5    and     q2: "Quotient R2 Abs2 Rep2"
     1.6    and     q3: "Quotient R3 Abs3 Rep3"
     1.7 -  shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
     1.8 +  shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
     1.9 +  and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
    1.10    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
    1.11 -  unfolding o_def expand_fun_eq by simp
    1.12 +  unfolding o_def expand_fun_eq by simp_all
    1.13  
    1.14  lemma o_rsp:
    1.15 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.16 -  and     q2: "Quotient R2 Abs2 Rep2"
    1.17 -  and     q3: "Quotient R3 Abs3 Rep3"
    1.18 -  and     a1: "(R2 ===> R3) f1 f2"
    1.19 -  and     a2: "(R1 ===> R2) g1 g2"
    1.20 -  shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
    1.21 -  using a1 a2 unfolding o_def expand_fun_eq
    1.22 -  by (auto)
    1.23 +  "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
    1.24 +  "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
    1.25 +  unfolding fun_rel_def o_def expand_fun_eq by auto
    1.26  
    1.27  lemma cond_prs:
    1.28    assumes a: "Quotient R absf repf"
    1.29 @@ -716,8 +712,8 @@
    1.30  declare [[map "fun" = (fun_map, fun_rel)]]
    1.31  
    1.32  lemmas [quot_thm] = fun_quotient
    1.33 -lemmas [quot_respect] = quot_rel_rsp if_rsp
    1.34 -lemmas [quot_preserve] = if_prs
    1.35 +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp
    1.36 +lemmas [quot_preserve] = if_prs o_prs
    1.37  lemmas [quot_equiv] = identity_equivp
    1.38  
    1.39