###### Cookies disclaimer

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 07

This is the task corresponding to the second part of homework 7.

## Resources

Download Files

### 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```

Terms and Conditions