Theory List_Group

theory List_Group
imports Sort_Descending
begin

section‹List Group›

function (sequential) list_group_eq :: "'a list ⇒ 'a list list" where
  "list_group_eq [] = []" |
  "list_group_eq (x#xs) = [x # takeWhile ((=) x) xs] @ list_group_eq (dropWhile ((=) x) xs)"
by pat_completeness auto
termination list_group_eq
apply (relation "measure (λN. length N )")
apply(simp_all add: le_imp_less_Suc length_dropWhile_le)
done

value "list_group_eq [1::int,2,2,2,3,1,4,5,5,5]"


function (sequential) list_group_eq_key :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list list" where
  "list_group_eq_key _ [] = []" |
  "list_group_eq_key f (x#xs) = [x # takeWhile (λy. f x = f y) xs] @ list_group_eq_key f (dropWhile (λy. f x = f y) xs)"
by pat_completeness auto
termination list_group_eq_key
apply (relation "measure (λ(f,N). length N )")
apply(simp_all add: le_imp_less_Suc length_dropWhile_le)
done

value "list_group_eq_key fst [(1::int, ''''), (2,''a''), (2,''b''), (2, ''c''), (3, ''c''), (1,''''), (4,'''')]"

lemma "list_group_eq_key id xs = list_group_eq xs"
apply(induction xs rule: list_group_eq.induct)
 by(simp_all add: id_def)

(*
lemma "sorted (map f (x#xs)) ⟹ list_group_eq_key f (x#xs) = [x # filter (λy. f x = f y) xs] @ list_group_eq_key f (filter (λy. f x ≠ f y) xs)"
  apply(simp)
  oops
lemma "sorted (x#xs) ⟹ distinct (list_group_eq_key f (x#xs)) ⟹ distinct (list_group_eq_key f xs)"
  apply(induction xs)
   apply(simp)
oops
*)

end