src/HOL/Library/RBT_Set.thy
changeset 79971 033f90dc441d
parent 73968 0274d442b7ea
equal deleted inserted replaced
79966:f83e9e9a898e 79971:033f90dc441d
    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))