src/HOL/Library/Quotient_Option.thy
changeset 45802 b16f976db515
parent 41372 551eb49a6e91
child 47094 1a7ad2601cb5
equal deleted inserted replaced
45801:5616fbda86e6 45802:b16f976db515
    14   "option_rel R None None = True"
    14   "option_rel R None None = True"
    15 | "option_rel R (Some x) None = False"
    15 | "option_rel R (Some x) None = False"
    16 | "option_rel R None (Some x) = False"
    16 | "option_rel R None (Some x) = False"
    17 | "option_rel R (Some x) (Some y) = R x y"
    17 | "option_rel R (Some x) (Some y) = R x y"
    18 
    18 
    19 declare [[map option = (Option.map, option_rel)]]
    19 declare [[map option = option_rel]]
    20 
    20 
    21 lemma option_rel_unfold:
    21 lemma option_rel_unfold:
    22   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    22   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    23     | (Some x, Some y) \<Rightarrow> R x y
    23     | (Some x, Some y) \<Rightarrow> R x y
    24     | _ \<Rightarrow> False)"
    24     | _ \<Rightarrow> False)"