src/HOL/Library/Quotient_Option.thy
changeset 40464 e1db06cf6254
parent 39302 d7728f65b353
child 40542 9a173a22771c
equal deleted inserted replaced
40463:75e544159549 40464:e1db06cf6254
     7 theory Quotient_Option
     7 theory Quotient_Option
     8 imports Main Quotient_Syntax
     8 imports Main Quotient_Syntax
     9 begin
     9 begin
    10 
    10 
    11 fun
    11 fun
    12   option_rel
    12   option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
    13 where
    13 where
    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"
    54   by simp
    54   by simp
    55 
    55 
    56 lemma option_Some_rsp[quot_respect]:
    56 lemma option_Some_rsp[quot_respect]:
    57   assumes q: "Quotient R Abs Rep"
    57   assumes q: "Quotient R Abs Rep"
    58   shows "(R ===> option_rel R) Some Some"
    58   shows "(R ===> option_rel R) Some Some"
    59   by simp
    59   by auto
    60 
    60 
    61 lemma option_None_prs[quot_preserve]:
    61 lemma option_None_prs[quot_preserve]:
    62   assumes q: "Quotient R Abs Rep"
    62   assumes q: "Quotient R Abs Rep"
    63   shows "Option.map Abs None = None"
    63   shows "Option.map Abs None = None"
    64   by simp
    64   by simp