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.

Download Files
### Definitions File

### Template File

### Check 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

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

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

Terms and Conditions