Cookies disclaimer

I agree 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.


Download Files

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"

  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)

  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)"

  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)))"


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'"

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"

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)"

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

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"

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


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)


Terms and Conditions