I agree 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.
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
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
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