src/HOL/Lifting_Option.thy
author wenzelm
Fri Mar 07 22:30:58 2014 +0100 (2014-03-07)
changeset 55990 41c6b99c5fb7
parent 55945 e96383acecf9
child 56092 1ba075db8fe4
permissions -rw-r--r--
more antiquotations;
     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) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    21   "option_pred \<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   assumes "Domainp A = P"
    38   shows "Domainp (rel_option A) = (option_pred P)"
    39 using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    40 by (auto iff: fun_eq_iff split: option.split)
    41 
    42 lemma left_total_rel_option[reflexivity_rule]:
    43   "left_total R \<Longrightarrow> left_total (rel_option R)"
    44   unfolding left_total_def split_option_all split_option_ex by simp
    45 
    46 lemma left_unique_rel_option [reflexivity_rule]:
    47   "left_unique R \<Longrightarrow> left_unique (rel_option R)"
    48   unfolding left_unique_def split_option_all by simp
    49 
    50 lemma right_total_rel_option [transfer_rule]:
    51   "right_total R \<Longrightarrow> right_total (rel_option R)"
    52   unfolding right_total_def split_option_all split_option_ex by simp
    53 
    54 lemma right_unique_rel_option [transfer_rule]:
    55   "right_unique R \<Longrightarrow> right_unique (rel_option R)"
    56   unfolding right_unique_def split_option_all by simp
    57 
    58 lemma bi_total_rel_option [transfer_rule]:
    59   "bi_total R \<Longrightarrow> bi_total (rel_option R)"
    60   unfolding bi_total_def split_option_all split_option_ex by simp
    61 
    62 lemma bi_unique_rel_option [transfer_rule]:
    63   "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
    64   unfolding bi_unique_def split_option_all by simp
    65 
    66 lemma option_invariant_commute [invariant_commute]:
    67   "rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)"
    68   by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    69 
    70 subsection {* Quotient theorem for the Lifting package *}
    71 
    72 lemma Quotient_option[quot_map]:
    73   assumes "Quotient R Abs Rep T"
    74   shows "Quotient (rel_option R) (map_option Abs)
    75     (map_option Rep) (rel_option T)"
    76   using assms unfolding Quotient_alt_def rel_option_iff
    77   by (simp split: option.split)
    78 
    79 subsection {* Transfer rules for the Transfer package *}
    80 
    81 context
    82 begin
    83 interpretation lifting_syntax .
    84 
    85 lemma None_transfer [transfer_rule]: "(rel_option A) None None"
    86   by (rule option.rel_inject)
    87 
    88 lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
    89   unfolding rel_fun_def by simp
    90 
    91 lemma case_option_transfer [transfer_rule]:
    92   "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
    93   unfolding rel_fun_def split_option_all by simp
    94 
    95 lemma map_option_transfer [transfer_rule]:
    96   "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
    97   unfolding map_option_case[abs_def] by transfer_prover
    98 
    99 lemma option_bind_transfer [transfer_rule]:
   100   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   101     Option.bind Option.bind"
   102   unfolding rel_fun_def split_option_all by simp
   103 
   104 end
   105 
   106 end