src/HOL/Library/Quotient_Option.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Fri Feb 19 13:54:19 2010 +0100 (2010-02-19)
changeset 35222 4f1fba00f66d
child 35788 f1deaca15ca3
permissions -rw-r--r--
Initial version of HOL quotient package.
     1 (*  Title:      Quotient_Option.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 theory Quotient_Option
     5 imports Main Quotient_Syntax
     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