header {* 
  \isaheader{Upgrading VCG Instantiations} 
*}

theory VCG_Upgrades = VCG_Correctness + VCG_Completeness + VCG_Invariant:

section {* Upgrading Correctness Requirements *}

subsection {* Refining wellformedness checker *}

theorem upgrade_wf:
assumes wf_refine: "\<forall> \<Pi>. wlf' \<Pi> \<longrightarrow> wlf \<Pi>"
assumes old: "correctVCG initS effS TT FF And Imp valid provable ipc anF succsF wlf initF wpF"
shows new: "correctVCG initS effS TT FF And Imp valid provable ipc anF succsF wlf' initF wpF"
proof -
(*<*)
from old have old_SafetyLogic: "SafetyLogic TT FF And Imp valid"
 by (simp only: correctVCG_def)

from old have old_CFG: "CFG_axioms anF succsF wlf"
  by (simp only: correctVCG_def)

from old have old_AbsSem: "AbsSem_axioms valid ipc wlf initF"
 by (simp only: correctVCG_def)

from old have old_correctVCG_ax: "correctVCG_axioms initS effS TT valid provable anF succsF wlf initF wpF"
 by (simp only: correctVCG_def)

from wf_refine old_CFG 
have new_CFG: "CFG_axioms anF succsF wlf'"
  by (simp add: CFG_axioms_def)

from wf_refine old_AbsSem
have new_AbsSem:"AbsSem_axioms valid ipc wlf' initF"
  by (simp add: AbsSem_axioms_def)

from wf_refine old_correctVCG_ax
have new_correctVCG_ax:"correctVCG_axioms initS effS TT valid provable anF succsF wlf' initF wpF"
 by (simp add: correctVCG_axioms_def)

from old_SafetyLogic new_CFG new_AbsSem new_correctVCG_ax
show "correctVCG initS effS TT FF And Imp valid provable ipc anF succsF wlf' initF wpF"
  by (simp add: correctVCG_def)
qed
(*>*)

subsection {* Refining successor function *}

theorem upgrade_succsF:
assumes wf_F: "\<forall> \<Pi>. wlf \<Pi> \<longrightarrow> (\<forall> s \<in> {s. \<exists> s0. s0 \<in> initS \<Pi> \<and> (s0,s) \<in> (effS \<Pi>)\<^sup>*}. (valid \<Pi> s (F \<Pi> (fst s))))"
assumes succsF'_def: "succsF' = (\<lambda> \<Pi> p. map (\<lambda> (p',B). (p',And [B, F \<Pi> p])) (succsF \<Pi> p))"
assumes old: "correctVCG initS effS TT FF And Imp valid provable ipc anF succsF wlf initF wpF"
shows   new: "correctVCG initS effS TT FF And Imp valid provable ipc anF succsF' wlf initF wpF"
(*<*)
proof -
 from succsF'_def have succsF'_succsF: "\<And> \<Pi> p p' B. (p',B) \<in> set (succsF' \<Pi> p) \<Longrightarrow> (\<exists> B'. (p',B') \<in> set (succsF \<Pi> p) \<and> B = And [B',F \<Pi> p])"
   apply -
   apply simp
   apply (erule imageE)
   apply (simp add: split_def split_paired_all)
   apply fastsimp
   done
 from succsF'_def have succsF_succsF': "\<And> \<Pi> p p' B. (p',B) \<in> set (succsF \<Pi> p) \<Longrightarrow> (p',And [B,F \<Pi> p]) \<in> set (succsF' \<Pi> p)"
   by fastsimp

 
 from old have old_SafetyLogic: "SafetyLogic TT FF And Imp valid"
   by (simp add: correctVCG_def)
   
 from old_SafetyLogic
 have old_semConj: "\<And> \<Pi> s L. valid \<Pi> s (And L) = (\<forall>f\<in>set L. valid \<Pi> s f)"
   apply -
   apply (unfold SafetyLogic_def)
   apply (erule conjE)+
   apply (erule_tac x="\<Pi>" in allE)
   apply (erule_tac x="s" in allE)
   apply (erule_tac x="L" in allE)
   apply assumption
   done

 from old_SafetyLogic 
 have old_semImpE: "\<And> \<Pi> s f1 f2. valid \<Pi> s (Imp f1 f2) \<Longrightarrow> (valid \<Pi> s f1 \<longrightarrow> valid \<Pi> s f2)" 
   apply -
   apply (subgoal_tac "\<forall>\<Pi> s f1 f2. valid \<Pi> s (Imp f1 f2) \<longrightarrow> valid \<Pi> s f1 \<longrightarrow> valid \<Pi> s f2")
    prefer 2
    apply (unfold SafetyLogic_def)
    apply (erule conjE)+
    apply assumption
   apply (erule_tac x="\<Pi>" in allE)
   apply (erule_tac x="s" in allE)
   apply (erule_tac x="f1" in allE)
   apply (erule_tac x="f2" in allE)
   apply (erule_tac V="?A \<and> ?B" in thin_rl)
   apply (simp only: simp_thms)
   done
   
 from old have old_CFG: "CFG_axioms anF succsF wlf"
  by (simp only: correctVCG_def)

from old_CFG have old_wlf_anF: "\<forall> \<Pi>. wlf \<Pi> \<longrightarrow> enoughAn succsF \<Pi> anF"
 apply - 
 apply (unfold CFG_axioms_def)
 apply assumption
 done
   
 from old_wlf_anF have new_wlf_anF:
 "(\<forall>\<Pi>. wlf \<Pi> \<longrightarrow> enoughAn succsF' \<Pi> anF)"
   apply - 
   apply (simp add: enoughAn_def isCycle_def)
   apply (rule allI | rule impI)+
   apply (erule_tac x="\<Pi>" in allE)
   apply simp
   apply (erule_tac x="l" in allE)
   apply (subgoal_tac "\<forall> l. l \<in> paths (succsF' \<Pi>) \<longrightarrow> l \<in> paths (succsF \<Pi>)")
    prefer 2
    apply (rule allI)
    apply (rule impI)
    apply (erule paths.induct)
    apply (simp add: succsF'_def)
    apply (erule imageE)
    apply (simp add: split_def split_paired_all)
    apply (rule paths.intros)
    apply assumption
    
    apply (drule succsF'_succsF)
    apply (erule exE | erule conjE)+
    apply (rule paths.step)
    apply assumption
    apply assumption

   apply simp
   done

 from new_wlf_anF have new_CFG: "CFG_axioms anF succsF' wlf"
   by (simp add: CFG_axioms_def)
 
 from old have old_AbsSem: "AbsSem_axioms valid ipc wlf initF"
   by (simp only: correctVCG_def)

 from old have old_correctVCG_ax: "correctVCG_axioms initS effS TT valid provable anF succsF wlf initF wpF"
   by (simp only: correctVCG_def)

 from old_correctVCG_ax have old_succsFcomplete: "\<forall> \<Pi> s s'. 
 wlf \<Pi> \<longrightarrow> s \<in> ReachableFromInv (effS \<Pi>) (initS \<Pi>) {s. valid \<Pi> s (case anF \<Pi> (fst s) of None \<Rightarrow> TT | Some An \<Rightarrow> An)}
 \<longrightarrow>  (s,s') \<in> (effS \<Pi>) \<longrightarrow> (\<exists> B. (fst s',B) \<in> set (succsF \<Pi> (fst s)) \<and> valid \<Pi> s B)" 
   apply - 
   apply (unfold correctVCG_axioms_def)
   apply (erule conjE)+
   apply assumption
 done

 have new_succsFcomplete:
   "\<forall> \<Pi> s s'.
    wlf \<Pi> \<longrightarrow>
    s \<in> (ReachableFromInv (effS \<Pi>) (initS \<Pi>) {s. valid \<Pi> s (case anF \<Pi> (fst s) of None \<Rightarrow> TT | Some An \<Rightarrow> An)}) \<longrightarrow>
   (s, s') \<in> effS \<Pi> \<longrightarrow>
   (\<exists>B. (fst s', B) \<in> set (succsF' \<Pi> (fst s)) \<and> valid \<Pi> s B)" 
   proof (intro allI impI)
     fix \<Pi> s s'
     assume s_ReachableFromInv: "s \<in> (ReachableFromInv (effS \<Pi>) (initS \<Pi>) {s. valid \<Pi> s (case anF \<Pi> (fst s) of None \<Rightarrow> TT | Some An \<Rightarrow> An)})"
     assume wf_Pi: "wlf \<Pi>"
     assume s_s'_effS: "(s,s') \<in> effS \<Pi>"
     show "\<exists>B. (fst s', B) \<in> set (succsF' \<Pi> (fst s)) \<and> valid \<Pi> s B"
       proof -
       from wf_Pi s_ReachableFromInv s_s'_effS 
       have old_succsF: "\<exists>B. (fst s', B) \<in> set (succsF \<Pi> (fst s)) \<and> valid \<Pi> s B"
	 by (rule old_succsFcomplete[rule_format])

       
       from wf_Pi s_ReachableFromInv wf_F
       have valid_s_F: "valid \<Pi> s (F \<Pi> (fst s))"
	 apply -
	 apply (erule_tac x="\<Pi>" in allE)
	 apply (drule ReachableFromInv_ReachableFrom)
	 apply (simp only: ReachableFrom_conv)
	 apply (erule exE)+
	 apply fastsimp
	 done

       from old_succsF succsF_succsF' valid_s_F 
       show ?thesis
	 apply atomize
	 apply (erule exE)
	 apply (rule_tac x="And [B, F \<Pi> (fst s)]" in exI)
	 apply (erule_tac x="fst s'" in allE)
	 apply (erule_tac x="B" in allE)
	 apply (erule_tac x="\<Pi>" in allE)
	 apply (erule_tac x="fst s" in allE)
	 apply (simp add: old_semConj)
	 done
       qed
     qed

 
 from old_correctVCG_ax new_succsFcomplete
 have new_correctVCG_ax :"correctVCG_axioms initS effS TT valid provable anF succsF' wlf initF wpF"
   by (simp add: correctVCG_axioms_def)

 from old_SafetyLogic new_CFG old_AbsSem new_correctVCG_ax
 show "correctVCG initS effS TT FF And Imp valid provable ipc anF succsF' wlf initF wpF"
   by (simp add: correctVCG_def)
qed
(*>*)


end