1(* Title: HOL/Predicate.thy 2 Author: Lukas Bulwahn and Florian Haftmann, TU Muenchen 3*) 4 5section \<open>Predicates as enumerations\<close> 6 7theory Predicate 8imports String 9begin 10 11subsection \<open>The type of predicate enumerations (a monad)\<close> 12 13datatype (plugins only: extraction) (dead 'a) pred = Pred (eval: "'a \<Rightarrow> bool") 14 15lemma pred_eqI: 16 "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q" 17 by (cases P, cases Q) (auto simp add: fun_eq_iff) 18 19lemma pred_eq_iff: 20 "P = Q \<Longrightarrow> (\<And>w. eval P w \<longleftrightarrow> eval Q w)" 21 by (simp add: pred_eqI) 22 23instantiation pred :: (type) complete_lattice 24begin 25 26definition 27 "P \<le> Q \<longleftrightarrow> eval P \<le> eval Q" 28 29definition 30 "P < Q \<longleftrightarrow> eval P < eval Q" 31 32definition 33 "\<bottom> = Pred \<bottom>" 34 35lemma eval_bot [simp]: 36 "eval \<bottom> = \<bottom>" 37 by (simp add: bot_pred_def) 38 39definition 40 "\<top> = Pred \<top>" 41 42lemma eval_top [simp]: 43 "eval \<top> = \<top>" 44 by (simp add: top_pred_def) 45 46definition 47 "P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)" 48 49lemma eval_inf [simp]: 50 "eval (P \<sqinter> Q) = eval P \<sqinter> eval Q" 51 by (simp add: inf_pred_def) 52 53definition 54 "P \<squnion> Q = Pred (eval P \<squnion> eval Q)" 55 56lemma eval_sup [simp]: 57 "eval (P \<squnion> Q) = eval P \<squnion> eval Q" 58 by (simp add: sup_pred_def) 59 60definition 61 "\<Sqinter>A = Pred (\<Sqinter>(eval ` A))" 62 63lemma eval_Inf [simp]: 64 "eval (\<Sqinter>A) = \<Sqinter>(eval ` A)" 65 by (simp add: Inf_pred_def) 66 67definition 68 "\<Squnion>A = Pred (\<Squnion>(eval ` A))" 69 70lemma eval_Sup [simp]: 71 "eval (\<Squnion>A) = \<Squnion>(eval ` A)" 72 by (simp add: Sup_pred_def) 73 74instance proof 75qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def le_fun_def less_fun_def) 76 77end 78 79lemma eval_INF [simp]: 80 "eval (\<Sqinter>(f ` A)) = \<Sqinter>((eval \<circ> f) ` A)" 81 by (simp add: image_comp) 82 83lemma eval_SUP [simp]: 84 "eval (\<Squnion>(f ` A)) = \<Squnion>((eval \<circ> f) ` A)" 85 by (simp add: image_comp) 86 87instantiation pred :: (type) complete_boolean_algebra 88begin 89 90definition 91 "- P = Pred (- eval P)" 92 93lemma eval_compl [simp]: 94 "eval (- P) = - eval P" 95 by (simp add: uminus_pred_def) 96 97definition 98 "P - Q = Pred (eval P - eval Q)" 99 100lemma eval_minus [simp]: 101 "eval (P - Q) = eval P - eval Q" 102 by (simp add: minus_pred_def) 103 104instance proof 105 fix A::"'a pred set set" 106 show "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})" 107 proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe) 108 fix w 109 assume A: "\<forall>x\<in>A. \<exists>f\<in>x. eval f w" 110 define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)" 111 have [simp]: "(\<forall>f\<in> (F ` A). eval f w)" 112 by (metis (no_types, lifting) A F_def image_iff some_eq_ex) 113 have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>(F ` A). eval f w)" 114 using A by (simp, metis (no_types, lifting) F_def someI)+ 115 from this show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)" 116 by (rule exI [of _ "F ` A"]) 117 qed 118qed (auto intro!: pred_eqI) 119 120end 121 122definition single :: "'a \<Rightarrow> 'a pred" where 123 "single x = Pred ((=) x)" 124 125lemma eval_single [simp]: 126 "eval (single x) = (=) x" 127 by (simp add: single_def) 128 129definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<bind>" 70) where 130 "P \<bind> f = (\<Squnion>(f ` {x. eval P x}))" 131 132lemma eval_bind [simp]: 133 "eval (P \<bind> f) = eval (\<Squnion>(f ` {x. eval P x}))" 134 by (simp add: bind_def) 135 136lemma bind_bind: 137 "(P \<bind> Q) \<bind> R = P \<bind> (\<lambda>x. Q x \<bind> R)" 138 by (rule pred_eqI) auto 139 140lemma bind_single: 141 "P \<bind> single = P" 142 by (rule pred_eqI) auto 143 144lemma single_bind: 145 "single x \<bind> P = P x" 146 by (rule pred_eqI) auto 147 148lemma bottom_bind: 149 "\<bottom> \<bind> P = \<bottom>" 150 by (rule pred_eqI) auto 151 152lemma sup_bind: 153 "(P \<squnion> Q) \<bind> R = P \<bind> R \<squnion> Q \<bind> R" 154 by (rule pred_eqI) auto 155 156lemma Sup_bind: 157 "(\<Squnion>A \<bind> f) = \<Squnion>((\<lambda>x. x \<bind> f) ` A)" 158 by (rule pred_eqI) auto 159 160lemma pred_iffI: 161 assumes "\<And>x. eval A x \<Longrightarrow> eval B x" 162 and "\<And>x. eval B x \<Longrightarrow> eval A x" 163 shows "A = B" 164 using assms by (auto intro: pred_eqI) 165 166lemma singleI: "eval (single x) x" 167 by simp 168 169lemma singleI_unit: "eval (single ()) x" 170 by simp 171 172lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P" 173 by simp 174 175lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" 176 by simp 177 178lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<bind> Q) y" 179 by auto 180 181lemma bindE: "eval (R \<bind> Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P" 182 by auto 183 184lemma botE: "eval \<bottom> x \<Longrightarrow> P" 185 by auto 186 187lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x" 188 by auto 189 190lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 191 by auto 192 193lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P" 194 by auto 195 196lemma single_not_bot [simp]: 197 "single x \<noteq> \<bottom>" 198 by (auto simp add: single_def bot_pred_def fun_eq_iff) 199 200lemma not_bot: 201 assumes "A \<noteq> \<bottom>" 202 obtains x where "eval A x" 203 using assms by (cases A) (auto simp add: bot_pred_def) 204 205 206subsection \<open>Emptiness check and definite choice\<close> 207 208definition is_empty :: "'a pred \<Rightarrow> bool" where 209 "is_empty A \<longleftrightarrow> A = \<bottom>" 210 211lemma is_empty_bot: 212 "is_empty \<bottom>" 213 by (simp add: is_empty_def) 214 215lemma not_is_empty_single: 216 "\<not> is_empty (single x)" 217 by (auto simp add: is_empty_def single_def bot_pred_def fun_eq_iff) 218 219lemma is_empty_sup: 220 "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B" 221 by (auto simp add: is_empty_def) 222 223definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where 224 "singleton default A = (if \<exists>!x. eval A x then THE x. eval A x else default ())" for default 225 226lemma singleton_eqI: 227 "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton default A = x" for default 228 by (auto simp add: singleton_def) 229 230lemma eval_singletonI: 231 "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton default A)" for default 232proof - 233 assume assm: "\<exists>!x. eval A x" 234 then obtain x where x: "eval A x" .. 235 with assm have "singleton default A = x" by (rule singleton_eqI) 236 with x show ?thesis by simp 237qed 238 239lemma single_singleton: 240 "\<exists>!x. eval A x \<Longrightarrow> single (singleton default A) = A" for default 241proof - 242 assume assm: "\<exists>!x. eval A x" 243 then have "eval A (singleton default A)" 244 by (rule eval_singletonI) 245 moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton default A = x" 246 by (rule singleton_eqI) 247 ultimately have "eval (single (singleton default A)) = eval A" 248 by (simp (no_asm_use) add: single_def fun_eq_iff) blast 249 then have "\<And>x. eval (single (singleton default A)) x = eval A x" 250 by simp 251 then show ?thesis by (rule pred_eqI) 252qed 253 254lemma singleton_undefinedI: 255 "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton default A = default ()" for default 256 by (simp add: singleton_def) 257 258lemma singleton_bot: 259 "singleton default \<bottom> = default ()" for default 260 by (auto simp add: bot_pred_def intro: singleton_undefinedI) 261 262lemma singleton_single: 263 "singleton default (single x) = x" for default 264 by (auto simp add: intro: singleton_eqI singleI elim: singleE) 265 266lemma singleton_sup_single_single: 267 "singleton default (single x \<squnion> single y) = (if x = y then x else default ())" for default 268proof (cases "x = y") 269 case True then show ?thesis by (simp add: singleton_single) 270next 271 case False 272 have "eval (single x \<squnion> single y) x" 273 and "eval (single x \<squnion> single y) y" 274 by (auto intro: supI1 supI2 singleI) 275 with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)" 276 by blast 277 then have "singleton default (single x \<squnion> single y) = default ()" 278 by (rule singleton_undefinedI) 279 with False show ?thesis by simp 280qed 281 282lemma singleton_sup_aux: 283 "singleton default (A \<squnion> B) = (if A = \<bottom> then singleton default B 284 else if B = \<bottom> then singleton default A 285 else singleton default 286 (single (singleton default A) \<squnion> single (singleton default B)))" for default 287proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)") 288 case True then show ?thesis by (simp add: single_singleton) 289next 290 case False 291 from False have A_or_B: 292 "singleton default A = default () \<or> singleton default B = default ()" 293 by (auto intro!: singleton_undefinedI) 294 then have rhs: "singleton default 295 (single (singleton default A) \<squnion> single (singleton default B)) = default ()" 296 by (auto simp add: singleton_sup_single_single singleton_single) 297 from False have not_unique: 298 "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp 299 show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>") 300 case True 301 then obtain a b where a: "eval A a" and b: "eval B b" 302 by (blast elim: not_bot) 303 with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)" 304 by (auto simp add: sup_pred_def bot_pred_def) 305 then have "singleton default (A \<squnion> B) = default ()" by (rule singleton_undefinedI) 306 with True rhs show ?thesis by simp 307 next 308 case False then show ?thesis by auto 309 qed 310qed 311 312lemma singleton_sup: 313 "singleton default (A \<squnion> B) = (if A = \<bottom> then singleton default B 314 else if B = \<bottom> then singleton default A 315 else if singleton default A = singleton default B then singleton default A else default ())" for default 316 using singleton_sup_aux [of default A B] by (simp only: singleton_sup_single_single) 317 318 319subsection \<open>Derived operations\<close> 320 321definition if_pred :: "bool \<Rightarrow> unit pred" where 322 if_pred_eq: "if_pred b = (if b then single () else \<bottom>)" 323 324definition holds :: "unit pred \<Rightarrow> bool" where 325 holds_eq: "holds P = eval P ()" 326 327definition not_pred :: "unit pred \<Rightarrow> unit pred" where 328 not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())" 329 330lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()" 331 unfolding if_pred_eq by (auto intro: singleI) 332 333lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P" 334 unfolding if_pred_eq by (cases b) (auto elim: botE) 335 336lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()" 337 unfolding not_pred_eq by (auto intro: singleI) 338 339lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()" 340 unfolding not_pred_eq by (auto intro: singleI) 341 342lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis" 343 unfolding not_pred_eq 344 by (auto split: if_split_asm elim: botE) 345 346lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" 347 unfolding not_pred_eq 348 by (auto split: if_split_asm elim: botE) 349lemma "f () = False \<or> f () = True" 350by simp 351 352lemma closure_of_bool_cases [no_atp]: 353 fixes f :: "unit \<Rightarrow> bool" 354 assumes "f = (\<lambda>u. False) \<Longrightarrow> P f" 355 assumes "f = (\<lambda>u. True) \<Longrightarrow> P f" 356 shows "P f" 357proof - 358 have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)" 359 apply (cases "f ()") 360 apply (rule disjI2) 361 apply (rule ext) 362 apply (simp add: unit_eq) 363 apply (rule disjI1) 364 apply (rule ext) 365 apply (simp add: unit_eq) 366 done 367 from this assms show ?thesis by blast 368qed 369 370lemma unit_pred_cases: 371 assumes "P \<bottom>" 372 assumes "P (single ())" 373 shows "P Q" 374using assms unfolding bot_pred_def bot_fun_def bot_bool_def empty_def single_def proof (cases Q) 375 fix f 376 assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))" 377 then have "P (Pred f)" 378 by (cases _ f rule: closure_of_bool_cases) simp_all 379 moreover assume "Q = Pred f" 380 ultimately show "P Q" by simp 381qed 382 383lemma holds_if_pred: 384 "holds (if_pred b) = b" 385unfolding if_pred_eq holds_eq 386by (cases b) (auto intro: singleI elim: botE) 387 388lemma if_pred_holds: 389 "if_pred (holds P) = P" 390unfolding if_pred_eq holds_eq 391by (rule unit_pred_cases) (auto intro: singleI elim: botE) 392 393lemma is_empty_holds: 394 "is_empty P \<longleftrightarrow> \<not> holds P" 395unfolding is_empty_def holds_eq 396by (rule unit_pred_cases) (auto elim: botE intro: singleI) 397 398definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where 399 "map f P = P \<bind> (single \<circ> f)" 400 401lemma eval_map [simp]: 402 "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))" 403 by (simp add: map_def comp_def image_comp) 404 405functor map: map 406 by (rule ext, rule pred_eqI, auto)+ 407 408 409subsection \<open>Implementation\<close> 410 411datatype (plugins only: code extraction) (dead 'a) seq = 412 Empty 413| Insert "'a" "'a pred" 414| Join "'a pred" "'a seq" 415 416primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where 417 "pred_of_seq Empty = \<bottom>" 418| "pred_of_seq (Insert x P) = single x \<squnion> P" 419| "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq" 420 421definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where 422 "Seq f = pred_of_seq (f ())" 423 424code_datatype Seq 425 426primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool" where 427 "member Empty x \<longleftrightarrow> False" 428| "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x" 429| "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x" 430 431lemma eval_member: 432 "member xq = eval (pred_of_seq xq)" 433proof (induct xq) 434 case Empty show ?case 435 by (auto simp add: fun_eq_iff elim: botE) 436next 437 case Insert show ?case 438 by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI) 439next 440 case Join then show ?case 441 by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2) 442qed 443 444lemma eval_code [(* FIXME declare simp *)code]: "eval (Seq f) = member (f ())" 445 unfolding Seq_def by (rule sym, rule eval_member) 446 447lemma single_code [code]: 448 "single x = Seq (\<lambda>u. Insert x \<bottom>)" 449 unfolding Seq_def by simp 450 451primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where 452 "apply f Empty = Empty" 453| "apply f (Insert x P) = Join (f x) (Join (P \<bind> f) Empty)" 454| "apply f (Join P xq) = Join (P \<bind> f) (apply f xq)" 455 456lemma apply_bind: 457 "pred_of_seq (apply f xq) = pred_of_seq xq \<bind> f" 458proof (induct xq) 459 case Empty show ?case 460 by (simp add: bottom_bind) 461next 462 case Insert show ?case 463 by (simp add: single_bind sup_bind) 464next 465 case Join then show ?case 466 by (simp add: sup_bind) 467qed 468 469lemma bind_code [code]: 470 "Seq g \<bind> f = Seq (\<lambda>u. apply f (g ()))" 471 unfolding Seq_def by (rule sym, rule apply_bind) 472 473lemma bot_set_code [code]: 474 "\<bottom> = Seq (\<lambda>u. Empty)" 475 unfolding Seq_def by simp 476 477primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where 478 "adjunct P Empty = Join P Empty" 479| "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)" 480| "adjunct P (Join Q xq) = Join Q (adjunct P xq)" 481 482lemma adjunct_sup: 483 "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq" 484 by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute) 485 486lemma sup_code [code]: 487 "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f () 488 of Empty \<Rightarrow> g () 489 | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g) 490 | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))" 491proof (cases "f ()") 492 case Empty 493 thus ?thesis 494 unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]) 495next 496 case Insert 497 thus ?thesis 498 unfolding Seq_def by (simp add: sup_assoc) 499next 500 case Join 501 thus ?thesis 502 unfolding Seq_def 503 by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) 504qed 505 506primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where 507 "contained Empty Q \<longleftrightarrow> True" 508| "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q" 509| "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q" 510 511lemma single_less_eq_eval: 512 "single x \<le> P \<longleftrightarrow> eval P x" 513 by (auto simp add: less_eq_pred_def le_fun_def) 514 515lemma contained_less_eq: 516 "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q" 517 by (induct xq) (simp_all add: single_less_eq_eval) 518 519lemma less_eq_pred_code [code]: 520 "Seq f \<le> Q = (case f () 521 of Empty \<Rightarrow> True 522 | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q 523 | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)" 524 by (cases "f ()") 525 (simp_all add: Seq_def single_less_eq_eval contained_less_eq) 526 527instantiation pred :: (type) equal 528begin 529 530definition equal_pred 531 where [simp]: "HOL.equal P Q \<longleftrightarrow> P = (Q :: 'a pred)" 532 533instance by standard simp 534 535end 536 537lemma [code]: 538 "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" for P Q :: "'a pred" 539 by auto 540 541lemma [code nbe]: 542 "HOL.equal P P \<longleftrightarrow> True" for P :: "'a pred" 543 by (fact equal_refl) 544 545lemma [code]: 546 "case_pred f P = f (eval P)" 547 by (fact pred.case_eq_if) 548 549lemma [code]: 550 "rec_pred f P = f (eval P)" 551 by (cases P) simp 552 553inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x" 554 555lemma eq_is_eq: "eq x y \<equiv> (x = y)" 556 by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) 557 558primrec null :: "'a seq \<Rightarrow> bool" where 559 "null Empty \<longleftrightarrow> True" 560| "null (Insert x P) \<longleftrightarrow> False" 561| "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq" 562 563lemma null_is_empty: 564 "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)" 565 by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup) 566 567lemma is_empty_code [code]: 568 "is_empty (Seq f) \<longleftrightarrow> null (f ())" 569 by (simp add: null_is_empty Seq_def) 570 571primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where 572 "the_only default Empty = default ()" for default 573| "the_only default (Insert x P) = 574 (if is_empty P then x else let y = singleton default P in if x = y then x else default ())" for default 575| "the_only default (Join P xq) = 576 (if is_empty P then the_only default xq else if null xq then singleton default P 577 else let x = singleton default P; y = the_only default xq in 578 if x = y then x else default ())" for default 579 580lemma the_only_singleton: 581 "the_only default xq = singleton default (pred_of_seq xq)" for default 582 by (induct xq) 583 (auto simp add: singleton_bot singleton_single is_empty_def 584 null_is_empty Let_def singleton_sup) 585 586lemma singleton_code [code]: 587 "singleton default (Seq f) = 588 (case f () of 589 Empty \<Rightarrow> default () 590 | Insert x P \<Rightarrow> if is_empty P then x 591 else let y = singleton default P in 592 if x = y then x else default () 593 | Join P xq \<Rightarrow> if is_empty P then the_only default xq 594 else if null xq then singleton default P 595 else let x = singleton default P; y = the_only default xq in 596 if x = y then x else default ())" for default 597 by (cases "f ()") 598 (auto simp add: Seq_def the_only_singleton is_empty_def 599 null_is_empty singleton_bot singleton_single singleton_sup Let_def) 600 601definition the :: "'a pred \<Rightarrow> 'a" where 602 "the A = (THE x. eval A x)" 603 604lemma the_eqI: 605 "(THE x. eval P x) = x \<Longrightarrow> the P = x" 606 by (simp add: the_def) 607 608lemma the_eq [code]: "the A = singleton (\<lambda>x. Code.abort (STR ''not_unique'') (\<lambda>_. the A)) A" 609 by (rule the_eqI) (simp add: singleton_def the_def) 610 611code_reflect Predicate 612 datatypes pred = Seq and seq = Empty | Insert | Join 613 614ML \<open> 615signature PREDICATE = 616sig 617 val anamorph: ('a -> ('b * 'a) option) -> int -> 'a -> 'b list * 'a 618 datatype 'a pred = Seq of (unit -> 'a seq) 619 and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq 620 val map: ('a -> 'b) -> 'a pred -> 'b pred 621 val yield: 'a pred -> ('a * 'a pred) option 622 val yieldn: int -> 'a pred -> 'a list * 'a pred 623end; 624 625structure Predicate : PREDICATE = 626struct 627 628fun anamorph f k x = 629 (if k = 0 then ([], x) 630 else case f x 631 of NONE => ([], x) 632 | SOME (v, y) => let 633 val k' = k - 1; 634 val (vs, z) = anamorph f k' y 635 in (v :: vs, z) end); 636 637datatype pred = datatype Predicate.pred 638datatype seq = datatype Predicate.seq 639 640fun map f = @{code Predicate.map} f; 641 642fun yield (Seq f) = next (f ()) 643and next Empty = NONE 644 | next (Insert (x, P)) = SOME (x, P) 645 | next (Join (P, xq)) = (case yield P 646 of NONE => next xq 647 | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq)))); 648 649fun yieldn k = anamorph yield k; 650 651end; 652\<close> 653 654text \<open>Conversion from and to sets\<close> 655 656definition pred_of_set :: "'a set \<Rightarrow> 'a pred" where 657 "pred_of_set = Pred \<circ> (\<lambda>A x. x \<in> A)" 658 659lemma eval_pred_of_set [simp]: 660 "eval (pred_of_set A) x \<longleftrightarrow> x \<in>A" 661 by (simp add: pred_of_set_def) 662 663definition set_of_pred :: "'a pred \<Rightarrow> 'a set" where 664 "set_of_pred = Collect \<circ> eval" 665 666lemma member_set_of_pred [simp]: 667 "x \<in> set_of_pred P \<longleftrightarrow> Predicate.eval P x" 668 by (simp add: set_of_pred_def) 669 670definition set_of_seq :: "'a seq \<Rightarrow> 'a set" where 671 "set_of_seq = set_of_pred \<circ> pred_of_seq" 672 673lemma member_set_of_seq [simp]: 674 "x \<in> set_of_seq xq = Predicate.member xq x" 675 by (simp add: set_of_seq_def eval_member) 676 677lemma of_pred_code [code]: 678 "set_of_pred (Predicate.Seq f) = (case f () of 679 Predicate.Empty \<Rightarrow> {} 680 | Predicate.Insert x P \<Rightarrow> insert x (set_of_pred P) 681 | Predicate.Join P xq \<Rightarrow> set_of_pred P \<union> set_of_seq xq)" 682 by (auto split: seq.split simp add: eval_code) 683 684lemma of_seq_code [code]: 685 "set_of_seq Predicate.Empty = {}" 686 "set_of_seq (Predicate.Insert x P) = insert x (set_of_pred P)" 687 "set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq" 688 by auto 689 690text \<open>Lazy Evaluation of an indexed function\<close> 691 692function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a Predicate.pred" 693where 694 "iterate_upto f n m = 695 Predicate.Seq (%u. if n > m then Predicate.Empty 696 else Predicate.Insert (f n) (iterate_upto f (n + 1) m))" 697by pat_completeness auto 698 699termination by (relation "measure (%(f, n, m). nat_of_natural (m + 1 - n))") 700 (auto simp add: less_natural_def) 701 702text \<open>Misc\<close> 703 704declare Inf_set_fold [where 'a = "'a Predicate.pred", code] 705declare Sup_set_fold [where 'a = "'a Predicate.pred", code] 706 707(* FIXME: better implement conversion by bisection *) 708 709lemma pred_of_set_fold_sup: 710 assumes "finite A" 711 shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") 712proof (rule sym) 713 interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" 714 by (fact comp_fun_idem_sup) 715 from \<open>finite A\<close> show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) 716qed 717 718lemma pred_of_set_set_fold_sup: 719 "pred_of_set (set xs) = fold sup (List.map Predicate.single xs) bot" 720proof - 721 interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred" 722 by (fact comp_fun_idem_sup) 723 show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) 724qed 725 726lemma pred_of_set_set_foldr_sup [code]: 727 "pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot" 728 by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff) 729 730no_notation 731 bind (infixl "\<bind>" 70) 732 733hide_type (open) pred seq 734hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds 735 Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map the 736 iterate_upto 737hide_fact (open) null_def member_def 738 739end 740