section \Run-Length Encoding\
theory "Curry-Club_May-2016_RLE"
imports Main "~~/src/HOL/Library/Code_Target_Nat"
begin
datatype element = a | b | c | d | e
\ \discrete elements for examples\
subsection \Decode\
fun decode :: "(nat \ 'a) list \ 'a list"
where
"decode [] = []"
| "decode ((n, x) # rest) = replicate n x @ decode rest"
value "decode [(4, a), (1, b), (2, c), (2, a), (1, d), (4, e)]"
subsection \Encode\
fun run_length :: "'a \ 'a list \ nat"
where
"run_length x [] = 0"
| "run_length x (y # ys) = (if x = y then Suc (run_length x ys) else 0)"
fun run_rest :: "'a \ 'a list \ 'a list"
where
"run_rest x [] = []"
| "run_rest x (y # ys) = (if x = y then run_rest x ys else y # ys)"
function encode :: "'a list \ (nat \ 'a) list"
where
"encode [] = []"
| "encode (x # xs) = (Suc (run_length x xs), x) # encode (run_rest x xs)"
by pat_completeness auto
lemma run_rest_length: "length (run_rest x xs) < Suc (length xs)"
by (induct xs) auto
termination encode
by (relation "measure length") (auto simp: run_rest_length)
value "encode [a, a, a, a, b, c, c, a, a, d, e, e, e, e]"
value "encode ''aaaabccaadeeee''"
subsection \Functional programs from mathematical specifications\
export_code encode decode in SML
export_code encode decode in OCaml
export_code encode decode in Scala
export_code encode decode in Haskell
subsection \Correctness\
lemma replicate_run_length: "replicate (run_length x xs) x @ run_rest x xs = xs"
by (induct xs) auto
theorem correctness: "decode (encode list) = list"
by (induct list rule: encode.induct) (auto simp: replicate_run_length)
subsection \Converse correctness for normal lists\
fun normal :: "(nat \ 'a) list \ bool"
where
"normal [] \ True"
| "normal ((n, x) # rest) \ n > 0 \ run_length x (decode rest) = 0 \ normal rest"
lemma run_rest0: "run_length x list = 0 \ run_rest x list = list"
by (induct list) auto
lemma run_length_replicate:
"run_length x (replicate n x @ list) = n + run_length x list"
by (induct n) auto
lemma run_rest_replicate: "run_rest x (replicate n x @ list) = run_rest x list"
by (induct n) auto
lemma encode_replicate:
"n > 0 \ run_length x list = 0 \
encode (replicate n x @ list) = (n, x) # encode (run_rest x list)"
by (cases n) (auto simp: run_length_replicate run_rest_replicate)
theorem converse_correctness: "normal list \ encode (decode list) = list"
by (induct list) (auto simp add: encode_replicate run_rest0)
end