Homework 7

Definitions File

theory Defs
  imports "HOL-IMP.Def_Init" "HOL-IMP.Big_Step" "HOL-IMP.Sec_Typing"
begin


consts erase :: "level \<Rightarrow> com \<Rightarrow> com"


end

Template File

theory Submission
  imports Defs
begin

fun erase :: "level \<Rightarrow> com \<Rightarrow> com"  where
  "erase _ = undefined"

theorem erase_correct:
  "\<lbrakk> (c,s) \<Rightarrow> s'; (erase l c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (< l) \<rbrakk>
   \<Longrightarrow> s' = t' (< l)"
  sorry

prop "\<lbrakk> (c,s) \<Rightarrow> s';  0 \<turnstile> c;  s = t (< l) \<rbrakk>
  \<Longrightarrow> \<exists>t'. (erase l c,t) \<Rightarrow> t' \<and> s' = t' (< l)"
prop "\<lbrakk> (erase l c,s) \<Rightarrow> s';  0 \<turnstile> c;  s = t (< l) \<rbrakk> \<Longrightarrow> \<exists>t'. (c,t) \<Rightarrow> t'"
theorem well_initialized_commands:
  assumes "D A c B"
      and "s = s' on A"
      and "(c,s) \<Rightarrow> t"
      and "(c,s') \<Rightarrow> t'"
  shows "t=t' on B"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem erase_correct: "\<lbrakk> (c,s) \<Rightarrow> s'; (erase l c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (< l) \<rbrakk>
   \<Longrightarrow> s' = t' (< l)"
  by (rule Submission.erase_correct)

theorem well_initialized_commands: "(D A c B) \<Longrightarrow> (s = s' on A) \<Longrightarrow> ((c,s) \<Rightarrow> t) \<Longrightarrow> ((c,s') \<Rightarrow> t') \<Longrightarrow> t=t' on B"
  by (rule Submission.well_initialized_commands)

end