src/HOL/Lifting_Option.thy
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 56525 b5b6ad5dc2ae
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
kuncar@53012
     1
(*  Title:      HOL/Lifting_Option.thy
kuncar@53012
     2
    Author:     Brian Huffman and Ondrej Kuncar
blanchet@55129
     3
    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
kuncar@53012
     4
*)
kuncar@53012
     5
kuncar@53012
     6
header {* Setup for Lifting/Transfer for the option type *}
kuncar@53012
     7
kuncar@53012
     8
theory Lifting_Option
kuncar@56525
     9
imports Lifting Option
kuncar@53012
    10
begin
kuncar@53012
    11
kuncar@53012
    12
subsection {* Relator and predicator properties *}
kuncar@53012
    13
blanchet@55525
    14
lemma rel_option_iff:
blanchet@55525
    15
  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
kuncar@53012
    16
    | (Some x, Some y) \<Rightarrow> R x y
kuncar@53012
    17
    | _ \<Rightarrow> False)"
blanchet@55525
    18
by (auto split: prod.split option.split)
kuncar@53012
    19
kuncar@53012
    20
subsection {* Transfer rules for the Transfer package *}
kuncar@53012
    21
kuncar@53012
    22
context
kuncar@53012
    23
begin
kuncar@53012
    24
interpretation lifting_syntax .
kuncar@53012
    25
blanchet@55525
    26
lemma None_transfer [transfer_rule]: "(rel_option A) None None"
blanchet@55525
    27
  by (rule option.rel_inject)
kuncar@53012
    28
blanchet@55525
    29
lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
blanchet@55945
    30
  unfolding rel_fun_def by simp
kuncar@53012
    31
blanchet@55404
    32
lemma case_option_transfer [transfer_rule]:
blanchet@55525
    33
  "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
blanchet@55945
    34
  unfolding rel_fun_def split_option_all by simp
kuncar@53012
    35
blanchet@55466
    36
lemma map_option_transfer [transfer_rule]:
blanchet@55525
    37
  "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
blanchet@55466
    38
  unfolding map_option_case[abs_def] by transfer_prover
kuncar@53012
    39
kuncar@53012
    40
lemma option_bind_transfer [transfer_rule]:
blanchet@55525
    41
  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
kuncar@53012
    42
    Option.bind Option.bind"
blanchet@55945
    43
  unfolding rel_fun_def split_option_all by simp
kuncar@53012
    44
kuncar@53012
    45
end
kuncar@53012
    46
kuncar@53012
    47
end