diff -r 455a9f89c47d -r 7aa35601ff65 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Thu May 24 13:56:21 2012 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Thu May 24 14:20:23 2012 +0200 @@ -46,10 +46,16 @@ lemma split_option_ex: "(\x. P x) \ P None \ (\x. P (Some x))" by (metis option.exhaust) (* TODO: move to Option.thy *) -lemma option_reflp[reflp_preserve]: +lemma option_reflp[reflexivity_rule]: "reflp R \ reflp (option_rel R)" unfolding reflp_def split_option_all by simp +lemma option_left_total[reflexivity_rule]: + "left_total R \ left_total (option_rel R)" + apply (intro left_totalI) + unfolding split_option_ex + by (case_tac x) (auto elim: left_totalE) + lemma option_symp: "symp R \ symp (option_rel R)" unfolding symp_def split_option_all option_rel.simps by fast