Leftpad.thy

theory Leftpad
  imports Main
begin

definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
  where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s"

definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool"
  where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded"

lemma "isPadded padChar s (leftPad padChar targetLength s)"
  unfolding isPadded_def by (intro exI [where x = "targetLength - length s"] conjI, auto simp add: leftPad_def)

lemma "length (leftPad padChar targetLength s) = max targetLength (length s)"
  by (auto simp add: leftPad_def)

(* Same task but without using the standard library's `replicate` function *)

fun myReplicate :: "nat ⇒ 'a ⇒ 'a list"
  where "myReplicate 0 c = []"
  | "myReplicate (Suc n) c = myReplicate n c @ [c]"

lemma length_myReplicate[simp]: "length (myReplicate n c) = n" by (induct n, auto)
lemma set_myReplicate[simp]: "set (myReplicate n c) = (if n = 0 then {} else {c})" by (induct n, auto)

definition leftPad2 :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
  where "leftPad2 padChar targetLength s ≡ myReplicate (targetLength - length s) padChar @ s"

lemma "length (leftPad2 padChar targetLength s) = max targetLength (length s)"
  by (auto simp add: leftPad2_def)

lemma "isPadded padChar s (leftPad2 padChar targetLength s)"
  unfolding isPadded_def by (intro exI [where x = "targetLength - length s"] conjI, auto simp add: leftPad2_def)

end

what is padChar? Is it part of Main?

EDIT: nvm if I am reading this correctly its the character you are padding with right?