equal
deleted
inserted
replaced
60 lemma option_None_prs[quot_preserve]: |
60 lemma option_None_prs[quot_preserve]: |
61 assumes q: "Quotient R Abs Rep" |
61 assumes q: "Quotient R Abs Rep" |
62 shows "Option.map Abs None = None" |
62 shows "Option.map Abs None = None" |
63 by simp |
63 by simp |
64 |
64 |
65 lemma option_Some_prs[quot_respect]: |
65 lemma option_Some_prs[quot_preserve]: |
66 assumes q: "Quotient R Abs Rep" |
66 assumes q: "Quotient R Abs Rep" |
67 shows "(Rep ---> Option.map Abs) Some = Some" |
67 shows "(Rep ---> Option.map Abs) Some = Some" |
68 apply(simp add: expand_fun_eq) |
68 apply(simp add: expand_fun_eq) |
69 apply(simp add: Quotient_abs_rep[OF q]) |
69 apply(simp add: Quotient_abs_rep[OF q]) |
70 done |
70 done |