src/HOL/Quotient.thy
changeset 36123 7f877bbad5b2
parent 36116 a6eab3be095b
child 36215 88ff48884d26
     1.1 --- a/src/HOL/Quotient.thy	Mon Apr 12 19:29:16 2010 -0700
     1.2 +++ b/src/HOL/Quotient.thy	Tue Apr 13 11:40:03 2010 +0200
     1.3 @@ -606,15 +606,14 @@
     1.4  
     1.5  lemma if_prs:
     1.6    assumes q: "Quotient R Abs Rep"
     1.7 -  shows "Abs (If a (Rep b) (Rep c)) = If a b c"
     1.8 -  using Quotient_abs_rep[OF q] by auto
     1.9 +  shows "(id ---> Rep ---> Rep ---> Abs) If = If"
    1.10 +  using Quotient_abs_rep[OF q]
    1.11 +  by (auto simp add: expand_fun_eq)
    1.12  
    1.13 -(* q not used *)
    1.14  lemma if_rsp:
    1.15    assumes q: "Quotient R Abs Rep"
    1.16 -  and     a: "a1 = a2" "R b1 b2" "R c1 c2"
    1.17 -  shows "R (If a1 b1 c1) (If a2 b2 c2)"
    1.18 -  using a by auto
    1.19 +  shows "(op = ===> R ===> R ===> R) If If"
    1.20 +  by auto
    1.21  
    1.22  lemma let_prs:
    1.23    assumes q1: "Quotient R1 Abs1 Rep1"
    1.24 @@ -717,7 +716,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
    1.29 +lemmas [quot_respect] = quot_rel_rsp if_rsp
    1.30 +lemmas [quot_preserve] = if_prs
    1.31  lemmas [quot_equiv] = identity_equivp
    1.32  
    1.33