src/HOL/Library/Quotient_Option.thy
author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 60500 903bb1495239
child 62954 c5d0fdc260fa
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 (*  Title:      HOL/Library/Quotient_Option.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 section \<open>Quotient infrastructure for the option type\<close>
     6 
     7 theory Quotient_Option
     8 imports Main Quotient_Syntax
     9 begin
    10 
    11 subsection \<open>Rules for the Quotient package\<close>
    12 
    13 lemma rel_option_map1:
    14   "rel_option R (map_option f x) y \<longleftrightarrow> rel_option (\<lambda>x. R (f x)) x y"
    15   by (simp add: rel_option_iff split: option.split)
    16 
    17 lemma rel_option_map2:
    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)
    20 
    21 declare
    22   map_option.id [id_simps]
    23   option.rel_eq [id_simps]
    24 
    25 lemma reflp_rel_option:
    26   "reflp R \<Longrightarrow> reflp (rel_option R)"
    27   unfolding reflp_def split_option_all by simp
    28 
    29 lemma option_symp:
    30   "symp R \<Longrightarrow> symp (rel_option R)"
    31   unfolding symp_def split_option_all
    32   by (simp only: option.rel_inject option.rel_distinct) fast
    33 
    34 lemma option_transp:
    35   "transp R \<Longrightarrow> transp (rel_option R)"
    36   unfolding transp_def split_option_all
    37   by (simp only: option.rel_inject option.rel_distinct) fast
    38 
    39 lemma option_equivp [quot_equiv]:
    40   "equivp R \<Longrightarrow> equivp (rel_option R)"
    41   by (blast intro: equivpI reflp_rel_option option_symp option_transp elim: equivpE)
    42 
    43 lemma option_quotient [quot_thm]:
    44   assumes "Quotient3 R Abs Rep"
    45   shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
    46   apply (rule Quotient3I)
    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]
    49   apply (simp add: rel_option_iff split: option.split)
    50   done
    51 
    52 declare [[mapQ3 option = (rel_option, option_quotient)]]
    53 
    54 lemma option_None_rsp [quot_respect]:
    55   assumes q: "Quotient3 R Abs Rep"
    56   shows "rel_option R None None"
    57   by (rule option.ctr_transfer(1))
    58 
    59 lemma option_Some_rsp [quot_respect]:
    60   assumes q: "Quotient3 R Abs Rep"
    61   shows "(R ===> rel_option R) Some Some"
    62   by (rule option.ctr_transfer(2))
    63 
    64 lemma option_None_prs [quot_preserve]:
    65   assumes q: "Quotient3 R Abs Rep"
    66   shows "map_option Abs None = None"
    67   by (rule Option.option.map(1))
    68 
    69 lemma option_Some_prs [quot_preserve]:
    70   assumes q: "Quotient3 R Abs Rep"
    71   shows "(Rep ---> map_option Abs) Some = Some"
    72   apply(simp add: fun_eq_iff)
    73   apply(simp add: Quotient3_abs_rep[OF q])
    74   done
    75 
    76 end