src/HOL/Library/Quotient_Option.thy
author kuncar
Fri Mar 23 14:20:09 2012 +0100 (2012-03-23)
changeset 47094 1a7ad2601cb5
parent 45802 b16f976db515
child 47308 9caab698dbe4
permissions -rw-r--r--
store the relational theorem for every relator
     1 (*  Title:      HOL/Library/Quotient_Option.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 header {* Quotient infrastructure for the option type *}
     6 
     7 theory Quotient_Option
     8 imports Main Quotient_Syntax
     9 begin
    10 
    11 fun
    12   option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    13 where
    14   "option_rel R None None = True"
    15 | "option_rel R (Some x) None = False"
    16 | "option_rel R None (Some x) = False"
    17 | "option_rel R (Some x) (Some y) = R x y"
    18 
    19 lemma option_rel_unfold:
    20   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    21     | (Some x, Some y) \<Rightarrow> R x y
    22     | _ \<Rightarrow> False)"
    23   by (cases x) (cases y, simp_all)+
    24 
    25 lemma option_rel_map1:
    26   "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
    27   by (simp add: option_rel_unfold split: option.split)
    28 
    29 lemma option_rel_map2:
    30   "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
    31   by (simp add: option_rel_unfold split: option.split)
    32 
    33 lemma option_map_id [id_simps]:
    34   "Option.map id = id"
    35   by (simp add: id_def Option.map.identity fun_eq_iff)
    36 
    37 lemma option_rel_eq [id_simps]:
    38   "option_rel (op =) = (op =)"
    39   by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    40 
    41 lemma option_reflp:
    42   "reflp R \<Longrightarrow> reflp (option_rel R)"
    43   by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
    44 
    45 lemma option_symp:
    46   "symp R \<Longrightarrow> symp (option_rel R)"
    47   by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
    48 
    49 lemma option_transp:
    50   "transp R \<Longrightarrow> transp (option_rel R)"
    51   by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
    52 
    53 lemma option_equivp [quot_equiv]:
    54   "equivp R \<Longrightarrow> equivp (option_rel R)"
    55   by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
    56 
    57 lemma option_quotient [quot_thm]:
    58   assumes "Quotient R Abs Rep"
    59   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
    60   apply (rule QuotientI)
    61   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])
    62   using Quotient_rel [OF assms]
    63   apply (simp add: option_rel_unfold split: option.split)
    64   done
    65 
    66 declare [[map option = (option_rel, option_quotient)]]
    67 
    68 lemma option_None_rsp [quot_respect]:
    69   assumes q: "Quotient R Abs Rep"
    70   shows "option_rel R None None"
    71   by simp
    72 
    73 lemma option_Some_rsp [quot_respect]:
    74   assumes q: "Quotient R Abs Rep"
    75   shows "(R ===> option_rel R) Some Some"
    76   by auto
    77 
    78 lemma option_None_prs [quot_preserve]:
    79   assumes q: "Quotient R Abs Rep"
    80   shows "Option.map Abs None = None"
    81   by simp
    82 
    83 lemma option_Some_prs [quot_preserve]:
    84   assumes q: "Quotient R Abs Rep"
    85   shows "(Rep ---> Option.map Abs) Some = Some"
    86   apply(simp add: fun_eq_iff)
    87   apply(simp add: Quotient_abs_rep[OF q])
    88   done
    89 
    90 end