src/HOL/Library/Option_ord.thy
author haftmann
Thu Jul 25 08:57:16 2013 +0200 (2013-07-25)
changeset 52729 412c9e0381a1
parent 49190 e1e1d427747d
child 56166 9a241bc276cd
permissions -rw-r--r--
factored syntactic type classes for bot and top (by Alessandro Coglio)
     1 (*  Title:      HOL/Library/Option_ord.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Canonical order on option type *}
     6 
     7 theory Option_ord
     8 imports Option Main
     9 begin
    10 
    11 notation
    12   bot ("\<bottom>") and
    13   top ("\<top>") and
    14   inf  (infixl "\<sqinter>" 70) and
    15   sup  (infixl "\<squnion>" 65) and
    16   Inf  ("\<Sqinter>_" [900] 900) and
    17   Sup  ("\<Squnion>_" [900] 900)
    18 
    19 syntax (xsymbols)
    20   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    21   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    22   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    23   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    24 
    25 
    26 instantiation option :: (preorder) preorder
    27 begin
    28 
    29 definition less_eq_option where
    30   "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
    31 
    32 definition less_option where
    33   "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
    34 
    35 lemma less_eq_option_None [simp]: "None \<le> x"
    36   by (simp add: less_eq_option_def)
    37 
    38 lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True"
    39   by simp
    40 
    41 lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None"
    42   by (cases x) (simp_all add: less_eq_option_def)
    43 
    44 lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False"
    45   by (simp add: less_eq_option_def)
    46 
    47 lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y"
    48   by (simp add: less_eq_option_def)
    49 
    50 lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False"
    51   by (simp add: less_option_def)
    52 
    53 lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z"
    54   by (cases x) (simp_all add: less_option_def)
    55 
    56 lemma less_option_None_Some [simp]: "None < Some x"
    57   by (simp add: less_option_def)
    58 
    59 lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True"
    60   by simp
    61 
    62 lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
    63   by (simp add: less_option_def)
    64 
    65 instance proof
    66 qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
    67 
    68 end 
    69 
    70 instance option :: (order) order proof
    71 qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
    72 
    73 instance option :: (linorder) linorder proof
    74 qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
    75 
    76 instantiation option :: (order) order_bot
    77 begin
    78 
    79 definition bot_option where
    80   "\<bottom> = None"
    81 
    82 instance proof
    83 qed (simp add: bot_option_def)
    84 
    85 end
    86 
    87 instantiation option :: (order_top) order_top
    88 begin
    89 
    90 definition top_option where
    91   "\<top> = Some \<top>"
    92 
    93 instance proof
    94 qed (simp add: top_option_def less_eq_option_def split: option.split)
    95 
    96 end
    97 
    98 instance option :: (wellorder) wellorder proof
    99   fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
   100   assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   101   have "P None" by (rule H) simp
   102   then have P_Some [case_names Some]:
   103     "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
   104   proof -
   105     fix z
   106     assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
   107     with `P None` show "P z" by (cases z) simp_all
   108   qed
   109   show "P z" proof (cases z rule: P_Some)
   110     case (Some w)
   111     show "(P o Some) w" proof (induct rule: less_induct)
   112       case (less x)
   113       have "P (Some x)" proof (rule H)
   114         fix y :: "'a option"
   115         assume "y < Some x"
   116         show "P y" proof (cases y rule: P_Some)
   117           case (Some v) with `y < Some x` have "v < x" by simp
   118           with less show "(P o Some) v" .
   119         qed
   120       qed
   121       then show ?case by simp
   122     qed
   123   qed
   124 qed
   125 
   126 instantiation option :: (inf) inf
   127 begin
   128 
   129 definition inf_option where
   130   "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))"
   131 
   132 lemma inf_None_1 [simp, code]:
   133   "None \<sqinter> y = None"
   134   by (simp add: inf_option_def)
   135 
   136 lemma inf_None_2 [simp, code]:
   137   "x \<sqinter> None = None"
   138   by (cases x) (simp_all add: inf_option_def)
   139 
   140 lemma inf_Some [simp, code]:
   141   "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
   142   by (simp add: inf_option_def)
   143 
   144 instance ..
   145 
   146 end
   147 
   148 instantiation option :: (sup) sup
   149 begin
   150 
   151 definition sup_option where
   152   "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))"
   153 
   154 lemma sup_None_1 [simp, code]:
   155   "None \<squnion> y = y"
   156   by (simp add: sup_option_def)
   157 
   158 lemma sup_None_2 [simp, code]:
   159   "x \<squnion> None = x"
   160   by (cases x) (simp_all add: sup_option_def)
   161 
   162 lemma sup_Some [simp, code]:
   163   "Some x \<squnion> Some y = Some (x \<squnion> y)"
   164   by (simp add: sup_option_def)
   165 
   166 instance ..
   167 
   168 end
   169 
   170 instantiation option :: (semilattice_inf) semilattice_inf
   171 begin
   172 
   173 instance proof
   174   fix x y z :: "'a option"
   175   show "x \<sqinter> y \<le> x"
   176     by - (cases x, simp_all, cases y, simp_all)
   177   show "x \<sqinter> y \<le> y"
   178     by - (cases x, simp_all, cases y, simp_all)
   179   show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
   180     by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
   181 qed
   182   
   183 end
   184 
   185 instantiation option :: (semilattice_sup) semilattice_sup
   186 begin
   187 
   188 instance proof
   189   fix x y z :: "'a option"
   190   show "x \<le> x \<squnion> y"
   191     by - (cases x, simp_all, cases y, simp_all)
   192   show "y \<le> x \<squnion> y"
   193     by - (cases x, simp_all, cases y, simp_all)
   194   fix x y z :: "'a option"
   195   show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
   196     by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
   197 qed
   198 
   199 end
   200 
   201 instance option :: (lattice) lattice ..
   202 
   203 instance option :: (lattice) bounded_lattice_bot ..
   204 
   205 instance option :: (bounded_lattice_top) bounded_lattice_top ..
   206 
   207 instance option :: (bounded_lattice_top) bounded_lattice ..
   208 
   209 instance option :: (distrib_lattice) distrib_lattice
   210 proof
   211   fix x y z :: "'a option"
   212   show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   213     by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
   214 qed 
   215 
   216 instantiation option :: (complete_lattice) complete_lattice
   217 begin
   218 
   219 definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
   220   "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
   221 
   222 lemma None_in_Inf [simp]:
   223   "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
   224   by (simp add: Inf_option_def)
   225 
   226 definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
   227   "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
   228 
   229 lemma empty_Sup [simp]:
   230   "\<Squnion>{} = None"
   231   by (simp add: Sup_option_def)
   232 
   233 lemma singleton_None_Sup [simp]:
   234   "\<Squnion>{None} = None"
   235   by (simp add: Sup_option_def)
   236 
   237 instance proof
   238   fix x :: "'a option" and A
   239   assume "x \<in> A"
   240   then show "\<Sqinter>A \<le> x"
   241     by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
   242 next
   243   fix z :: "'a option" and A
   244   assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   245   show "z \<le> \<Sqinter>A"
   246   proof (cases z)
   247     case None then show ?thesis by simp
   248   next
   249     case (Some y)
   250     show ?thesis
   251       by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
   252   qed
   253 next
   254   fix x :: "'a option" and A
   255   assume "x \<in> A"
   256   then show "x \<le> \<Squnion>A"
   257     by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
   258 next
   259   fix z :: "'a option" and A
   260   assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   261   show "\<Squnion>A \<le> z "
   262   proof (cases z)
   263     case None
   264     with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None)
   265     then have "A = {} \<or> A = {None}" by blast
   266     then show ?thesis by (simp add: Sup_option_def)
   267   next
   268     case (Some y)
   269     from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" .
   270     with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y"
   271       by (simp add: in_these_eq)
   272     then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
   273     with Some show ?thesis by (simp add: Sup_option_def)
   274   qed
   275 next
   276   show "\<Squnion>{} = (\<bottom>::'a option)"
   277   by (auto simp: bot_option_def)
   278 next
   279   show "\<Sqinter>{} = (\<top>::'a option)"
   280   by (auto simp: top_option_def Inf_option_def)
   281 qed
   282 
   283 end
   284 
   285 lemma Some_Inf:
   286   "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
   287   by (auto simp add: Inf_option_def)
   288 
   289 lemma Some_Sup:
   290   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
   291   by (auto simp add: Sup_option_def)
   292 
   293 lemma Some_INF:
   294   "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
   295   by (simp add: INF_def Some_Inf image_image)
   296 
   297 lemma Some_SUP:
   298   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
   299   by (simp add: SUP_def Some_Sup image_image)
   300 
   301 instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
   302 begin
   303 
   304 instance proof
   305   fix a :: "'a option" and B
   306   show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   307   proof (cases a)
   308     case None
   309     then show ?thesis by (simp add: INF_def)
   310   next
   311     case (Some c)
   312     show ?thesis
   313     proof (cases "None \<in> B")
   314       case True
   315       then have "Some c = (\<Sqinter>b\<in>B. Some c \<squnion> b)"
   316         by (auto intro!: antisym INF_lower2 INF_greatest)
   317       with True Some show ?thesis by simp
   318     next
   319       case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
   320       from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
   321       then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
   322         by (simp add: Some_INF Some_Inf)
   323       with Some B show ?thesis by (simp add: Some_image_these_eq)
   324     qed
   325   qed
   326   show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   327   proof (cases a)
   328     case None
   329     then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
   330   next
   331     case (Some c)
   332     show ?thesis
   333     proof (cases "B = {} \<or> B = {None}")
   334       case True
   335       then show ?thesis by (auto simp add: SUP_def)
   336     next
   337       have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
   338         by auto
   339       then have Sup_B: "\<Squnion>B = \<Squnion>({x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None})"
   340         and SUP_B: "\<And>f. (\<Squnion>x \<in> B. f x) = (\<Squnion>x \<in> {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}. f x)"
   341         by simp_all
   342       have Sup_None: "\<Squnion>{x. x = None \<and> x \<in> B} = None"
   343         by (simp add: bot_option_def [symmetric])
   344       have SUP_None: "(\<Squnion>x\<in>{x. x = None \<and> x \<in> B}. Some c \<sqinter> x) = None"
   345         by (simp add: bot_option_def [symmetric])
   346       case False then have "Option.these B \<noteq> {}" by (simp add: these_not_empty_eq)
   347       moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
   348         by simp
   349       ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
   350         by (simp add: Some_SUP Some_Sup)
   351       with Some show ?thesis
   352         by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
   353     qed
   354   qed
   355 qed
   356 
   357 end
   358 
   359 instantiation option :: (complete_linorder) complete_linorder
   360 begin
   361 
   362 instance ..
   363 
   364 end
   365 
   366 
   367 no_notation
   368   bot ("\<bottom>") and
   369   top ("\<top>") and
   370   inf  (infixl "\<sqinter>" 70) and
   371   sup  (infixl "\<squnion>" 65) and
   372   Inf  ("\<Sqinter>_" [900] 900) and
   373   Sup  ("\<Squnion>_" [900] 900)
   374 
   375 no_syntax (xsymbols)
   376   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   377   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   378   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   379   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   380 
   381 end
   382