src/HOL/Lifting_Option.thy
author kuncar
Thu Apr 10 17:48:15 2014 +0200 (2014-04-10)
changeset 56520 3373f5d1e074
parent 56519 c1048f5bbb45
child 56525 b5b6ad5dc2ae
permissions -rw-r--r--
abstract Domainp in relator_domain rules => more natural statement of the rule
     1 (*  Title:      HOL/Lifting_Option.thy
     2     Author:     Brian Huffman and Ondrej Kuncar
     3     Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
     4 *)
     5 
     6 header {* Setup for Lifting/Transfer for the option type *}
     7 
     8 theory Lifting_Option
     9 imports Lifting Partial_Function
    10 begin
    11 
    12 subsection {* Relator and predicator properties *}
    13 
    14 lemma rel_option_iff:
    15   "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
    16     | (Some x, Some y) \<Rightarrow> R x y
    17     | _ \<Rightarrow> False)"
    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 
    78 subsection {* Transfer rules for the Transfer package *}
    79 
    80 context
    81 begin
    82 interpretation lifting_syntax .
    83 
    84 lemma None_transfer [transfer_rule]: "(rel_option A) None None"
    85   by (rule option.rel_inject)
    86 
    87 lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
    88   unfolding rel_fun_def by simp
    89 
    90 lemma case_option_transfer [transfer_rule]:
    91   "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
    92   unfolding rel_fun_def split_option_all by simp
    93 
    94 lemma map_option_transfer [transfer_rule]:
    95   "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
    96   unfolding map_option_case[abs_def] by transfer_prover
    97 
    98 lemma option_bind_transfer [transfer_rule]:
    99   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   100     Option.bind Option.bind"
   101   unfolding rel_fun_def split_option_all by simp
   102 
   103 end
   104 
   105 end