# HG changeset patch
# User kuncar
# Date 1370438512 -7200
# Node ID 32c433c38ddd3faf1fcd096e1aebd6f20ce23581
# Parent  0f5099b451714ee05121799b69c33564d358a9c5
more reflexivity rules (for OO)

diff -r 0f5099b45171 -r 32c433c38ddd src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Jun 05 13:39:02 2013 +0200
+++ b/src/HOL/Lifting.thy	Wed Jun 05 15:21:52 2013 +0200
@@ -430,6 +430,12 @@
 using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
 by fastforce
 
+lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
+unfolding left_total_def OO_def by fast
+
+lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
+unfolding left_unique_def OO_def by fast
+
 lemma reflp_equality: "reflp (op =)"
 by (auto intro: reflpI)
 
@@ -602,7 +608,8 @@
 
 lemmas [reflexivity_rule] = 
   reflp_equality reflp_Quotient_composition is_equality_Quotient_composition 
-  left_total_fun left_unique_fun left_total_eq left_unique_eq
+  left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition
+  left_unique_composition
 
 text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
   because we don't want to get reflp' variant of these theorems *}