src/HOL/Lifting_Option.thy
author blanchet
Fri Jan 24 11:51:45 2014 +0100 (2014-01-24)
changeset 55129 26bd1cba3ab5
parent 55090 9475b16e520b
child 55404 5cb95b79a51f
permissions -rw-r--r--
killed 'More_BNFs' by moving its various bits where they (now) belong
     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> option_case 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 option_case_transfer [transfer_rule]:
   104   "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
   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 
   119 subsubsection {* BNF setup *}
   120 
   121 lemma option_rec_conv_option_case: "option_rec = option_case"
   122 by (simp add: fun_eq_iff split: option.split)
   123 
   124 bnf "'a option"
   125   map: Option.map
   126   sets: Option.set
   127   bd: natLeq
   128   wits: None
   129   rel: option_rel
   130 proof -
   131   show "Option.map id = id" by (rule Option.map.id)
   132 next
   133   fix f g
   134   show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
   135     by (auto simp add: fun_eq_iff Option.map_def split: option.split)
   136 next
   137   fix f g x
   138   assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
   139   thus "Option.map f x = Option.map g x"
   140     by (simp cong: Option.map_cong)
   141 next
   142   fix f
   143   show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
   144     by fastforce
   145 next
   146   show "card_order natLeq" by (rule natLeq_card_order)
   147 next
   148   show "cinfinite natLeq" by (rule natLeq_cinfinite)
   149 next
   150   fix x
   151   show "|Option.set x| \<le>o natLeq"
   152     by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
   153 next
   154   fix R S
   155   show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
   156     by (auto simp: option_rel_def split: option.splits)
   157 next
   158   fix z
   159   assume "z \<in> Option.set None"
   160   thus False by simp
   161 next
   162   fix R
   163   show "option_rel R =
   164         (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
   165          Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
   166   unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
   167   by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
   168            split: option.splits)
   169 qed
   170 
   171 end