###### Cookies disclaimer

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

Download Files

### Definitions File

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

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

lemma "length (deduplicate xs) \<le> length xs"
by (induction xs rule: deduplicate.induct) auto

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 | PI' vname | Plus' aexp' aexp'

fun aval' where
"aval' (N' n) s = (n,s)" |
"aval' (V' x) s = (s x, s)" |
"aval' (PI' x) s = (s x, s(x := 1 + s x))" |
"aval' (Plus' a1 a2) s = (
let (v1, s') = aval' a1 s; (v2, s'') = aval' a2 s'
in (v1 + v2, s''))"

lemma "aval' (Plus' (PI' x) (V' x)) <> \<noteq> aval' (Plus' (V' x) (PI' x)) <>"
by auto

lemma aval'_inc': "aval' a s = (v,s') \<Longrightarrow> s x \<le> s' x"
apply (induct a arbitrary: s s' v)
apply (auto split: prod.splits)
apply fastforce
done

lemma aval'_inc:
"aval' a <> = (v, s') \<Longrightarrow> 0 \<le> s' x"
using aval'_inc' by (fastforce simp: null_state_def)

end```

### Template File

```theory Submission
imports Defs
begin

fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"add _ = undefined"

theorem add_assoc: "add (add x y) z = add x (add y z)"
sorry

theorem add_commut: "add x y = add y x"
sorry

datatype wexp = N val | V vname | Plus wexp wexp | Where wexp vname wexp

fun wval :: "wexp \<Rightarrow> state \<Rightarrow> val" where
"wval _ = undefined"

fun inline :: "wexp \<Rightarrow> aexp" where
"inline _ = undefined"

value
"inline (Where (Plus (V ''x'') (V ''x'')) ''x'' (Plus (N 1) (N 1))) =
aexp.Plus (aexp.Plus (aexp.N 1) (aexp.N 1)) (aexp.Plus (aexp.N 1) (aexp.N 1))"

theorem val_inline: "aval (inline e) s = wval e s"
sorry

fun elim :: "wexp \<Rightarrow> wexp" where
"elim _ = undefined"

theorem wval_elim: "wval (elim e) s = wval e s"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem add_assoc: "add (add x y) z = add x (add y z)"
by (rule Submission.add_assoc)

theorem add_commut: "add x y = add y x"
by (rule Submission.add_commut)

theorem val_inline: "aval (inline e) s = wval e s"
by (rule Submission.val_inline)

theorem wval_elim: "wval (elim e) s = wval e s"
by (rule Submission.wval_elim)

end```

Terms and Conditions