header {* 
  \isaheader{VCG Invariant} 
*}


theory VCG_Invariant = VCG:

--{* In invariantVCG we show that if wpF computes weakest(!) preconditions and if branch conditions of succsF ensure progress
     then VCG emits invariants. *}

locale invariantVCG = VCG +

fixes isSafe'::"'prog \<Rightarrow> bool"
defines "isSafe' \<equiv> \<lambda> prg. \<forall> s s'. s \<in> initS prg \<and> (s,s') \<in> (effS prg)\<^sup>* \<longrightarrow> prg,s' \<Turnstile> saF prg (fst s')" 

assumes semImpI: "\<lbrakk> prg,s \<Turnstile> f1 \<Longrightarrow> prg,s \<Turnstile> f2 \<rbrakk> \<Longrightarrow> prg,s \<Turnstile> f1 \<Impl> f2"


assumes succsFprogress: "\<lbrakk> wf prg; correctAn prg; isSafe prg; (p,m) \<in> Reachables prg; 
                           prg,(p,m) \<Turnstile> B; (p',B) \<in> set (succsF prg p'') \<rbrakk> \<Longrightarrow> p=p'' \<and> (\<exists> m'. ((p,m),(p',m')) \<in> (effS prg))"



assumes completeWpF: "\<lbrakk> wf prg;  correctAn prg; isSafe prg; (p,m) \<in> Reachables prg; 
                        ((p,m),(p',m')) \<in> (effS prg) ; prg,(p',m') \<Turnstile> Q; \<exists> B. (p',B) \<in> set (succsF prg p)  \<rbrakk> \<Longrightarrow> prg,(p,m) \<Turnstile> wpF prg p p' Q"


assumes ipc_domC:
"wf prg \<Longrightarrow> ipc prg \<in> set (domC prg)"

assumes succsF_domC:
"\<lbrakk> wf \<Pi>; (p',B) \<in> set (succsF \<Pi> p) \<rbrakk> \<Longrightarrow> (p \<in> set (domC \<Pi>)) \<and> (p' \<in> set (domC \<Pi>))"

(*
lemma (in invariantVCG) paths_domC: "\<lbrakk> wf \<Pi> ; cfp \<in> paths (succsF \<Pi>) \<rbrakk> \<Longrightarrow> (\<forall> p \<in> set cfp. p \<in> set (domC \<Pi>))"
apply (erule paths.induct)
apply (subgoal_tac "pc \<in> set (domC \<Pi>) \<and> pc' \<in> set (domC \<Pi>)")
 prefer 2
 apply (rule succsF_domC)
 apply simp
 apply simp
apply simp

apply (rule ballI)
apply (erule_tac x="p" in ballE)
apply simp

apply (subgoal_tac "pc \<in> set (domC \<Pi>) \<and> pc' \<in> set (domC \<Pi>)")
 prefer 2
 apply (rule succsF_domC)
 apply simp
 apply simp
apply simp
done
*)


lemma (in invariantVCG) isSafe'_correctAn_isSafe:
"isSafe' \<Pi> = (isSafe \<Pi>  \<and> correctAn \<Pi>)"
(*<*)
apply (rule iffI)
apply (rule conjI)
apply (simp only: isSafe'_def isSafe_def Reachables_conv saF_def semConj)
apply fastsimp

apply (simp only: isSafe'_def correctAn_def Reachables_conv saF_def semConj)
apply fastsimp

apply (simp only: isSafe'_def correctAn_def isSafe_def  Reachables_conv saF_def semConj)
apply  fastsimp
done
(*>*)

(*<*)
lemma (in invariantVCG) isSafe_correctAn_isafeF: "\<And> S. \<lbrakk> wf \<Pi>; isSafe \<Pi>; correctAn \<Pi>  \<rbrakk> \<Longrightarrow> (\<forall> s \<in> Reachables \<Pi>. 
 ((\<exists> V. noAnn V (anF \<Pi>) \<and> set V \<union> set S = set (domC \<Pi>) \<and> set V \<inter> set S = {} \<and> (V \<noteq> [] \<longrightarrow> V@[fst s] \<in> (paths (succsF \<Pi>)))) 
\<longrightarrow> ((fst s \<in> set (domC \<Pi>)) \<longrightarrow> (\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)))))"
apply (subgoal_tac "\<exists> k. length S = k")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)

apply (rule allI | rule impI | rule ballI | simp add: Let_def split_def)+
apply (erule exE | erule conjE)+
apply (subgoal_tac "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> aF \<Pi> (fst s)")
 prefer 2
 apply (subgoal_tac "isSafe' \<Pi>")
  prefer 2
  apply (simp add: isSafe'_correctAn_isSafe)
 apply (simp add: isSafe'_def Reachables_conv)
 apply (erule exE | erule conjE)+
 apply (erule_tac x="a" in allE) 
 apply (erule_tac x="b" in allE) 
 apply (erule_tac x="fst s" in allE)
 apply (erule_tac x="snd s" in allE)
 apply (simp add: saF_def semConj)
apply (erule conjE)+
apply (case_tac "anF \<Pi> (fst s)")
prefer 2
--{* anF Pi (fst s) = Some a *}
apply (simp add: isafeFdef semConj aF_def)

--{* anF Pi (fst s) = None *}
apply (subgoal_tac "\<exists> p m. s = (p,m)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (case_tac "p \<in> set S")
--{* p in set S *}
apply (erule_tac x="length [q \<in> S. q \<noteq> p]" in allE)
apply (subgoal_tac "length [q \<in> S. q \<noteq> p] < length S")
 prefer 2
 apply (rule AuxBox.length_filter_less)
 apply (simp add: set_mem_eq)
apply simp
apply (erule_tac x="[q \<in> S. q \<noteq> p]" in allE)
apply simp
apply (subgoal_tac "(p,m) \<in> Reachables \<Pi>")
 prefer 2
 apply (simp only: Reachables_conv)

apply (simplesubst isafeFdef)
apply assumption
apply (simp add: semConj)
apply (rule ballI)
apply (subgoal_tac "\<exists> p' B. x = (p',B)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp only: split_def snd_conv)
apply (rule semImpI)

apply (subgoal_tac "p = p \<and> (\<exists> m'. ((p,m),(p',m')) \<in> (effS \<Pi>))")
 prefer 2
 apply (rule_tac B="B" in succsFprogress)
 apply assumption
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp
apply (erule conjE | erule exE)+
apply (subgoal_tac "(p',m') \<in>  Reachables \<Pi>")
 prefer 2
 apply (simp add: Reachables_def)
 apply (rule_tac a="(p,m)" in ReachableFrom.step)
 apply simp
 apply simp

apply (subgoal_tac "\<Pi>,(p',m') \<Turnstile> isafeF \<Pi> p'")
 prefer 2
 apply (subgoal_tac "(\<exists>V. noAnn V (anF \<Pi>) \<and>
             set V \<union> {x \<in> set S. x \<noteq> fst s} = set (domC \<Pi>) \<and> set V \<inter> {x \<in> set S. x \<noteq> fst s} = {} \<and> (V \<noteq> [] \<longrightarrow> V @ [fst (p', m')] \<in> paths (succsF \<Pi>)))")
  prefer 2
  apply (rule_tac x="V@[p]" in exI)
  apply (rule conjI)
  apply (rule noAnn_ext)
  apply simp+
  apply (rule conjI)
  apply (simplesubst insert_union_right)
  apply (simplesubst insert_set_filter)
  apply (subgoal_tac "insert p (set S) = set S")
   prefer 2
   apply (simp add: set_mem_eq insert_absorb)
  apply (simp only:)

  apply (rule conjI)
  apply (subgoal_tac "set V \<inter> {x. x \<in> set S \<and> x \<noteq> p} \<subseteq>  set V \<inter> set S")
   prefer 2
   apply (rule intersect_mono)
  apply simp
 
  apply (case_tac "V")
  apply simp
  apply (rule paths.start)
  apply simp

  apply simp
  apply (subgoal_tac "(a # list) @ [p] @ [p'] \<in>  paths (succsF \<Pi>)")
   prefer 2
   apply (rule paths.step)
   apply simp
   apply simp
  apply simp
 apply simp
apply (subgoal_tac "p' \<in> set (domC \<Pi>)")
 prefer 2
 apply (rule succsF_domC[THEN conjE])
 apply simp
 apply simp
 apply simp
apply (erule_tac x="(p',m')" in ballE)
 prefer 2
 apply simp
apply simp


apply (subgoal_tac "\<Pi>,(p, m) \<Turnstile> wpF \<Pi> p p' (isafeF \<Pi> p')")
 prefer 2
 apply (rule completeWpF)
 apply assumption
 apply assumption
 apply assumption
 apply assumption
 apply assumption
 apply assumption
apply simp

apply (rule_tac x="B" in exI)
apply simp

apply simp


--{* fst notin set S *}
apply (subgoal_tac "noAnn (V@[p]) (anF \<Pi>)")
 prefer 2
 apply (rule noAnn_ext)
 apply simp
 apply simp
apply (subgoal_tac "p \<in> set V")
 prefer 2
 apply (drule_tac t="set (domC \<Pi>)" in sym)
 apply simp
--{* p in V and noAnn V@[p] contradicts wf Pi, which enforces loop annotations. *}
apply (frule wf_anF)
apply (unfold enoughAn_def)
apply (simp only: in_set_conv_decomp)
apply (erule exE | erule conjE)+
apply (erule_tac x="p # zsa @ [p]" in allE)
apply (simp add: isCycle_def)
apply (subgoal_tac "p # zsa @ [p] \<in> (paths (succsF \<Pi>))")
 prefer 2
 apply (rule_tac ps="ysa" in paths_append)
 apply simp
 apply (case_tac "ysa")
 apply simp

 apply simp

 apply simp
apply simp

apply (simp add:noAnn_def)
done
(*>*)


lemma (in invariantVCG) isSafe'_isafeF:
"\<lbrakk> wf \<Pi>; isSafe' \<Pi>; s \<in> initS \<Pi>; (s,s') \<in>  (effS \<Pi>)\<^sup>* ; fst s' \<in> set (domC \<Pi>)\<rbrakk> \<Longrightarrow> \<Pi>,s' \<Turnstile> isafeF \<Pi> (fst s')"
(*<*)
apply (simp only: isSafe'_correctAn_isSafe)
apply (drule_tac S="domC \<Pi>" in isSafe_correctAn_isafeF)
apply simp

apply simp

apply (erule_tac x="s'" in ballE)
 prefer 2
 apply (simp add: Reachables_conv)
 apply (erule_tac x="fst s" in allE)
 apply (erule_tac x="snd s" in allE)
 apply simp

apply (subgoal_tac "(\<exists>V. noAnn V (anF \<Pi>) \<and>
          set V \<union> set (domC \<Pi>) = set (domC \<Pi>) \<and>
          set V \<inter> set (domC \<Pi>) = {} \<and> (V \<noteq> [] \<longrightarrow> V @ [fst s'] \<in> paths (succsF \<Pi>)))")
 prefer 2
 apply (rule_tac x="[]" in exI)
 apply (simp add: noAnn_def)
apply simp
done
(*>*)


lemma (in invariantVCG) vcg_invariant:
"\<lbrakk> wf \<Pi>; isSafe' \<Pi> \<rbrakk> \<Longrightarrow> (\<forall> s \<in> Reachables \<Pi>. \<Pi>,s \<Turnstile> vcg \<Pi>)"
(*<*)
 apply (rule ballI)
 apply (subgoal_tac "\<exists> p m. s = (p,m)")
  prefer 2
  apply simp
  apply (erule exE)+
  apply (simp add: vcgdef semConj)
  apply (rule conjI)
  apply (rule semImpI) 
  apply (subgoal_tac "(s,s) \<in> (effS \<Pi>)\<^sup>*")
  prefer 2
   apply (rule rtrancl.intros)
  apply (frule initF_ipc)
  apply assumption
  apply (drule_tac t="ipc \<Pi>" in sym)
  apply simp
  apply (simp add: Reachables_conv)
  apply (erule exE | erule conjE)+
  apply (rename_tac "s" "p" "m" "p0" "m0")
  apply (frule_tac s="(p0,m0)" and s'="(p,m)" in isSafe'_isafeF)
  apply assumption
  apply simp
  apply assumption+
  apply (drule ipc_domC)
  apply simp
  apply simp
 
apply (rule ballI)
apply (rule ballI)
apply (subgoal_tac "\<exists> p' B. xa = (p',B)")
 prefer 2
 apply simp
apply (erule exE)+
apply (simp only: split_def fst_conv snd_conv)
apply (rule semImpI)
apply (simp add: semConj)
apply (erule conjE)+
apply (subgoal_tac "p=x \<and> (\<exists> m'. ((p,m),(p',m')) \<in> (effS \<Pi>))")
 prefer 2
 apply (rule_tac p''="x" and B="B" in succsFprogress)
 apply (simp add: isSafe'_correctAn_isSafe)+
apply (erule exE | erule conjE)+
apply (drule_tac t="x" in sym)
apply (simp only:)
apply (rule completeWpF)
apply (simp add: isSafe'_correctAn_isSafe)+
apply (simp add: Reachables_conv)
apply (erule exE | erule conjE)+
apply (rename_tac "s" "p" "m" "x" "xa" "p'" "B" "m'" "p0" "m0")
apply (frule_tac s="(p0,m0)" and s'="(p',m')" in isSafe'_isafeF)
apply (simp add: isSafe'_correctAn_isSafe)+
apply (rule succsF_domC[THEN conjE])
 apply simp
 apply simp
apply assumption
apply simp
apply (rule_tac x="B" in exI)
apply simp
done
(*>*)


lemma (in invariantVCG) vcg_inv_completeness:
"\<lbrakk> wf \<Pi>; isSafe \<Pi>; correctAn \<Pi>; (\<forall> s \<in> Reachables \<Pi>. \<Pi>,s \<Turnstile> vcg \<Pi>) \<longrightarrow> \<Pi> \<turnstile> vcg \<Pi> \<rbrakk> \<Longrightarrow> \<Pi> \<turnstile> vcg \<Pi>"
(*<*)
apply (subgoal_tac "isSafe' \<Pi>")
 prefer 2
 apply (simp add: isSafe'_correctAn_isSafe)
apply (drule vcg_invariant)
apply simp+
done
(*>*)

end