# Theory Lib_Enum_toString

```section‹Enum toString Functions›
theory Lib_Enum_toString
imports Main IP_Addresses.Lib_List_toString
begin

fun bool_toString :: "bool ⇒ string" where
"bool_toString True = ''True''" |
"bool_toString False = ''False''"

subsection‹Enum set to string›
fun enum_set_get_one :: "'a list ⇒ 'a set ⇒ 'a option" where
"enum_set_get_one []     S = None" |
"enum_set_get_one (s#ss) S = (if s ∈ S then Some s else enum_set_get_one ss S)"

lemma enum_set_get_one_empty: "enum_set_get_one ss {} = None"
by(induction ss) simp_all

lemma enum_set_get_one_None: "S ⊆ set ss ⟹ enum_set_get_one ss S = None ⟷ S = {}"
apply(induction ss)
apply(simp; fail)
apply(simp)
apply(intro conjI)
apply blast
by fast

lemma enum_set_get_one_Some: "S ⊆ set ss ⟹ enum_set_get_one ss S = Some x ⟹ x ∈ S"
apply(induction ss)
apply(simp; fail)
apply(simp split: if_split_asm)
apply(blast)
done
corollary enum_set_get_one_enum_Some: "enum_set_get_one enum_class.enum S = Some x ⟹ x ∈ S"
using enum_set_get_one_Some[where ss=enum_class.enum, simplified enum_UNIV] by auto

lemma enum_set_get_one_Ex_Some: "S ⊆ set ss ⟹ S ≠ {} ⟹ ∃x. enum_set_get_one ss S = Some x"
apply(induction ss)
apply(simp; fail)
apply(simp split: if_split_asm)
apply(blast)
done
corollary enum_set_get_one_enum_Ex_Some:
"S ≠ {} ⟹ ∃x. enum_set_get_one enum_class.enum S = Some x"
using enum_set_get_one_Ex_Some[where ss=enum_class.enum, simplified enum_UNIV] by auto

function enum_set_to_list :: "('a::enum) set ⇒ 'a list" where
"enum_set_to_list S = (if S = {} then [] else
case enum_set_get_one Enum.enum S of None ⇒ []
|  Some a ⇒ a#enum_set_to_list (S - {a}))"
by(pat_completeness) auto

termination enum_set_to_list
apply(relation "measure (λ(S). card S)")
apply(simp_all add: card_gt_0_iff)
apply(drule enum_set_get_one_enum_Some)
apply(subgoal_tac "finite S")
prefer 2
apply force
apply (meson card_Diff1_less)
done

(*this definition is simpler*)
lemma enum_set_to_list_simps: "enum_set_to_list S =
(case enum_set_get_one (Enum.enum) S of None ⇒ []
|  Some a ⇒ a#enum_set_to_list (S - {a}))"
by(simp add: enum_set_get_one_empty)
declare enum_set_to_list.simps[simp del]

lemma enum_set_to_list: "set (enum_set_to_list A) = A"
apply(induction A rule: enum_set_to_list.induct)
apply(case_tac "S = {}")
apply(simp add: enum_set_to_list.simps; fail)
apply(simp)
apply(subst enum_set_to_list_simps)
apply(simp)
apply(drule enum_set_get_one_enum_Ex_Some)
apply(clarify)
apply(simp)
apply(drule enum_set_get_one_enum_Some)
by blast

lemma "list_toString bool_toString (enum_set_to_list {True, False}) = ''[False, True]''" by eval

end
```