src/HOL/Transfer.thy
changeset 47660 7a5c681c0265
parent 47658 7631f6f7873d
child 47684 ead185e60b8c
     1.1 --- a/src/HOL/Transfer.thy	Sat Apr 21 21:38:08 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Sun Apr 22 11:05:04 2012 +0200
     1.3 @@ -153,6 +153,25 @@
     1.4    "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
     1.5    unfolding bi_unique_def fun_rel_def by auto
     1.6  
     1.7 +text {* Properties are preserved by relation composition. *}
     1.8 +
     1.9 +lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
    1.10 +  by auto
    1.11 +
    1.12 +lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
    1.13 +  unfolding bi_total_def OO_def by metis
    1.14 +
    1.15 +lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
    1.16 +  unfolding bi_unique_def OO_def by metis
    1.17 +
    1.18 +lemma right_total_OO:
    1.19 +  "\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
    1.20 +  unfolding right_total_def OO_def by metis
    1.21 +
    1.22 +lemma right_unique_OO:
    1.23 +  "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
    1.24 +  unfolding right_unique_def OO_def by metis
    1.25 +
    1.26  
    1.27  subsection {* Properties of relators *}
    1.28