Skip to content

Instantly share code, notes, and snippets.

@DaveCTurner
Last active May 29, 2018
Embed
What would you like to do?
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
@mssabr01
Copy link

mssabr01 commented Apr 22, 2018

what is padChar? Is it part of Main?

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment