src/HOL/Library/Quotient_Option.thy
changeset 41372 551eb49a6e91
parent 40820 fd9c98ead9a9
child 45802 b16f976db515
equal deleted inserted replaced
41371:35d2241c169c 41372:551eb49a6e91
    58 
    58 
    59 lemma option_quotient [quot_thm]:
    59 lemma option_quotient [quot_thm]:
    60   assumes "Quotient R Abs Rep"
    60   assumes "Quotient R Abs Rep"
    61   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
    61   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
    62   apply (rule QuotientI)
    62   apply (rule QuotientI)
    63   apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
    63   apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
    64   using Quotient_rel [OF assms]
    64   using Quotient_rel [OF assms]
    65   apply (simp add: option_rel_unfold split: option.split)
    65   apply (simp add: option_rel_unfold split: option.split)
    66   done
    66   done
    67 
    67 
    68 lemma option_None_rsp [quot_respect]:
    68 lemma option_None_rsp [quot_respect]: