1(* Title: HOL/Library/Option_ord.thy 2 Author: Florian Haftmann, TU Muenchen 3*) 4 5section \<open>Canonical order on option type\<close> 6 7theory Option_ord 8imports Main 9begin 10 11notation 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 19syntax 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 26instantiation option :: (preorder) preorder 27begin 28 29definition 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 32definition 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 35lemma less_eq_option_None [simp]: "None \<le> x" 36 by (simp add: less_eq_option_def) 37 38lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True" 39 by simp 40 41lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None" 42 by (cases x) (simp_all add: less_eq_option_def) 43 44lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False" 45 by (simp add: less_eq_option_def) 46 47lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y" 48 by (simp add: less_eq_option_def) 49 50lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False" 51 by (simp add: less_option_def) 52 53lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z" 54 by (cases x) (simp_all add: less_option_def) 55 56lemma less_option_None_Some [simp]: "None < Some x" 57 by (simp add: less_option_def) 58 59lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True" 60 by simp 61 62lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y" 63 by (simp add: less_option_def) 64 65instance 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 70end 71 72instance option :: (order) order 73 by standard (auto simp add: less_eq_option_def less_option_def split: option.splits) 74 75instance option :: (linorder) linorder 76 by standard (auto simp add: less_eq_option_def less_option_def split: option.splits) 77 78instantiation option :: (order) order_bot 79begin 80 81definition bot_option where "\<bottom> = None" 82 83instance 84 by standard (simp add: bot_option_def) 85 86end 87 88instantiation option :: (order_top) order_top 89begin 90 91definition top_option where "\<top> = Some \<top>" 92 93instance 94 by standard (simp add: top_option_def less_eq_option_def split: option.split) 95 96end 97 98instance option :: (wellorder) wellorder 99proof 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 126qed 127 128instantiation option :: (inf) inf 129begin 130 131definition 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 134lemma inf_None_1 [simp, code]: "None \<sqinter> y = None" 135 by (simp add: inf_option_def) 136 137lemma inf_None_2 [simp, code]: "x \<sqinter> None = None" 138 by (cases x) (simp_all add: inf_option_def) 139 140lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)" 141 by (simp add: inf_option_def) 142 143instance .. 144 145end 146 147instantiation option :: (sup) sup 148begin 149 150definition 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 153lemma sup_None_1 [simp, code]: "None \<squnion> y = y" 154 by (simp add: sup_option_def) 155 156lemma sup_None_2 [simp, code]: "x \<squnion> None = x" 157 by (cases x) (simp_all add: sup_option_def) 158 159lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)" 160 by (simp add: sup_option_def) 161 162instance .. 163 164end 165 166instance option :: (semilattice_inf) semilattice_inf 167proof 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) 175qed 176 177instance option :: (semilattice_sup) semilattice_sup 178proof 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) 187qed 188 189instance option :: (lattice) lattice .. 190 191instance option :: (lattice) bounded_lattice_bot .. 192 193instance option :: (bounded_lattice_top) bounded_lattice_top .. 194 195instance option :: (bounded_lattice_top) bounded_lattice .. 196 197instance option :: (distrib_lattice) distrib_lattice 198proof 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) 202qed 203 204instantiation option :: (complete_lattice) complete_lattice 205begin 206 207definition 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 210lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None" 211 by (simp add: Inf_option_def) 212 213definition 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 216lemma empty_Sup [simp]: "\<Squnion>{} = None" 217 by (simp add: Sup_option_def) 218 219lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None" 220 by (simp add: Sup_option_def) 221 222instance 223proof 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) 228next 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 239next 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) 244next 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 261next 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) 266qed 267 268end 269 270lemma Some_Inf: 271 "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)" 272 by (auto simp add: Inf_option_def) 273 274lemma Some_Sup: 275 "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)" 276 by (auto simp add: Sup_option_def) 277 278lemma Some_INF: 279 "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))" 280 by (simp add: Some_Inf image_comp) 281 282lemma Some_SUP: 283 "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))" 284 by (simp add: Some_Sup image_comp) 285 286lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 287 for A :: "('a::complete_distrib_lattice option) set set" 288proof (cases "{} \<in> A") 289 case True 290 then show ?thesis 291 by (rule INF_lower2, simp_all) 292next 293 case False 294 from this have X: "{} \<notin> A" 295 by simp 296 then show ?thesis 297 proof (cases "{None} \<in> A") 298 case True 299 then show ?thesis 300 by (rule INF_lower2, simp_all) 301 next 302 case False 303 304 {fix y 305 assume A: "y \<in> A" 306 have "Sup (y - {None}) = Sup y" 307 by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq) 308 from A and this have "(\<exists>z. y - {None} = z - {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y - {None})" 309 by auto 310 } 311 from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})" 312 by (auto simp add: image_def) 313 314 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} 315 = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A" 316 by (rule exI, auto) 317 318 have [simp]: "\<And>y. y \<in> A \<Longrightarrow> 319 (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} 320 = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}" 321 apply (safe, blast) 322 by (rule arg_cong [of _ _ Sup], auto) 323 {fix y 324 assume [simp]: "y \<in> A" 325 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" 326 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}" 327 apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp) 328 by (rule exI [of _ "y - {None}"], simp) 329 } 330 from this have C: "(\<lambda>x. (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} = (Sup ` {the ` (y - {None}) |y. y \<in> A})" 331 by (simp add: image_def Option.these_def, safe, simp_all) 332 333 have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False" 334 by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq) 335 336 define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))" 337 338 have G: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> x . x \<in> Y - {None}" 339 by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq) 340 341 have F: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> (Y - {None})" 342 by (metis F_def G empty_iff some_in_eq) 343 344 have "Some \<bottom> \<le> Inf (F ` A)" 345 by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff 346 less_eq_option_Some singletonI) 347 348 from this have "Inf (F ` A) \<noteq> None" 349 by (cases "\<Sqinter>x\<in>A. F x", simp_all) 350 351 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}" 352 using F by auto 353 354 from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}" 355 by blast 356 357 from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False" 358 by blast 359 360 have [simp]: "((\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x) = None) = False" 361 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> 362 ex_in_conv option.simps(3)) 363 364 have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}) 365 = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})" 366 by (metis image_image these_image_Some_eq) 367 { 368 fix f 369 assume A: "\<And> Y . (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y" 370 371 have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))" 372 by (simp add: image_def) 373 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}))" 374 by blast 375 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" 376 by (simp add: image_def) 377 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" 378 by blast 379 380 { 381 fix Y 382 have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y" 383 using A [of "the ` (Y - {None})"] apply (simp add: image_def) 384 using option.collapse by fastforce 385 } 386 from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y" 387 by blast 388 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}" 389 by (simp add: Setcompr_eq_image) 390 391 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" 392 apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}"], safe) 393 by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y - {None})))) "], safe, simp_all) 394 395 { 396 fix xb 397 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}" 398 apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb - {None}. y = the x}"]) 399 by blast+ 400 } 401 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}))))" 402 apply (simp add: Inf_option_def image_def Option.these_def) 403 by (rule Inf_greatest, clarsimp) 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 (auto simp add: Option.these_def) 406 apply (rule imageI) 407 apply auto 408 using \<open>\<And>Y. Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y\<close> apply blast 409 apply (auto simp add: Some_INF [symmetric]) 410 done 411 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})" 412 by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all) 413 } 414 from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow> 415 (\<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})" 416 by blast 417 418 419 have [simp]: "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow> x \<noteq> {} \<and> x \<noteq> {None}" 420 using F by fastforce 421 422 have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))" 423 by (subst A, simp) 424 425 also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. if x = {} \<or> x = {None} then None else Some (\<Squnion>Option.these x))" 426 by (simp add: Sup_option_def) 427 428 also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))" 429 using G by fastforce 430 431 also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))" 432 by (simp add: Inf_option_def, safe) 433 434 also have "... = Some (\<Sqinter> ((\<lambda>x. (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))" 435 by (simp add: B) 436 437 also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y \<in> A}))" 438 by (unfold C, simp) 439 thm Inf_Sup 440 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) " 441 by (simp add: Inf_Sup) 442 443 also have "... \<le> \<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 444 proof (cases "\<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})") 445 case None 446 then show ?thesis by (simp add: less_eq_option_def) 447 next 448 case (Some a) 449 then show ?thesis 450 apply simp 451 apply (rule Sup_least, safe) 452 apply (simp add: Sup_option_def) 453 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) 454 by (drule X, simp) 455 qed 456 finally show ?thesis by simp 457 qed 458qed 459 460instance option :: (complete_distrib_lattice) complete_distrib_lattice 461 by (standard, simp add: option_Inf_Sup) 462 463instance option :: (complete_linorder) complete_linorder .. 464 465 466no_notation 467 bot ("\<bottom>") and 468 top ("\<top>") and 469 inf (infixl "\<sqinter>" 70) and 470 sup (infixl "\<squnion>" 65) and 471 Inf ("\<Sqinter> _" [900] 900) and 472 Sup ("\<Squnion> _" [900] 900) 473 474no_syntax 475 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 476 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 477 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 478 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 479 480end 481