Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 2

This is the task corresponding to homework 2.

## Resources

### 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"

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```

Terms and Conditions