theory SALTypeSafetyFWInst = SALTypeSafetyPlatform + VerificationConditionGenerator:


section {* Proving the Safety Logic requirements *}

theorem SALSafetyLogicIns:
"SafetyLogic Conj Impl TrueF FalseF valid"
(*<*)
apply (unfold SafetyLogic_def)

--{* semConj *}
apply (rule conjI)
apply (rule allI)+
apply (simp add: valid_def Conj_def)

--{* semImp *}
apply (rule conjI)
apply (rule allI)+
apply (simp only: valid_def Impl_def)

--{* TrueFSem *}
apply (simp only: TrueF_def)
apply (simp only: valid_def)
apply simp
--{* semFalseF *}
apply (rule allI)+
apply (simp add: FalseF_def)
(*>*)
done

section {* Proving the VCG requirements *}

lemma list_length_nth:
"(la@[i,j])!(length la)=i"
(*<*)
apply (induct_tac la)
apply simp
apply simp
(*>*)
done

lemma list_length_nth2:
"(la@[i])!(length la)=i"
(*<*)
apply (induct_tac la)
apply simp
apply simp
(*>*)
done

lemma list_length_suc_nth:
"(la@[i,j])!(Suc (length la))=j"
(*<*)
apply (induct_tac la)
apply simp
apply simp
(*>*)
done

lemma path_succsF:
"\<lbrakk> l \<in> paths prg succsF; k+1<length l \<rbrakk> \<Longrightarrow> \<exists> B. (l!(k+1),B) \<in> set (succsF prg (l!k))"
(*<*)
apply (rotate_tac 1)
apply (erule rev_mp)
apply (rule_tac  prg="prg" and succsF'="succsF" in paths.induct)
apply assumption
apply simp
apply (rule impI)
apply (rule_tac x="B" in exI)
apply assumption
apply (case_tac "k= length (la)")
apply simp
apply (rule_tac x="B" in exI)
apply (rename_tac "pc''")
apply (subgoal_tac "(la@[pc,pc''])!(Suc (length la)) = pc''")
 prefer 2
 apply (rule list_length_suc_nth)
apply (subgoal_tac "(la@[pc,pc''])!(length la) = pc")
 prefer 2
 apply (rule list_length_nth)
apply simp
apply (rule impI)
apply (simp (no_asm) only: nth_append)
apply (case_tac "k + 1 = length la")
apply (simp add: list_length_nth2)
apply (simp add: nth_append)
apply (subgoal_tac "k + 1 < length (la @ [pc])")
apply simp
apply (simp only: nth_append)
apply simp
apply (subgoal_tac "k + 1 \<noteq> length (la @ [pc])")
apply simp
apply simp
(*>*)
done

lemma less_chain_simp:
"\<lbrakk> \<forall> k. length l <= k+1 \<or> l!k < l!(k+1); 1 < length (l::nat  list) \<rbrakk> \<Longrightarrow> hd l < last l"
(*<*)
apply (erule rev_mp)
apply (erule rev_mp)
apply (induct l)
apply simp
apply (case_tac list)
apply simp
apply (case_tac lista)
apply simp
apply (rule impI)
apply (erule_tac x="0" in allE)
apply simp
apply (rule impI)
apply (rule impI)
apply hypsubst
apply simp
apply (rule conjI)
apply (rule impI)
apply simp
apply (frule_tac x="0" and P="\<lambda> k. Suc (Suc 0) <= k \<or> (?Q k)" in spec)
apply simp
apply (frule_tac x="Suc 0" and P="\<lambda> k. Suc (Suc 0) <= k \<or> (?Q k)" in spec)
apply simp

apply (frule_tac x="0" and P="\<lambda> k. Suc (Suc (length listb)) <= k \<or> (?Q k)" in spec)
apply simp
apply (frule_tac x="1" and P="\<lambda> k. Suc (Suc (length listb)) <= k \<or> (?Q k)" in spec)
apply simp
apply (frule_tac x="0" in spec)
apply (subgoal_tac "\<forall> k. Suc (length listb) <= k \<or> ((aa#ab#listb)!k < (ab#listb)!k)")
apply (rule impI)
apply simp

apply (rule allI)
apply (case_tac k)
apply simp
apply (case_tac listb)
apply simp
apply (case_tac nat)
apply simp
apply (frule_tac x="2" and P="\<lambda> k. Suc (Suc (Suc (length list))) <= k \<or> (?Q k)" in spec)
apply simp
apply simp
apply (frule_tac x="Suc (Suc (Suc nata))" and P="\<lambda> k. Suc (Suc (Suc (length list))) <= k \<or> (?Q k)" in spec)
apply simp
(*>*)
done

lemma path_length:
"\<lbrakk> l \<in> paths prg succsF \<rbrakk> \<Longrightarrow> 1 < length l"
(*<*)
apply (rule_tac prg="prg" and succsF'="succsF" in paths.induct)
apply assumption
apply simp
apply simp
(*>*)
done

lemma loop_has_back_jump:
"\<lbrakk> l \<in> paths prg succsF; hd l = last l \<rbrakk> \<Longrightarrow> \<exists> k. (k+1)<length l \<and> l!(k+1) <= l!k"
(*<*)
apply (frule path_length)
apply (rule classical)
apply (simp only: not_ex)
apply (simp only: de_Morgan_conj)
apply (simp only: linorder_not_less)
apply (subgoal_tac "\<forall>k. length ?l \<le> k + 1 \<or> ?l ! k < ?l ! (k + 1)")
apply (drule less_chain_simp)
apply assumption
apply simp
apply (rule allI)
apply (erule_tac x="k" in allE)
apply (subgoal_tac "(\<not> l ! (k+1) <= l ! k) = (l!k < l!(k+1))")
apply simp
apply (rule_tac x="l!(k+1)" and y="l!k" in linorder_not_le)
(*>*)
done

lemma domC_split:
"\<And> p. cmd prg p = Some a \<Longrightarrow> \<exists> l1 l2. (domC prg) = (l1@[p]@l2)" 
(*<*)
apply (simp only: cmd_def)
apply (case_tac "p < length prg")
apply (simp add: domC_def)
apply (rule_tac x="[0..p(]" in exI)
apply (rule_tac x="[(Suc p)..(length prg) (]" in exI)
apply (frule upt_conv_Cons)
apply (drule_tac s="[p..(length prg) (]" in sym)
apply simp
apply (subgoal_tac "[p .. length prg (] = [ p .. p + (length prg - p) (]")
 prefer 2
 apply simp
apply (subgoal_tac "[0 .. length prg (] = [ 0 .. p + (length prg - p) (]")
 prefer 2
 apply (erule_tac P="p < length prg" in rev_mp)
 apply (simp (no_asm))
apply (simp only:)
apply (rule  upt_add_eq_append)
apply (simp (no_asm))

apply simp
(*>*)
done


lemma cmd_domC:
"\<forall> instr pc prg. cmd prg pc = Some instr \<longrightarrow> pc\<in> set (domC prg)"
(*<*)
apply (rule allI)+
apply (auto simp add: cmd_def domC_def)
(*>*)
done

lemma domC_cmd:
"\<forall> pc. pc\<notin> set (domC prg) \<longrightarrow>  cmd prg pc = None"
(*<*)
apply (auto simp add: domC_def cmd_def)
(*>*)
done

lemma checkPos_split:
"checkPos prg (l1@l2) = ((checkPos prg l1) \<and> (checkPos prg l2))"
(*<*)
apply (induct_tac l1)
apply simp
apply (simp add: checkPos.simps Let_def split_def fst_conv snd_conv bool.cases)
(*>*)
done

lemma back_jumps_annotated:
" wf prg  \<Longrightarrow> \<forall> pc'' pc B. (pc'',B) \<in> set (succsF prg pc) \<longrightarrow> pc''<=pc \<longrightarrow> (anF prg pc'') \<noteq> None"
(*<*)
apply (rule allI)+
apply (rename_tac "p'" "p" "B")
apply (rule impI)+
apply (subgoal_tac "\<exists> ins. cmd prg p = Some ins")
 prefer 2
 apply (simp add: succsF_def)
 apply (case_tac "cmd prg p")
 apply simp
 apply simp
apply (erule exE)
apply (simp only: wf_def)
apply (frule domC_split)
apply (erule exE)+
apply (simp only: checkPos_split)
apply (erule conjE)+
apply (simp add: checkPos_split Let_def split_def fst_conv snd_conv option.cases succsF_def)
apply (case_tac ins)
--{* SET nat1 nat2 *}
apply simp
--{* ADD nat1 nat2 *}
apply simp
--{* INC nat *}
apply simp
--{* JMPEQ nat1 nat2 nat3 *}
apply simp
apply (case_tac "\<exists>y. anF prg p = Some y")
apply assumption
apply simp
--{* JMPB nat *}
apply simp
apply (case_tac "\<exists>y. anF prg (p - nat) = Some y")
apply assumption
apply simp
done

lemma correct_wf:
"\<forall>prg. wf prg \<longrightarrow> enoughAn succsF prg anF"
apply (rule allI)
apply (rule impI)
apply (drule back_jumps_annotated)
apply (simp only: enoughAn_def isLoop_def noAnn_def)
apply (rule allI)
apply (rule impI)
apply clarify
apply (frule loop_has_back_jump)
apply assumption
apply (erule exE)
apply (erule conjE)
apply (frule_tac l="l" and prg="prg" and k="k" in path_succsF)
apply assumption
apply (erule exE)

apply (erule_tac x="(l!(k+1))" in allE)
apply (erule_tac x="l!(k+1)" in allE)
apply (erule_tac x="l!k" in allE)
apply (erule_tac x="B" in allE)
apply (subgoal_tac "l!(k+1) \<in> set l")
apply (drule mp)
apply assumption
apply clarify
apply simp
done

theorem SAL_VCG_Ins:
"VerificationConditionGenerator Conj Impl TrueF FalseF valid provable effS wpF succsF initF ipc safeF anF domC wf"
(*<*)
apply (unfold VerificationConditionGenerator_def)
--{* SafetyLogic *}
apply (rule conjI)
apply (rule SALSafetyLogicIns)

--{* VerificationConditionGenerator *}
apply (unfold VerificationConditionGenerator_axioms_def)

apply (rule conjI)
--{* correctIpc *}
apply (rule allI)+
apply (simp add: valid_def initF_def ipc_def Let_def split_def fst_conv snd_conv)

apply (rule conjI)
--{* correctWpF *}
apply (rule allI | rule impI)+
apply (simp add: valid_def wpF_def step.simps effS_def)
apply (case_tac "cmd prg pc")
apply simp

apply simp
apply (case_tac "a")
--{* SET *}
apply simp
--{* ADD *}
apply simp
--{* INC *}
apply simp
--{* JMPEQ *}
apply simp
apply (case_tac "m nat1 = m nat2")
apply simp
apply simp
--{* JMPB *}
apply simp

apply (rule conjI)
--{* succsFcomplete *}
apply (rule allI)+
apply (rule impI)+
apply (simp only: effS_def)
apply simp
apply (simp only: split_paired_all)
apply (rename_tac "prg" "p" "m" "p'" "m'")
apply (case_tac "cmd prg p")
apply simp

apply simp
apply (case_tac a)
apply simp
apply (unfold succsF_def)
apply (rule_tac x="TrueF" in exI)
apply simp
apply (simp add: TrueF_def valid_def)
apply (simp add: TrueF_def valid_def)
apply (simp add: TrueF_def valid_def)
apply (case_tac "m nat1 = m nat2")
apply (rule_tac x="\<lambda> (p,m). m nat1 = m nat2" in exI)
apply (simp add: valid_def)
apply (rule_tac x="\<lambda> (p,m). m nat1 \<noteq> m nat2" in exI)
apply (simp add: valid_def)
apply (rule_tac x="TrueF" in exI)
apply (simp add: TrueF_def valid_def)

apply (rule conjI)
--{* correct Safety Logic *}
apply (rule allI)+
apply (rule impI)+
apply (simp only: provable_def)

--{* correct_wf *}
apply (rule correct_wf)
(*>*)
done

section {* Platform Soundness *}

constdefs isSafe::"SALprogram \<Rightarrow> bool"
"isSafe prg \<equiv> (\<forall> s s'. prg,s \<Turnstile> initF prg \<and> (s,s') \<in> (effS prg)\<^sup>* \<longrightarrow> prg,s' \<Turnstile> safeF prg (fst s'))"
 
theorem platform_soundness:
"\<lbrakk> wf prg; provable prg (vcgTSAL prg) \<rbrakk> \<Longrightarrow> isSafe prg"
(*<*)
apply (subgoal_tac "VerificationConditionGenerator Conj Impl TrueF FalseF valid provable effS wpF succsF initF ipc safeF anF domC wf")
 prefer 2
 apply (rule SAL_VCG_Ins)
apply (drule_tac prg="prg" and anF="anF" in VerificationConditionGenerator.vcg_soundness)
apply assumption
apply (simp only: vcgTSAL_def domA_def vcG_def)
apply (simp only: isSafe_def)
(*>*)
done

end