theory VCGExec = ProofCalculus + VCOpt + TermCodegen:

section {* Control Flow Graph *}

lemma [code]:
"addr_of_sys_xcpt s = (if s = NullPointer then 0 else if s = ClassCast then 1 
 else if s = OutOfMemory then 2 else (arbitrary::nat))"
(*<*)
by (simp add: addr_of_sys_xcpt_def)
(*>*)


lemma [code]:
"extractTy (Ty ex' tp, ex) = (if ex'=ex then [tp] else [])"
(*<*) by simp (*>*)


section {* Weakest Precondition Operator *}

section {* Wellformedness *}

consts prefix :: "('a list \<times> 'a list) \<Rightarrow> bool" 

recdef prefix "measure (\<lambda> (xs,ys). length xs)"
"prefix ([],ys) = True"
"prefix (x#xs,[]) = False"
"prefix (x#xs,y#ys) = ((x = y) \<and> prefix (xs,ys))"

lemma prefix_append:
"\<And> ys. prefix (xs,ys) = (\<exists> zs. ys = xs @ zs)"
(*<*)
apply (induct xs)
apply simp
apply simp
apply (rule iffI)
apply (case_tac ys)
apply simp
apply simp

apply atomize
apply (case_tac ys)
apply simp
apply simp
done
(*>*)

consts
  checkPosS :: "jbc_prog \<Rightarrow> (pos list) \<Rightarrow> StrBool"

constdefs toString::"pos \<Rightarrow> string"
"toString \<equiv> (\<lambda> (C,M,pc::nat). ''(''@C@'',''@M@'',''@BCVExec.toString pc@'')'')"

primrec
 "checkPosS \<Pi> [] = TRUE"
 "checkPosS \<Pi> (p#ps) = (if (let scsn = map fst (succsNormal \<Pi> p);
                            scse = map fst (succsExcept \<Pi> p)
                       in list_all (\<lambda>p'. ((idx (domC \<Pi>) p' \<le> idx (domC \<Pi>) p) 
                                          \<longrightarrow> anF \<Pi> p' \<noteq> None) \<and> p' mem (domC \<Pi>) \<and> 
                                          (p' mem scsn \<longrightarrow> handlesEx (fst \<Pi>) p' = None)) 
                          (scsn @ scse) \<and>  (set scse \<subset> set (domC \<Pi>)) ) \<and> throwChk (\<Pi>,cmd \<Pi> p,anF \<Pi> p,p) \<and> 
                                            invokeChk (\<Pi>,cmd \<Pi> p,anF \<Pi> p,p) 
                       then (checkPosS \<Pi> ps) else FALSE (''Error at position::''@(toString p)))"



constdefs wfS::"jbc_prog \<Rightarrow> StrBool"
"wfS \<Pi> == (let cp = (checkPosS \<Pi> (domC \<Pi>))
           in (if (cp \<noteq> TRUE) 
               then cp
               else (if (\<not> (checkExTables \<Pi>)) 
                     then FALSE ''Exception tables malformed''
                     else (if (\<not> (distinct (classnames (fst \<Pi>))))
                           then FALSE ''Classnames not distinct''
                           else (if (\<not> (distinct (methodnames (fst \<Pi>))))
                                 then FALSE ''Methodnames not distinct''
                                 else (if (\<not> (prefix (SystemClasses,fst \<Pi>)))
                                       then FALSE ''Systemclasses are expected in front.''
                                       else (if (\<not> (ipc \<Pi> mem (domC \<Pi>)))
                                             then FALSE ''initial position missing''
                                             else (let wfTy_P = (wf_jvm_prog_phi (pTy (fst \<Pi>)) (fst \<Pi>)) 
                                                   in (if \<not> wfTy_P
                                                   then FALSE ''program not welltyped''
                                                   else (if (\<not> (fst (snd (method (fst \<Pi>) (fst (ipc \<Pi>)) (fst (snd (ipc \<Pi>))))) = []))
                                                         then FALSE ''main method malformed''
                                                         else TRUE))))))))))"



lemma wf_eq [code]:
"wf Pi = (checkPos Pi (domC Pi) \<and>  checkExTables Pi \<and> 
         distinct (classnames (fst Pi)) \<and> 
         distinct (methodnames (fst Pi))  \<and> 
         prefix (SystemClasses,fst Pi) \<and> (ipc Pi mem (domC Pi))
         \<and>  wf_jvm_prog_phi (pTy (fst Pi)) (fst Pi) \<and> fst (snd (method (fst Pi) (fst (ipc Pi)) (fst (snd (ipc Pi))))) = []
         )"
(*<*)
apply (rule iffI)
apply (simp only: JBC_VCG.wf_def)
apply (erule conjE)+
apply (subgoal_tac "\<exists> P An. Pi = (P,An)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add:  prefix_append set_mem_eq BCVExec.methodnames_def methodnames_def JBC_VCG.wf_def)

apply (simp only: JBC_VCG.wf_def)
apply (erule conjE)+
apply (subgoal_tac "\<exists> P An. Pi = (P,An)")
 prefer 2
 apply fastsimp
apply (erule exE)+

apply (simp add: prefix_append set_mem_eq methodnames_def)
done
(*>*)



section {* Setting up the verification environment *}

lemma safeP_frs_length:
"\<lbrakk> s \<in> safeP \<Pi>; fst (snd (fst s)) \<noteq> fst (snd (ipc \<Pi>)) \<rbrakk> \<Longrightarrow> Suc 0 < length (snd (snd (fst (snd s))))"
(*<*)
apply (drule JBC_SafetyLogic.safeP_state)
apply (erule exE)+
apply (case_tac "frs")
apply (simp add: ipc_def main_def)

apply simp
done
(*>*)

lemma evalE_Call_Cn:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow> evalE \<Pi> s (Call (Cn v)) = v"
(*<*) by (simp add: evalE_evalEs.simps split_def) (*>*)

lemma evalE_Call_Neg:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow> evalE \<Pi> s (Call (Neg ex)) = Bool (\<not> the_Bool (evalE \<Pi> s (Call ex)))"
(*<*) by (simp add: evalE_evalEs.simps split_def) (*>*)

lemma evalE_Call_Imp:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow> 
 evalE \<Pi> s (Call (Imp ex ex')) = Bool (the_Bool (evalE \<Pi> s (Call ex)) \<longrightarrow> the_Bool (evalE \<Pi> s (Call ex')))"
(*<*) by (simp add: evalE_evalEs.simps split_def) (*>*)


lemma evalE_Call_And:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow>
 evalE \<Pi> s (Call (And es)) = Bool (list_all (\<lambda> ex. the_Bool (evalE \<Pi> s (Call ex))) es)"
(*<*)
apply (simp add: evalE_evalEs.simps split_def)
apply (induct "es" rule: list.induct)
apply simp
apply (rule iffI)
apply simp
apply ( simp add: the_Bool_True)
done
(*>*)


lemma evalE_Call_Num:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow>
 evalE \<Pi> s (Call (Num ex no ex')) = liftI (numop no) (evalE \<Pi> s (Call ex)) (evalE \<Pi> s (Call ex'))"
(*<*) by (simp add: evalE_evalEs.simps split_def) (*>*)


lemma evalE_Call_Rel:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow> evalE \<Pi> s (Call (Rel ex ro ex')) = liftR (relop ro) (evalE \<Pi> s (Call ex)) (evalE \<Pi> s (Call ex'))"
(*<*) by (simp add: evalE_evalEs.simps split_def) (*>*)

lemma evalE_Call_Eq:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow> evalE \<Pi> s (Call (Eq ex ex')) = Bool (evalE \<Pi> s (Call ex) = (evalE \<Pi> s (Call ex')))"
(*<*) by (simp add: evalE_evalEs.simps split_def) (*>*)


lemma triple_simp:
"(fst x, fst (snd x), snd (snd x)) = x"
(*<*) by fastsimp (*>*)

lemma evalE_Call_Forall:
"Suc 0 < length (snd (snd (fst (snd s)))) \<Longrightarrow> evalE \<Pi> s (Call (Forall v ex)) =
(let (p, \<sigma>, e) = s
 in Bool (\<forall>v'. the_Bool (evalE \<Pi> (p, \<sigma>, e\<lparr>lv := (lv e)(v := v')\<rparr>) (Call ex))))"
(*<*)
apply (simp add: evalE_evalEs.simps split_def)
apply (rule doubleAllI, rule allI)
apply (simp only: callstate_lv triple_simp Let_def split_def fst_conv snd_conv)
apply (subgoal_tac "\<exists> p \<sigma> e. s = (p,\<sigma>,e)") 
 prefer 2
 apply (rule_tac x="fst s" in exI)
 apply (rule_tac x="fst (snd s)" in exI)
 apply (rule_tac x="snd (snd s)" in exI)
 apply (simp only: triple_simp)
apply (subgoal_tac "\<exists> p' \<sigma>' e'. callstate s = (p',\<sigma>',e')") 
 prefer 2
 apply (rule_tac x="fst (callstate s)" in exI)
 apply (rule_tac x="fst (snd (callstate s))" in exI)
 apply (rule_tac x="snd (snd (callstate s))" in exI)
 apply (simp only: triple_simp)
apply (erule exE)+
apply (simp add: callstate_lv_inv)
done
(*>*)

lemma evalE_Ty_Integer:
"evalE \<Pi> s (Ty ex Integer) = Bool (\<exists>x. evalE \<Pi> s ex = Intg x)"
(*<*)
apply (simp add: evalE_evalEs.simps split_def)
apply (case_tac "evalE \<Pi> s ex")
apply simp+
apply (simp add: split_def)
done
(*>*)

lemma evalE_FrNr':
"evalE \<Pi> s FrNr = Intg (int (length (snd (snd (fst (snd s))))))"
(*<*) by (simp add: split_def) (*>*)


lemma evalE_And':
"evalE \<Pi> s (And es) = Bool (list_all (\<lambda> ex. the_Bool (evalE \<Pi> s ex)) es)"
(*<*)
apply (simp add: evalE_And list_all_conv)
apply (rule iffI)
apply (rule ballI)
apply (erule_tac x="evalE \<Pi> s x" in ballE)
apply simp

apply (induct es rule: list.induct)
apply simp

apply simp
apply (case_tac "x = a")
apply simp

apply simp

apply (rule ballI)
apply (induct es rule: list.induct)
apply simp

apply simp
apply (case_tac "x = evalE \<Pi> s a")
apply simp
apply (rule the_Bool_True)
apply simp

apply simp
done
(*>*)

lemma evalE_Pos':
"the_Bool (evalE \<Pi> s (Pos p)) \<Longrightarrow> fst s = p"
(*<*) by (simp add: evalE_Pos) (*>*)


lemmas evalE_simps = evalEs_empty evalEs_cons evalE_Cn evalE_Num evalE_Imp evalE_Neg evalE_Rel evalE_Eq evalE_Forall 
                     evalE_Neg evalE_And' evalE_Ty_Integer evalE_Ite evalE_FrNr'
                     evalE_Call_Cn evalE_Call_And evalE_Call_Neg evalE_Call_Imp evalE_Call_Num evalE_Call_Rel evalE_Call_Eq
                     evalE_Call_Forall 

lemmas sem_simps =  valid_def evalE_simps liftR_def relop_def liftI_def numop_def the_Intg.simps the_Bool.simps val.simps

end