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 5_1

This is the task corresponding to homework 5_1.

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.BExp" "HOL-IMP.Star"
begin

datatype
com = SKIP
| Assign vname aexp       ("_ ::= _" [1000, 61] 61)
| Seq    com  com         ("_;;/ _"  [60, 61] 60)
| If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
| While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
| THROW
| Attempt com com         ("(ATTEMPT _/ CLEANUP _)"  [0, 61] 61)

consts big_step :: "com \<times> state \<Rightarrow> com \<times> state \<Rightarrow> bool"

consts small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool"

end```

### Template File

```theory Submission
imports Defs
begin

paragraph "Step 1"

inductive big_step :: "com \<times> state \<Rightarrow> com \<times> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)

paragraph "Step 2"

lemmas big_step_induct = big_step.induct[split_format(complete)]
declare big_step.intros[intro]

paragraph "Step 3"

lemma big_step_result: "(c,s) \<Rightarrow> (c',s') \<Longrightarrow> (c' = SKIP \<or> c' = THROW)"
sorry

paragraph "Step 4"

inductive small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)

abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"

declare small_step.intros[simp,intro]

lemma big_to_small: "cs \<Rightarrow> xt \<Longrightarrow> cs \<rightarrow>* xt"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma big_step_result: "(c,s) \<Rightarrow> (c',s') \<Longrightarrow> (c' = SKIP \<or> c' = THROW)"
by (rule Submission.big_step_result)

lemma big_to_small: "cs \<Rightarrow> xt \<Longrightarrow> cs \<rightarrow>* xt"
by (rule Submission.big_to_small)

end```

Terms and Conditions