Theory Code_Target_Set

section‹Sets›
text‹While the default code generator setup for sets works fine, it does not make for particularly
readable code. The reason for this is that the default setup needs to work with potentially infinite
sets. All of the sets we need to use here are finite so we present an alternative setup for the
basic set operations which generates much cleaner code.›

theory Code_Target_Set
  imports "HOL-Library.Code_Cardinality"
begin

code_datatype set

lemma [code]:
  "Code_Cardinality.finite' = finite"
  "Code_Cardinality.card' = card"
  "Code_Cardinality.eq_set = HOL.equal"
  "Code_Cardinality.subset' = (⊆)"
  by (simp_all add: equal)

lemma [code]:
  ‹x ∈ set xs = List.member xs x›
  by simp

lemma [code]:
  ‹finite (set xs) ⟷ True›
  by simp

lemma [code]:
  ‹insert x (set xs) = set (List.insert x xs)›
  by (fact insert_code)

lemma [code]:
  ‹Set.remove x (set xs) = set (removeAll x xs)›
  by (fact remove_code)

lemma [code]:
  ‹set xs ∪ set ys = set (xs @ ys)›
  by simp

lemma [code]:
  ‹A - set xs = fold Set.remove xs A›
  by (fact minus_set_fold)

lemma [code]:
  ‹A ∩ set xs = set (filter (λx. x ∈ A) xs)›
  by (fact inter_set_filter)

lemma [code]:
  ‹card (set xs) = length (remdups xs)›
  by (fact List.card_set)

lemma [code]:
  ‹set xs ⊆ A ⟷ list_all (λx. x ∈ A) xs›
  by (auto simp add: list_all_iff)

lemma [code]:
  ‹A ⊂ set xs ⟷ A ⊆ set xs ∧ list_ex (λx. x ∉ A) xs›
  by (auto simp add: list_ex_iff)

lemma [code]:
  ‹HOL.equal A B ⟷ A ⊆ B ∧ B ⊆ A›
  by (fact equal_set_def)

end