Theory Lib_List_toString
theory Lib_List_toString
imports Lib_Numbers_toString
begin
section‹Printing Lists›
fun intersperse :: "'a ⇒ 'a list list ⇒ 'a list" where
"intersperse _ [] = []" |
"intersperse a [x] = x" |
"intersperse a (x#xs) = x @ a # intersperse a xs"
definition list_separated_toString :: "string ⇒ ('a ⇒ string) ⇒ 'a list ⇒ string" where
"list_separated_toString sep toStr ls = concat (splice (map toStr ls) (replicate (length ls - 1) sep))"
text‹A slightly more efficient code equation, which is actually not really faster (in certain languages)›
fun list_separated_toString_helper :: "string ⇒ ('a ⇒ string) ⇒ 'a list ⇒ string" where
"list_separated_toString_helper sep toStr [] = ''''" |
"list_separated_toString_helper sep toStr [l] = toStr l" |
"list_separated_toString_helper sep toStr (l#ls) = (toStr l)@sep@list_separated_toString_helper sep toStr ls"
lemma list_separated_toString_helper: "list_separated_toString = list_separated_toString_helper"
proof -
{ fix sep and toStr::"('a ⇒ char list)" and ls
have "list_separated_toString sep toStr ls = list_separated_toString_helper sep toStr ls"
by(induction sep toStr ls rule: list_separated_toString_helper.induct) (simp_all add: list_separated_toString_def)
} thus ?thesis by(simp add: fun_eq_iff)
qed
lemma list_separated_toString_intersperse:
"intersperse sep (map f xs) = list_separated_toString [sep] f xs"
apply(simp add: list_separated_toString_helper)
apply(induction "[sep]" f xs rule: list_separated_toString_helper.induct)
by simp+
definition list_toString :: "('a ⇒ string) ⇒ 'a list ⇒ string" where
"list_toString toStr ls = ''[''@ list_separated_toString '', '' toStr ls @'']''"
lemma "list_toString string_of_nat [1,2,3] = ''[1, 2, 3]''" by eval
end