Homework 7_1

Definitions File

theory Defs
  imports "HOL-IMP.Def_Init_Small"
begin

hide_const D



consts AV :: "com \<Rightarrow> vname set"

consts D :: "vname set \<Rightarrow> com \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

fun AV :: "com \<Rightarrow> vname set"  where
  "AV _ = undefined"

fun D :: "vname set \<Rightarrow> com \<Rightarrow> bool"  where
  "D _ = undefined"

theorem %invisible D_progress:
  assumes "c \<noteq> SKIP"
  shows "D (dom s) c \<Longrightarrow> \<exists> cs'. (c,s) \<rightarrow> cs'"
  using assms
proof (induction c arbitrary: s)
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
next
  case (If b c1 c2)
  then obtain bv where "bval b s = Some bv" by (auto dest!: bval_Some)
  then show ?case
    by(cases bv) (auto intro: small_step.IfTrue small_step.IfFalse)
qed (fastforce intro: small_step.intros)+

lemma %invisible D_incr: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> dom s \<union> AV c \<subseteq> dom s' \<union> AV c'"
  by (induction rule: small_step_induct) auto

lemma D_mono: "A \<subseteq> A' \<Longrightarrow> D A c \<Longrightarrow> D A' c"
  sorry

theorem D_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c \<Longrightarrow> D (dom s') c'"
  sorry

theorem D_sound: "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> c' \<noteq> SKIP \<Longrightarrow> D (dom s) c \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma D_mono: "A \<subseteq> A' \<Longrightarrow> D A c \<Longrightarrow> D A' c"
  by (rule Submission.D_mono)

theorem D_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c \<Longrightarrow> D (dom s') c'"
  by (rule Submission.D_preservation)

theorem D_sound: "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> c' \<noteq> SKIP \<Longrightarrow> D (dom s) c \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
  by (rule Submission.D_sound)

end