1 (*  Title:      Quotient_Option.thy

     2     Author:     Cezary Kaliszyk and Christian Urban

     3 *)

     4 theory Quotient_Option

     5 imports Quotient

     6 begin

     7 

     8 section {* Quotient infrastructure for the option type. *}

     9 

    10 fun

    11   option_rel

    12 where

    13   "option_rel R None None = True"

    14 | "option_rel R (Some x) None = False"

    15 | "option_rel R None (Some x) = False"

    16 | "option_rel R (Some x) (Some y) = R x y"

    17 

    18 declare [[map option = (Option.map, option_rel)]]

    19 

    20 text {* should probably be in Option.thy *}

    21 lemma split_option_all:

    22   shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"

    23   apply(auto)

    24   apply(case_tac x)

    25   apply(simp_all)

    26   done

    27 

    28 lemma option_quotient[quot_thm]:

    29   assumes q: "Quotient R Abs Rep"

    30   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"

    31   unfolding Quotient_def

    32   apply(simp add: split_option_all)

    33   apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])

    34   using q

    35   unfolding Quotient_def

    36   apply(blast)

    37   done

    38 

    39 lemma option_equivp[quot_equiv]:

    40   assumes a: "equivp R"

    41   shows "equivp (option_rel R)"

    42   apply(rule equivpI)

    43   unfolding reflp_def symp_def transp_def

    44   apply(simp_all add: split_option_all)

    45   apply(blast intro: equivp_reflp[OF a])

    46   apply(blast intro: equivp_symp[OF a])

    47   apply(blast intro: equivp_transp[OF a])

    48   done

    49 

    50 lemma option_None_rsp[quot_respect]:

    51   assumes q: "Quotient R Abs Rep"

    52   shows "option_rel R None None"

    53   by simp

    54 

    55 lemma option_Some_rsp[quot_respect]:

    56   assumes q: "Quotient R Abs Rep"

    57   shows "(R ===> option_rel R) Some Some"

    58   by simp

    59 

    60 lemma option_None_prs[quot_preserve]:

    61   assumes q: "Quotient R Abs Rep"

    62   shows "Option.map Abs None = None"

    63   by simp

    64 

    65 lemma option_Some_prs[quot_preserve]:

    66   assumes q: "Quotient R Abs Rep"

    67   shows "(Rep ---> Option.map Abs) Some = Some"

    68   apply(simp add: expand_fun_eq)

    69   apply(simp add: Quotient_abs_rep[OF q])

    70   done

    71 

    72 lemma option_map_id[id_simps]:

    73   shows "Option.map id = id"

    74   by (simp add: expand_fun_eq split_option_all)

    75 

    76 lemma option_rel_eq[id_simps]:

    77   shows "option_rel (op =) = (op =)"

    78   by (simp add: expand_fun_eq split_option_all)

    79 

    80 end