src/HOL/Relation.thy
 changeset 46664 1f6c140f9c72 parent 46638 fc315796794e child 46689 f559866a7aa2
```     1.1 --- a/src/HOL/Relation.thy	Fri Feb 24 22:46:16 2012 +0100
1.2 +++ b/src/HOL/Relation.thy	Fri Feb 24 22:46:44 2012 +0100
1.3 @@ -1,15 +1,107 @@
1.4  (*  Title:      HOL/Relation.thy
1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.6 -    Copyright   1996  University of Cambridge
1.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
1.8  *)
1.9
1.11 +header {* Relations – as sets of pairs, and binary predicates *}
1.12
1.13  theory Relation
1.14  imports Datatype Finite_Set
1.15  begin
1.16
1.17 -subsection {* Definitions *}
1.18 +notation
1.19 +  bot ("\<bottom>") and
1.20 +  top ("\<top>") and
1.21 +  inf (infixl "\<sqinter>" 70) and
1.22 +  sup (infixl "\<squnion>" 65) and
1.23 +  Inf ("\<Sqinter>_" [900] 900) and
1.24 +  Sup ("\<Squnion>_" [900] 900)
1.25 +
1.26 +syntax (xsymbols)
1.27 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
1.28 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
1.29 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
1.30 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
1.31 +
1.32 +
1.33 +subsection {* Classical rules for reasoning on predicates *}
1.34 +
1.35 +declare predicate1D [Pure.dest?, dest?]
1.36 +declare predicate2I [Pure.intro!, intro!]
1.37 +declare predicate2D [Pure.dest, dest]
1.38 +declare bot1E [elim!]
1.39 +declare bot2E [elim!]
1.40 +declare top1I [intro!]
1.41 +declare top2I [intro!]
1.42 +declare inf1I [intro!]
1.43 +declare inf2I [intro!]
1.44 +declare inf1E [elim!]
1.45 +declare inf2E [elim!]
1.46 +declare sup1I1 [intro?]
1.47 +declare sup2I1 [intro?]
1.48 +declare sup1I2 [intro?]
1.49 +declare sup2I2 [intro?]
1.50 +declare sup1E [elim!]
1.51 +declare sup2E [elim!]
1.52 +declare sup1CI [intro!]
1.53 +declare sup2CI [intro!]
1.54 +declare INF1_I [intro!]
1.55 +declare INF2_I [intro!]
1.56 +declare INF1_D [elim]
1.57 +declare INF2_D [elim]
1.58 +declare INF1_E [elim]
1.59 +declare INF2_E [elim]
1.60 +declare SUP1_I [intro]
1.61 +declare SUP2_I [intro]
1.62 +declare SUP1_E [elim!]
1.63 +declare SUP2_E [elim!]
1.64 +
1.65 +
1.66 +subsection {* Conversions between set and predicate relations *}
1.67 +
1.68 +lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
1.69 +  by (simp add: set_eq_iff fun_eq_iff)
1.70 +
1.71 +lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
1.72 +  by (simp add: set_eq_iff fun_eq_iff)
1.73 +
1.74 +lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
1.75 +  by (simp add: subset_iff le_fun_def)
1.76 +
1.77 +lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
1.78 +  by (simp add: subset_iff le_fun_def)
1.79 +
1.80 +lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
1.81 +  by (auto simp add: fun_eq_iff)
1.82 +
1.83 +lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
1.84 +  by (auto simp add: fun_eq_iff)
1.85 +
1.86 +lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
1.87 +  by (simp add: inf_fun_def)
1.88 +
1.89 +lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
1.90 +  by (simp add: inf_fun_def)
1.91 +
1.92 +lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
1.93 +  by (simp add: sup_fun_def)
1.94 +
1.95 +lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
1.96 +  by (simp add: sup_fun_def)
1.97 +
1.98 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
1.99 +  by (simp add: INF_apply fun_eq_iff)
1.100 +
1.101 +lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
1.102 +  by (simp add: INF_apply fun_eq_iff)
1.103 +
1.104 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
1.105 +  by (simp add: SUP_apply fun_eq_iff)
1.106 +
1.107 +lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
1.108 +  by (simp add: SUP_apply fun_eq_iff)
1.109 +
1.110 +
1.111 +subsection {* Relations as sets of pairs *}
1.112
1.113  type_synonym 'a rel = "('a * 'a) set"
1.114
1.115 @@ -90,7 +182,7 @@
1.116    "inv_image r f = {(x, y). (f x, f y) : r}"
1.117
1.118
1.119 -subsection {* The identity relation *}
1.120 +subsubsection {* The identity relation *}
1.121
1.122  lemma IdI [intro]: "(a, a) : Id"
1.124 @@ -115,7 +207,7 @@
1.126
1.127
1.128 -subsection {* Diagonal: identity over a set *}
1.129 +subsubsection {* Diagonal: identity over a set *}
1.130
1.131  lemma Id_on_empty [simp]: "Id_on {} = {}"
1.133 @@ -142,7 +234,7 @@
1.134  by blast
1.135
1.136
1.137 -subsection {* Composition of two relations *}
1.138 +subsubsection {* Composition of two relations *}
1.139
1.140  lemma rel_compI [intro]:
1.141    "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
1.142 @@ -194,7 +286,7 @@
1.143  by auto
1.144
1.145
1.146 -subsection {* Reflexivity *}
1.147 +subsubsection {* Reflexivity *}
1.148
1.149  lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
1.150  by (unfold refl_on_def) (iprover intro!: ballI)
1.151 @@ -232,7 +324,8 @@
1.152    "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
1.153  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
1.154
1.155 -subsection {* Antisymmetry *}
1.156 +
1.157 +subsubsection {* Antisymmetry *}
1.158
1.159  lemma antisymI:
1.160    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
1.161 @@ -251,7 +344,7 @@
1.162  by (unfold antisym_def) blast
1.163
1.164
1.165 -subsection {* Symmetry *}
1.166 +subsubsection {* Symmetry *}
1.167
1.168  lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
1.169  by (unfold sym_def) iprover
1.170 @@ -275,7 +368,7 @@
1.171  by (rule symI) clarify
1.172
1.173
1.174 -subsection {* Transitivity *}
1.175 +subsubsection {* Transitivity *}
1.176
1.177  lemma trans_join [code]:
1.178    "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
1.179 @@ -300,7 +393,8 @@
1.180  lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
1.181  unfolding antisym_def trans_def by blast
1.182
1.183 -subsection {* Irreflexivity *}
1.184 +
1.185 +subsubsection {* Irreflexivity *}
1.186
1.187  lemma irrefl_distinct [code]:
1.188    "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
1.189 @@ -310,7 +404,7 @@
1.191
1.192
1.193 -subsection {* Totality *}
1.194 +subsubsection {* Totality *}
1.195
1.196  lemma total_on_empty[simp]: "total_on {} r"
1.198 @@ -318,7 +412,8 @@
1.199  lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
1.201
1.202 -subsection {* Converse *}
1.203 +
1.204 +subsubsection {* Converse *}
1.205
1.206  lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
1.208 @@ -383,7 +478,7 @@
1.209  by (auto simp: total_on_def)
1.210
1.211
1.212 -subsection {* Domain *}
1.213 +subsubsection {* Domain *}
1.214
1.215  declare Domain_def [no_atp]
1.216
1.217 @@ -444,7 +539,7 @@
1.218  by auto
1.219
1.220
1.221 -subsection {* Range *}
1.222 +subsubsection {* Range *}
1.223
1.224  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
1.225  by (simp add: Domain_def Range_def)
1.226 @@ -493,7 +588,7 @@
1.227    by force
1.228
1.229
1.230 -subsection {* Field *}
1.231 +subsubsection {* Field *}
1.232
1.233  lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
1.234  by(auto simp:Field_def Domain_def Range_def)
1.235 @@ -514,7 +609,7 @@
1.236  by(auto simp:Field_def)
1.237
1.238
1.239 -subsection {* Image of a set under a relation *}
1.240 +subsubsection {* Image of a set under a relation *}
1.241
1.242  declare Image_def [no_atp]
1.243
1.244 @@ -588,7 +683,7 @@
1.245  by blast
1.246
1.247
1.248 -subsection {* Single valued relations *}
1.249 +subsubsection {* Single valued relations *}
1.250
1.251  lemma single_valuedI:
1.252    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
1.253 @@ -613,7 +708,7 @@
1.254  by (unfold single_valued_def) blast
1.255
1.256
1.257 -subsection {* Graphs given by @{text Collect} *}
1.258 +subsubsection {* Graphs given by @{text Collect} *}
1.259
1.260  lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
1.261  by auto
1.262 @@ -625,7 +720,7 @@
1.263  by auto
1.264
1.265
1.266 -subsection {* Inverse image *}
1.267 +subsubsection {* Inverse image *}
1.268
1.269  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
1.270  by (unfold sym_def inv_image_def) blast
1.271 @@ -643,7 +738,7 @@
1.272  unfolding inv_image_def converse_def by auto
1.273
1.274
1.275 -subsection {* Finiteness *}
1.276 +subsubsection {* Finiteness *}
1.277
1.278  lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.279    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
1.280 @@ -671,7 +766,7 @@
1.281    done
1.282
1.283
1.284 -subsection {* Miscellaneous *}
1.285 +subsubsection {* Miscellaneous *}
1.286
1.287  text {* Version of @{thm[source] lfp_induct} for binary relations *}
1.288
1.289 @@ -683,4 +778,171 @@
1.290  lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
1.291  by auto
1.292
1.293 +
1.294 +subsection {* Relations as binary predicates *}
1.295 +
1.296 +subsubsection {* Composition *}
1.297 +
1.298 +inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
1.299 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
1.300 +  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
1.301 +
1.302 +inductive_cases pred_compE [elim!]: "(r OO s) a c"
1.303 +
1.304 +lemma pred_comp_rel_comp_eq [pred_set_conv]:
1.305 +  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
1.306 +  by (auto simp add: fun_eq_iff)
1.307 +
1.308 +
1.309 +subsubsection {* Converse *}
1.310 +
1.311 +inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
1.312 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.313 +  conversepI: "r a b \<Longrightarrow> r^--1 b a"
1.314 +
1.315 +notation (xsymbols)
1.316 +  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
1.317 +
1.318 +lemma conversepD:
1.319 +  assumes ab: "r^--1 a b"
1.320 +  shows "r b a" using ab
1.321 +  by cases simp
1.322 +
1.323 +lemma conversep_iff [iff]: "r^--1 a b = r b a"
1.324 +  by (iprover intro: conversepI dest: conversepD)
1.325 +
1.326 +lemma conversep_converse_eq [pred_set_conv]:
1.327 +  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
1.328 +  by (auto simp add: fun_eq_iff)
1.329 +
1.330 +lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
1.331 +  by (iprover intro: order_antisym conversepI dest: conversepD)
1.332 +
1.333 +lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
1.334 +  by (iprover intro: order_antisym conversepI pred_compI
1.335 +    elim: pred_compE dest: conversepD)
1.336 +
1.337 +lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
1.338 +  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
1.339 +
1.340 +lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
1.341 +  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
1.342 +
1.343 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
1.344 +  by (auto simp add: fun_eq_iff)
1.345 +
1.346 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
1.347 +  by (auto simp add: fun_eq_iff)
1.348 +
1.349 +
1.350 +subsubsection {* Domain *}
1.351 +
1.352 +inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
1.353 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.354 +  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
1.355 +
1.356 +inductive_cases DomainPE [elim!]: "DomainP r a"
1.357 +
1.358 +lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
1.359 +  by (blast intro!: Orderings.order_antisym predicate1I)
1.360 +
1.361 +
1.362 +subsubsection {* Range *}
1.363 +
1.364 +inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
1.365 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.366 +  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
1.367 +
1.368 +inductive_cases RangePE [elim!]: "RangeP r b"
1.369 +
1.370 +lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
1.371 +  by (blast intro!: Orderings.order_antisym predicate1I)
1.372 +
1.373 +
1.374 +subsubsection {* Inverse image *}
1.375 +
1.376 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
1.377 +  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
1.378 +
1.379 +lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
1.380 +  by (simp add: inv_image_def inv_imagep_def)
1.381 +
1.382 +lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
1.383 +  by (simp add: inv_imagep_def)
1.384 +
1.385 +
1.386 +subsubsection {* Powerset *}
1.387 +
1.388 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
1.389 +  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
1.390 +
1.391 +lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
1.392 +  by (auto simp add: Powp_def fun_eq_iff)
1.393 +
1.394 +lemmas Powp_mono [mono] = Pow_mono [to_pred]
1.395 +
1.396 +
1.397 +subsubsection {* Properties of predicate relations *}
1.398 +
1.399 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.400 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
1.401 +
1.402 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.403 +  "transP r \<equiv> trans {(x, y). r x y}"
1.404 +
1.405 +abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
1.406 +  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
1.407 +
1.408 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
1.409 +
1.410 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.411 +  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
1.412 +
1.413 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.414 +  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
1.415 +
1.416 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.417 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
1.418 +
1.419 +lemma reflpI:
1.420 +  "(\<And>x. r x x) \<Longrightarrow> reflp r"
1.421 +  by (auto intro: refl_onI simp add: reflp_def)
1.422 +
1.423 +lemma reflpE:
1.424 +  assumes "reflp r"
1.425 +  obtains "r x x"
1.426 +  using assms by (auto dest: refl_onD simp add: reflp_def)
1.427 +
1.428 +lemma sympI:
1.429 +  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
1.430 +  by (auto intro: symI simp add: symp_def)
1.431 +
1.432 +lemma sympE:
1.433 +  assumes "symp r" and "r x y"
1.434 +  obtains "r y x"
1.435 +  using assms by (auto dest: symD simp add: symp_def)
1.436 +
1.437 +lemma transpI:
1.438 +  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
1.439 +  by (auto intro: transI simp add: transp_def)
1.440 +
1.441 +lemma transpE:
1.442 +  assumes "transp r" and "r x y" and "r y z"
1.443 +  obtains "r x z"
1.444 +  using assms by (auto dest: transD simp add: transp_def)
1.445 +
1.446 +no_notation
1.447 +  bot ("\<bottom>") and
1.448 +  top ("\<top>") and
1.449 +  inf (infixl "\<sqinter>" 70) and
1.450 +  sup (infixl "\<squnion>" 65) and
1.451 +  Inf ("\<Sqinter>_" [900] 900) and
1.452 +  Sup ("\<Squnion>_" [900] 900)
1.453 +
1.454 +no_syntax (xsymbols)
1.455 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
1.456 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
1.457 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
1.458 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
1.459 +
1.460  end
```