theory Test

imports Main

begin

consts list_add_aux :: "'a list \<Rightarrow> 'a list list \<Rightarrow> 'a list list"

function list_add:: "'a list list \<Rightarrow> 'a list list \<Rightarrow> 'a list list"
  where
    "list_add [] xs = xs"
  | "list_add [y] xs = list_add_aux y xs"
  | "list_add ((y'#ys)@[y]) xs = list_add (y'#ys) (list_add [y] xs)"
by(auto)(metis remdups_adj.cases rev_exhaust)
termination list_add  by(size_change)

lemma "list_add ((x#xs)@[x']) ys = list_add (x#xs) (list_add_aux x' ys)"
  sledgehammer
  by auto
  by (metis list_add.simps(2) list_add.simps(3))

end