Homework 4.1

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)"
  by (metis exec_add le_Suc_ex le_add_same_cancel1)

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)"
  by (rule Submission.exec_add)

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

end