Theory Singleton_List

section ‹Auxiliary Algorithm for Testing Whether "set xs" is a Singleton Set›
theory Singleton_List
  imports Main
begin

definition "singleton x = [x]" 

fun is_singleton_list :: "'a list ⇒ bool" where
  "is_singleton_list [x] = True" 
| "is_singleton_list (x # y # xs) = (x = y ∧ is_singleton_list (x # xs))"
| "is_singleton_list _ = False"


lemma is_singleton_list: "is_singleton_list xs ⟷ set (singleton (hd xs)) = set xs"
  by (induct xs rule: is_singleton_list.induct, auto simp: singleton_def)

lemma is_singleton_list2: "is_singleton_list xs ⟷ (∃ x. set xs = {x})"  
  by (induct xs rule: is_singleton_list.induct, auto)

end