Homework 4

Definitions File

theory Defs
  imports "HOL-IMP.AExp"
begin

declare [[names_short]]
declare Let_def[simp]

datatype lexp = N int | V vname | Plus lexp lexp | Let vname lexp lexp

fun lval :: "lexp \<Rightarrow> state \<Rightarrow> val" where
"lval (N n) s = n" |
"lval (V x) s = s x" |
"lval (Plus a\<^sub>1 a\<^sub>2) s = lval a\<^sub>1 s + lval a\<^sub>2 s" |
"lval (Let x a b) s = lval b (s(x := lval a s))"

fun vars_of :: "lexp \<Rightarrow> string set" where
  "vars_of (N _) = {}"
| "vars_of (V x) = {x}"
| "vars_of (Plus a b) = vars_of a \<union> vars_of b"
| "vars_of (Let x a b) = {x} \<union> vars_of a \<union> vars_of b"

fun bounds_of :: "lexp \<Rightarrow> string set" where
  "bounds_of (N _) = {}"
| "bounds_of (V x) = {}"
| "bounds_of (Plus a b) = bounds_of a \<union> bounds_of b"
| "bounds_of (Let x a b) = {x} \<union> bounds_of a \<union> bounds_of b"

fun collect :: "lexp \<Rightarrow> lexp list" where
  "collect (N n) = []"
| "collect (V _) = []"
| "collect (Plus a b) = collect a @ Plus a b # collect b"
| "collect (Let x a b) = collect a @ collect b"

fun invent_names :: "nat \<Rightarrow> string list" where
  "invent_names 0 = []"
| "invent_names (Suc n) = replicate (Suc n) (CHR ''v'') # invent_names n"

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


consts path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"

consts replace :: "lexp \<Rightarrow> vname \<Rightarrow> lexp \<Rightarrow> lexp"

consts linearize :: "lexp \<Rightarrow> lexp"


end

Template File

theory Submission
  imports Defs
begin

inductive path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" for E 

theorem no_cycle:
  assumes "\<forall>a b. E a b \<longrightarrow> (f::'a \<Rightarrow> nat) a \<le> f b"
      and "\<forall>w. E v w \<longrightarrow> f v < f w"
  shows "\<not> (\<exists>xs. path E (v # xs @ [v]))"
  sorry

value "lval (Let ''x'' (N 5) (Let ''y'' (V ''x'') (Plus (V ''x'') (Plus (V ''y'') (V ''x''))))) <> = 15"

paragraph \<open>Step 1\<close>

fun replace :: "lexp \<Rightarrow> vname \<Rightarrow> lexp \<Rightarrow> lexp" where
"replace e x (Let u a b) = Let u (replace e x a) (replace e x b)"
| "replace _ = undefined"
| "replace e x a = a"

paragraph \<open>Step 2\<close>

theorem lval_upd_state_same:
  "x \<notin> vars_of a \<Longrightarrow> lval a (s(x := v)) = lval a s"
  sorry

paragraph \<open>Step 3\<close>

theorem lval_replace:
  assumes "x \<notin> vars_of a"
      and "bounds_of a \<inter> vars_of e = {}"
  shows "lval (replace e x a) (s(x := lval e s)) = lval a s"
  sorry

paragraph \<open>Step 4\<close>

definition linearize :: "lexp \<Rightarrow> lexp" where
 "linearize e = (let
     exps = undefined;
     names = undefined;
     m = zip exps names
   in fold (\<lambda>(a, x) e. Let x a (replace a x e)) m e)"

value "linearize (Plus (Plus (Plus (V ''a'') (N 3)) (N 4)) (Plus (V ''a'') (N 3)))
= Let ''v'' (Plus (V ''a'') (N 3)) (Plus (Plus (V ''v'') (N 4)) (V ''v''))"

value "linearize (Plus (Plus (Plus (V ''a'') (N 3)) (N 4)) (Plus (Plus (V ''a'') (N 3)) (N 4)))
= Let ''v'' (Plus (V ''a'') (N 3)) (Let ''vv'' (Plus (V ''v'') (N 4)) (Plus (V ''vv'') (V ''vv'')))"

paragraph \<open>(Bonus) Step 5\<close>

lemma linearize_correct:
  assumes "\<forall>x. x \<in> vars_of e \<longrightarrow> CHR ''v'' \<notin> set x"
      and "bounds_of e = {}"
  shows "lval (linearize e) s = lval e s"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem no_cycle: "(\<forall>a b. E a b \<longrightarrow> (f::'a \<Rightarrow> nat) a \<le> f b) \<Longrightarrow> (\<forall>w. E v w \<longrightarrow> f v < f w) \<Longrightarrow> \<not> (\<exists>xs. path E (v # xs @ [v]))"
  by (rule Submission.no_cycle)

theorem lval_upd_state_same: "x \<notin> vars_of a \<Longrightarrow> lval a (s(x := v)) = lval a s"
  by (rule Submission.lval_upd_state_same)

theorem lval_replace: "(x \<notin> vars_of a) \<Longrightarrow> (bounds_of a \<inter> vars_of e = {}) \<Longrightarrow> lval (replace e x a) (s(x := lval e s)) = lval a s"
  by (rule Submission.lval_replace)

lemma linearize_correct: "(\<forall>x. x \<in> vars_of e \<longrightarrow> CHR ''v'' \<notin> set x) \<Longrightarrow> (bounds_of e = {}) \<Longrightarrow> lval (linearize e) s = lval e s"
  by (rule Submission.linearize_correct)

end