626 lemma subset_code [code]: |
626 lemma subset_code [code]: |
627 "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)" |
627 "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)" |
628 "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)" |
628 "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)" |
629 by auto |
629 by auto |
630 |
630 |
631 definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2" |
|
632 |
|
633 code_abort non_empty_trees |
|
634 |
|
635 lemma subset_Coset_empty_Set_empty [code]: |
631 lemma subset_Coset_empty_Set_empty [code]: |
636 "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of |
632 "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of |
637 (rbt.Empty, rbt.Empty) => False | |
633 (rbt.Empty, rbt.Empty) => False | |
638 (_, _) => non_empty_trees t1 t2)" |
634 (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))" |
639 proof - |
635 proof - |
640 have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty" |
636 have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty" |
641 by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) |
637 by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) |
642 have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp |
638 have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp |
643 show ?thesis |
639 show ?thesis |
644 by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def) |
640 by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split) |
645 qed |
641 qed |
646 |
642 |
647 text {* A frequent case – avoid intermediate sets *} |
643 text {* A frequent case – avoid intermediate sets *} |
648 lemma [code_unfold]: |
644 lemma [code_unfold]: |
649 "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True" |
645 "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True" |
659 have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac) |
655 have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac) |
660 then show ?thesis |
656 then show ?thesis |
661 by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def) |
657 by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def) |
662 qed |
658 qed |
663 |
659 |
664 definition not_a_singleton_tree where [code del]: "not_a_singleton_tree x y = x y" |
|
665 |
|
666 code_abort not_a_singleton_tree |
|
667 |
|
668 lemma the_elem_set [code]: |
660 lemma the_elem_set [code]: |
669 fixes t :: "('a :: linorder, unit) rbt" |
661 fixes t :: "('a :: linorder, unit) rbt" |
670 shows "the_elem (Set t) = (case impl_of t of |
662 shows "the_elem (Set t) = (case impl_of t of |
671 (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x |
663 (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x |
672 | _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))" |
664 | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))" |
673 proof - |
665 proof - |
674 { |
666 { |
675 fix x :: "'a :: linorder" |
667 fix x :: "'a :: linorder" |
676 let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" |
668 let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" |
677 have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto |
669 have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto |
679 |
671 |
680 have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" |
672 have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" |
681 by (subst(asm) RBT_inverse[symmetric, OF *]) |
673 by (subst(asm) RBT_inverse[symmetric, OF *]) |
682 (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject) |
674 (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject) |
683 } |
675 } |
684 then show ?thesis unfolding not_a_singleton_tree_def |
676 then show ?thesis |
685 by(auto split: rbt.split unit.split color.split) |
677 by(auto split: rbt.split unit.split color.split) |
686 qed |
678 qed |
687 |
679 |
688 lemma Pow_Set [code]: |
680 lemma Pow_Set [code]: |
689 "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}" |
681 "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}" |
727 |
719 |
728 lemma wf_set [code]: |
720 lemma wf_set [code]: |
729 "wf (Set t) = acyclic (Set t)" |
721 "wf (Set t) = acyclic (Set t)" |
730 by (simp add: wf_iff_acyclic_if_finite) |
722 by (simp add: wf_iff_acyclic_if_finite) |
731 |
723 |
732 definition not_non_empty_tree where [code del]: "not_non_empty_tree x y = x y" |
|
733 |
|
734 code_abort not_non_empty_tree |
|
735 |
|
736 lemma Min_fin_set_fold [code]: |
724 lemma Min_fin_set_fold [code]: |
737 "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)" |
725 "Min (Set t) = |
|
726 (if is_empty t |
|
727 then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t)) |
|
728 else r_min_opt t)" |
738 proof - |
729 proof - |
739 have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" .. |
730 have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" .. |
740 with finite_fold1_fold1_keys [OF *, folded Min_def] |
731 with finite_fold1_fold1_keys [OF *, folded Min_def] |
741 show ?thesis |
732 show ?thesis |
742 by (simp add: not_non_empty_tree_def r_min_alt_def r_min_eq_r_min_opt [symmetric]) |
733 by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric]) |
743 qed |
734 qed |
744 |
735 |
745 lemma Inf_fin_set_fold [code]: |
736 lemma Inf_fin_set_fold [code]: |
746 "Inf_fin (Set t) = Min (Set t)" |
737 "Inf_fin (Set t) = Min (Set t)" |
747 by (simp add: inf_min Inf_fin_def Min_def) |
738 by (simp add: inf_min Inf_fin_def Min_def) |
769 then show ?thesis |
760 then show ?thesis |
770 by (auto simp: INF_fold_inf finite_fold_fold_keys) |
761 by (auto simp: INF_fold_inf finite_fold_fold_keys) |
771 qed |
762 qed |
772 |
763 |
773 lemma Max_fin_set_fold [code]: |
764 lemma Max_fin_set_fold [code]: |
774 "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)" |
765 "Max (Set t) = |
|
766 (if is_empty t |
|
767 then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t)) |
|
768 else r_max_opt t)" |
775 proof - |
769 proof - |
776 have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" .. |
770 have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" .. |
777 with finite_fold1_fold1_keys [OF *, folded Max_def] |
771 with finite_fold1_fold1_keys [OF *, folded Max_def] |
778 show ?thesis |
772 show ?thesis |
779 by (simp add: not_non_empty_tree_def r_max_alt_def r_max_eq_r_max_opt [symmetric]) |
773 by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric]) |
780 qed |
774 qed |
781 |
775 |
782 lemma Sup_fin_set_fold [code]: |
776 lemma Sup_fin_set_fold [code]: |
783 "Sup_fin (Set t) = Max (Set t)" |
777 "Sup_fin (Set t) = Max (Set t)" |
784 by (simp add: sup_max Sup_fin_def Max_def) |
778 by (simp add: sup_max Sup_fin_def Max_def) |