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
```