Homework 6

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