Theory Code_Set

theory Code_Set
imports Main
begin

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

text{*The following setup could help to get code generation for List.coset, 
  but it neither works correctly it complains that code
  equations for remove are missed, even when List.coset should be rewritten
  to an enum:*}

declare union_coset_filter [code del]
declare minus_coset_filter [code del]
declare inter_coset_fold [code del]
declare remove_code(2) [code del] (*changed*)
declare insert_code(2) [code del] (*changed*)

code_datatype set

(*
text{*The following code equation could be useful to avoid the problem of
  code generation for List.coset []:*}

lemma [code]: "List.coset ([]::'a::enum list) = set (enum_class.enum)"
  unfolding UNIV_coset [symmetric] using UNIV_enum .
*)

text{*The following code equation does never work, because the minus for sets
  requires Set.remove, which has been deleted from the code generation setup:*}

lemma [code]: "List.coset (l::'a::enum list) = set (enum_class.enum) - set l"
  by (metis Compl_eq_Diff_UNIV coset_def enum_UNIV)

text{*Now the following examples work:*}

value [code] "UNIV::bool set"
value [code] "List.coset ([]::bool list)"
value [code] "UNIV::Enum.finite_2 set"
value [code] "List.coset ([]::Enum.finite_2 list)"
value [code] "List.coset ([]::Enum.finite_5 list)"

text{*This declare allows to calculate the cardinal of the non-zero rows set.*}
declare compl_coset[code del]

end