src/HOL/Lifting_Option.thy
changeset 56525 b5b6ad5dc2ae
parent 56520 3373f5d1e074
child 58889 5b7a9633cfa8
equal deleted inserted replaced
56524:f4ba736040fa 56525:b5b6ad5dc2ae
     4 *)
     4 *)
     5 
     5 
     6 header {* Setup for Lifting/Transfer for the option type *}
     6 header {* Setup for Lifting/Transfer for the option type *}
     7 
     7 
     8 theory Lifting_Option
     8 theory Lifting_Option
     9 imports Lifting Partial_Function
     9 imports Lifting Option
    10 begin
    10 begin
    11 
    11 
    12 subsection {* Relator and predicator properties *}
    12 subsection {* Relator and predicator properties *}
    13 
    13 
    14 lemma rel_option_iff:
    14 lemma rel_option_iff:
    15   "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
    15   "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
    16     | (Some x, Some y) \<Rightarrow> R x y
    16     | (Some x, Some y) \<Rightarrow> R x y
    17     | _ \<Rightarrow> False)"
    17     | _ \<Rightarrow> False)"
    18 by (auto split: prod.split option.split)
    18 by (auto split: prod.split option.split)
    19 
       
    20 abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
       
    21   "pred_option \<equiv> case_option True"
       
    22 
       
    23 lemma rel_option_eq [relator_eq]:
       
    24   "rel_option (op =) = (op =)"
       
    25   by (simp add: rel_option_iff fun_eq_iff split: option.split)
       
    26 
       
    27 lemma rel_option_mono[relator_mono]:
       
    28   assumes "A \<le> B"
       
    29   shows "(rel_option A) \<le> (rel_option B)"
       
    30 using assms by (auto simp: rel_option_iff split: option.splits)
       
    31 
       
    32 lemma rel_option_OO[relator_distr]:
       
    33   "(rel_option A) OO (rel_option B) = rel_option (A OO B)"
       
    34 by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
       
    35 
       
    36 lemma Domainp_option[relator_domain]: 
       
    37   "Domainp (rel_option A) = (pred_option (Domainp A))"
       
    38 unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
       
    39 by (auto iff: fun_eq_iff split: option.split)
       
    40 
       
    41 lemma left_total_rel_option[transfer_rule]:
       
    42   "left_total R \<Longrightarrow> left_total (rel_option R)"
       
    43   unfolding left_total_def split_option_all split_option_ex by simp
       
    44 
       
    45 lemma left_unique_rel_option [transfer_rule]:
       
    46   "left_unique R \<Longrightarrow> left_unique (rel_option R)"
       
    47   unfolding left_unique_def split_option_all by simp
       
    48 
       
    49 lemma right_total_rel_option [transfer_rule]:
       
    50   "right_total R \<Longrightarrow> right_total (rel_option R)"
       
    51   unfolding right_total_def split_option_all split_option_ex by simp
       
    52 
       
    53 lemma right_unique_rel_option [transfer_rule]:
       
    54   "right_unique R \<Longrightarrow> right_unique (rel_option R)"
       
    55   unfolding right_unique_def split_option_all by simp
       
    56 
       
    57 lemma bi_total_rel_option [transfer_rule]:
       
    58   "bi_total R \<Longrightarrow> bi_total (rel_option R)"
       
    59   unfolding bi_total_def split_option_all split_option_ex by simp
       
    60 
       
    61 lemma bi_unique_rel_option [transfer_rule]:
       
    62   "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
       
    63   unfolding bi_unique_def split_option_all by simp
       
    64 
       
    65 lemma option_relator_eq_onp [relator_eq_onp]:
       
    66   "rel_option (eq_onp P) = eq_onp (pred_option P)"
       
    67   by (auto simp add: fun_eq_iff eq_onp_def split_option_all)
       
    68 
       
    69 subsection {* Quotient theorem for the Lifting package *}
       
    70 
       
    71 lemma Quotient_option[quot_map]:
       
    72   assumes "Quotient R Abs Rep T"
       
    73   shows "Quotient (rel_option R) (map_option Abs)
       
    74     (map_option Rep) (rel_option T)"
       
    75   using assms unfolding Quotient_alt_def rel_option_iff
       
    76   by (simp split: option.split)
       
    77 
    19 
    78 subsection {* Transfer rules for the Transfer package *}
    20 subsection {* Transfer rules for the Transfer package *}
    79 
    21 
    80 context
    22 context
    81 begin
    23 begin