src/HOL/Predicate.thy
author haftmann
Sun Aug 21 19:47:52 2011 +0200 (2011-08-21)
changeset 44363 53f4f8287606
parent 44033 bc45393f497b
child 44414 fb25c131bd73
permissions -rw-r--r--
avoid pred/set mixture
     1 (*  Title:      HOL/Predicate.thy
     2     Author:     Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Predicates as relations and enumerations *}
     6 
     7 theory Predicate
     8 imports Inductive Relation
     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 subsection {* Predicates as (complete) lattices *}
    27 
    28 text {*
    29   Handy introduction and elimination rules for @{text "\<le>"}
    30   on unary and binary predicates
    31 *}
    32 
    33 lemma predicate1I:
    34   assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    35   shows "P \<le> Q"
    36   apply (rule le_funI)
    37   apply (rule le_boolI)
    38   apply (rule PQ)
    39   apply assumption
    40   done
    41 
    42 lemma predicate1D [Pure.dest?, dest?]:
    43   "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    44   apply (erule le_funE)
    45   apply (erule le_boolE)
    46   apply assumption+
    47   done
    48 
    49 lemma rev_predicate1D:
    50   "P x ==> P <= Q ==> Q x"
    51   by (rule predicate1D)
    52 
    53 lemma predicate2I [Pure.intro!, intro!]:
    54   assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    55   shows "P \<le> Q"
    56   apply (rule le_funI)+
    57   apply (rule le_boolI)
    58   apply (rule PQ)
    59   apply assumption
    60   done
    61 
    62 lemma predicate2D [Pure.dest, dest]:
    63   "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    64   apply (erule le_funE)+
    65   apply (erule le_boolE)
    66   apply assumption+
    67   done
    68 
    69 lemma rev_predicate2D:
    70   "P x y ==> P <= Q ==> Q x y"
    71   by (rule predicate2D)
    72 
    73 
    74 subsubsection {* Equality *}
    75 
    76 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
    77   by (simp add: mem_def)
    78 
    79 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
    80   by (simp add: fun_eq_iff mem_def)
    81 
    82 
    83 subsubsection {* Order relation *}
    84 
    85 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
    86   by (simp add: mem_def)
    87 
    88 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
    89   by fast
    90 
    91 
    92 subsubsection {* Top and bottom elements *}
    93 
    94 lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
    95   by (simp add: bot_fun_def)
    96 
    97 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
    98   by (simp add: bot_fun_def)
    99 
   100 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   101   by (auto simp add: fun_eq_iff)
   102 
   103 lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
   104   by (auto simp add: fun_eq_iff)
   105 
   106 lemma top1I [intro!]: "top x"
   107   by (simp add: top_fun_def)
   108 
   109 lemma top2I [intro!]: "top x y"
   110   by (simp add: top_fun_def)
   111 
   112 
   113 subsubsection {* Binary intersection *}
   114 
   115 lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
   116   by (simp add: inf_fun_def)
   117 
   118 lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
   119   by (simp add: inf_fun_def)
   120 
   121 lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
   122   by (simp add: inf_fun_def)
   123 
   124 lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
   125   by (simp add: inf_fun_def)
   126 
   127 lemma inf1D1: "inf A B x ==> A x"
   128   by (simp add: inf_fun_def)
   129 
   130 lemma inf2D1: "inf A B x y ==> A x y"
   131   by (simp add: inf_fun_def)
   132 
   133 lemma inf1D2: "inf A B x ==> B x"
   134   by (simp add: inf_fun_def)
   135 
   136 lemma inf2D2: "inf A B x y ==> B x y"
   137   by (simp add: inf_fun_def)
   138 
   139 lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   140   by (simp add: inf_fun_def mem_def)
   141 
   142 lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   143   by (simp add: inf_fun_def mem_def)
   144 
   145 
   146 subsubsection {* Binary union *}
   147 
   148 lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
   149   by (simp add: sup_fun_def)
   150 
   151 lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
   152   by (simp add: sup_fun_def)
   153 
   154 lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
   155   by (simp add: sup_fun_def)
   156 
   157 lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
   158   by (simp add: sup_fun_def)
   159 
   160 lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
   161   by (simp add: sup_fun_def) iprover
   162 
   163 lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
   164   by (simp add: sup_fun_def) iprover
   165 
   166 text {*
   167   \medskip Classical introduction rule: no commitment to @{text A} vs
   168   @{text B}.
   169 *}
   170 
   171 lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
   172   by (auto simp add: sup_fun_def)
   173 
   174 lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
   175   by (auto simp add: sup_fun_def)
   176 
   177 lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   178   by (simp add: sup_fun_def mem_def)
   179 
   180 lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   181   by (simp add: sup_fun_def mem_def)
   182 
   183 
   184 subsubsection {* Intersections of families *}
   185 
   186 lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
   187   by (simp add: INFI_apply)
   188 
   189 lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
   190   by (simp add: INFI_apply)
   191 
   192 lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
   193   by (auto simp add: INFI_apply)
   194 
   195 lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
   196   by (auto simp add: INFI_apply)
   197 
   198 lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
   199   by (auto simp add: INFI_apply)
   200 
   201 lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
   202   by (auto simp add: INFI_apply)
   203 
   204 lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
   205   by (auto simp add: INFI_apply)
   206 
   207 lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
   208   by (auto simp add: INFI_apply)
   209 
   210 lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
   211   by (simp add: INFI_apply fun_eq_iff)
   212 
   213 lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
   214   by (simp add: INFI_apply fun_eq_iff)
   215 
   216 
   217 subsubsection {* Unions of families *}
   218 
   219 lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
   220   by (simp add: SUPR_apply)
   221 
   222 lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
   223   by (simp add: SUPR_apply)
   224 
   225 lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
   226   by (auto simp add: SUPR_apply)
   227 
   228 lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
   229   by (auto simp add: SUPR_apply)
   230 
   231 lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
   232   by (auto simp add: SUPR_apply)
   233 
   234 lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
   235   by (auto simp add: SUPR_apply)
   236 
   237 lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
   238   by (simp add: SUPR_apply fun_eq_iff)
   239 
   240 lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
   241   by (simp add: SUPR_apply fun_eq_iff)
   242 
   243 
   244 subsection {* Predicates as relations *}
   245 
   246 subsubsection {* Composition  *}
   247 
   248 inductive
   249   pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
   250     (infixr "OO" 75)
   251   for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
   252 where
   253   pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
   254 
   255 inductive_cases pred_compE [elim!]: "(r OO s) a c"
   256 
   257 lemma pred_comp_rel_comp_eq [pred_set_conv]:
   258   "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
   259   by (auto simp add: fun_eq_iff)
   260 
   261 
   262 subsubsection {* Converse *}
   263 
   264 inductive
   265   conversep :: "('a => 'b => bool) => 'b => 'a => bool"
   266     ("(_^--1)" [1000] 1000)
   267   for r :: "'a => 'b => bool"
   268 where
   269   conversepI: "r a b ==> r^--1 b a"
   270 
   271 notation (xsymbols)
   272   conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   273 
   274 lemma conversepD:
   275   assumes ab: "r^--1 a b"
   276   shows "r b a" using ab
   277   by cases simp
   278 
   279 lemma conversep_iff [iff]: "r^--1 a b = r b a"
   280   by (iprover intro: conversepI dest: conversepD)
   281 
   282 lemma conversep_converse_eq [pred_set_conv]:
   283   "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   284   by (auto simp add: fun_eq_iff)
   285 
   286 lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   287   by (iprover intro: order_antisym conversepI dest: conversepD)
   288 
   289 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   290   by (iprover intro: order_antisym conversepI pred_compI
   291     elim: pred_compE dest: conversepD)
   292 
   293 lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
   294   by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   295 
   296 lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
   297   by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   298 
   299 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
   300   by (auto simp add: fun_eq_iff)
   301 
   302 lemma conversep_eq [simp]: "(op =)^--1 = op ="
   303   by (auto simp add: fun_eq_iff)
   304 
   305 
   306 subsubsection {* Domain *}
   307 
   308 inductive
   309   DomainP :: "('a => 'b => bool) => 'a => bool"
   310   for r :: "'a => 'b => bool"
   311 where
   312   DomainPI [intro]: "r a b ==> DomainP r a"
   313 
   314 inductive_cases DomainPE [elim!]: "DomainP r a"
   315 
   316 lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
   317   by (blast intro!: Orderings.order_antisym predicate1I)
   318 
   319 
   320 subsubsection {* Range *}
   321 
   322 inductive
   323   RangeP :: "('a => 'b => bool) => 'b => bool"
   324   for r :: "'a => 'b => bool"
   325 where
   326   RangePI [intro]: "r a b ==> RangeP r b"
   327 
   328 inductive_cases RangePE [elim!]: "RangeP r b"
   329 
   330 lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
   331   by (blast intro!: Orderings.order_antisym predicate1I)
   332 
   333 
   334 subsubsection {* Inverse image *}
   335 
   336 definition
   337   inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
   338   "inv_imagep r f == %x y. r (f x) (f y)"
   339 
   340 lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
   341   by (simp add: inv_image_def inv_imagep_def)
   342 
   343 lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   344   by (simp add: inv_imagep_def)
   345 
   346 
   347 subsubsection {* Powerset *}
   348 
   349 definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   350   "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
   351 
   352 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   353   by (auto simp add: Powp_def fun_eq_iff)
   354 
   355 lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
   356 
   357 
   358 subsubsection {* Properties of relations *}
   359 
   360 abbreviation antisymP :: "('a => 'a => bool) => bool" where
   361   "antisymP r == antisym {(x, y). r x y}"
   362 
   363 abbreviation transP :: "('a => 'a => bool) => bool" where
   364   "transP r == trans {(x, y). r x y}"
   365 
   366 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   367   "single_valuedP r == single_valued {(x, y). r x y}"
   368 
   369 (*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
   370 
   371 definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   372   "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
   373 
   374 definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   375   "symp r \<longleftrightarrow> sym {(x, y). r x y}"
   376 
   377 definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   378   "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   379 
   380 lemma reflpI:
   381   "(\<And>x. r x x) \<Longrightarrow> reflp r"
   382   by (auto intro: refl_onI simp add: reflp_def)
   383 
   384 lemma reflpE:
   385   assumes "reflp r"
   386   obtains "r x x"
   387   using assms by (auto dest: refl_onD simp add: reflp_def)
   388 
   389 lemma sympI:
   390   "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
   391   by (auto intro: symI simp add: symp_def)
   392 
   393 lemma sympE:
   394   assumes "symp r" and "r x y"
   395   obtains "r y x"
   396   using assms by (auto dest: symD simp add: symp_def)
   397 
   398 lemma transpI:
   399   "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   400   by (auto intro: transI simp add: transp_def)
   401   
   402 lemma transpE:
   403   assumes "transp r" and "r x y" and "r y z"
   404   obtains "r x z"
   405   using assms by (auto dest: transD simp add: transp_def)
   406 
   407 
   408 subsection {* Predicates as enumerations *}
   409 
   410 subsubsection {* The type of predicate enumerations (a monad) *}
   411 
   412 datatype 'a pred = Pred "'a \<Rightarrow> bool"
   413 
   414 primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
   415   eval_pred: "eval (Pred f) = f"
   416 
   417 lemma Pred_eval [simp]:
   418   "Pred (eval x) = x"
   419   by (cases x) simp
   420 
   421 lemma pred_eqI:
   422   "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
   423   by (cases P, cases Q) (auto simp add: fun_eq_iff)
   424 
   425 instantiation pred :: (type) complete_lattice
   426 begin
   427 
   428 definition
   429   "P \<le> Q \<longleftrightarrow> eval P \<le> eval Q"
   430 
   431 definition
   432   "P < Q \<longleftrightarrow> eval P < eval Q"
   433 
   434 definition
   435   "\<bottom> = Pred \<bottom>"
   436 
   437 lemma eval_bot [simp]:
   438   "eval \<bottom>  = \<bottom>"
   439   by (simp add: bot_pred_def)
   440 
   441 definition
   442   "\<top> = Pred \<top>"
   443 
   444 lemma eval_top [simp]:
   445   "eval \<top>  = \<top>"
   446   by (simp add: top_pred_def)
   447 
   448 definition
   449   "P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)"
   450 
   451 lemma eval_inf [simp]:
   452   "eval (P \<sqinter> Q) = eval P \<sqinter> eval Q"
   453   by (simp add: inf_pred_def)
   454 
   455 definition
   456   "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
   457 
   458 lemma eval_sup [simp]:
   459   "eval (P \<squnion> Q) = eval P \<squnion> eval Q"
   460   by (simp add: sup_pred_def)
   461 
   462 definition
   463   "\<Sqinter>A = Pred (INFI A eval)"
   464 
   465 lemma eval_Inf [simp]:
   466   "eval (\<Sqinter>A) = INFI A eval"
   467   by (simp add: Inf_pred_def)
   468 
   469 definition
   470   "\<Squnion>A = Pred (SUPR A eval)"
   471 
   472 lemma eval_Sup [simp]:
   473   "eval (\<Squnion>A) = SUPR A eval"
   474   by (simp add: Sup_pred_def)
   475 
   476 instance proof
   477 qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def)
   478 
   479 end
   480 
   481 lemma eval_INFI [simp]:
   482   "eval (INFI A f) = INFI A (eval \<circ> f)"
   483   by (unfold INFI_def) simp
   484 
   485 lemma eval_SUPR [simp]:
   486   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   487   by (unfold SUPR_def) simp
   488 
   489 instantiation pred :: (type) complete_boolean_algebra
   490 begin
   491 
   492 definition
   493   "- P = Pred (- eval P)"
   494 
   495 lemma eval_compl [simp]:
   496   "eval (- P) = - eval P"
   497   by (simp add: uminus_pred_def)
   498 
   499 definition
   500   "P - Q = Pred (eval P - eval Q)"
   501 
   502 lemma eval_minus [simp]:
   503   "eval (P - Q) = eval P - eval Q"
   504   by (simp add: minus_pred_def)
   505 
   506 instance proof
   507 qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply)
   508 
   509 end
   510 
   511 definition single :: "'a \<Rightarrow> 'a pred" where
   512   "single x = Pred ((op =) x)"
   513 
   514 lemma eval_single [simp]:
   515   "eval (single x) = (op =) x"
   516   by (simp add: single_def)
   517 
   518 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   519   "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
   520 
   521 lemma eval_bind [simp]:
   522   "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
   523   by (simp add: bind_def)
   524 
   525 lemma bind_bind:
   526   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
   527   by (rule pred_eqI) auto
   528 
   529 lemma bind_single:
   530   "P \<guillemotright>= single = P"
   531   by (rule pred_eqI) auto
   532 
   533 lemma single_bind:
   534   "single x \<guillemotright>= P = P x"
   535   by (rule pred_eqI) auto
   536 
   537 lemma bottom_bind:
   538   "\<bottom> \<guillemotright>= P = \<bottom>"
   539   by (rule pred_eqI) auto
   540 
   541 lemma sup_bind:
   542   "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
   543   by (rule pred_eqI) auto
   544 
   545 lemma Sup_bind:
   546   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   547   by (rule pred_eqI) auto
   548 
   549 lemma pred_iffI:
   550   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
   551   and "\<And>x. eval B x \<Longrightarrow> eval A x"
   552   shows "A = B"
   553   using assms by (auto intro: pred_eqI)
   554   
   555 lemma singleI: "eval (single x) x"
   556   by simp
   557 
   558 lemma singleI_unit: "eval (single ()) x"
   559   by simp
   560 
   561 lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P"
   562   by simp
   563 
   564 lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   565   by simp
   566 
   567 lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
   568   by auto
   569 
   570 lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   571   by auto
   572 
   573 lemma botE: "eval \<bottom> x \<Longrightarrow> P"
   574   by auto
   575 
   576 lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
   577   by auto
   578 
   579 lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
   580   by auto
   581 
   582 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   583   by auto
   584 
   585 lemma single_not_bot [simp]:
   586   "single x \<noteq> \<bottom>"
   587   by (auto simp add: single_def bot_pred_def fun_eq_iff)
   588 
   589 lemma not_bot:
   590   assumes "A \<noteq> \<bottom>"
   591   obtains x where "eval A x"
   592   using assms by (cases A)
   593     (auto simp add: bot_pred_def, auto simp add: mem_def)
   594   
   595 
   596 subsubsection {* Emptiness check and definite choice *}
   597 
   598 definition is_empty :: "'a pred \<Rightarrow> bool" where
   599   "is_empty A \<longleftrightarrow> A = \<bottom>"
   600 
   601 lemma is_empty_bot:
   602   "is_empty \<bottom>"
   603   by (simp add: is_empty_def)
   604 
   605 lemma not_is_empty_single:
   606   "\<not> is_empty (single x)"
   607   by (auto simp add: is_empty_def single_def bot_pred_def fun_eq_iff)
   608 
   609 lemma is_empty_sup:
   610   "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
   611   by (auto simp add: is_empty_def)
   612 
   613 definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
   614   "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
   615 
   616 lemma singleton_eqI:
   617   "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x"
   618   by (auto simp add: singleton_def)
   619 
   620 lemma eval_singletonI:
   621   "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
   622 proof -
   623   assume assm: "\<exists>!x. eval A x"
   624   then obtain x where "eval A x" ..
   625   moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
   626   ultimately show ?thesis by simp 
   627 qed
   628 
   629 lemma single_singleton:
   630   "\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A"
   631 proof -
   632   assume assm: "\<exists>!x. eval A x"
   633   then have "eval A (singleton dfault A)"
   634     by (rule eval_singletonI)
   635   moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
   636     by (rule singleton_eqI)
   637   ultimately have "eval (single (singleton dfault A)) = eval A"
   638     by (simp (no_asm_use) add: single_def fun_eq_iff) blast
   639   then have "\<And>x. eval (single (singleton dfault A)) x = eval A x"
   640     by simp
   641   then show ?thesis by (rule pred_eqI)
   642 qed
   643 
   644 lemma singleton_undefinedI:
   645   "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()"
   646   by (simp add: singleton_def)
   647 
   648 lemma singleton_bot:
   649   "singleton dfault \<bottom> = dfault ()"
   650   by (auto simp add: bot_pred_def intro: singleton_undefinedI)
   651 
   652 lemma singleton_single:
   653   "singleton dfault (single x) = x"
   654   by (auto simp add: intro: singleton_eqI singleI elim: singleE)
   655 
   656 lemma singleton_sup_single_single:
   657   "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())"
   658 proof (cases "x = y")
   659   case True then show ?thesis by (simp add: singleton_single)
   660 next
   661   case False
   662   have "eval (single x \<squnion> single y) x"
   663     and "eval (single x \<squnion> single y) y"
   664   by (auto intro: supI1 supI2 singleI)
   665   with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
   666     by blast
   667   then have "singleton dfault (single x \<squnion> single y) = dfault ()"
   668     by (rule singleton_undefinedI)
   669   with False show ?thesis by simp
   670 qed
   671 
   672 lemma singleton_sup_aux:
   673   "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
   674     else if B = \<bottom> then singleton dfault A
   675     else singleton dfault
   676       (single (singleton dfault A) \<squnion> single (singleton dfault B)))"
   677 proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
   678   case True then show ?thesis by (simp add: single_singleton)
   679 next
   680   case False
   681   from False have A_or_B:
   682     "singleton dfault A = dfault () \<or> singleton dfault B = dfault ()"
   683     by (auto intro!: singleton_undefinedI)
   684   then have rhs: "singleton dfault
   685     (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()"
   686     by (auto simp add: singleton_sup_single_single singleton_single)
   687   from False have not_unique:
   688     "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
   689   show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
   690     case True
   691     then obtain a b where a: "eval A a" and b: "eval B b"
   692       by (blast elim: not_bot)
   693     with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
   694       by (auto simp add: sup_pred_def bot_pred_def)
   695     then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI)
   696     with True rhs show ?thesis by simp
   697   next
   698     case False then show ?thesis by auto
   699   qed
   700 qed
   701 
   702 lemma singleton_sup:
   703   "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
   704     else if B = \<bottom> then singleton dfault A
   705     else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())"
   706 using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
   707 
   708 
   709 subsubsection {* Derived operations *}
   710 
   711 definition if_pred :: "bool \<Rightarrow> unit pred" where
   712   if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
   713 
   714 definition holds :: "unit pred \<Rightarrow> bool" where
   715   holds_eq: "holds P = eval P ()"
   716 
   717 definition not_pred :: "unit pred \<Rightarrow> unit pred" where
   718   not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
   719 
   720 lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()"
   721   unfolding if_pred_eq by (auto intro: singleI)
   722 
   723 lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
   724   unfolding if_pred_eq by (cases b) (auto elim: botE)
   725 
   726 lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()"
   727   unfolding not_pred_eq eval_pred by (auto intro: singleI)
   728 
   729 lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()"
   730   unfolding not_pred_eq by (auto intro: singleI)
   731 
   732 lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   733   unfolding not_pred_eq
   734   by (auto split: split_if_asm elim: botE)
   735 
   736 lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   737   unfolding not_pred_eq
   738   by (auto split: split_if_asm elim: botE)
   739 lemma "f () = False \<or> f () = True"
   740 by simp
   741 
   742 lemma closure_of_bool_cases [no_atp]:
   743   fixes f :: "unit \<Rightarrow> bool"
   744   assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
   745   assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
   746   shows "P f"
   747 proof -
   748   have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
   749     apply (cases "f ()")
   750     apply (rule disjI2)
   751     apply (rule ext)
   752     apply (simp add: unit_eq)
   753     apply (rule disjI1)
   754     apply (rule ext)
   755     apply (simp add: unit_eq)
   756     done
   757   from this assms show ?thesis by blast
   758 qed
   759 
   760 lemma unit_pred_cases:
   761   assumes "P \<bottom>"
   762   assumes "P (single ())"
   763   shows "P Q"
   764 using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
   765   fix f
   766   assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
   767   then have "P (Pred f)" 
   768     by (cases _ f rule: closure_of_bool_cases) simp_all
   769   moreover assume "Q = Pred f"
   770   ultimately show "P Q" by simp
   771 qed
   772   
   773 lemma holds_if_pred:
   774   "holds (if_pred b) = b"
   775 unfolding if_pred_eq holds_eq
   776 by (cases b) (auto intro: singleI elim: botE)
   777 
   778 lemma if_pred_holds:
   779   "if_pred (holds P) = P"
   780 unfolding if_pred_eq holds_eq
   781 by (rule unit_pred_cases) (auto intro: singleI elim: botE)
   782 
   783 lemma is_empty_holds:
   784   "is_empty P \<longleftrightarrow> \<not> holds P"
   785 unfolding is_empty_def holds_eq
   786 by (rule unit_pred_cases) (auto elim: botE intro: singleI)
   787 
   788 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
   789   "map f P = P \<guillemotright>= (single o f)"
   790 
   791 lemma eval_map [simp]:
   792   "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
   793   by (auto simp add: map_def)
   794 
   795 enriched_type map: map
   796   by (rule ext, rule pred_eqI, auto)+
   797 
   798 
   799 subsubsection {* Implementation *}
   800 
   801 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
   802 
   803 primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
   804     "pred_of_seq Empty = \<bottom>"
   805   | "pred_of_seq (Insert x P) = single x \<squnion> P"
   806   | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
   807 
   808 definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
   809   "Seq f = pred_of_seq (f ())"
   810 
   811 code_datatype Seq
   812 
   813 primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool"  where
   814   "member Empty x \<longleftrightarrow> False"
   815   | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
   816   | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
   817 
   818 lemma eval_member:
   819   "member xq = eval (pred_of_seq xq)"
   820 proof (induct xq)
   821   case Empty show ?case
   822   by (auto simp add: fun_eq_iff elim: botE)
   823 next
   824   case Insert show ?case
   825   by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI)
   826 next
   827   case Join then show ?case
   828   by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2)
   829 qed
   830 
   831 lemma eval_code [code]: "eval (Seq f) = member (f ())"
   832   unfolding Seq_def by (rule sym, rule eval_member)
   833 
   834 lemma single_code [code]:
   835   "single x = Seq (\<lambda>u. Insert x \<bottom>)"
   836   unfolding Seq_def by simp
   837 
   838 primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   839     "apply f Empty = Empty"
   840   | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
   841   | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
   842 
   843 lemma apply_bind:
   844   "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
   845 proof (induct xq)
   846   case Empty show ?case
   847     by (simp add: bottom_bind)
   848 next
   849   case Insert show ?case
   850     by (simp add: single_bind sup_bind)
   851 next
   852   case Join then show ?case
   853     by (simp add: sup_bind)
   854 qed
   855   
   856 lemma bind_code [code]:
   857   "Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))"
   858   unfolding Seq_def by (rule sym, rule apply_bind)
   859 
   860 lemma bot_set_code [code]:
   861   "\<bottom> = Seq (\<lambda>u. Empty)"
   862   unfolding Seq_def by simp
   863 
   864 primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
   865     "adjunct P Empty = Join P Empty"
   866   | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
   867   | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
   868 
   869 lemma adjunct_sup:
   870   "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
   871   by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute)
   872 
   873 lemma sup_code [code]:
   874   "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f ()
   875     of Empty \<Rightarrow> g ()
   876      | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
   877      | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))"
   878 proof (cases "f ()")
   879   case Empty
   880   thus ?thesis
   881     unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
   882 next
   883   case Insert
   884   thus ?thesis
   885     unfolding Seq_def by (simp add: sup_assoc)
   886 next
   887   case Join
   888   thus ?thesis
   889     unfolding Seq_def
   890     by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
   891 qed
   892 
   893 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   894     "contained Empty Q \<longleftrightarrow> True"
   895   | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
   896   | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
   897 
   898 lemma single_less_eq_eval:
   899   "single x \<le> P \<longleftrightarrow> eval P x"
   900   by (auto simp add: single_def less_eq_pred_def mem_def)
   901 
   902 lemma contained_less_eq:
   903   "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
   904   by (induct xq) (simp_all add: single_less_eq_eval)
   905 
   906 lemma less_eq_pred_code [code]:
   907   "Seq f \<le> Q = (case f ()
   908    of Empty \<Rightarrow> True
   909     | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q
   910     | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)"
   911   by (cases "f ()")
   912     (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
   913 
   914 lemma eq_pred_code [code]:
   915   fixes P Q :: "'a pred"
   916   shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
   917   by (auto simp add: equal)
   918 
   919 lemma [code nbe]:
   920   "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
   921   by (fact equal_refl)
   922 
   923 lemma [code]:
   924   "pred_case f P = f (eval P)"
   925   by (cases P) simp
   926 
   927 lemma [code]:
   928   "pred_rec f P = f (eval P)"
   929   by (cases P) simp
   930 
   931 inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
   932 
   933 lemma eq_is_eq: "eq x y \<equiv> (x = y)"
   934   by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
   935 
   936 primrec null :: "'a seq \<Rightarrow> bool" where
   937     "null Empty \<longleftrightarrow> True"
   938   | "null (Insert x P) \<longleftrightarrow> False"
   939   | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
   940 
   941 lemma null_is_empty:
   942   "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
   943   by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
   944 
   945 lemma is_empty_code [code]:
   946   "is_empty (Seq f) \<longleftrightarrow> null (f ())"
   947   by (simp add: null_is_empty Seq_def)
   948 
   949 primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
   950   [code del]: "the_only dfault Empty = dfault ()"
   951   | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
   952   | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
   953        else let x = singleton dfault P; y = the_only dfault xq in
   954        if x = y then x else dfault ())"
   955 
   956 lemma the_only_singleton:
   957   "the_only dfault xq = singleton dfault (pred_of_seq xq)"
   958   by (induct xq)
   959     (auto simp add: singleton_bot singleton_single is_empty_def
   960     null_is_empty Let_def singleton_sup)
   961 
   962 lemma singleton_code [code]:
   963   "singleton dfault (Seq f) = (case f ()
   964    of Empty \<Rightarrow> dfault ()
   965     | Insert x P \<Rightarrow> if is_empty P then x
   966         else let y = singleton dfault P in
   967           if x = y then x else dfault ()
   968     | Join P xq \<Rightarrow> if is_empty P then the_only dfault xq
   969         else if null xq then singleton dfault P
   970         else let x = singleton dfault P; y = the_only dfault xq in
   971           if x = y then x else dfault ())"
   972   by (cases "f ()")
   973    (auto simp add: Seq_def the_only_singleton is_empty_def
   974       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
   975 
   976 definition not_unique :: "'a pred => 'a"
   977 where
   978   [code del]: "not_unique A = (THE x. eval A x)"
   979 
   980 definition the :: "'a pred => 'a"
   981 where
   982   "the A = (THE x. eval A x)"
   983 
   984 lemma the_eqI:
   985   "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   986   by (simp add: the_def)
   987 
   988 lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
   989   by (rule the_eqI) (simp add: singleton_def not_unique_def)
   990 
   991 code_abort not_unique
   992 
   993 code_reflect Predicate
   994   datatypes pred = Seq and seq = Empty | Insert | Join
   995   functions map
   996 
   997 ML {*
   998 signature PREDICATE =
   999 sig
  1000   datatype 'a pred = Seq of (unit -> 'a seq)
  1001   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
  1002   val yield: 'a pred -> ('a * 'a pred) option
  1003   val yieldn: int -> 'a pred -> 'a list * 'a pred
  1004   val map: ('a -> 'b) -> 'a pred -> 'b pred
  1005 end;
  1006 
  1007 structure Predicate : PREDICATE =
  1008 struct
  1009 
  1010 datatype pred = datatype Predicate.pred
  1011 datatype seq = datatype Predicate.seq
  1012 
  1013 fun map f = Predicate.map f;
  1014 
  1015 fun yield (Seq f) = next (f ())
  1016 and next Empty = NONE
  1017   | next (Insert (x, P)) = SOME (x, P)
  1018   | next (Join (P, xq)) = (case yield P
  1019      of NONE => next xq
  1020       | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
  1021 
  1022 fun anamorph f k x = (if k = 0 then ([], x)
  1023   else case f x
  1024    of NONE => ([], x)
  1025     | SOME (v, y) => let
  1026         val (vs, z) = anamorph f (k - 1) y
  1027       in (v :: vs, z) end);
  1028 
  1029 fun yieldn P = anamorph yield P;
  1030 
  1031 end;
  1032 *}
  1033 
  1034 lemma eval_mem [simp]:
  1035   "x \<in> eval P \<longleftrightarrow> eval P x"
  1036   by (simp add: mem_def)
  1037 
  1038 lemma eq_mem [simp]:
  1039   "x \<in> (op =) y \<longleftrightarrow> x = y"
  1040   by (auto simp add: mem_def)
  1041 
  1042 no_notation
  1043   bot ("\<bottom>") and
  1044   top ("\<top>") and
  1045   inf (infixl "\<sqinter>" 70) and
  1046   sup (infixl "\<squnion>" 65) and
  1047   Inf ("\<Sqinter>_" [900] 900) and
  1048   Sup ("\<Squnion>_" [900] 900) and
  1049   bind (infixl "\<guillemotright>=" 70)
  1050 
  1051 no_syntax (xsymbols)
  1052   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  1053   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
  1054   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  1055   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
  1056 
  1057 hide_type (open) pred seq
  1058 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
  1059   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
  1060 
  1061 end