src/HOL/Predicate.thy
 author wenzelm Mon Mar 22 20:58:52 2010 +0100 (2010-03-22) changeset 35898 c890a3835d15 parent 34065 6f8f9835e219 child 36008 23dfa8678c7c permissions -rw-r--r--
1 (*  Title:      HOL/Predicate.thy
2     Author:     Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen
3 *)
5 header {* Predicates as relations and enumerations *}
7 theory Predicate
8 imports Inductive Relation
9 begin
11 notation
12   inf (infixl "\<sqinter>" 70) and
13   sup (infixl "\<squnion>" 65) and
14   Inf ("\<Sqinter>_" [900] 900) and
15   Sup ("\<Squnion>_" [900] 900) and
16   top ("\<top>") and
17   bot ("\<bottom>")
20 subsection {* Predicates as (complete) lattices *}
23 text {*
24   Handy introduction and elimination rules for @{text "\<le>"}
25   on unary and binary predicates
26 *}
28 lemma predicate1I:
29   assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
30   shows "P \<le> Q"
31   apply (rule le_funI)
32   apply (rule le_boolI)
33   apply (rule PQ)
34   apply assumption
35   done
37 lemma predicate1D [Pure.dest?, dest?]:
38   "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
39   apply (erule le_funE)
40   apply (erule le_boolE)
41   apply assumption+
42   done
44 lemma rev_predicate1D:
45   "P x ==> P <= Q ==> Q x"
46   by (rule predicate1D)
48 lemma predicate2I [Pure.intro!, intro!]:
49   assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
50   shows "P \<le> Q"
51   apply (rule le_funI)+
52   apply (rule le_boolI)
53   apply (rule PQ)
54   apply assumption
55   done
57 lemma predicate2D [Pure.dest, dest]:
58   "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
59   apply (erule le_funE)+
60   apply (erule le_boolE)
61   apply assumption+
62   done
64 lemma rev_predicate2D:
65   "P x y ==> P <= Q ==> Q x y"
66   by (rule predicate2D)
69 subsubsection {* Equality *}
71 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
74 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
75   by (simp add: expand_fun_eq mem_def)
78 subsubsection {* Order relation *}
80 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
83 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
84   by fast
87 subsubsection {* Top and bottom elements *}
89 lemma top1I [intro!]: "top x"
90   by (simp add: top_fun_eq top_bool_eq)
92 lemma top2I [intro!]: "top x y"
93   by (simp add: top_fun_eq top_bool_eq)
95 lemma bot1E [elim!]: "bot x \<Longrightarrow> P"
96   by (simp add: bot_fun_eq bot_bool_eq)
98 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
99   by (simp add: bot_fun_eq bot_bool_eq)
101 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
102   by (auto simp add: expand_fun_eq)
104 lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
105   by (auto simp add: expand_fun_eq)
108 subsubsection {* Binary union *}
110 lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
111   by (simp add: sup_fun_eq sup_bool_eq)
113 lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
114   by (simp add: sup_fun_eq sup_bool_eq)
116 lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
117   by (simp add: sup_fun_eq sup_bool_eq)
119 lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
120   by (simp add: sup_fun_eq sup_bool_eq)
122 lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
123   by (simp add: sup_fun_eq sup_bool_eq) iprover
125 lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
126   by (simp add: sup_fun_eq sup_bool_eq) iprover
128 text {*
129   \medskip Classical introduction rule: no commitment to @{text A} vs
130   @{text B}.
131 *}
133 lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
134   by (auto simp add: sup_fun_eq sup_bool_eq)
136 lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
137   by (auto simp add: sup_fun_eq sup_bool_eq)
139 lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
140   by (simp add: sup_fun_eq sup_bool_eq mem_def)
142 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)"
143   by (simp add: sup_fun_eq sup_bool_eq mem_def)
146 subsubsection {* Binary intersection *}
148 lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
149   by (simp add: inf_fun_eq inf_bool_eq)
151 lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
152   by (simp add: inf_fun_eq inf_bool_eq)
154 lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
155   by (simp add: inf_fun_eq inf_bool_eq)
157 lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
158   by (simp add: inf_fun_eq inf_bool_eq)
160 lemma inf1D1: "inf A B x ==> A x"
161   by (simp add: inf_fun_eq inf_bool_eq)
163 lemma inf2D1: "inf A B x y ==> A x y"
164   by (simp add: inf_fun_eq inf_bool_eq)
166 lemma inf1D2: "inf A B x ==> B x"
167   by (simp add: inf_fun_eq inf_bool_eq)
169 lemma inf2D2: "inf A B x y ==> B x y"
170   by (simp add: inf_fun_eq inf_bool_eq)
172 lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
173   by (simp add: inf_fun_eq inf_bool_eq mem_def)
175 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)"
176   by (simp add: inf_fun_eq inf_bool_eq mem_def)
179 subsubsection {* Unions of families *}
181 lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
182   by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
184 lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
185   by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
187 lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
188   by (auto simp add: SUP1_iff)
190 lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
191   by (auto simp add: SUP2_iff)
193 lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
194   by (auto simp add: SUP1_iff)
196 lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
197   by (auto simp add: SUP2_iff)
199 lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
200   by (simp add: SUP1_iff expand_fun_eq)
202 lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
203   by (simp add: SUP2_iff expand_fun_eq)
206 subsubsection {* Intersections of families *}
208 lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
209   by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
211 lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
212   by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
214 lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
215   by (auto simp add: INF1_iff)
217 lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
218   by (auto simp add: INF2_iff)
220 lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
221   by (auto simp add: INF1_iff)
223 lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
224   by (auto simp add: INF2_iff)
226 lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
227   by (auto simp add: INF1_iff)
229 lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
230   by (auto simp add: INF2_iff)
232 lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
233   by (simp add: INF1_iff expand_fun_eq)
235 lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
236   by (simp add: INF2_iff expand_fun_eq)
239 subsection {* Predicates as relations *}
241 subsubsection {* Composition  *}
243 inductive
244   pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
245     (infixr "OO" 75)
246   for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
247 where
248   pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
250 inductive_cases pred_compE [elim!]: "(r OO s) a c"
252 lemma pred_comp_rel_comp_eq [pred_set_conv]:
253   "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
254   by (auto simp add: expand_fun_eq elim: pred_compE)
257 subsubsection {* Converse *}
259 inductive
260   conversep :: "('a => 'b => bool) => 'b => 'a => bool"
261     ("(_^--1)" [1000] 1000)
262   for r :: "'a => 'b => bool"
263 where
264   conversepI: "r a b ==> r^--1 b a"
266 notation (xsymbols)
267   conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
269 lemma conversepD:
270   assumes ab: "r^--1 a b"
271   shows "r b a" using ab
272   by cases simp
274 lemma conversep_iff [iff]: "r^--1 a b = r b a"
275   by (iprover intro: conversepI dest: conversepD)
277 lemma conversep_converse_eq [pred_set_conv]:
278   "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
279   by (auto simp add: expand_fun_eq)
281 lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
282   by (iprover intro: order_antisym conversepI dest: conversepD)
284 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
285   by (iprover intro: order_antisym conversepI pred_compI
286     elim: pred_compE dest: conversepD)
288 lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
289   by (simp add: inf_fun_eq inf_bool_eq)
290     (iprover intro: conversepI ext dest: conversepD)
292 lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
293   by (simp add: sup_fun_eq sup_bool_eq)
294     (iprover intro: conversepI ext dest: conversepD)
296 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
297   by (auto simp add: expand_fun_eq)
299 lemma conversep_eq [simp]: "(op =)^--1 = op ="
300   by (auto simp add: expand_fun_eq)
303 subsubsection {* Domain *}
305 inductive
306   DomainP :: "('a => 'b => bool) => 'a => bool"
307   for r :: "'a => 'b => bool"
308 where
309   DomainPI [intro]: "r a b ==> DomainP r a"
311 inductive_cases DomainPE [elim!]: "DomainP r a"
313 lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
314   by (blast intro!: Orderings.order_antisym predicate1I)
317 subsubsection {* Range *}
319 inductive
320   RangeP :: "('a => 'b => bool) => 'b => bool"
321   for r :: "'a => 'b => bool"
322 where
323   RangePI [intro]: "r a b ==> RangeP r b"
325 inductive_cases RangePE [elim!]: "RangeP r b"
327 lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
328   by (blast intro!: Orderings.order_antisym predicate1I)
331 subsubsection {* Inverse image *}
333 definition
334   inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
335   "inv_imagep r f == %x y. r (f x) (f y)"
337 lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
338   by (simp add: inv_image_def inv_imagep_def)
340 lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
344 subsubsection {* Powerset *}
346 definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
347   "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
349 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
350   by (auto simp add: Powp_def expand_fun_eq)
352 lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
355 subsubsection {* Properties of relations *}
357 abbreviation antisymP :: "('a => 'a => bool) => bool" where
358   "antisymP r == antisym {(x, y). r x y}"
360 abbreviation transP :: "('a => 'a => bool) => bool" where
361   "transP r == trans {(x, y). r x y}"
363 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
364   "single_valuedP r == single_valued {(x, y). r x y}"
367 subsection {* Predicates as enumerations *}
369 subsubsection {* The type of predicate enumerations (a monad) *}
371 datatype 'a pred = Pred "'a \<Rightarrow> bool"
373 primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
374   eval_pred: "eval (Pred f) = f"
376 lemma Pred_eval [simp]:
377   "Pred (eval x) = x"
378   by (cases x) simp
380 lemma eval_inject: "eval x = eval y \<longleftrightarrow> x = y"
381   by (cases x) auto
383 definition single :: "'a \<Rightarrow> 'a pred" where
384   "single x = Pred ((op =) x)"
386 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
387   "P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
389 instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
390 begin
392 definition
393   "P \<le> Q \<longleftrightarrow> eval P \<le> eval Q"
395 definition
396   "P < Q \<longleftrightarrow> eval P < eval Q"
398 definition
399   "\<bottom> = Pred \<bottom>"
401 definition
402   "\<top> = Pred \<top>"
404 definition
405   "P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)"
407 definition
408   "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
410 definition
411   [code del]: "\<Sqinter>A = Pred (INFI A eval)"
413 definition
414   [code del]: "\<Squnion>A = Pred (SUPR A eval)"
416 definition
417   "- P = Pred (- eval P)"
419 definition
420   "P - Q = Pred (eval P - eval Q)"
422 instance proof
423 qed (auto simp add: less_eq_pred_def less_pred_def
424     inf_pred_def sup_pred_def bot_pred_def top_pred_def
425     Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def,
426     auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
427     eval_inject mem_def)
429 end
431 lemma bind_bind:
432   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
433   by (auto simp add: bind_def expand_fun_eq)
435 lemma bind_single:
436   "P \<guillemotright>= single = P"
437   by (simp add: bind_def single_def)
439 lemma single_bind:
440   "single x \<guillemotright>= P = P x"
441   by (simp add: bind_def single_def)
443 lemma bottom_bind:
444   "\<bottom> \<guillemotright>= P = \<bottom>"
445   by (auto simp add: bot_pred_def bind_def expand_fun_eq)
447 lemma sup_bind:
448   "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
449   by (auto simp add: bind_def sup_pred_def expand_fun_eq)
451 lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
452   by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq)
454 lemma pred_iffI:
455   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
456   and "\<And>x. eval B x \<Longrightarrow> eval A x"
457   shows "A = B"
458 proof -
459   from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast
460   then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq)
461 qed
463 lemma singleI: "eval (single x) x"
464   unfolding single_def by simp
466 lemma singleI_unit: "eval (single ()) x"
467   by simp (rule singleI)
469 lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P"
470   unfolding single_def by simp
472 lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
473   by (erule singleE) simp
475 lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
476   unfolding bind_def by auto
478 lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
479   unfolding bind_def by auto
481 lemma botE: "eval \<bottom> x \<Longrightarrow> P"
482   unfolding bot_pred_def by auto
484 lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
485   unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq)
487 lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x"
488   unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq)
490 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
491   unfolding sup_pred_def by auto
493 lemma single_not_bot [simp]:
494   "single x \<noteq> \<bottom>"
495   by (auto simp add: single_def bot_pred_def expand_fun_eq)
497 lemma not_bot:
498   assumes "A \<noteq> \<bottom>"
499   obtains x where "eval A x"
500 using assms by (cases A)
504 subsubsection {* Emptiness check and definite choice *}
506 definition is_empty :: "'a pred \<Rightarrow> bool" where
507   "is_empty A \<longleftrightarrow> A = \<bottom>"
509 lemma is_empty_bot:
510   "is_empty \<bottom>"
513 lemma not_is_empty_single:
514   "\<not> is_empty (single x)"
515   by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
517 lemma is_empty_sup:
518   "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
519   by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
521 definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
522   "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
524 lemma singleton_eqI:
525   "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x"
526   by (auto simp add: singleton_def)
528 lemma eval_singletonI:
529   "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
530 proof -
531   assume assm: "\<exists>!x. eval A x"
532   then obtain x where "eval A x" ..
533   moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
534   ultimately show ?thesis by simp
535 qed
537 lemma single_singleton:
538   "\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A"
539 proof -
540   assume assm: "\<exists>!x. eval A x"
541   then have "eval A (singleton dfault A)"
542     by (rule eval_singletonI)
543   moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
544     by (rule singleton_eqI)
545   ultimately have "eval (single (singleton dfault A)) = eval A"
546     by (simp (no_asm_use) add: single_def expand_fun_eq) blast
547   then show ?thesis by (simp add: eval_inject)
548 qed
550 lemma singleton_undefinedI:
551   "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()"
554 lemma singleton_bot:
555   "singleton dfault \<bottom> = dfault ()"
556   by (auto simp add: bot_pred_def intro: singleton_undefinedI)
558 lemma singleton_single:
559   "singleton dfault (single x) = x"
560   by (auto simp add: intro: singleton_eqI singleI elim: singleE)
562 lemma singleton_sup_single_single:
563   "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())"
564 proof (cases "x = y")
565   case True then show ?thesis by (simp add: singleton_single)
566 next
567   case False
568   have "eval (single x \<squnion> single y) x"
569     and "eval (single x \<squnion> single y) y"
570   by (auto intro: supI1 supI2 singleI)
571   with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
572     by blast
573   then have "singleton dfault (single x \<squnion> single y) = dfault ()"
574     by (rule singleton_undefinedI)
575   with False show ?thesis by simp
576 qed
578 lemma singleton_sup_aux:
579   "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
580     else if B = \<bottom> then singleton dfault A
581     else singleton dfault
582       (single (singleton dfault A) \<squnion> single (singleton dfault B)))"
583 proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
584   case True then show ?thesis by (simp add: single_singleton)
585 next
586   case False
587   from False have A_or_B:
588     "singleton dfault A = dfault () \<or> singleton dfault B = dfault ()"
589     by (auto intro!: singleton_undefinedI)
590   then have rhs: "singleton dfault
591     (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()"
592     by (auto simp add: singleton_sup_single_single singleton_single)
593   from False have not_unique:
594     "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
595   show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
596     case True
597     then obtain a b where a: "eval A a" and b: "eval B b"
598       by (blast elim: not_bot)
599     with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
600       by (auto simp add: sup_pred_def bot_pred_def)
601     then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI)
602     with True rhs show ?thesis by simp
603   next
604     case False then show ?thesis by auto
605   qed
606 qed
608 lemma singleton_sup:
609   "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
610     else if B = \<bottom> then singleton dfault A
611     else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())"
612 using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
615 subsubsection {* Derived operations *}
617 definition if_pred :: "bool \<Rightarrow> unit pred" where
618   if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
620 definition holds :: "unit pred \<Rightarrow> bool" where
621   holds_eq: "holds P = eval P ()"
623 definition not_pred :: "unit pred \<Rightarrow> unit pred" where
624   not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
626 lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()"
627   unfolding if_pred_eq by (auto intro: singleI)
629 lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
630   unfolding if_pred_eq by (cases b) (auto elim: botE)
632 lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()"
633   unfolding not_pred_eq eval_pred by (auto intro: singleI)
635 lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()"
636   unfolding not_pred_eq by (auto intro: singleI)
638 lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis"
639   unfolding not_pred_eq
640   by (auto split: split_if_asm elim: botE)
642 lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
643   unfolding not_pred_eq
644   by (auto split: split_if_asm elim: botE)
645 lemma "f () = False \<or> f () = True"
646 by simp
648 lemma closure_of_bool_cases:
649 assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
650 assumes "f = (%u. True) \<Longrightarrow> P f"
651 shows "P f"
652 proof -
653   have "f = (%u. False) \<or> f = (%u. True)"
654     apply (cases "f ()")
655     apply (rule disjI2)
656     apply (rule ext)
658     apply (rule disjI1)
659     apply (rule ext)
661     done
662   from this prems show ?thesis by blast
663 qed
665 lemma unit_pred_cases:
666 assumes "P \<bottom>"
667 assumes "P (single ())"
668 shows "P Q"
669 using assms
670 unfolding bot_pred_def Collect_def empty_def single_def
671 apply (cases Q)
672 apply simp
673 apply (rule_tac f="fun" in closure_of_bool_cases)
674 apply auto
675 apply (subgoal_tac "(%x. () = x) = (%x. True)")
676 apply auto
677 done
679 lemma holds_if_pred:
680   "holds (if_pred b) = b"
681 unfolding if_pred_eq holds_eq
682 by (cases b) (auto intro: singleI elim: botE)
684 lemma if_pred_holds:
685   "if_pred (holds P) = P"
686 unfolding if_pred_eq holds_eq
687 by (rule unit_pred_cases) (auto intro: singleI elim: botE)
689 lemma is_empty_holds:
690   "is_empty P \<longleftrightarrow> \<not> holds P"
691 unfolding is_empty_def holds_eq
692 by (rule unit_pred_cases) (auto elim: botE intro: singleI)
694 subsubsection {* Implementation *}
696 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
698 primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
699     "pred_of_seq Empty = \<bottom>"
700   | "pred_of_seq (Insert x P) = single x \<squnion> P"
701   | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
703 definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
704   "Seq f = pred_of_seq (f ())"
706 code_datatype Seq
708 primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool"  where
709   "member Empty x \<longleftrightarrow> False"
710   | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
711   | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
713 lemma eval_member:
714   "member xq = eval (pred_of_seq xq)"
715 proof (induct xq)
716   case Empty show ?case
717   by (auto simp add: expand_fun_eq elim: botE)
718 next
719   case Insert show ?case
720   by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI)
721 next
722   case Join then show ?case
723   by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2)
724 qed
726 lemma eval_code [code]: "eval (Seq f) = member (f ())"
727   unfolding Seq_def by (rule sym, rule eval_member)
729 lemma single_code [code]:
730   "single x = Seq (\<lambda>u. Insert x \<bottom>)"
731   unfolding Seq_def by simp
733 primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
734     "apply f Empty = Empty"
735   | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
736   | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
738 lemma apply_bind:
739   "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
740 proof (induct xq)
741   case Empty show ?case
743 next
744   case Insert show ?case
745     by (simp add: single_bind sup_bind)
746 next
747   case Join then show ?case
749 qed
751 lemma bind_code [code]:
752   "Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))"
753   unfolding Seq_def by (rule sym, rule apply_bind)
755 lemma bot_set_code [code]:
756   "\<bottom> = Seq (\<lambda>u. Empty)"
757   unfolding Seq_def by simp
759 primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
760     "adjunct P Empty = Join P Empty"
761   | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
762   | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
765   "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
766   by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute)
768 lemma sup_code [code]:
769   "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f ()
770     of Empty \<Rightarrow> g ()
771      | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
772      | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))"
773 proof (cases "f ()")
774   case Empty
775   thus ?thesis
776     unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
777 next
778   case Insert
779   thus ?thesis
780     unfolding Seq_def by (simp add: sup_assoc)
781 next
782   case Join
783   thus ?thesis
784     unfolding Seq_def
786 qed
788 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
789     "contained Empty Q \<longleftrightarrow> True"
790   | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
791   | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
793 lemma single_less_eq_eval:
794   "single x \<le> P \<longleftrightarrow> eval P x"
795   by (auto simp add: single_def less_eq_pred_def mem_def)
797 lemma contained_less_eq:
798   "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
799   by (induct xq) (simp_all add: single_less_eq_eval)
801 lemma less_eq_pred_code [code]:
802   "Seq f \<le> Q = (case f ()
803    of Empty \<Rightarrow> True
804     | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q
805     | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)"
806   by (cases "f ()")
807     (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
809 lemma eq_pred_code [code]:
810   fixes P Q :: "'a pred"
811   shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
812   unfolding eq by auto
814 lemma [code]:
815   "pred_case f P = f (eval P)"
816   by (cases P) simp
818 lemma [code]:
819   "pred_rec f P = f (eval P)"
820   by (cases P) simp
822 inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
824 lemma eq_is_eq: "eq x y \<equiv> (x = y)"
825   by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
827 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
828   "map f P = P \<guillemotright>= (single o f)"
830 primrec null :: "'a seq \<Rightarrow> bool" where
831     "null Empty \<longleftrightarrow> True"
832   | "null (Insert x P) \<longleftrightarrow> False"
833   | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
835 lemma null_is_empty:
836   "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
837   by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
839 lemma is_empty_code [code]:
840   "is_empty (Seq f) \<longleftrightarrow> null (f ())"
841   by (simp add: null_is_empty Seq_def)
843 primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
844   [code del]: "the_only dfault Empty = dfault ()"
845   | "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 ())"
846   | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
847        else let x = singleton dfault P; y = the_only dfault xq in
848        if x = y then x else dfault ())"
850 lemma the_only_singleton:
851   "the_only dfault xq = singleton dfault (pred_of_seq xq)"
852   by (induct xq)
853     (auto simp add: singleton_bot singleton_single is_empty_def
854     null_is_empty Let_def singleton_sup)
856 lemma singleton_code [code]:
857   "singleton dfault (Seq f) = (case f ()
858    of Empty \<Rightarrow> dfault ()
859     | Insert x P \<Rightarrow> if is_empty P then x
860         else let y = singleton dfault P in
861           if x = y then x else dfault ()
862     | Join P xq \<Rightarrow> if is_empty P then the_only dfault xq
863         else if null xq then singleton dfault P
864         else let x = singleton dfault P; y = the_only dfault xq in
865           if x = y then x else dfault ())"
866   by (cases "f ()")
867    (auto simp add: Seq_def the_only_singleton is_empty_def
868       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
870 definition not_unique :: "'a pred => 'a"
871 where
872   [code del]: "not_unique A = (THE x. eval A x)"
874 definition the :: "'a pred => 'a"
875 where
876   [code del]: "the A = (THE x. eval A x)"
878 lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
879 by (auto simp add: the_def singleton_def not_unique_def)
881 code_abort not_unique
883 ML {*
884 signature PREDICATE =
885 sig
886   datatype 'a pred = Seq of (unit -> 'a seq)
887   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
888   val yield: 'a pred -> ('a * 'a pred) option
889   val yieldn: int -> 'a pred -> 'a list * 'a pred
890   val map: ('a -> 'b) -> 'a pred -> 'b pred
891 end;
893 structure Predicate : PREDICATE =
894 struct
896 @{code_datatype pred = Seq};
897 @{code_datatype seq = Empty | Insert | Join};
899 fun yield (@{code Seq} f) = next (f ())
900 and next @{code Empty} = NONE
901   | next (@{code Insert} (x, P)) = SOME (x, P)
902   | next (@{code Join} (P, xq)) = (case yield P
903      of NONE => next xq
904       | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))));
906 fun anamorph f k x = (if k = 0 then ([], x)
907   else case f x
908    of NONE => ([], x)
909     | SOME (v, y) => let
910         val (vs, z) = anamorph f (k - 1) y
911       in (v :: vs, z) end);
913 fun yieldn P = anamorph yield P;
915 fun map f = @{code map} f;
917 end;
918 *}
920 code_reserved Eval Predicate
922 code_type pred and seq
923   (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
925 code_const Seq and Empty and Insert and Join
926   (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
928 no_notation
929   inf (infixl "\<sqinter>" 70) and
930   sup (infixl "\<squnion>" 65) and
931   Inf ("\<Sqinter>_" [900] 900) and
932   Sup ("\<Squnion>_" [900] 900) and
933   top ("\<top>") and
934   bot ("\<bottom>") and
935   bind (infixl "\<guillemotright>=" 70)
937 hide (open) type pred seq
938 hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
939   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
941 end