src/HOL/Library/Option_ord.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (12 months ago)
changeset 68658 16cc1161ad7f
parent 67951 655aa11359dc
child 68980 5717fbc55521
permissions -rw-r--r--
tuned equation
     1 (*  Title:      HOL/Library/Option_ord.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Canonical order on option type\<close>
     6 
     7 theory Option_ord
     8 imports 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
    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
    66   by standard
    67     (auto simp add: less_eq_option_def less_option_def less_le_not_le
    68       elim: order_trans split: option.splits)
    69 
    70 end
    71 
    72 instance option :: (order) order
    73   by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
    74 
    75 instance option :: (linorder) linorder
    76   by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
    77 
    78 instantiation option :: (order) order_bot
    79 begin
    80 
    81 definition bot_option where "\<bottom> = None"
    82 
    83 instance
    84   by standard (simp add: bot_option_def)
    85 
    86 end
    87 
    88 instantiation option :: (order_top) order_top
    89 begin
    90 
    91 definition top_option where "\<top> = Some \<top>"
    92 
    93 instance
    94   by standard (simp add: top_option_def less_eq_option_def split: option.split)
    95 
    96 end
    97 
    98 instance option :: (wellorder) wellorder
    99 proof
   100   fix P :: "'a option \<Rightarrow> bool"
   101   fix z :: "'a option"
   102   assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   103   have "P None" by (rule H) simp
   104   then have P_Some [case_names Some]: "P z" if "\<And>x. z = Some x \<Longrightarrow> (P \<circ> Some) x" for z
   105     using \<open>P None\<close> that by (cases z) simp_all
   106   show "P z"
   107   proof (cases z rule: P_Some)
   108     case (Some w)
   109     show "(P \<circ> Some) w"
   110     proof (induct rule: less_induct)
   111       case (less x)
   112       have "P (Some x)"
   113       proof (rule H)
   114         fix y :: "'a option"
   115         assume "y < Some x"
   116         show "P y"
   117         proof (cases y rule: P_Some)
   118           case (Some v)
   119           with \<open>y < Some x\<close> have "v < x" by simp
   120           with less show "(P \<circ> Some) v" .
   121         qed
   122       qed
   123       then show ?case by simp
   124     qed
   125   qed
   126 qed
   127 
   128 instantiation option :: (inf) inf
   129 begin
   130 
   131 definition inf_option where
   132   "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)))"
   133 
   134 lemma inf_None_1 [simp, code]: "None \<sqinter> y = None"
   135   by (simp add: inf_option_def)
   136 
   137 lemma inf_None_2 [simp, code]: "x \<sqinter> None = None"
   138   by (cases x) (simp_all add: inf_option_def)
   139 
   140 lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
   141   by (simp add: inf_option_def)
   142 
   143 instance ..
   144 
   145 end
   146 
   147 instantiation option :: (sup) sup
   148 begin
   149 
   150 definition sup_option where
   151   "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)))"
   152 
   153 lemma sup_None_1 [simp, code]: "None \<squnion> y = y"
   154   by (simp add: sup_option_def)
   155 
   156 lemma sup_None_2 [simp, code]: "x \<squnion> None = x"
   157   by (cases x) (simp_all add: sup_option_def)
   158 
   159 lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)"
   160   by (simp add: sup_option_def)
   161 
   162 instance ..
   163 
   164 end
   165 
   166 instance option :: (semilattice_inf) semilattice_inf
   167 proof
   168   fix x y z :: "'a option"
   169   show "x \<sqinter> y \<le> x"
   170     by (cases x, simp_all, cases y, simp_all)
   171   show "x \<sqinter> y \<le> y"
   172     by (cases x, simp_all, cases y, simp_all)
   173   show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
   174     by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
   175 qed
   176 
   177 instance option :: (semilattice_sup) semilattice_sup
   178 proof
   179   fix x y z :: "'a option"
   180   show "x \<le> x \<squnion> y"
   181     by (cases x, simp_all, cases y, simp_all)
   182   show "y \<le> x \<squnion> y"
   183     by (cases x, simp_all, cases y, simp_all)
   184   fix x y z :: "'a option"
   185   show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
   186     by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
   187 qed
   188 
   189 instance option :: (lattice) lattice ..
   190 
   191 instance option :: (lattice) bounded_lattice_bot ..
   192 
   193 instance option :: (bounded_lattice_top) bounded_lattice_top ..
   194 
   195 instance option :: (bounded_lattice_top) bounded_lattice ..
   196 
   197 instance option :: (distrib_lattice) distrib_lattice
   198 proof
   199   fix x y z :: "'a option"
   200   show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   201     by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
   202 qed
   203 
   204 instantiation option :: (complete_lattice) complete_lattice
   205 begin
   206 
   207 definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
   208   "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
   209 
   210 lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
   211   by (simp add: Inf_option_def)
   212 
   213 definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
   214   "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
   215 
   216 lemma empty_Sup [simp]: "\<Squnion>{} = None"
   217   by (simp add: Sup_option_def)
   218 
   219 lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None"
   220   by (simp add: Sup_option_def)
   221 
   222 instance
   223 proof
   224   fix x :: "'a option" and A
   225   assume "x \<in> A"
   226   then show "\<Sqinter>A \<le> x"
   227     by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
   228 next
   229   fix z :: "'a option" and A
   230   assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   231   show "z \<le> \<Sqinter>A"
   232   proof (cases z)
   233     case None then show ?thesis by simp
   234   next
   235     case (Some y)
   236     show ?thesis
   237       by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
   238   qed
   239 next
   240   fix x :: "'a option" and A
   241   assume "x \<in> A"
   242   then show "x \<le> \<Squnion>A"
   243     by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
   244 next
   245   fix z :: "'a option" and A
   246   assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   247   show "\<Squnion>A \<le> z "
   248   proof (cases z)
   249     case None
   250     with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None)
   251     then have "A = {} \<or> A = {None}" by blast
   252     then show ?thesis by (simp add: Sup_option_def)
   253   next
   254     case (Some y)
   255     from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" .
   256     with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y"
   257       by (simp add: in_these_eq)
   258     then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
   259     with Some show ?thesis by (simp add: Sup_option_def)
   260   qed
   261 next
   262   show "\<Squnion>{} = (\<bottom>::'a option)"
   263     by (auto simp: bot_option_def)
   264   show "\<Sqinter>{} = (\<top>::'a option)"
   265     by (auto simp: top_option_def Inf_option_def)
   266 qed
   267 
   268 end
   269 
   270 lemma Some_Inf:
   271   "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
   272   by (auto simp add: Inf_option_def)
   273 
   274 lemma Some_Sup:
   275   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
   276   by (auto simp add: Sup_option_def)
   277 
   278 lemma Some_INF:
   279   "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
   280   using Some_Inf [of "f ` A"] by (simp add: comp_def)
   281 
   282 lemma Some_SUP:
   283   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
   284   using Some_Sup [of "f ` A"] by (simp add: comp_def)
   285 
   286 lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   287 proof (cases "{} \<in> A")
   288   case True
   289   then show ?thesis
   290     by (rule INF_lower2, simp_all)
   291 next
   292   case False
   293   from this have X: "{} \<notin> A"
   294     by simp
   295   then show ?thesis
   296   proof (cases "{None} \<in> A")
   297     case True
   298     then show ?thesis
   299       by (rule INF_lower2, simp_all)
   300   next
   301     case False
   302 
   303     {fix y
   304       assume A: "y \<in> A"
   305       have "Sup (y - {None}) = Sup y"
   306         by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
   307       from A and this have "(\<exists>z. y - {None} = z - {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y - {None})"
   308         by auto
   309     }
   310     from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
   311       by (auto simp add: image_def)
   312 
   313     have [simp]: "\<And>y. y \<in> A \<Longrightarrow> \<exists>ya. {ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} 
   314           = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
   315       by (rule exI, auto)
   316 
   317     have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
   318          (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} 
   319           = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
   320       apply (safe, blast)
   321       by (rule arg_cong [of _ _ Sup], auto)
   322     {fix y
   323       assume [simp]: "y \<in> A"
   324       have "\<exists>x. (\<exists>y. x = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} = \<Squnion>x"
   325       and "\<exists>x. (\<exists>y. x = y - {None} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} = \<Squnion>{y. \<exists>xa. xa \<in> x \<and> (\<exists>y. xa = Some y) \<and> y = the xa}"
   326          apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp)
   327         by (rule exI [of _ "y - {None}"], simp)
   328     }
   329     from this have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
   330       by (simp add: image_def Option.these_def, safe, simp_all)
   331   
   332     have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
   333       by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq)
   334   
   335     define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
   336   
   337     have G: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> x . x \<in> Y - {None}"
   338       by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq)
   339   
   340     have F: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> (Y - {None})"
   341       by (metis F_def G empty_iff some_in_eq)
   342   
   343     have "Some \<bottom> \<le> Inf (F ` A)"
   344       by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff 
   345           less_eq_option_Some singletonI)
   346       
   347     from this have "Inf (F ` A) \<noteq> None"
   348       by (cases "\<Sqinter>x\<in>A. F x", simp_all)
   349 
   350     from this have "Inf (F ` A) \<noteq> None \<and> Inf (F ` A) \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
   351       using F by auto
   352 
   353     from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
   354       by blast
   355   
   356     from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
   357       by blast
   358 
   359     have [simp]: "((\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x) = None) = False"
   360       by (metis (no_types, lifting) E Sup_option_def \<open>\<exists>x. x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}\<close> 
   361           ex_in_conv option.simps(3))
   362   
   363     have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}) 
   364         = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
   365       by (metis image_image these_image_Some_eq)
   366     {
   367       fix f
   368       assume A: "\<And> Y . (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y"
   369 
   370       have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))"
   371         by  (simp add: image_def)
   372       from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x\<in>A. f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (x - {None}))"
   373         by blast
   374       have "\<And>xa. xa \<in> A \<Longrightarrow> f (the ` (xa - {None})) = f {y. \<exists>a \<in> xa - {None}. y = the a} \<and> xa \<in> A"
   375         by (simp add: image_def)
   376       from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x. f (the ` (xa - {None})) = f {y. \<exists>a\<in>x - {None}. y = the a} \<and> x \<in> A"
   377         by blast
   378 
   379       {
   380         fix Y
   381         have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
   382           using A [of "the ` (Y - {None})"] apply (simp add: image_def)
   383           using option.collapse by fastforce
   384       }
   385       from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
   386         by blast
   387       have [simp]: "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A}"
   388         by (simp add: Setcompr_eq_image)
   389       
   390       have [simp]: "\<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A} = \<Sqinter>x"
   391         apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}"], safe)
   392         by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)
   393 
   394       {
   395         fix xb
   396         have "xb \<in> A \<Longrightarrow> (\<Sqinter>x\<in>{{ya. \<exists>x\<in>y - {None}. ya = the x} |y. y \<in> A}. f x) \<le> f {y. \<exists>x\<in>xb - {None}. y = the x}"
   397           apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb - {None}. y = the x}"])
   398           by blast+
   399       }
   400       from this have [simp]: "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
   401         apply (simp add: Inf_option_def image_def Option.these_def)
   402         by (rule Inf_greatest, clarsimp)
   403 
   404       have [simp]: "the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None})))) \<in> Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   405         apply (simp add:  Option.these_def image_def)
   406         apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))"], simp)
   407         by (simp add: Inf_option_def)
   408 
   409       have "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   410         by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
   411     }
   412     from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
   413       (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   414       by blast
   415     
   416 
   417     have [simp]: "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}"
   418       using F by fastforce
   419 
   420     have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
   421       by (subst A, simp)
   422 
   423     also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. if x = {} \<or> x = {None} then None else Some (\<Squnion>Option.these x))"
   424       by (simp add: Sup_option_def)
   425 
   426     also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
   427       using G by fastforce
   428   
   429     also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
   430       by (simp add: Inf_option_def, safe)
   431   
   432     also have "... =  Some (\<Sqinter> ((\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
   433       by (simp add: B)
   434   
   435     also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y \<in> A}))"
   436       by (unfold C, simp)
   437     thm Inf_Sup
   438     also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y - {None}) |y. y \<in> A} |f. \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) "
   439       by (simp add: Inf_Sup)
   440   
   441     also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   442     proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
   443       case None
   444       then show ?thesis by (simp add: less_eq_option_def)
   445     next
   446       case (Some a)
   447       then show ?thesis
   448         apply simp
   449         apply (rule Sup_least, safe)
   450         apply (simp add: Sup_option_def)
   451         apply (cases "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
   452         by (drule X, simp)
   453     qed
   454     finally show ?thesis by simp
   455   qed
   456 qed
   457 
   458 instance option :: (complete_distrib_lattice) complete_distrib_lattice
   459   by (standard, simp add: option_Inf_Sup)
   460 
   461 instance option :: (complete_linorder) complete_linorder ..
   462 
   463 
   464 no_notation
   465   bot ("\<bottom>") and
   466   top ("\<top>") and
   467   inf  (infixl "\<sqinter>" 70) and
   468   sup  (infixl "\<squnion>" 65) and
   469   Inf  ("\<Sqinter>_" [900] 900) and
   470   Sup  ("\<Squnion>_" [900] 900)
   471 
   472 no_syntax
   473   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   474   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   475   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   476   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   477 
   478 end