Theory Code_Set

(*  
    Title:      Code_Set.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

section "Code set"

theory Code_Set
  imports
    "HOL-Library.Code_Cardinality"
begin

lemma [code]:
  ‹UNIV = set Enum.enum›
  by (fact UNIV_enum)

lemma [code_unfold]:
  ‹- (Collect P) = Set.filter (Not ∘ P) UNIV›
  by auto

end