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 6

This is the task corresponding to homework 6.

## Resources

### Definitions File

```theory Defs imports "HOL-IMP.Compiler" begin

fun index_map :: "(int \<Rightarrow> 'a \<Rightarrow>'a) \<Rightarrow> int \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"index_map f i [] = []"
| "index_map f i (x#xs) = f i x # index_map f (i+1) xs"

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)
| Par com com             (infix "\<parallel>" 59)

inductive
small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) where
Assign:  "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
Seq1:   "(SKIP;c2,s) \<rightarrow> (c2,s)" |
Seq2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
IfTrue:  "bval b s \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
ParL: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1 \<parallel> c2,s) \<rightarrow> (c1' \<parallel> c2,s')" |
ParLSkip: "(SKIP \<parallel> c,s) \<rightarrow> (c,s)" |
ParR: "(c2,s) \<rightarrow> (c2',s') \<Longrightarrow> (c1 \<parallel> c2,s) \<rightarrow> (c1 \<parallel> c2',s')" |
ParRSkip: "(c \<parallel> SKIP,s) \<rightarrow> (c,s)"

inductive
nsteps :: "com * state \<Rightarrow> nat \<Rightarrow> com * state \<Rightarrow> bool" ("_ \<rightarrow>^_ _" [60,1000,60]999) where
zero_steps[simp,intro]: "cs \<rightarrow>^0 cs" |
one_step[intro]: "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow>^n cs'' \<Longrightarrow> cs \<rightarrow>^(Suc n) cs''"

lemmas small_step_induct = small_step.induct[split_format(complete)]
lemmas nsteps_induct = nsteps.induct[split_format(complete)]

definition small_step_pre :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<preceq>" 50) where
"c \<preceq> c' \<equiv> (\<forall>s t n. (c,s) \<rightarrow>^n (SKIP, t)  \<longrightarrow> (\<exists> n' \<ge> n. (c', s) \<rightarrow>^n' (SKIP, t)))"

end```

### Template File

```theory Submission imports Defs begin

fun iexec_abs :: "instr \<Rightarrow> config \<Rightarrow> config" where
"iexec_abs _ = undefined"

definition exec1_abs :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
("(_/ \<turnstile>\<^sub>a (_ \<rightarrow>/ _))" [59,0,59] 60) where
"exec1_abs _ \<equiv> undefined"

lemma exec1_absI [intro]:
"\<lbrakk>c' = iexec_abs (P!!i) (i,s,stk); 0 \<le> i; i < size P\<rbrakk> \<Longrightarrow> P \<turnstile>\<^sub>a (i,s,stk) \<rightarrow> c'"
sorry

abbreviation exec_abs :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
("(_/ \<turnstile>\<^sub>a (_ \<rightarrow>*/ _))" 50) where
"exec_abs _ \<equiv> undefined"

lemma index_map_len[simp]: "size (index_map f i l) = size l"
sorry

lemma index_map_idx[simp]: "\<lbrakk> 0 \<le> i; i < size l \<rbrakk> \<Longrightarrow> index_map f k l !! i = f (i + k) (l !! i)"
sorry

theorem cnv_correct: "P \<turnstile>\<^sub>a c \<rightarrow>* c' \<longleftrightarrow> cnv_to_rel P \<turnstile> c \<rightarrow>* c'"
sorry

definition small_step_equiv :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<approx>" 50) where
"small_step_equiv _ \<equiv> undefined"

theorem Par_commute: "c \<parallel> d \<approx> d \<parallel> c"
sorry

theorem Par_assoc: "(c \<parallel> d) \<parallel> e \<approx> c \<parallel> (d \<parallel> e)"
sorry

end```

### Check File

```theory Check imports Submission begin

theorem cnv_correct: "P \<turnstile>\<^sub>a c \<rightarrow>* c' \<longleftrightarrow> cnv_to_rel P \<turnstile> c \<rightarrow>* c'"
by (rule Submission.cnv_correct)

theorem Par_commute: "c \<parallel> d \<approx> d \<parallel> c"
by (rule Submission.Par_commute)

theorem Par_assoc: "(c \<parallel> d) \<parallel> e \<approx> c \<parallel> (d \<parallel> e)"
by (rule Submission.Par_assoc)

end```

Terms and Conditions