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

This is the task corresponding to homework 5.

## Resources

### Definitions File

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

declare[[syntax_ambiguity_warning=false]]

definition "is_false (x :: int) \<equiv> x = 0"
definition "is_true (x :: int) \<equiv> \<not>(is_false x)"

lemma is_false_iff_eq_zero [iff]: "is_false x \<longleftrightarrow> x = 0" unfolding is_false_def by simp
lemma is_true_iff_neq_zero [iff]: "is_true x \<longleftrightarrow> x \<noteq> 0" unfolding is_true_def by simp

datatype scom = sSKIP
| sAssign vname aexp                ("_ ::= _" [1000, 61] 61)
| sSeq    scom  scom                  ("_;;/ _"  [60, 61] 60)
| sWhile  aexp scom                  ("(WHILE _/ DO _)"  [0, 61] 61)
| sSwitch aexp "(aexp * scom) list"  ("(SWITCH _/ CASES _)"  [0, 61] 61)

consts sbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool"

consts scom_to_com :: "scom \<Rightarrow> com"

consts ssmall_step :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool"

consts ssmall_steps :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool"

consts nsbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool"

end```

### Template File

```theory Submission
imports Defs
begin

declare fun_upd_apply[simp del](* helpful for the automation here *)

inductive sbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>s" 55)

fun scom_to_com :: "scom \<Rightarrow> com"  where
"scom_to_com _ = SKIP"

lemma big_step_scom_to_com_if_big_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (scom_to_com c, s) \<Rightarrow> t"
sorry

lemma sbig_step_if_big_step_scom_to_com: "(scom_to_com c, s) \<Rightarrow> t \<Longrightarrow> (c, s) \<Rightarrow>s t"
sorry

corollary "(c, s) \<Rightarrow>s t \<longleftrightarrow> (scom_to_com c, s) \<Rightarrow> t" inductive ssmall_step :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool" (infix "\<rightarrow>s" 55)
sorry

abbreviation ssmall_steps :: "scom * state \<Rightarrow> scom * state \<Rightarrow> bool" (infix "\<rightarrow>s*" 55)
where "x \<rightarrow>s* y \<equiv> star ssmall_step x y"

lemma ssmall_steps_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<rightarrow>s* (sSKIP, t)"
sorry

lemma sbig_step_if_ssmall_steps: "cs \<rightarrow>s* (sSKIP, t) \<Longrightarrow> cs \<Rightarrow>s t"
sorry

corollary "(c, s) \<Rightarrow>s t \<longleftrightarrow> (c, s) \<rightarrow>s* (sSKIP, t)" inductive nsbig_step :: "scom \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>ns" 55)
sorry

lemma nsbig_step_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<Rightarrow>ns t"
sorry

lemma conjecture_true: "(c, s) \<Rightarrow>ns t \<Longrightarrow> \<exists>t. (c, s) \<Rightarrow>ns t \<and> (c, s) \<Rightarrow>s t"
sorry

lemma conjecture_false: "\<exists>c s t. (c, s) \<Rightarrow>ns t \<and> \<not>(\<exists>t. (c, s) \<Rightarrow>ns t \<and> (c, s) \<Rightarrow>s t)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma big_step_scom_to_com_if_big_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (scom_to_com c, s) \<Rightarrow> t"
by (rule Submission.big_step_scom_to_com_if_big_step)

lemma sbig_step_if_big_step_scom_to_com: "(scom_to_com c, s) \<Rightarrow> t \<Longrightarrow> (c, s) \<Rightarrow>s t"
by (rule Submission.sbig_step_if_big_step_scom_to_com)

lemma ssmall_steps_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<rightarrow>s* (sSKIP, t)"
by (rule Submission.ssmall_steps_if_sbig_step)

lemma sbig_step_if_ssmall_steps: "cs \<rightarrow>s* (sSKIP, t) \<Longrightarrow> cs \<Rightarrow>s t"
by (rule Submission.sbig_step_if_ssmall_steps)

lemma nsbig_step_if_sbig_step: "(c, s) \<Rightarrow>s t \<Longrightarrow> (c, s) \<Rightarrow>ns t"
by (rule Submission.nsbig_step_if_sbig_step)

end```

Terms and Conditions