Homework 2

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