src/HOL/Library/Quotient_Option.thy
 changeset 40464 e1db06cf6254 parent 39302 d7728f65b353 child 40542 9a173a22771c
equal 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`