src/HOL/Lifting_Option.thy
 author blanchet Thu Mar 06 15:40:33 2014 +0100 (2014-03-06) changeset 55945 e96383acecf9 parent 55564 e81ee43ab290 child 56092 1ba075db8fe4 permissions -rw-r--r--
renamed 'fun_rel' to 'rel_fun'
```     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
```