# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271151603 -7200
# Node ID 7f877bbad5b2474949e5bc70f48c8c636425e859
# Parent  dd6e69cdcc1ed1745cfcdcd0abf288bae508d272
add If respectfullness and preservation to Quotient package database

diff -r dd6e69cdcc1e -r 7f877bbad5b2 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Mon Apr 12 19:29:16 2010 -0700
+++ b/src/HOL/Quotient.thy	Tue Apr 13 11:40:03 2010 +0200
@@ -606,15 +606,14 @@
 
 lemma if_prs:
   assumes q: "Quotient R Abs Rep"
-  shows "Abs (If a (Rep b) (Rep c)) = If a b c"
-  using Quotient_abs_rep[OF q] by auto
+  shows "(id ---> Rep ---> Rep ---> Abs) If = If"
+  using Quotient_abs_rep[OF q]
+  by (auto simp add: expand_fun_eq)
 
-(* q not used *)
 lemma if_rsp:
   assumes q: "Quotient R Abs Rep"
-  and     a: "a1 = a2" "R b1 b2" "R c1 c2"
-  shows "R (If a1 b1 c1) (If a2 b2 c2)"
-  using a by auto
+  shows "(op = ===> R ===> R ===> R) If If"
+  by auto
 
 lemma let_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -717,7 +716,8 @@
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp
+lemmas [quot_respect] = quot_rel_rsp if_rsp
+lemmas [quot_preserve] = if_prs
 lemmas [quot_equiv] = identity_equivp