Homework 2

Definitions File

theory Defs
  imports "HOL-IMP.AExp"
begin

fun count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
  "count [] _ = 0" |
  "count (x # xs) y = (if x = y then Suc (count xs y) else count xs y)"

fun subst :: "vname \<Rightarrow> aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
  "subst x a' (N n) = N n"
| "subst x a' (V y) = (if x=y then a' else V y)"
| "subst x a' (Plus a1 a2) = Plus (subst x a' a1) (subst x a' a2)"

lemma subst_lemma: "aval (subst x a' a) s = aval a (s(x := aval a' s))"
  by (induct a) auto

lemma comp: "aval a1 s = aval a2 s \<Longrightarrow> aval (subst x a1 a) s = aval (subst x a2 a) s"
  by (simp add: subst_lemma)


datatype aexp' = N' int | V' vname | Plus' aexp' aexp' | Let' vname aexp' 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' (Let' x a b) s = aval' b (s(x := aval' a s))"



consts count_tr :: "'a list \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> nat"

consts inline :: "aexp' \<Rightarrow> aexp"

consts elim :: "aexp' \<Rightarrow> aexp'"


end

Template File

theory Submission
  imports Defs
begin

fun count_tr :: "'a list \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> nat"   where
  "count_tr _ _ _ = 0"

lemma tailrec_count: "count_tr xs y 0 = count xs y"
  sorry

fun inline :: "aexp' \<Rightarrow> aexp"  where
  "inline _ = (N 0)"

value "inline (Let' ''x'' (Plus' (N' 1) (N' 1)) (Plus' (V' ''x'') (V' ''x''))) =
   Plus (Plus (N 1) (N 1)) (Plus (N 1) (N 1))"

theorem aval_inline: "aval (inline e) s = aval' e s"
  sorry

fun elim :: "aexp' \<Rightarrow> aexp'"  where
  "elim a = a"

value "elim (Let' ''x'' (N' 1) (N' 0)) = N' 0"
value "elim (Let' ''x'' (N' 1) (Let' ''x'' (N' 2) (V' ''x''))) = Let' ''x'' (N' 2) (V' ''x'')"

theorem aval'_elim: "aval' (elim e) s = aval' e s"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma tailrec_count: "count_tr xs y 0 = count xs y"
  by (rule Submission.tailrec_count)

theorem aval_inline: "aval (inline e) s = aval' e s"
  by (rule Submission.aval_inline)

theorem aval'_elim: "aval' (elim e) s = aval' e s"
  by (rule Submission.aval'_elim)

end