Homework 6

Definitions File

theory Defs
  imports "HOL-IMP.AExp" "HOL-IMP.Star"
begin

declare fun_upd_apply[simp del]
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 com = SKIP
  | Assign vname aexp                ("_ ::= _" [1000, 61] 61)
  | Seq    com  com                  ("_;;/ _"  [60, 61] 60)
  | While  aexp com                  ("(WHILE _/ DO _)"  [0, 61] 61)
  | Switch aexp "(aexp * com) list"  ("(SWITCH _/ CASES _)"  [0, 61] 61)

inductive big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55) where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk>(c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3\<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
WhileFalse: "is_false (aval a s) \<Longrightarrow> (WHILE a DO c,s) \<Rightarrow> s" |
WhileTrue: "\<lbrakk>is_true (aval a s\<^sub>1); (c,s\<^sub>1) \<Rightarrow> s\<^sub>2;  (WHILE a DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3\<rbrakk> \<Longrightarrow> (WHILE a DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
SwitchEmpty: "(SWITCH x CASES [],s) \<Rightarrow> s" |
SwitchTrue: "aval a1 s = aval a2 s \<Longrightarrow> (c,s) \<Rightarrow> s' \<Longrightarrow> (SWITCH a1 CASES ((a2,c)#acs), s) \<Rightarrow> s'" |
SwitchFalse: "aval a1 s \<noteq> aval a2 s \<Longrightarrow> (SWITCH a1 CASES acs,s) \<Rightarrow> s' \<Longrightarrow> (SWITCH a1 CASES ((a2,c)#acs), s) \<Rightarrow> s'"

code_pred big_step .
declare big_step.intros[intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]

inductive_cases sSkipE[elim!]: "(SKIP,s) \<Rightarrow> s'"
inductive_cases sAssignE[elim!]: "(x ::= a,s) \<Rightarrow> s'"
inductive_cases sSeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases sWhileE[elim]: "(WHILE a DO c, s) \<Rightarrow> s'"
inductive_cases sSwitch_nilE[elim!]: "(SWITCH a1 CASES [], s) \<Rightarrow> s'"
inductive_cases sSwitch_consE[elim!]: "(SWITCH a1 CASES ((a2, c)#acs), s) \<Rightarrow> s'"
declare [[coercion_enabled]] 
declare [[coercion "int :: nat \<Rightarrow> int"]]


fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"


lemma inth_append [simp]:
  "0 \<le> i \<Longrightarrow>
  (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
by (induction xs arbitrary: i) (auto simp: algebra_simps)

abbreviation (output)
  "isize xs == int (length xs)"

notation isize ("size")

datatype instr = 
  LOADI int | LOAD vname | ADD | STORE vname |
  JMP int | JMPNE int | JMPEQ int

type_synonym stack = "val list"
type_synonym config = "int \<times> state \<times> stack"

abbreviation "hd2 xs == hd(tl xs)"
abbreviation "tl2 xs == tl(tl xs)"

fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
"iexec instr (i,s,stk) = (case instr of
  LOADI n \<Rightarrow> (i+1,s, n#stk) |
  LOAD x \<Rightarrow> (i+1,s, s x # stk) |
  ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
  STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
  JMP n \<Rightarrow>  (i+1+n,s,stk) |
  JMPNE n \<Rightarrow> (if hd2 stk \<noteq> hd stk then i+1+n else i+1,s,tl2 stk) |
  JMPEQ n \<Rightarrow> (if hd2 stk = hd stk then i+1+n else i+1,s,tl2 stk))"

definition
  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
     ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
where
  "P \<turnstile> c \<rightarrow> c' = 
  (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"

lemma exec1I [intro, code_pred_intro]:
  "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
  \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
by (simp add: exec1_def)

abbreviation 
  exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
where
  "exec P \<equiv> star (exec1 P)"

lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]

code_pred exec1 by (metis exec1_def)

lemma iexec_shift [simp]: 
  "((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
by(auto split:instr.split)

lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
by (auto simp: exec1_def)

lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
by (induction rule: star.induct) (fastforce intro: star.step exec1_appendR)+

lemma exec1_appendL:
  fixes i i' :: int 
  shows
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
   P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
  unfolding exec1_def
  by (auto simp del: iexec.simps)

lemma exec_appendL:
  fixes i i' :: int 
  shows
 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
  P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
  by (induction rule: exec_induct) (blast intro: star.step exec1_appendL)+

lemma exec_Cons_1 [intro]:
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
by (drule exec_appendL[where P'="[instr]"]) simp

lemma exec_appendL_if[intro]:
  fixes i i' j :: int
  shows
  "size P' <= i
   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
   \<Longrightarrow> i' = size P' + j
   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
by (drule exec_appendL[where P'=P']) simp

text\<open>Split the execution of a compound program up into the execution of its
parts:\<close>

lemma exec_append_trans[intro]:
  fixes i' i'' j'' :: int
  shows
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
 size P \<le> i' \<Longrightarrow>
 P' \<turnstile>  (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
 j'' = size P + i''
 \<Longrightarrow>
 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
by(metis star_trans[OF exec_appendR exec_appendL_if])


declare Let_def[simp]

fun acomp :: "aexp \<Rightarrow> instr list" where
"acomp (N n) = [LOADI n]" |
"acomp (V x) = [LOAD x]" |
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"

lemma acomp_correct[intro]:
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
by (induction a arbitrary: stk) fastforce+



consts ccomp :: "com \<Rightarrow> instr list"


end

Template File

theory Submission
  imports Defs
begin

fun ccomp :: "com \<Rightarrow> instr list"  where
  "ccomp _ = undefined"

lemma ccomp_bigstep:
  "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma ccomp_bigstep: "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
  by (rule Submission.ccomp_bigstep)

end