src/HOL/Library/Quotient_Option.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 41372 551eb49a6e91
child 47094 1a7ad2601cb5
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 declare [[map option = option_rel]]
    20 
    21 lemma option_rel_unfold:
    22   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    23     | (Some x, Some y) \<Rightarrow> R x y
    24     | _ \<Rightarrow> False)"
    25   by (cases x) (cases y, simp_all)+
    26 
    27 lemma option_rel_map1:
    28   "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
    29   by (simp add: option_rel_unfold split: option.split)
    30 
    31 lemma option_rel_map2:
    32   "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
    33   by (simp add: option_rel_unfold split: option.split)
    34 
    35 lemma option_map_id [id_simps]:
    36   "Option.map id = id"
    37   by (simp add: id_def Option.map.identity fun_eq_iff)
    38 
    39 lemma option_rel_eq [id_simps]:
    40   "option_rel (op =) = (op =)"
    41   by (simp add: option_rel_unfold fun_eq_iff split: option.split)
    42 
    43 lemma option_reflp:
    44   "reflp R \<Longrightarrow> reflp (option_rel R)"
    45   by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
    46 
    47 lemma option_symp:
    48   "symp R \<Longrightarrow> symp (option_rel R)"
    49   by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
    50 
    51 lemma option_transp:
    52   "transp R \<Longrightarrow> transp (option_rel R)"
    53   by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
    54 
    55 lemma option_equivp [quot_equiv]:
    56   "equivp R \<Longrightarrow> equivp (option_rel R)"
    57   by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
    58 
    59 lemma option_quotient [quot_thm]:
    60   assumes "Quotient R Abs Rep"
    61   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
    62   apply (rule QuotientI)
    63   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])
    64   using Quotient_rel [OF assms]
    65   apply (simp add: option_rel_unfold split: option.split)
    66   done
    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