src/HOL/Lifting_Option.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56525 b5b6ad5dc2ae
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 Option
    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 subsection {* Transfer rules for the Transfer package *}
    21 
    22 context
    23 begin
    24 interpretation lifting_syntax .
    25 
    26 lemma None_transfer [transfer_rule]: "(rel_option A) None None"
    27   by (rule option.rel_inject)
    28 
    29 lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
    30   unfolding rel_fun_def by simp
    31 
    32 lemma case_option_transfer [transfer_rule]:
    33   "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
    34   unfolding rel_fun_def split_option_all by simp
    35 
    36 lemma map_option_transfer [transfer_rule]:
    37   "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
    38   unfolding map_option_case[abs_def] by transfer_prover
    39 
    40 lemma option_bind_transfer [transfer_rule]:
    41   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
    42     Option.bind Option.bind"
    43   unfolding rel_fun_def split_option_all by simp
    44 
    45 end
    46 
    47 end