diff -r 8e38ff09864a -r 7da251a6c16e src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Mar 08 13:21:45 2013 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Mar 08 13:21:52 2013 +0100
@@ -46,6 +46,15 @@
 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
   by (metis option.exhaust) (* TODO: move to Option.thy *)
 
+lemma option_rel_mono[relator_mono]:
+  assumes "A \<le> B"
+  shows "(option_rel A) \<le> (option_rel B)"
+using assms by (auto simp: option_rel_unfold split: option.splits)
+
+lemma option_rel_OO[relator_distr]:
+  "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
+by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
+
 lemma option_reflp[reflexivity_rule]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp