Homework 02

Definitions File

theory Defs
  imports "HOL-IMP.AExp" "HOL-IMP.BExp"
begin

datatype aexp = N int | V vname | Plus aexp aexp | Mult int aexp

fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a⇩1 a⇩2) s = aval a⇩1 s + aval a⇩2 s" |
"aval (Mult i a) s = i * aval a s"

end

Template File

theory Submission
  imports Defs
begin

fun rlenc :: "'a ⇒ nat ⇒ 'a list ⇒ ('a × nat) list" where
  "rlenc _ = undefined"

value "replicate (3::nat) (1::nat) = [1,1,1]"

theorem test1:
  ‹rlenc 0 0 ([1,3,3,8] :: int list) = [(0,0),(1,1),(3,2),(8,1)]›
  by eval
theorem test2:
  ‹rlenc 1 0 ([3,4,5] :: int list) = [(1,0),(3,1),(4,1),(5,1)]›
  by eval

fun rldec :: "('a × nat) list ⇒ 'a list" where
  "rldec _ = undefined"

theorem enc_dec: "rldec (rlenc a 0 l) = l"
  sorry



lemmas [simp] = algebra_simps

fun normal :: "aexp ⇒ bool" where
  "normal _ = undefined"

fun normalize :: "aexp ⇒ aexp" where
  "normalize _ = undefined"

theorem semantics_unchanged: "aval (normalize a) s = aval a s"
  sorry

theorem normalize_normalizes: "normal (normalize a)"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem test1:
  ‹rlenc 0 0 ([1,3,3,8] :: int list) = [(0,0),(1,1),(3,2),(8,1)]›
  by (rule Submission.test1)

theorem test2:
  ‹rlenc 1 0 ([3,4,5] :: int list) = [(1,0),(3,1),(4,1),(5,1)]›
  by (rule Submission.test2)

theorem enc_dec: "rldec (rlenc a 0 l) = l"
  by (rule Submission.enc_dec)

theorem semantics_unchanged: "aval (normalize a) s = aval a s"
  by (rule Submission.semantics_unchanged)

theorem normalize_normalizes: "normal (normalize a)"
  by (rule Submission.normalize_normalizes)

end