src/HOL/Library/Quotient_Option.thy
changeset 56525 b5b6ad5dc2ae
parent 55564 e81ee43ab290
child 58881 b9556a055632
equal deleted inserted replaced
56524:f4ba736040fa 56525:b5b6ad5dc2ae
    18   "rel_option R x (map_option f y) \<longleftrightarrow> rel_option (\<lambda>x y. R x (f y)) x y"
    18   "rel_option R x (map_option f y) \<longleftrightarrow> rel_option (\<lambda>x y. R x (f y)) x y"
    19   by (simp add: rel_option_iff split: option.split)
    19   by (simp add: rel_option_iff split: option.split)
    20 
    20 
    21 declare
    21 declare
    22   map_option.id [id_simps]
    22   map_option.id [id_simps]
    23   rel_option_eq [id_simps]
    23   option.rel_eq [id_simps]
    24 
    24 
    25 lemma reflp_rel_option:
    25 lemma reflp_rel_option:
    26   "reflp R \<Longrightarrow> reflp (rel_option R)"
    26   "reflp R \<Longrightarrow> reflp (rel_option R)"
    27   unfolding reflp_def split_option_all by simp
    27   unfolding reflp_def split_option_all by simp
    28 
    28 
    42 
    42 
    43 lemma option_quotient [quot_thm]:
    43 lemma option_quotient [quot_thm]:
    44   assumes "Quotient3 R Abs Rep"
    44   assumes "Quotient3 R Abs Rep"
    45   shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
    45   shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
    46   apply (rule Quotient3I)
    46   apply (rule Quotient3I)
    47   apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] rel_option_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    47   apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option.rel_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    48   using Quotient3_rel [OF assms]
    48   using Quotient3_rel [OF assms]
    49   apply (simp add: rel_option_iff split: option.split)
    49   apply (simp add: rel_option_iff split: option.split)
    50   done
    50   done
    51 
    51 
    52 declare [[mapQ3 option = (rel_option, option_quotient)]]
    52 declare [[mapQ3 option = (rel_option, option_quotient)]]