src/HOL/Lifting_Option.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 55404 5cb95b79a51f
child 55466 786edc984c98
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     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 definition
    15   option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    16 where
    17   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    18     | (Some x, Some y) \<Rightarrow> R x y
    19     | _ \<Rightarrow> False)"
    20 
    21 lemma option_rel_simps[simp]:
    22   "option_rel R None None = True"
    23   "option_rel R (Some x) None = False"
    24   "option_rel R None (Some y) = False"
    25   "option_rel R (Some x) (Some y) = R x y"
    26   unfolding option_rel_def by simp_all
    27 
    28 abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    29   "option_pred \<equiv> case_option True"
    30 
    31 lemma option_rel_eq [relator_eq]:
    32   "option_rel (op =) = (op =)"
    33   by (simp add: option_rel_def fun_eq_iff split: option.split)
    34 
    35 lemma option_rel_mono[relator_mono]:
    36   assumes "A \<le> B"
    37   shows "(option_rel A) \<le> (option_rel B)"
    38 using assms by (auto simp: option_rel_def split: option.splits)
    39 
    40 lemma option_rel_OO[relator_distr]:
    41   "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
    42 by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split)
    43 
    44 lemma Domainp_option[relator_domain]:
    45   assumes "Domainp A = P"
    46   shows "Domainp (option_rel A) = (option_pred P)"
    47 using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def]
    48 by (auto iff: fun_eq_iff split: option.split)
    49 
    50 lemma reflp_option_rel[reflexivity_rule]:
    51   "reflp R \<Longrightarrow> reflp (option_rel R)"
    52   unfolding reflp_def split_option_all by simp
    53 
    54 lemma left_total_option_rel[reflexivity_rule]:
    55   "left_total R \<Longrightarrow> left_total (option_rel R)"
    56   unfolding left_total_def split_option_all split_option_ex by simp
    57 
    58 lemma left_unique_option_rel [reflexivity_rule]:
    59   "left_unique R \<Longrightarrow> left_unique (option_rel R)"
    60   unfolding left_unique_def split_option_all by simp
    61 
    62 lemma right_total_option_rel [transfer_rule]:
    63   "right_total R \<Longrightarrow> right_total (option_rel R)"
    64   unfolding right_total_def split_option_all split_option_ex by simp
    65 
    66 lemma right_unique_option_rel [transfer_rule]:
    67   "right_unique R \<Longrightarrow> right_unique (option_rel R)"
    68   unfolding right_unique_def split_option_all by simp
    69 
    70 lemma bi_total_option_rel [transfer_rule]:
    71   "bi_total R \<Longrightarrow> bi_total (option_rel R)"
    72   unfolding bi_total_def split_option_all split_option_ex by simp
    73 
    74 lemma bi_unique_option_rel [transfer_rule]:
    75   "bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
    76   unfolding bi_unique_def split_option_all by simp
    77 
    78 lemma option_invariant_commute [invariant_commute]:
    79   "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
    80   by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    81 
    82 subsection {* Quotient theorem for the Lifting package *}
    83 
    84 lemma Quotient_option[quot_map]:
    85   assumes "Quotient R Abs Rep T"
    86   shows "Quotient (option_rel R) (Option.map Abs)
    87     (Option.map Rep) (option_rel T)"
    88   using assms unfolding Quotient_alt_def option_rel_def
    89   by (simp split: option.split)
    90 
    91 subsection {* Transfer rules for the Transfer package *}
    92 
    93 context
    94 begin
    95 interpretation lifting_syntax .
    96 
    97 lemma None_transfer [transfer_rule]: "(option_rel A) None None"
    98   by simp
    99 
   100 lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
   101   unfolding fun_rel_def by simp
   102 
   103 lemma case_option_transfer [transfer_rule]:
   104   "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
   105   unfolding fun_rel_def split_option_all by simp
   106 
   107 lemma option_map_transfer [transfer_rule]:
   108   "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
   109   unfolding Option.map_def by transfer_prover
   110 
   111 lemma option_bind_transfer [transfer_rule]:
   112   "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
   113     Option.bind Option.bind"
   114   unfolding fun_rel_def split_option_all by simp
   115 
   116 end
   117 
   118 end