src/HOL/Library/Quotient_Option.thy
changeset 47982 7aa35601ff65
parent 47936 756f30eac792
child 51377 7da251a6c16e
equal deleted inserted replaced
47977:455a9f89c47d 47982:7aa35601ff65
    44   by (metis option.exhaust) (* TODO: move to Option.thy *)
    44   by (metis option.exhaust) (* TODO: move to Option.thy *)
    45 
    45 
    46 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    46 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    47   by (metis option.exhaust) (* TODO: move to Option.thy *)
    47   by (metis option.exhaust) (* TODO: move to Option.thy *)
    48 
    48 
    49 lemma option_reflp[reflp_preserve]:
    49 lemma option_reflp[reflexivity_rule]:
    50   "reflp R \<Longrightarrow> reflp (option_rel R)"
    50   "reflp R \<Longrightarrow> reflp (option_rel R)"
    51   unfolding reflp_def split_option_all by simp
    51   unfolding reflp_def split_option_all by simp
       
    52 
       
    53 lemma option_left_total[reflexivity_rule]:
       
    54   "left_total R \<Longrightarrow> left_total (option_rel R)"
       
    55   apply (intro left_totalI)
       
    56   unfolding split_option_ex
       
    57   by (case_tac x) (auto elim: left_totalE)
    52 
    58 
    53 lemma option_symp:
    59 lemma option_symp:
    54   "symp R \<Longrightarrow> symp (option_rel R)"
    60   "symp R \<Longrightarrow> symp (option_rel R)"
    55   unfolding symp_def split_option_all option_rel.simps by fast
    61   unfolding symp_def split_option_all option_rel.simps by fast
    56 
    62