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