Homework 04

Definitions File

theory Defs
  imports Main "HOL-IMP.AExp"
begin

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

fun lval :: "lexp ⇒ state ⇒ val" where
"lval (N n) s = n" |
"lval (V x) s = s x" |
"lval (Plus a⇩1 a⇩2) s = lval a⇩1 s + lval a⇩2 s" |
"lval (Let x a b) s = lval b (s(x := lval a s))"


fun vars_of :: "lexp ⇒ string set" where
  "vars_of (N _) = {}"
| "vars_of (V x) = {x}"
| "vars_of (Plus a b) = vars_of a ∪ vars_of b"
| "vars_of (Let x a b) = {x} ∪ vars_of a ∪ vars_of b"

fun bounds_of :: "lexp ⇒ string set" where
  "bounds_of (N _) = {}"
| "bounds_of (V x) = {}"
| "bounds_of (Plus a b) = bounds_of a ∪ bounds_of b"
| "bounds_of (Let x a b) = {x} ∪ bounds_of a ∪ bounds_of b"


fun collect :: "lexp ⇒ 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 ⇒ string list" where
  "invent_names 0 = []"
| "invent_names (Suc n) = replicate (Suc n) (CHR ''v'') # invent_names n"

fun duplicates :: "'a list ⇒ 'a list" where
  "duplicates [] = []"
| "duplicates (x # xs) = (if x ∈ set xs then x # duplicates xs else duplicates xs)"

end

Template File

theory Submission
  imports Defs
begin

inductive path :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for E :: "('a ⇒ 'a ⇒ bool)"

theorem no_cycle:
  fixes f :: "'a ⇒ nat"
  assumes "∀a b. E a b ⟶ f a ≤ f b" "∀w. E v w ⟶ f v < f w"
  shows "¬ (∃xs. path E (v # xs @ [v]))"
  sorry





lemma example:
  "lval (Let ''x'' (N 5) (Let ''y'' (V ''x'') (Plus (V ''x'') (Plus (V ''y'') (V ''x''))))) <> = 15"
  by eval

paragraph ‹Step 1›
fun replace :: "lexp ⇒ vname ⇒ lexp ⇒ lexp" where
"replace e x (Let u a b) = Let u (replace e x a) (replace e x b)"
(* Fill in missing cases *)
| "replace e x a = a"

paragraph ‹Step 2›
theorem lval_upd_state_same:
  "x ∉ vars_of a ⟹ lval a (s(x := v)) = lval a s"
  sorry

paragraph ‹Step 3›
theorem lval_replace:
  assumes "x ∉ vars_of a" "bounds_of a ∩ vars_of e = {}"
  shows "lval (replace e x a) (s(x := lval e s)) = lval a s"
  sorry

paragraph ‹Step 4›
definition linearize :: "lexp ⇒ lexp" where (* Complete definition *)
  "linearize e = (let
    exps = undefined;
    names = undefined;
    m = zip exps names
  in fold (λ(a, x) e. Let x a (replace a x e)) m e)"

theorem test_case1:
  "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''))"
  sorry (* by eval *)

theorem test_case2:
  "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'')))"
  sorry (* by eval *)

paragraph ‹(Bonus) Step 6›
theorem linearize_correct:
  assumes "∀x. x ∈ vars_of e ⟶ CHR ''v'' ∉ set x" "bounds_of e = {}"
  shows "lval (linearize e) s = lval e s"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem no_cycle:
  fixes f :: "'a ⇒ nat"
  assumes "∀a b. E a b ⟶ f a ≤ f b" "∀w. E v w ⟶ f v < f w"
  shows "¬ (∃xs. path E (v # xs @ [v]))"
  using assms by (rule Submission.no_cycle)

theorem lval_upd_state_same:
  "x ∉ vars_of a ⟹ lval a (s(x := v)) = lval a s"
  by (rule Submission.lval_upd_state_same)

theorem lval_replace:
  assumes "x ∉ vars_of a" "bounds_of a ∩ vars_of e = {}"
  shows "lval (replace e x a) (s(x := lval e s)) = lval a s"
  using assms by (rule Submission.lval_replace)

theorem test_case1:
  "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''))"
  by (rule Submission.test_case1)

theorem test_case2:
  "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'')))"
  by (rule Submission.test_case2)

theorem linearize_correct:
  assumes "∀x. x ∈ vars_of e ⟶ CHR ''v'' ∉ set x" "bounds_of e = {}"
  shows "lval (linearize e) s = lval e s"
  using assms by (rule Submission.linearize_correct)

end