461 lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" |
467 lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" |
462 unfolding sup_pred_def by simp |
468 unfolding sup_pred_def by simp |
463 |
469 |
464 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P" |
470 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P" |
465 unfolding sup_pred_def by auto |
471 unfolding sup_pred_def by auto |
|
472 |
|
473 lemma single_not_bot [simp]: |
|
474 "single x \<noteq> \<bottom>" |
|
475 by (auto simp add: single_def bot_pred_def expand_fun_eq) |
|
476 |
|
477 lemma not_bot: |
|
478 assumes "A \<noteq> \<bottom>" |
|
479 obtains x where "eval A x" |
|
480 using assms by (cases A) |
|
481 (auto simp add: bot_pred_def, auto simp add: mem_def) |
|
482 |
|
483 |
|
484 subsubsection {* Emptiness check and definite choice *} |
|
485 |
|
486 definition is_empty :: "'a pred \<Rightarrow> bool" where |
|
487 "is_empty A \<longleftrightarrow> A = \<bottom>" |
|
488 |
|
489 lemma is_empty_bot: |
|
490 "is_empty \<bottom>" |
|
491 by (simp add: is_empty_def) |
|
492 |
|
493 lemma not_is_empty_single: |
|
494 "\<not> is_empty (single x)" |
|
495 by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq) |
|
496 |
|
497 lemma is_empty_sup: |
|
498 "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B" |
|
499 by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2) |
|
500 |
|
501 definition singleton :: "'a pred \<Rightarrow> 'a" where |
|
502 "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)" |
|
503 |
|
504 lemma singleton_eqI: |
|
505 "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton A = x" |
|
506 by (auto simp add: singleton_def) |
|
507 |
|
508 lemma eval_singletonI: |
|
509 "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)" |
|
510 proof - |
|
511 assume assm: "\<exists>!x. eval A x" |
|
512 then obtain x where "eval A x" .. |
|
513 moreover with assm have "singleton A = x" by (rule singleton_eqI) |
|
514 ultimately show ?thesis by simp |
|
515 qed |
|
516 |
|
517 lemma single_singleton: |
|
518 "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A" |
|
519 proof - |
|
520 assume assm: "\<exists>!x. eval A x" |
|
521 then have "eval A (singleton A)" |
|
522 by (rule eval_singletonI) |
|
523 moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x" |
|
524 by (rule singleton_eqI) |
|
525 ultimately have "eval (single (singleton A)) = eval A" |
|
526 by (simp (no_asm_use) add: single_def expand_fun_eq) blast |
|
527 then show ?thesis by (simp add: eval_inject) |
|
528 qed |
|
529 |
|
530 lemma singleton_undefinedI: |
|
531 "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined" |
|
532 by (simp add: singleton_def) |
|
533 |
|
534 lemma singleton_bot: |
|
535 "singleton \<bottom> = undefined" |
|
536 by (auto simp add: bot_pred_def intro: singleton_undefinedI) |
|
537 |
|
538 lemma singleton_single: |
|
539 "singleton (single x) = x" |
|
540 by (auto simp add: intro: singleton_eqI singleI elim: singleE) |
|
541 |
|
542 lemma singleton_sup_single_single: |
|
543 "singleton (single x \<squnion> single y) = (if x = y then x else undefined)" |
|
544 proof (cases "x = y") |
|
545 case True then show ?thesis by (simp add: singleton_single) |
|
546 next |
|
547 case False |
|
548 have "eval (single x \<squnion> single y) x" |
|
549 and "eval (single x \<squnion> single y) y" |
|
550 by (auto intro: supI1 supI2 singleI) |
|
551 with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)" |
|
552 by blast |
|
553 then have "singleton (single x \<squnion> single y) = undefined" |
|
554 by (rule singleton_undefinedI) |
|
555 with False show ?thesis by simp |
|
556 qed |
|
557 |
|
558 lemma singleton_sup_aux: |
|
559 "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B |
|
560 else if B = \<bottom> then singleton A |
|
561 else singleton |
|
562 (single (singleton A) \<squnion> single (singleton B)))" |
|
563 proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)") |
|
564 case True then show ?thesis by (simp add: single_singleton) |
|
565 next |
|
566 case False |
|
567 from False have A_or_B: |
|
568 "singleton A = undefined \<or> singleton B = undefined" |
|
569 by (auto intro!: singleton_undefinedI) |
|
570 then have rhs: "singleton |
|
571 (single (singleton A) \<squnion> single (singleton B)) = undefined" |
|
572 by (auto simp add: singleton_sup_single_single singleton_single) |
|
573 from False have not_unique: |
|
574 "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp |
|
575 show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>") |
|
576 case True |
|
577 then obtain a b where a: "eval A a" and b: "eval B b" |
|
578 by (blast elim: not_bot) |
|
579 with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)" |
|
580 by (auto simp add: sup_pred_def bot_pred_def) |
|
581 then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI) |
|
582 with True rhs show ?thesis by simp |
|
583 next |
|
584 case False then show ?thesis by auto |
|
585 qed |
|
586 qed |
|
587 |
|
588 lemma singleton_sup: |
|
589 "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B |
|
590 else if B = \<bottom> then singleton A |
|
591 else if singleton A = singleton B then singleton A else undefined)" |
|
592 using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single) |
466 |
593 |
467 |
594 |
468 subsubsection {* Derived operations *} |
595 subsubsection {* Derived operations *} |
469 |
596 |
470 definition if_pred :: "bool \<Rightarrow> unit pred" where |
597 definition if_pred :: "bool \<Rightarrow> unit pred" where |
628 by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) |
755 by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) |
629 |
756 |
630 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where |
757 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where |
631 "map f P = P \<guillemotright>= (single o f)" |
758 "map f P = P \<guillemotright>= (single o f)" |
632 |
759 |
|
760 primrec null :: "'a seq \<Rightarrow> bool" where |
|
761 "null Empty \<longleftrightarrow> True" |
|
762 | "null (Insert x P) \<longleftrightarrow> False" |
|
763 | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq" |
|
764 |
|
765 lemma null_is_empty: |
|
766 "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)" |
|
767 by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup) |
|
768 |
|
769 lemma is_empty_code [code]: |
|
770 "is_empty (Seq f) \<longleftrightarrow> null (f ())" |
|
771 by (simp add: null_is_empty Seq_def) |
|
772 |
|
773 primrec the_only :: "'a seq \<Rightarrow> 'a" where |
|
774 [code del]: "the_only Empty = undefined" |
|
775 | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)" |
|
776 | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P |
|
777 else let x = singleton P; y = the_only xq in |
|
778 if x = y then x else undefined)" |
|
779 |
|
780 lemma the_only_singleton: |
|
781 "the_only xq = singleton (pred_of_seq xq)" |
|
782 by (induct xq) |
|
783 (auto simp add: singleton_bot singleton_single is_empty_def |
|
784 null_is_empty Let_def singleton_sup) |
|
785 |
|
786 lemma singleton_code [code]: |
|
787 "singleton (Seq f) = (case f () |
|
788 of Empty \<Rightarrow> undefined |
|
789 | Insert x P \<Rightarrow> if is_empty P then x |
|
790 else let y = singleton P in |
|
791 if x = y then x else undefined |
|
792 | Join P xq \<Rightarrow> if is_empty P then the_only xq |
|
793 else if null xq then singleton P |
|
794 else let x = singleton P; y = the_only xq in |
|
795 if x = y then x else undefined)" |
|
796 by (cases "f ()") |
|
797 (auto simp add: Seq_def the_only_singleton is_empty_def |
|
798 null_is_empty singleton_bot singleton_single singleton_sup Let_def) |
|
799 |
633 ML {* |
800 ML {* |
634 signature PREDICATE = |
801 signature PREDICATE = |
635 sig |
802 sig |
636 datatype 'a pred = Seq of (unit -> 'a seq) |
803 datatype 'a pred = Seq of (unit -> 'a seq) |
637 and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq |
804 and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq |