equal
deleted
inserted
replaced
29 |
29 |
30 declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set |
30 declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set |
31 Set.member Set.insert Set.remove UNIV Set.filter image |
31 Set.member Set.insert Set.remove UNIV Set.filter image |
32 Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter |
32 Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter |
33 card the_elem Pow sum prod Product_Type.product Id_on |
33 card the_elem Pow sum prod Product_Type.product Id_on |
34 Image trancl relcomp wf Min Inf_fin Max Sup_fin |
34 Image trancl relcomp wf_on wf_code Min Inf_fin Max Sup_fin |
35 "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)" |
35 "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)" |
36 sorted_list_of_set List.map_project List.Bleast]] |
36 sorted_list_of_set List.map_project List.Bleast]] |
37 |
37 |
38 |
38 |
39 section \<open>Lemmas\<close> |
39 section \<open>Lemmas\<close> |
642 show ?thesis |
642 show ?thesis |
643 using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1] |
643 using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1] |
644 by (simp add: relcomp_fold finite_fold_fold_keys[OF *]) |
644 by (simp add: relcomp_fold finite_fold_fold_keys[OF *]) |
645 qed |
645 qed |
646 |
646 |
647 lemma wf_set [code]: |
647 lemma wf_set: "wf (Set t) = acyclic (Set t)" |
648 "wf (Set t) = acyclic (Set t)" |
648 by (simp add: wf_iff_acyclic_if_finite) |
649 by (simp add: wf_iff_acyclic_if_finite) |
649 |
|
650 lemma wf_code_set[code]: "wf_code (Set t) = acyclic (Set t)" |
|
651 unfolding wf_code_def using wf_set . |
650 |
652 |
651 lemma Min_fin_set_fold [code]: |
653 lemma Min_fin_set_fold [code]: |
652 "Min (Set t) = |
654 "Min (Set t) = |
653 (if RBT.is_empty t |
655 (if RBT.is_empty t |
654 then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t)) |
656 then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t)) |