Homework 2

Definitions File

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

declare [[names_short]]
lemmas [simp] = algebra_simps

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

fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
"aval (Mult i a) s = i * aval a s"


consts rlenc :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> ('a \<times> nat) list"

consts rldec :: "('a \<times> nat) list \<Rightarrow> 'a list"

consts normal :: "aexp \<Rightarrow> bool"

consts normalize :: "aexp \<Rightarrow> aexp"


end

Template File

theory Submission
  imports Defs
begin

fun rlenc :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> ('a \<times> nat) list"  where
  "rlenc _ = undefined"

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

value "rlenc 0 0 ([1,3,3,8] :: int list) = [(0,0),(1,1),(3,2),(8,1)]"
value "rlenc 1 0 ([3,4,5] :: int list) = [(1,0),(3,1),(4,1),(5,1)]"

fun rldec :: "('a \<times> nat) list \<Rightarrow> 'a list"  where
  "rldec _ = undefined"

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

fun normal :: "aexp \<Rightarrow> bool"  where
  "normal _ = undefined"

fun normalize :: "aexp \<Rightarrow> 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 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