src/HOL/Predicate.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45630 0dd654a01217
child 45970 b6d0cff57d96
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    77   by (simp add: set_eq_iff fun_eq_iff 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)) \<longleftrightarrow> (R = S)"
    80   by (simp add: set_eq_iff fun_eq_iff mem_def)
    81 
    82 
    83 subsubsection {* Order relation *}
    84 
    85 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    86   by (simp add: subset_iff le_fun_def mem_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 mem_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: "(\<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 mem_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 mem_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: "(\<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 mem_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 mem_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: "(\<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: "(\<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 pred_subset_eq]
   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 instantiation pred :: (type) complete_lattice
   415 begin
   416 
   417 definition
   418   "P \<le> Q \<longleftrightarrow> eval P \<le> eval Q"
   419 
   420 definition
   421   "P < Q \<longleftrightarrow> eval P < eval Q"
   422 
   423 definition
   424   "\<bottom> = Pred \<bottom>"
   425 
   426 lemma eval_bot [simp]:
   427   "eval \<bottom>  = \<bottom>"
   428   by (simp add: bot_pred_def)
   429 
   430 definition
   431   "\<top> = Pred \<top>"
   432 
   433 lemma eval_top [simp]:
   434   "eval \<top>  = \<top>"
   435   by (simp add: top_pred_def)
   436 
   437 definition
   438   "P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)"
   439 
   440 lemma eval_inf [simp]:
   441   "eval (P \<sqinter> Q) = eval P \<sqinter> eval Q"
   442   by (simp add: inf_pred_def)
   443 
   444 definition
   445   "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
   446 
   447 lemma eval_sup [simp]:
   448   "eval (P \<squnion> Q) = eval P \<squnion> eval Q"
   449   by (simp add: sup_pred_def)
   450 
   451 definition
   452   "\<Sqinter>A = Pred (INFI A eval)"
   453 
   454 lemma eval_Inf [simp]:
   455   "eval (\<Sqinter>A) = INFI A eval"
   456   by (simp add: Inf_pred_def)
   457 
   458 definition
   459   "\<Squnion>A = Pred (SUPR A eval)"
   460 
   461 lemma eval_Sup [simp]:
   462   "eval (\<Squnion>A) = SUPR A eval"
   463   by (simp add: Sup_pred_def)
   464 
   465 instance proof
   466 qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def le_fun_def less_fun_def)
   467 
   468 end
   469 
   470 lemma eval_INFI [simp]:
   471   "eval (INFI A f) = INFI A (eval \<circ> f)"
   472   by (simp only: INF_def eval_Inf image_compose)
   473 
   474 lemma eval_SUPR [simp]:
   475   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   476   by (simp only: SUP_def eval_Sup image_compose)
   477 
   478 instantiation pred :: (type) complete_boolean_algebra
   479 begin
   480 
   481 definition
   482   "- P = Pred (- eval P)"
   483 
   484 lemma eval_compl [simp]:
   485   "eval (- P) = - eval P"
   486   by (simp add: uminus_pred_def)
   487 
   488 definition
   489   "P - Q = Pred (eval P - eval Q)"
   490 
   491 lemma eval_minus [simp]:
   492   "eval (P - Q) = eval P - eval Q"
   493   by (simp add: minus_pred_def)
   494 
   495 instance proof
   496 qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
   497 
   498 end
   499 
   500 definition single :: "'a \<Rightarrow> 'a pred" where
   501   "single x = Pred ((op =) x)"
   502 
   503 lemma eval_single [simp]:
   504   "eval (single x) = (op =) x"
   505   by (simp add: single_def)
   506 
   507 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   508   "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
   509 
   510 lemma eval_bind [simp]:
   511   "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
   512   by (simp add: bind_def)
   513 
   514 lemma bind_bind:
   515   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
   516   by (rule pred_eqI) (auto simp add: SUP_apply)
   517 
   518 lemma bind_single:
   519   "P \<guillemotright>= single = P"
   520   by (rule pred_eqI) auto
   521 
   522 lemma single_bind:
   523   "single x \<guillemotright>= P = P x"
   524   by (rule pred_eqI) auto
   525 
   526 lemma bottom_bind:
   527   "\<bottom> \<guillemotright>= P = \<bottom>"
   528   by (rule pred_eqI) auto
   529 
   530 lemma sup_bind:
   531   "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
   532   by (rule pred_eqI) auto
   533 
   534 lemma Sup_bind:
   535   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   536   by (rule pred_eqI) (auto simp add: SUP_apply)
   537 
   538 lemma pred_iffI:
   539   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
   540   and "\<And>x. eval B x \<Longrightarrow> eval A x"
   541   shows "A = B"
   542   using assms by (auto intro: pred_eqI)
   543   
   544 lemma singleI: "eval (single x) x"
   545   by simp
   546 
   547 lemma singleI_unit: "eval (single ()) x"
   548   by simp
   549 
   550 lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P"
   551   by simp
   552 
   553 lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   554   by simp
   555 
   556 lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
   557   by auto
   558 
   559 lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   560   by auto
   561 
   562 lemma botE: "eval \<bottom> x \<Longrightarrow> P"
   563   by auto
   564 
   565 lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
   566   by auto
   567 
   568 lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
   569   by auto
   570 
   571 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   572   by auto
   573 
   574 lemma single_not_bot [simp]:
   575   "single x \<noteq> \<bottom>"
   576   by (auto simp add: single_def bot_pred_def fun_eq_iff)
   577 
   578 lemma not_bot:
   579   assumes "A \<noteq> \<bottom>"
   580   obtains x where "eval A x"
   581   using assms by (cases A) (auto simp add: bot_pred_def, simp add: mem_def)
   582   
   583 
   584 subsubsection {* Emptiness check and definite choice *}
   585 
   586 definition is_empty :: "'a pred \<Rightarrow> bool" where
   587   "is_empty A \<longleftrightarrow> A = \<bottom>"
   588 
   589 lemma is_empty_bot:
   590   "is_empty \<bottom>"
   591   by (simp add: is_empty_def)
   592 
   593 lemma not_is_empty_single:
   594   "\<not> is_empty (single x)"
   595   by (auto simp add: is_empty_def single_def bot_pred_def fun_eq_iff)
   596 
   597 lemma is_empty_sup:
   598   "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
   599   by (auto simp add: is_empty_def)
   600 
   601 definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
   602   "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
   603 
   604 lemma singleton_eqI:
   605   "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x"
   606   by (auto simp add: singleton_def)
   607 
   608 lemma eval_singletonI:
   609   "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
   610 proof -
   611   assume assm: "\<exists>!x. eval A x"
   612   then obtain x where "eval A x" ..
   613   moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
   614   ultimately show ?thesis by simp 
   615 qed
   616 
   617 lemma single_singleton:
   618   "\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A"
   619 proof -
   620   assume assm: "\<exists>!x. eval A x"
   621   then have "eval A (singleton dfault A)"
   622     by (rule eval_singletonI)
   623   moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
   624     by (rule singleton_eqI)
   625   ultimately have "eval (single (singleton dfault A)) = eval A"
   626     by (simp (no_asm_use) add: single_def fun_eq_iff) blast
   627   then have "\<And>x. eval (single (singleton dfault A)) x = eval A x"
   628     by simp
   629   then show ?thesis by (rule pred_eqI)
   630 qed
   631 
   632 lemma singleton_undefinedI:
   633   "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()"
   634   by (simp add: singleton_def)
   635 
   636 lemma singleton_bot:
   637   "singleton dfault \<bottom> = dfault ()"
   638   by (auto simp add: bot_pred_def intro: singleton_undefinedI)
   639 
   640 lemma singleton_single:
   641   "singleton dfault (single x) = x"
   642   by (auto simp add: intro: singleton_eqI singleI elim: singleE)
   643 
   644 lemma singleton_sup_single_single:
   645   "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())"
   646 proof (cases "x = y")
   647   case True then show ?thesis by (simp add: singleton_single)
   648 next
   649   case False
   650   have "eval (single x \<squnion> single y) x"
   651     and "eval (single x \<squnion> single y) y"
   652   by (auto intro: supI1 supI2 singleI)
   653   with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
   654     by blast
   655   then have "singleton dfault (single x \<squnion> single y) = dfault ()"
   656     by (rule singleton_undefinedI)
   657   with False show ?thesis by simp
   658 qed
   659 
   660 lemma singleton_sup_aux:
   661   "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
   662     else if B = \<bottom> then singleton dfault A
   663     else singleton dfault
   664       (single (singleton dfault A) \<squnion> single (singleton dfault B)))"
   665 proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
   666   case True then show ?thesis by (simp add: single_singleton)
   667 next
   668   case False
   669   from False have A_or_B:
   670     "singleton dfault A = dfault () \<or> singleton dfault B = dfault ()"
   671     by (auto intro!: singleton_undefinedI)
   672   then have rhs: "singleton dfault
   673     (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()"
   674     by (auto simp add: singleton_sup_single_single singleton_single)
   675   from False have not_unique:
   676     "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
   677   show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
   678     case True
   679     then obtain a b where a: "eval A a" and b: "eval B b"
   680       by (blast elim: not_bot)
   681     with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
   682       by (auto simp add: sup_pred_def bot_pred_def)
   683     then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI)
   684     with True rhs show ?thesis by simp
   685   next
   686     case False then show ?thesis by auto
   687   qed
   688 qed
   689 
   690 lemma singleton_sup:
   691   "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
   692     else if B = \<bottom> then singleton dfault A
   693     else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())"
   694 using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
   695 
   696 
   697 subsubsection {* Derived operations *}
   698 
   699 definition if_pred :: "bool \<Rightarrow> unit pred" where
   700   if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
   701 
   702 definition holds :: "unit pred \<Rightarrow> bool" where
   703   holds_eq: "holds P = eval P ()"
   704 
   705 definition not_pred :: "unit pred \<Rightarrow> unit pred" where
   706   not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
   707 
   708 lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()"
   709   unfolding if_pred_eq by (auto intro: singleI)
   710 
   711 lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
   712   unfolding if_pred_eq by (cases b) (auto elim: botE)
   713 
   714 lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()"
   715   unfolding not_pred_eq eval_pred by (auto intro: singleI)
   716 
   717 lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()"
   718   unfolding not_pred_eq by (auto intro: singleI)
   719 
   720 lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   721   unfolding not_pred_eq
   722   by (auto split: split_if_asm elim: botE)
   723 
   724 lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   725   unfolding not_pred_eq
   726   by (auto split: split_if_asm elim: botE)
   727 lemma "f () = False \<or> f () = True"
   728 by simp
   729 
   730 lemma closure_of_bool_cases [no_atp]:
   731   fixes f :: "unit \<Rightarrow> bool"
   732   assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
   733   assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
   734   shows "P f"
   735 proof -
   736   have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
   737     apply (cases "f ()")
   738     apply (rule disjI2)
   739     apply (rule ext)
   740     apply (simp add: unit_eq)
   741     apply (rule disjI1)
   742     apply (rule ext)
   743     apply (simp add: unit_eq)
   744     done
   745   from this assms show ?thesis by blast
   746 qed
   747 
   748 lemma unit_pred_cases:
   749   assumes "P \<bottom>"
   750   assumes "P (single ())"
   751   shows "P Q"
   752 using assms unfolding bot_pred_def bot_fun_def bot_bool_def empty_def single_def proof (cases Q)
   753   fix f
   754   assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
   755   then have "P (Pred f)" 
   756     by (cases _ f rule: closure_of_bool_cases) simp_all
   757   moreover assume "Q = Pred f"
   758   ultimately show "P Q" by simp
   759 qed
   760   
   761 lemma holds_if_pred:
   762   "holds (if_pred b) = b"
   763 unfolding if_pred_eq holds_eq
   764 by (cases b) (auto intro: singleI elim: botE)
   765 
   766 lemma if_pred_holds:
   767   "if_pred (holds P) = P"
   768 unfolding if_pred_eq holds_eq
   769 by (rule unit_pred_cases) (auto intro: singleI elim: botE)
   770 
   771 lemma is_empty_holds:
   772   "is_empty P \<longleftrightarrow> \<not> holds P"
   773 unfolding is_empty_def holds_eq
   774 by (rule unit_pred_cases) (auto elim: botE intro: singleI)
   775 
   776 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
   777   "map f P = P \<guillemotright>= (single o f)"
   778 
   779 lemma eval_map [simp]:
   780   "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
   781   by (auto simp add: map_def comp_def)
   782 
   783 enriched_type map: map
   784   by (rule ext, rule pred_eqI, auto)+
   785 
   786 
   787 subsubsection {* Implementation *}
   788 
   789 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
   790 
   791 primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
   792   "pred_of_seq Empty = \<bottom>"
   793 | "pred_of_seq (Insert x P) = single x \<squnion> P"
   794 | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
   795 
   796 definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
   797   "Seq f = pred_of_seq (f ())"
   798 
   799 code_datatype Seq
   800 
   801 primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool"  where
   802   "member Empty x \<longleftrightarrow> False"
   803 | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
   804 | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
   805 
   806 lemma eval_member:
   807   "member xq = eval (pred_of_seq xq)"
   808 proof (induct xq)
   809   case Empty show ?case
   810   by (auto simp add: fun_eq_iff elim: botE)
   811 next
   812   case Insert show ?case
   813   by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI)
   814 next
   815   case Join then show ?case
   816   by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2)
   817 qed
   818 
   819 lemma eval_code [code]: "eval (Seq f) = member (f ())"
   820   unfolding Seq_def by (rule sym, rule eval_member)
   821 
   822 lemma single_code [code]:
   823   "single x = Seq (\<lambda>u. Insert x \<bottom>)"
   824   unfolding Seq_def by simp
   825 
   826 primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   827   "apply f Empty = Empty"
   828 | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
   829 | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
   830 
   831 lemma apply_bind:
   832   "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
   833 proof (induct xq)
   834   case Empty show ?case
   835     by (simp add: bottom_bind)
   836 next
   837   case Insert show ?case
   838     by (simp add: single_bind sup_bind)
   839 next
   840   case Join then show ?case
   841     by (simp add: sup_bind)
   842 qed
   843   
   844 lemma bind_code [code]:
   845   "Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))"
   846   unfolding Seq_def by (rule sym, rule apply_bind)
   847 
   848 lemma bot_set_code [code]:
   849   "\<bottom> = Seq (\<lambda>u. Empty)"
   850   unfolding Seq_def by simp
   851 
   852 primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
   853   "adjunct P Empty = Join P Empty"
   854 | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
   855 | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
   856 
   857 lemma adjunct_sup:
   858   "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
   859   by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute)
   860 
   861 lemma sup_code [code]:
   862   "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f ()
   863     of Empty \<Rightarrow> g ()
   864      | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
   865      | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))"
   866 proof (cases "f ()")
   867   case Empty
   868   thus ?thesis
   869     unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
   870 next
   871   case Insert
   872   thus ?thesis
   873     unfolding Seq_def by (simp add: sup_assoc)
   874 next
   875   case Join
   876   thus ?thesis
   877     unfolding Seq_def
   878     by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
   879 qed
   880 
   881 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   882   "contained Empty Q \<longleftrightarrow> True"
   883 | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
   884 | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
   885 
   886 lemma single_less_eq_eval:
   887   "single x \<le> P \<longleftrightarrow> eval P x"
   888   by (auto simp add: less_eq_pred_def le_fun_def)
   889 
   890 lemma contained_less_eq:
   891   "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
   892   by (induct xq) (simp_all add: single_less_eq_eval)
   893 
   894 lemma less_eq_pred_code [code]:
   895   "Seq f \<le> Q = (case f ()
   896    of Empty \<Rightarrow> True
   897     | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q
   898     | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)"
   899   by (cases "f ()")
   900     (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
   901 
   902 lemma eq_pred_code [code]:
   903   fixes P Q :: "'a pred"
   904   shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
   905   by (auto simp add: equal)
   906 
   907 lemma [code nbe]:
   908   "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
   909   by (fact equal_refl)
   910 
   911 lemma [code]:
   912   "pred_case f P = f (eval P)"
   913   by (cases P) simp
   914 
   915 lemma [code]:
   916   "pred_rec f P = f (eval P)"
   917   by (cases P) simp
   918 
   919 inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
   920 
   921 lemma eq_is_eq: "eq x y \<equiv> (x = y)"
   922   by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
   923 
   924 primrec null :: "'a seq \<Rightarrow> bool" where
   925   "null Empty \<longleftrightarrow> True"
   926 | "null (Insert x P) \<longleftrightarrow> False"
   927 | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
   928 
   929 lemma null_is_empty:
   930   "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
   931   by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
   932 
   933 lemma is_empty_code [code]:
   934   "is_empty (Seq f) \<longleftrightarrow> null (f ())"
   935   by (simp add: null_is_empty Seq_def)
   936 
   937 primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
   938   [code del]: "the_only dfault Empty = dfault ()"
   939 | "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 ())"
   940 | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
   941        else let x = singleton dfault P; y = the_only dfault xq in
   942        if x = y then x else dfault ())"
   943 
   944 lemma the_only_singleton:
   945   "the_only dfault xq = singleton dfault (pred_of_seq xq)"
   946   by (induct xq)
   947     (auto simp add: singleton_bot singleton_single is_empty_def
   948     null_is_empty Let_def singleton_sup)
   949 
   950 lemma singleton_code [code]:
   951   "singleton dfault (Seq f) = (case f ()
   952    of Empty \<Rightarrow> dfault ()
   953     | Insert x P \<Rightarrow> if is_empty P then x
   954         else let y = singleton dfault P in
   955           if x = y then x else dfault ()
   956     | Join P xq \<Rightarrow> if is_empty P then the_only dfault xq
   957         else if null xq then singleton dfault P
   958         else let x = singleton dfault P; y = the_only dfault xq in
   959           if x = y then x else dfault ())"
   960   by (cases "f ()")
   961    (auto simp add: Seq_def the_only_singleton is_empty_def
   962       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
   963 
   964 definition the :: "'a pred \<Rightarrow> 'a" where
   965   "the A = (THE x. eval A x)"
   966 
   967 lemma the_eqI:
   968   "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   969   by (simp add: the_def)
   970 
   971 definition not_unique :: "'a pred \<Rightarrow> 'a" where
   972   [code del]: "not_unique A = (THE x. eval A x)"
   973 
   974 code_abort not_unique
   975 
   976 lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
   977   by (rule the_eqI) (simp add: singleton_def not_unique_def)
   978 
   979 code_reflect Predicate
   980   datatypes pred = Seq and seq = Empty | Insert | Join
   981   functions map
   982 
   983 ML {*
   984 signature PREDICATE =
   985 sig
   986   datatype 'a pred = Seq of (unit -> 'a seq)
   987   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
   988   val yield: 'a pred -> ('a * 'a pred) option
   989   val yieldn: int -> 'a pred -> 'a list * 'a pred
   990   val map: ('a -> 'b) -> 'a pred -> 'b pred
   991 end;
   992 
   993 structure Predicate : PREDICATE =
   994 struct
   995 
   996 datatype pred = datatype Predicate.pred
   997 datatype seq = datatype Predicate.seq
   998 
   999 fun map f = Predicate.map f;
  1000 
  1001 fun yield (Seq f) = next (f ())
  1002 and next Empty = NONE
  1003   | next (Insert (x, P)) = SOME (x, P)
  1004   | next (Join (P, xq)) = (case yield P
  1005      of NONE => next xq
  1006       | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
  1007 
  1008 fun anamorph f k x = (if k = 0 then ([], x)
  1009   else case f x
  1010    of NONE => ([], x)
  1011     | SOME (v, y) => let
  1012         val (vs, z) = anamorph f (k - 1) y
  1013       in (v :: vs, z) end);
  1014 
  1015 fun yieldn P = anamorph yield P;
  1016 
  1017 end;
  1018 *}
  1019 
  1020 lemma eval_mem [simp]:
  1021   "x \<in> eval P \<longleftrightarrow> eval P x"
  1022   by (simp add: mem_def)
  1023 
  1024 lemma eq_mem [simp]:
  1025   "x \<in> (op =) y \<longleftrightarrow> x = y"
  1026   by (auto simp add: mem_def)
  1027 
  1028 no_notation
  1029   bot ("\<bottom>") and
  1030   top ("\<top>") and
  1031   inf (infixl "\<sqinter>" 70) and
  1032   sup (infixl "\<squnion>" 65) and
  1033   Inf ("\<Sqinter>_" [900] 900) and
  1034   Sup ("\<Squnion>_" [900] 900) and
  1035   bind (infixl "\<guillemotright>=" 70)
  1036 
  1037 no_syntax (xsymbols)
  1038   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  1039   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
  1040   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  1041   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
  1042 
  1043 hide_type (open) pred seq
  1044 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
  1045   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
  1046 
  1047 end