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
```