header {* 
  \isaheader{VCG Correctness} 
*}

theory VCG_Correctness = VCG:

locale correctVCG = VCG +

fixes ReachablesAn::"'prog \<Rightarrow> ('pos \<times> 'mem) set"
defines
"ReachablesAn \<equiv> \<lambda> \<Pi>. ReachableFromInv (effS \<Pi>) (initS \<Pi>) ({s. \<Pi>,s \<Turnstile> aF \<Pi> (fst s)})"

assumes correctInitF:
"\<lbrakk> wf \<Pi>; s \<in> initS \<Pi> \<rbrakk> \<Longrightarrow> valid \<Pi> s (initF \<Pi>)"

assumes correctWpF: 
"\<lbrakk> wf \<Pi>; s \<in> (ReachablesAn \<Pi>); (s,s')\<in>(effS \<Pi>); \<Pi>,s \<Turnstile> (wpF \<Pi> (fst s) (fst s') Q) 
 \<rbrakk> \<Longrightarrow> \<Pi>,s' \<Turnstile> Q"

assumes succsF_complete: 
"\<lbrakk>  wf \<Pi>; s \<in> (ReachablesAn \<Pi>); (s,s') \<in> (effS \<Pi>)  \<rbrakk> 
 \<Longrightarrow> (\<exists> B. (fst s',B) \<in> set (succsF \<Pi> (fst s)) \<and> valid \<Pi> s B)"

assumes correctSafetyLogic: 
"\<lbrakk> wf \<Pi>; \<Pi> \<turnstile> f; s \<in> (ReachablesAn \<Pi>) \<rbrakk> \<Longrightarrow> \<Pi>,s \<Turnstile> f"


(*<*)
lemma (in correctVCG) ReachablesAn_init:
"\<lbrakk>  s \<in> (initS \<Pi>) \<rbrakk> \<Longrightarrow> s \<in> (ReachablesAn \<Pi>)"
apply (simp add: ReachablesAn_def)
apply (rule ReachableFromInv.init)
apply assumption+
done
(*>*)

(*<*)
lemma (in correctVCG) ReachablesAn_step:
"\<lbrakk>  s \<in> (ReachablesAn \<Pi>); 
   \<Pi>,s \<Turnstile> aF \<Pi> (fst s); 
   \<Pi>,s' \<Turnstile> aF \<Pi> (fst s'); 
   (s,s') \<in> (effS \<Pi>)  \<rbrakk> \<Longrightarrow> s' \<in> (ReachablesAn \<Pi>)"
apply (simp add: ReachablesAn_def)
apply (rule ReachableFromInv.step)
apply simp+
done
(*>*)

(*<*)
lemma (in correctVCG) ReachablesAn_initF_aF:
"s \<in> (ReachablesAn \<Pi>) \<Longrightarrow>  s \<in> (initS \<Pi>) \<or> \<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
apply (simp only: ReachablesAn_def)
apply (erule ReachableFromInv.elims)
apply simp+
done
(*>*)


(*<*)
lemma (in correctVCG) vc_init:
"\<lbrakk> wf \<Pi>; \<Pi> \<turnstile> vcg \<Pi>; s \<in> initS \<Pi> \<rbrakk> \<Longrightarrow> \<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)"
apply (subgoal_tac "s \<in> (ReachablesAn \<Pi>)")
 prefer 2
 apply (rule ReachablesAn_init)
 apply assumption
apply (frule_tac s="s" and f="vcg \<Pi>" in correctSafetyLogic)
apply assumption+
apply (simp add: vcgdef)
apply (subgoal_tac "\<Pi>,s \<Turnstile> Impl (initF \<Pi>) (isafeF \<Pi> (ipc \<Pi>))")
 prefer 2
 apply (simp add: semConj)
apply (drule semImpE)
apply (frule_tac s="s" in correctInitF)
apply assumption
apply (subgoal_tac "fst s = ipc \<Pi>")
 prefer 2
 apply (rule initF_ipc)
 apply assumption
 apply simp
apply simp
done
(*>*)


lemma (in correctVCG) isafeF_saF:
"\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s) \<Longrightarrow> \<Pi>, s \<Turnstile> saF \<Pi> (fst s)" 
(*<*)
apply (simp add: isafeF_def isafe'_def)
apply (case_tac "(fst s) mem domC \<Pi>")
prefer 2
apply (simp add: semFalse)

--{* fst s mem domC \<Pi> *}
apply (simp add: saF_def del: isafe.simps)
apply (case_tac "anF \<Pi> (fst s)")
apply (simp add: semConj semTrue aF_def)

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

lemma (in correctVCG) vc_isafeF_ReachablesAn:
assumes wf_Pi: "wf \<Pi>"
assumes vc_provable: "\<Pi> \<turnstile> vcg \<Pi>" 
assumes s_Reach: "s \<in> (Reachables \<Pi>)"
shows "(\<Pi>, s \<Turnstile> isafeF \<Pi> (fst s) \<and> s \<in> ReachablesAn \<Pi>)"
using s_Reach
proof (induct rule: Reachables_induct) 

--{* induction base *}
case (init s)
 show "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s) \<and> s \<in> ReachablesAn \<Pi>"
   proof (rule conjI)
     from wf_Pi vc_provable init
     show "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)"
       by (rule vc_init)
   next
     show "s \<in> ReachablesAn \<Pi>"
       by (rule ReachablesAn_init)
   qed

next

case (step s s')

have s_Reach: "s \<in> Reachables \<Pi>" .

have s_isafeF: "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)" and
   
     s_ReachAn: "s \<in> ReachablesAn \<Pi>" 
  using step by auto

have s_s'_effS: "(s,s') \<in> effS \<Pi>" .

from s_isafeF 
have s_saF: "\<Pi>,s \<Turnstile> saF \<Pi> (fst s)"
  by (rule isafeF_saF)

from s_saF
 have s_aF: "\<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
   by (simp add: saF_def semConj)

from wf_Pi s_ReachAn s_s'_effS
obtain B where B_succsF: "(fst s',B) \<in> set (succsF \<Pi> (fst s))" and s_B: "\<Pi>,s \<Turnstile> B"
 apply -
 apply (drule_tac s="s" and s'="s'" in succsF_complete)
 apply assumption
 apply assumption
 apply fastsimp
 done

from B_succsF 
obtain su su' 
where su_B_su'_succsF: "succsF \<Pi> (fst s) = su@(fst s',B)#su'"
 by (fastsimp simp add: in_set_conv_decomp)

from wf_Pi s_isafeF
have s_domC: "fst s \<in> (set (domC \<Pi>))"
  apply -
  apply (drule_tac  pc="fst s" in isafeFdef)
  apply (rule classical)
  apply (simp add: isafeFdef semFalse)
  done

from s_domC
obtain dC dC' where domC_dC_dC': "domC \<Pi> = dC@(fst s)#dC'"
  by (fastsimp simp add: in_set_conv_decomp)

have s'_isafeF: "\<Pi>,s' \<Turnstile> isafeF \<Pi> (fst s')"
 proof (cases "anF \<Pi> (fst s)")
   case None

   from None wf_Pi s_domC s_isafeF su_B_su'_succsF
   have B_imp_wpF: "\<Pi>,s \<Turnstile> B \<Impl> wpF \<Pi> (fst s) (fst s') (isafeF \<Pi> (fst s'))"
     apply -
     apply (drule_tac pc="fst s" in isafeFdef)
     apply (simp add: semConj)
     done

   from s_B B_imp_wpF
   have wpF_isafeF: "\<Pi>,s \<Turnstile> wpF \<Pi> (fst s) (fst s') (isafeF \<Pi> (fst s'))"
     apply -
     apply (drule semImpE)
     apply simp
     done

  from wf_Pi s_ReachAn B_succsF s_s'_effS wpF_isafeF
  show "\<Pi>,s' \<Turnstile> isafeF \<Pi> (fst s')"
    by (rule_tac Q="isafeF \<Pi> (fst s')" and s="s" in correctWpF)
  
next

  case (Some A)

  from Some domC_dC_dC'
  obtain dA dA' where domA_dA_dA': "domA \<Pi> = dA@(fst s)#dA'"
    by (simp add: domA_def in_set_conv_decomp)
    
  from wf_Pi vc_provable s_ReachAn
  have s_vc: "\<Pi>,s \<Turnstile> (vcg \<Pi>)"
    by (rule correctSafetyLogic)

  from wf_Pi Some s_isafeF s_domC
  have isafeF_safeF_A: "isafeF \<Pi> (fst s) = \<Conj> [safeF \<Pi> (fst s), A]"
    by (drule_tac pc="fst s" in isafeFdef, simp)
  
  from wf_Pi domA_dA_dA' s_vc su_B_su'_succsF
  have isafeF_B_imp_wpF: "\<Pi>,s \<Turnstile> \<Conj> [isafeF \<Pi> (fst s),B] \<Impl> wpF \<Pi> (fst s) (fst s') (isafeF \<Pi> (fst s'))"
    apply -
    by (drule vcgdef, simp add: semConj)
   
  from isafeF_B_imp_wpF s_isafeF s_B
  have s_wpF_isafeF: "\<Pi>,s \<Turnstile> wpF \<Pi> (fst s) (fst s') (isafeF \<Pi> (fst s'))"
    apply -
    apply (drule semImpE)
    apply (simp add: semConj)
    done

  from wf_Pi s_ReachAn B_succsF s_s'_effS s_wpF_isafeF
  show "\<Pi>,s' \<Turnstile> isafeF \<Pi> (fst s')"
    by (rule_tac Q="isafeF \<Pi> (fst s')" and s="s" in correctWpF)
  
   
qed

from s'_isafeF have s'_aF: "\<Pi>,s' \<Turnstile> aF \<Pi> (fst s')"
  apply -
  apply (drule isafeF_saF)
  apply (simp add: saF_def semConj)
  done

show "\<Pi>,s' \<Turnstile> isafeF \<Pi> (fst s') \<and> s' \<in> ReachablesAn \<Pi>"
  proof (rule conjI)
    show "\<Pi>,s' \<Turnstile> isafeF \<Pi> (fst s')"
      by (rule s'_isafeF)
    
   next
     from s_ReachAn s_aF s'_aF s_s'_effS
     show "s' \<in> ReachablesAn \<Pi>"
       by (rule ReachablesAn_step)
  qed
qed


text {* The Soundness proof of our VCG *}


theorem (in correctVCG) vcg_soundness:
assumes wf_Pi: "wf \<Pi>"
assumes vc_provable: "\<Pi> \<turnstile> vcg \<Pi>"
shows "isSafe \<Pi>"
proof -

have isSafePi: "\<forall> s \<in> Reachables \<Pi>. \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
 proof (rule ballI)
 fix s
 assume s_Reach: "s \<in> Reachables \<Pi>"
 show "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
   proof -
     from wf_Pi vc_provable s_Reach
     have s_isafeF_ReachAn: "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s) \<and> s \<in> ReachablesAn \<Pi>"
       by (rule vc_isafeF_ReachablesAn)

     from s_isafeF_ReachAn
     have s_isafeF: "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)"
       by simp
     
     from s_isafeF
     show "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
       apply -
       apply (drule isafeF_saF)
       apply (simp add: saF_def semConj)
       done
   qed
 qed
from isSafePi show "isSafe \<Pi>"
 by (simp add: isSafe_def)
qed


text {* Verification Conditions also guarantee correct annotations. *}

lemma (in correctVCG) vcg_correctAn:
assumes wf_Pi: "wf \<Pi>"
assumes vc_provable: "\<Pi> \<turnstile> vcg \<Pi>"
shows "correctAn \<Pi>"
proof -

have correctAnPi: "\<forall> s \<in> Reachables \<Pi>. \<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
 proof (rule ballI)
 fix s
 assume s_Reach: "s \<in> Reachables \<Pi>"
 show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
   proof -
     from wf_Pi vc_provable s_Reach
     have s_isafeF_ReachAn: "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s) \<and> s \<in> ReachablesAn \<Pi>"
       by (rule vc_isafeF_ReachablesAn)

     from s_isafeF_ReachAn
     have s_isafeF: "\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)"
       by simp
     
     from s_isafeF
     show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
       apply -
       apply (drule isafeF_saF)
       apply (simp add: saF_def semConj)
       done
   qed
 qed
from correctAnPi show "correctAn \<Pi>"
 by (simp add: correctAn_def)
qed


end