Homework 07

Definitions File

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


end

Template File

theory Submission
  imports Defs
begin

fun erase :: "level ⇒ com ⇒ com" where
  "erase _ _ = undefined"

theorem erase_correct:
  "⟦ (c,s) ⇒ s'; (erase l c,t) ⇒ t';  0 ⊢ c;  s = t (< l) ⟧
   ⟹ s' = t' (< l)"
  sorry

text ‹
In the theorem above we assumed that both @{term"(c,s)"}
and @{term "(erase l c,t)"} terminate. How about the following two properties:
›
lemma "⟦ (c,s) ⇒ s';  0 ⊢ c;  s = t (< l) ⟧
  ⟹ ∃t'. (erase l c,t) ⇒ t' ∧ s' = t' (< l)"
  oops
lemma "⟦ (erase l c,s) ⇒ s';  0 ⊢ c;  s = t (< l) ⟧ ⟹ ∃t'. (c,t) ⇒ t'"
  oops
text ‹Give an informal justification or a counterexample for each property!›

theorem well_initialized_commands:
  assumes "D A c B"
  assumes "s1 = s2 on A"
  assumes "(c,s1) ⇒ s1'"
  shows "∃s2'. (c,s2) ⇒ s2' ∧ s1'=s2' on B"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem erase_correct:
  "⟦ (c,s) ⇒ s'; (erase l c,t) ⇒ t';  0 ⊢ c;  s = t (< l) ⟧
   ⟹ s' = t' (< l)"
  by (rule Submission.erase_correct)

theorem well_initialized_commands:
  assumes "D A c B"
  assumes "s1 = s2 on A"
  assumes "(c,s1) ⇒ s1'"
  shows "∃s2'. (c,s2) ⇒ s2' ∧ s1'=s2' on B"
  using assms by (rule Submission.well_initialized_commands)

end