src/HOL/Quotient.thy
changeset 37049 ca1c293e521e
parent 36276 92011cc923f5
child 37493 2377d246a631
     1.1 --- a/src/HOL/Quotient.thy	Thu May 20 21:19:38 2010 -0700
     1.2 +++ b/src/HOL/Quotient.thy	Fri May 21 10:40:59 2010 +0200
     1.3 @@ -618,15 +618,13 @@
     1.4  lemma let_prs:
     1.5    assumes q1: "Quotient R1 Abs1 Rep1"
     1.6    and     q2: "Quotient R2 Abs2 Rep2"
     1.7 -  shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
     1.8 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
     1.9 +  shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
    1.10 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
    1.11 +  by (auto simp add: expand_fun_eq)
    1.12  
    1.13  lemma let_rsp:
    1.14 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.15 -  and     a1: "(R1 ===> R2) f g"
    1.16 -  and     a2: "R1 x y"
    1.17 -  shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
    1.18 -  using apply_rsp[OF q1 a1] a2 by auto
    1.19 +  shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
    1.20 +  by auto
    1.21  
    1.22  locale quot_type =
    1.23    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.24 @@ -716,8 +714,8 @@
    1.25  declare [[map "fun" = (fun_map, fun_rel)]]
    1.26  
    1.27  lemmas [quot_thm] = fun_quotient
    1.28 -lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp
    1.29 -lemmas [quot_preserve] = if_prs o_prs
    1.30 +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp
    1.31 +lemmas [quot_preserve] = if_prs o_prs let_prs
    1.32  lemmas [quot_equiv] = identity_equivp
    1.33  
    1.34