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