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