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.

# Homework 4.1

This task corresponds to homework 4.1. Deadline: November 20, 2018, 10 am.

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.Big_Step"
begin

end```

### Template File

```theory Submission
imports Defs
begin

fun exec :: "com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> state \<times> nat" where
"exec SKIP s f = (s, f)"
| "exec (x::=v) s f = (s(x:=aval v s), f)"
| "exec (c1;;c2) s f = (
let (s, f') = exec c1 s f in exec c2 s f')"
| "exec (IF b THEN c1 ELSE c2) s f =
(if bval b s then exec c1 s f else exec c2 s f)"
| "exec (WHILE b DO c) s (Suc f) = (
if bval b s then
(let (s, f') = exec c s f in
if f > 0 then exec (WHILE b DO c) s (min f f') else (s, 0)
) else (s, Suc f))"
| "exec _ s 0 = (s, 0)"

lemma exec_equiv_bigstep: "(\<exists>f f'. exec c s f = (s', f') \<and> f' > 0) \<longleftrightarrow> (c,s) \<Rightarrow> s'"
oops

paragraph "Step 1"

fun while_free :: "com \<Rightarrow> bool" where
"while_free _ = undefined"

paragraph "Step 2"

theorem while_free_fuel: "while_free c \<Longrightarrow> \<exists>f s' f'. exec c s f = (s', f') \<and> f' > 0"
sorry

paragraph "Step 3"

text \<open>Show this directly with one induction proof (using Isar)\<close>
theorem exec_imp_bigstep: "exec c s f = (s', f') \<Longrightarrow> f' > 0 \<Longrightarrow> (c,s) \<Rightarrow> s'"
sorry

text \<open>We show that the amount of fuel can never increase during an execution.\<close>
lemma exec_fuel_nonincreasing:
"exec c s f = (s', f') \<Longrightarrow> f' \<le> f"
sorry

text \<open>Show the following helpful lemma from which we get the two corollaries below,
which will be useful in the final proof:\<close>
lemma exec_add: "exec c s f = (s', f') \<Longrightarrow> f' > 0 \<Longrightarrow> exec c s (f + k) = (s', f' + k)"
sorry

lemma exec_mono:
"exec c s f = (s', f') \<Longrightarrow> f' > 0 \<Longrightarrow> f1 \<ge> f \<Longrightarrow> \<exists>f2. f2 \<ge> f' \<and> exec c s f1 = (s', f2)"
by (auto simp: exec_add dest: le_Suc_ex)

lemma exec_mono':
"exec c s f = (s', f') \<Longrightarrow> f' > 0 \<Longrightarrow> f2 \<ge> f' \<Longrightarrow> \<exists>f1. f1 \<ge> f \<and> exec c s f1 = (s', f2)"

text \<open>Use induction and the auxiliary lemmas above.\<close>
theorem bigstep_imp_exec: "(c,s) \<Rightarrow> s' \<Longrightarrow> \<exists>f f'. f' > 0 \<and> exec c s f = (s', f')"
sorry

corollary exec_equiv_bigstep: "(\<exists>f f'. exec c s f = (s', f') \<and> f' > 0) \<longleftrightarrow> (c,s) \<Rightarrow> s'"
by (metis bigstep_imp_exec exec_imp_bigstep)

end```

### Check File

```theory Check
imports Submission
begin

theorem while_free_fuel: "while_free c \<Longrightarrow> \<exists>f s' f'. exec c s f = (s', f') \<and> f' > 0"
by (rule Submission.while_free_fuel)

theorem bigstep_imp_exec: "(c,s) \<Rightarrow> s' \<Longrightarrow> \<exists>f f'. f' > 0 \<and> exec c s f = (s', f')"
by (rule Submission.bigstep_imp_exec)

lemma exec_fuel_nonincreasing:
"exec c s f = (s', f') \<Longrightarrow> f' \<le> f"
by (rule Submission.exec_fuel_nonincreasing)

lemma exec_add: "exec c s f = (s', f') \<Longrightarrow> f' > 0 \<Longrightarrow> exec c s (f + k) = (s', f' + k)"