src/HOL/Lifting.thy
changeset 52307 32c433c38ddd
parent 52036 1aa2e40df9ff
child 53011 aeee0a4be6cf
     1.1 --- a/src/HOL/Lifting.thy	Wed Jun 05 13:39:02 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Jun 05 15:21:52 2013 +0200
     1.3 @@ -430,6 +430,12 @@
     1.4  using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
     1.5  by fastforce
     1.6  
     1.7 +lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
     1.8 +unfolding left_total_def OO_def by fast
     1.9 +
    1.10 +lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
    1.11 +unfolding left_unique_def OO_def by fast
    1.12 +
    1.13  lemma reflp_equality: "reflp (op =)"
    1.14  by (auto intro: reflpI)
    1.15  
    1.16 @@ -602,7 +608,8 @@
    1.17  
    1.18  lemmas [reflexivity_rule] = 
    1.19    reflp_equality reflp_Quotient_composition is_equality_Quotient_composition 
    1.20 -  left_total_fun left_unique_fun left_total_eq left_unique_eq
    1.21 +  left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition
    1.22 +  left_unique_composition
    1.23  
    1.24  text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
    1.25    because we don't want to get reflp' variant of these theorems *}