header {* 
  \isaheader{Verification Condition Generator} 
*}

theory VCG = AbsSem:

text {* For technical reasons Isabelle's locales do not (yet?) support recursive definitions. Hence, we define the VCG outside and 
refer to this defintion inside the locale VCG, which we define below. This external definition looks quite ugly as a rat tail
of parameters is in the signature. The definition as it shoul be is derived as lemma {\bf vcgdef} below. *}

section {* Inductive Safety Formulas *}

(*<*)
lemma filterreduction:
"i mem (S:: 'a list) \<longrightarrow> (length [a\<in>S . a\<noteq>i] < length S)"
apply (induct S)
apply simp
apply (case_tac "i=a")
apply (rule impI)
apply auto
apply (subgoal_tac "\<forall> a\<in>set S. a \<noteq> i")
apply (simp add: set_mem_eq)
apply (simp add: set_mem_eq)
apply auto
done
(*>*)

consts
isafe:: "('pos list \<times>  'program \<times> ('pos \<Rightarrow> 'form option) \<times> 'pos \<times> 'form \<times> ('form list \<Rightarrow> 'form) \<times> ('form \<Rightarrow> 'form \<Rightarrow> 'form) \<times> ( 'program  \<Rightarrow> 'pos \<Rightarrow> 'form) \<times>  ( 'program  \<Rightarrow> 'pos \<Rightarrow> ('pos \<times> 'form) list) \<times> ( 'program  \<Rightarrow> 'pos \<Rightarrow> 'pos \<Rightarrow> 'form \<Rightarrow> 'form)) \<Rightarrow> 'form"

recdef 
isafe  "measure (\<lambda> a. length (fst a))"
"isafe (S,prg,anF,pc,FalseF',Conj',Impl',appF',succsF',wpF') = 
  (if \<not> (pc mem S) 
   then FalseF' 
   else  Conj' ([appF' prg pc] @ 
         (case (anF pc) of 
          None \<Rightarrow> (map (\<lambda> (pc',B). Impl' B 
                           (wpF' prg pc pc' (isafe ((filter (\<lambda> a. a \<noteq> pc) S),
                                                     prg,
                                                     anF,
                                                     pc',
                                                     FalseF',
                                                     Conj',
                                                     Impl',
                                                     appF',
                                                     succsF',
                                                     wpF')
                                            )
                            )
                       ) 
                      (succsF' prg pc)) 
       | Some a \<Rightarrow> [a])))"
(hints recdef_simp: filterreduction)


section {* External VCG *}


text {* The vcG functions takes the auxiliary functions from the framework as additional arguments *}

consts
vcG:: "('form list \<Rightarrow> 'form) \<Rightarrow> ('form \<Rightarrow> 'form \<Rightarrow> 'form) \<Rightarrow> 'form \<Rightarrow> ('program \<Rightarrow> 'pos) \<Rightarrow> ('program \<Rightarrow> 'form) \<Rightarrow> ('program \<Rightarrow> 'pos \<Rightarrow> 'form) \<Rightarrow> ('program \<Rightarrow> 'pos \<Rightarrow> ('pos \<times> 'form) list) \<Rightarrow> ('program \<Rightarrow> 'pos \<Rightarrow> 'pos \<Rightarrow> 'form \<Rightarrow> 'form) \<Rightarrow> ('program \<Rightarrow> 'pos list) \<Rightarrow> ('program \<Rightarrow> 'pos list) \<Rightarrow> ('program \<Rightarrow> ('pos \<Rightarrow> 'form option)) \<Rightarrow> 'program  \<Rightarrow> 'form"

defs vcG_def:
"vcG Conj Impl FalseF ipc initF safeF succsF wpF domC domA an p \<equiv> 
    (let an' = (\<lambda> i. isafe(domC p,p,an p,i,FalseF,Conj,Impl,safeF,succsF,wpF))
      in  (Conj ((Impl (initF p) (an' (ipc p)))#(map (\<lambda> i. Conj (map (\<lambda> (j,B). Impl (Conj [ (an' i), B]) 
                                                     ((wpF p i j) (an' j))) 
                                      (succsF p i))) 
                     (domA p)))))"

section {* Pre Safe States *}

text {* Here we define the set of pre safe states. These are all initial states and states that are reachable from those
by only traversing inductively safe intermediate states *}




section {* Generic Verification Conditons *}

locale VCG = AbsSem +

fixes vcg:: " 'prog  \<Rightarrow> 'form"
defines "vcg \<equiv> \<lambda> \<Pi>. vcG Conj Impl FalseF ipc initF safeF succsF wpF domC domA anF \<Pi>"

fixes isafe'::"('pos list \<times>  'prog \<times> 'pos) \<Rightarrow> 'form"
defines "isafe' \<equiv> \<lambda> (S,\<Pi>,pc). isafe(S,\<Pi>,(anF \<Pi>),pc,FalseF,Conj,Impl,safeF,succsF,wpF)" 
fixes isafeF::" 'prog  \<Rightarrow> 'pos \<Rightarrow> 'form"
defines "isafeF \<equiv> (\<lambda> \<Pi> pc. isafe' (domC \<Pi>,\<Pi>,pc))"




(*<*)
theorem (in VCG) isafe'_simps: 
"isafe' (S,\<Pi>,pc) = (if \<not> (pc mem S) 
                  then FalseF 
                  else Conj ([safeF \<Pi> pc]@
                       (case (anF \<Pi> pc) of 
                         None \<Rightarrow> (map (\<lambda> (pc',B). (Impl B ((wpF \<Pi> pc pc') 
                                                   (isafe' ((filter (\<lambda> a. a \<noteq> pc) S),\<Pi>,pc'))))
                                      ) 
                                      (succsF \<Pi> pc))   
                      | Some a \<Rightarrow> [a])))"
apply (unfold isafe'_def)
apply simp
apply (rule impI)
apply (simp only: split_def)
apply (simp only: fst_conv)
apply (simp only: snd_conv)
apply (simp only: fst_conv)
done
(*>*)

(*<*)
lemma (in VCG) isafe'induct:
assumes IH: "\<And>S \<Pi> pc. 
             \<forall> pc' B. (pc',B) \<in> set (succsF \<Pi> pc) \<and> (anF \<Pi> pc) = None \<and> (pc mem S) \<longrightarrow> P [a\<in>S. a\<noteq>pc] \<Pi> pc' \<Longrightarrow> P S \<Pi> pc"
shows "P (u\<Colon>'pos list) (v\<Colon>'prog) (x\<Colon>'pos)"
proof -
  have "(anF v) = (anF v) \<longrightarrow> succsF = succsF \<longrightarrow> P (u\<Colon>'pos list) (v::'prog) (x\<Colon>'pos)"
    apply (rule_tac P = "\<lambda>S \<Pi> pan pc FalseF' Conj' Impl' safeF' succsF' wpF'. (pan = (anF \<Pi>)) \<longrightarrow> succsF' = succsF \<longrightarrow>
      P (S\<Colon>'pos list) (\<Pi>\<Colon>'prog) (pc\<Colon>'pos)" in isafe.induct)
    apply (rule impI)+
    apply (rule IH)
    apply simp
    done
  thus ?thesis by simp

qed
(*>*)


(*<*)
lemma (in VCG) isafe'_red:
"(wf \<Pi>) \<longrightarrow> 
 (\<forall> pc. \<forall> B. (anF \<Pi> pc) = None \<longrightarrow> (noAnnOnWay succsF anF \<Pi> pc pc') \<longrightarrow> 
  isafe'([x\<in>l. x\<noteq>pc],\<Pi>,pc') = isafe'(l,\<Pi>,pc'))"
apply (rule_tac P="\<lambda> u v x. (wf v) \<longrightarrow>(\<forall> pc. \<forall> B. (anF v pc) = None \<longrightarrow> 
 (noAnnOnWay succsF anF v pc x) \<longrightarrow> isafe'([x\<in>u. x\<noteq>pc],v,x) = isafe'(u,v,x))" 
  and  u="l" and v="\<Pi>" and x="pc'" in isafe'induct)

apply (rule allI | rule impI)+
apply (rule_tac P="\<lambda> x. isafe' ([x \<in> S. x \<noteq> pca],\<Pi>,pc) = x" in ssubst[OF isafe'_simps])
apply (rule_tac P="\<lambda> x. x = (if \<not> pc mem S then \<FalseF>
           else \<Conj>([safeF \<Pi> pc] @
                  (case anF \<Pi> pc of None \<Rightarrow> map (\<lambda>(pc', B). B \<Impl> wpF \<Pi> pc pc' (isafe' ([a\<in>S . a \<noteq> pc], \<Pi>, pc'))) (succsF \<Pi> pc) | Some a \<Rightarrow> [a])))"
       in ssubst[OF isafe'_simps])
apply (subgoal_tac "pc \<noteq> pca")
apply (case_tac "\<not> (pc mem S)")
apply (simp only: split_if set_mem_eq)
apply (rule conjI)
prefer 2
apply (rule impI)
apply clarify
apply (rule impI)
apply (frule_tac pc'="pc" and l="S" and pc="pca" in notin_simp)
apply (simp only:split_if)
apply simp
apply (simp only:split_if)
apply (rule conjI)
apply (rule impI)
apply clarify
apply (rule impI)
apply (frule not_sym)
apply (simp only: set_mem_eq)
apply (frule_tac pc'="pc" and l="S" and pc="pca" in neg_notin_simp)
apply assumption
apply (simp only:split_if)
apply simp
apply (case_tac "(anF \<Pi> pc) = None")
prefer 2
apply (drule option_case_simp)
apply (erule exE)
apply (simp  del:isafe'_simps)
apply (simp (no_asm_simp) del:isafe'_simps)
apply (rule ConjEq)
apply (simp only: ListEq)
apply (rule conjI)
apply simp

apply (rule map_simp)
apply simp
apply (rule allI)
apply (simp only: split_paired_all)
apply (rename_tac "S" "\<Pi>" "pc" "pca" "pc'a" "Ba")
apply (rule impI)
apply (simp (no_asm_simp) del:isafe'_simps)
apply (rule ImplEq)
apply simp
apply (rule_tac f="(wpF \<Pi> pc pc'a)" in arg_cong)
apply (case_tac "pca \<in> set S")
prefer 2
apply (rule_tac f="isafe'" in arg_cong)
apply simp
apply (rule_tac pc="pca" and l="S" and pc'="pc" in filter_list_simp)
apply assumption

apply (erule_tac x="pc'a" in allE)
apply (subgoal_tac "None = None")
 prefer 2
 apply simp
apply (erule impE)
apply simp
apply (erule_tac x="Ba" in exI)

apply (erule_tac x="pca" in allE)
apply (drule mp, assumption)+
apply (subgoal_tac "noAnnOnWay succsF anF \<Pi> pca pc'a")
 prefer 2
 apply (simp only:noAnnOnWay_def)
 apply (erule exE) 
 apply (rule_tac x="l@[pc]" in exI)
 apply (rule conjI)
 apply (erule conjE)
 apply (frule_tac l="(pca#l)" and p="pc" and sc="succsF \<Pi>" and p'="pc'a" and B="Ba" in paths.step)
 apply assumption
 apply simp
 apply (simp only:noAnn_def)
 apply (rule allI)
 apply (rule impI)
 apply (subgoal_tac "p \<in> set (pca#l) \<or> p=pc")
  prefer 2
  apply simp
  apply (simp only:disj_commute)
 apply (case_tac "p = pc")
 apply simp
 apply simp
 apply (case_tac "p = pca")
 apply simp
 apply simp

apply (drule mp, assumption)
apply (drule_tac t="isafe' ?P" in sym)
apply simp
apply (rule_tac f="isafe'" in arg_cong)
apply simp
apply (rule_tac f="\<lambda> P. filter P S " in arg_cong)
apply (rule ext)
apply blast

apply (case_tac "pc = pca")
apply (simp only:noAnnOnWay_def)
apply (erule exE)
apply (subgoal_tac "isCycle succsF \<Pi> ((pca # l) @ [pca])")
apply (drule wf_anF)
apply (unfold enoughAn_def)
apply (erule_tac x="(pca#l)@[pca]" in allE)
apply (drule mp)
apply assumption
apply (erule conjE)
apply (drule_tac l="(pca#l)" and p="pca" in noAnn_ext)
apply assumption
apply clarify

apply (simp only:simp_thms)
apply (erule conjE)
apply (unfold isCycle_def)
apply (rule conjI)
apply assumption
apply simp
apply assumption
done
(*>*)

(*<*)
lemma (in VCG) isafeF_no_annotation:
"\<lbrakk> wf \<Pi>; 
   (anF \<Pi> pc) = None; 
   pc\<in> set (domC \<Pi>) \<rbrakk> \<Longrightarrow> 
(isafeF \<Pi> pc) = Conj ([safeF \<Pi> pc]@ 
                       (map (\<lambda> (pc',B). (Impl B ((wpF \<Pi> pc pc') (isafeF \<Pi> pc')))) 
                                (succsF \<Pi> pc)
                       ) 
                       )"
--{* This lemma proves that in sufficiently annotated programs (wf p pan) a function call isafe(domL p, pan, pc, ) never reaches address pc twice. It terminates without the artificial break implemented by feeding in (domL p). *}  
apply (subgoal_tac "enoughAn succsF \<Pi> anF")
 prefer 2
 apply (drule wf_anF)
 apply assumption
apply (unfold isafeF_def)
apply (simplesubst isafe'_simps)
apply (simp del:isafe'_simps add: set_mem_eq)
apply (rule ConjEq)
apply (simp only:ListEq)
apply (rule conjI)
apply simp
apply (rule map_simp)
apply simp
apply (rule allI)
apply (simp only: split_paired_all)
apply (rename_tac "pc''" "B")
apply (rule impI)
apply (simp only:split_def)
apply (rule ImplEq)
apply simp
apply (simp del:isafe'_simps)
apply (rule_tac f="(wpF \<Pi> pc pc'')" in arg_cong)
apply (erule_tac \<Pi>1="\<Pi>" and l1="domC \<Pi>" and pc'1="pc''" in isafe'_red[THEN impE])
apply (erule_tac x="pc" in allE)
apply (erule_tac x="B'" in allE)
apply (drule_tac P="(anF \<Pi> pc) = None" in mp)
apply assumption
apply (subgoal_tac "noAnnOnWay succsF anF \<Pi> pc pc''")
apply (drule_tac P="noAnnOnWay succsF anF \<Pi> pc pc''" in mp)
apply assumption
apply assumption
apply (erule_tac V="noAnnOnWay succsF anF \<Pi> pc pc'' \<longrightarrow> ?P" in thin_rl)
apply (unfold noAnnOnWay_def)
apply (rule_tac x="[]" in exI)
apply (rule conjI)
apply simp
apply (rule_tac p'="pc''" and B="B" and p="pc" and sc="succsF \<Pi>" in paths.start)
apply assumption
apply (unfold noAnn_def)
apply (rule allI)
apply (rule impI)
apply simp
done
(*>*)

(*<*)
lemma (in VCG) isafeFdef:
"\<lbrakk> wf \<Pi> \<rbrakk> \<Longrightarrow> 
(isafeF \<Pi> pc) = 
(if (pc \<in> set (domC \<Pi>))
 then Conj ([safeF \<Pi> pc] @
     (case (anF \<Pi> pc)
       of None \<Rightarrow> (map (\<lambda> (pc',B). (Impl B ((wpF \<Pi> pc pc') (isafeF \<Pi> pc')))) 
                  (succsF \<Pi> pc)) 
       | Some an \<Rightarrow> [an]))
 else FalseF
)"
apply (case_tac "pc\<in> set (domC \<Pi>)")
apply (simp only: if_True)
apply (case_tac "anF \<Pi> pc")
apply (simp only: if_True option.cases)
apply (drule_tac \<Pi>="\<Pi>" and pc="pc" in isafeF_no_annotation, assumption+)
apply (simp only: option.cases)
apply (simp add: isafeF_def isafe'_def  set_mem_eq )
apply (simp add: isafeF_def isafe'_def  set_mem_eq )
done
(*>*)

text {* This lemma shows that vcg could be defined as follows, if the locale
mechanism allowed us recursive definitions *}

lemma (in VCG) vcgdef:
"\<lbrakk> wf \<Pi> \<rbrakk> \<Longrightarrow> 
vcg \<Pi> = Conj ((Impl (initF \<Pi>) (isafeF \<Pi> (ipc \<Pi>)))#(map (\<lambda> pc. Conj (map (\<lambda> (pc',B). Impl (Conj [ (isafeF \<Pi> pc), B]) 
                                                        ((wpF \<Pi> pc pc') (isafeF \<Pi> pc'))) 
                                      (succsF \<Pi> pc))) 
                     (domA \<Pi>)))
           "
(*<*)
apply (simp only: vcg_def vcG_def Let_def isafeF_def isafe'_def)
apply simp
done
(*>*)


end