clib: improve ccorres_While
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
parent
5568eb56a1
commit
4d19f6616f
|
@ -1040,76 +1040,197 @@ lemma ccorres_Guard_True_Seq:
|
||||||
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F \<lbrace>True\<rbrace> c ;; d)"
|
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F \<lbrace>True\<rbrace> c ;; d)"
|
||||||
by (simp, ccorres_rewrite, assumption)
|
by (simp, ccorres_rewrite, assumption)
|
||||||
|
|
||||||
|
lemma ccorres_While_Normal_helper:
|
||||||
|
assumes setter_inv:
|
||||||
|
"\<Gamma> \<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> Cnd rv s s')}"
|
||||||
|
assumes body_inv: "\<Gamma> \<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}"
|
||||||
|
shows "\<Gamma> \<turnstile> ({s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> Cnd rv s s')})
|
||||||
|
While {s'. cond_xf s' \<noteq> 0} (Seq B setter)
|
||||||
|
{s'. \<exists>rv s. G rv s s'}"
|
||||||
|
apply (insert assms)
|
||||||
|
apply (rule hoare_complete)
|
||||||
|
apply (simp add: cvalid_def HoarePartialDef.valid_def)
|
||||||
|
apply (intro allI)
|
||||||
|
apply (rename_tac xstate xstate')
|
||||||
|
apply (rule impI)
|
||||||
|
apply (case_tac "\<not> isNormal xstate")
|
||||||
|
apply fastforce
|
||||||
|
apply (simp add: isNormal_def)
|
||||||
|
apply (elim exE)
|
||||||
|
apply (simp add: image_def)
|
||||||
|
apply (erule exec_While_final_inv''[where C="{s'. cond_xf s' \<noteq> 0}" and B="B;; setter"]; clarsimp)
|
||||||
|
apply (frule intermediate_Normal_state[OF _ _ body_inv])
|
||||||
|
apply fastforce
|
||||||
|
apply clarsimp
|
||||||
|
apply (rename_tac inter_t)
|
||||||
|
apply (frule hoarep_exec[OF _ _ body_inv, rotated], fastforce)
|
||||||
|
apply (frule_tac s=inter_t in hoarep_exec[rotated 2], fastforce+)[1]
|
||||||
|
apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_abrupt mem_Collect_eq)
|
||||||
|
apply (metis (mono_tags, lifting) HoarePartial.SeqSwap exec_stuck mem_Collect_eq)
|
||||||
|
apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq)
|
||||||
|
done
|
||||||
|
|
||||||
lemma ccorres_While:
|
lemma ccorres_While:
|
||||||
assumes body_ccorres:
|
assumes body_ccorres:
|
||||||
"\<And>r. ccorresG srel \<Gamma> (=) xf (G and (\<lambda>s. the (C r s))) (G' \<inter> C') hs (B r) B'"
|
"\<And>r. ccorresG srel \<Gamma> rrel xf (\<lambda>s. G r s \<and> C r s = Some True) (G' \<inter> C') [] (B r) B'"
|
||||||
and cond_ccorres:
|
assumes setter_ccorres:
|
||||||
"\<And>r. ccorresG srel \<Gamma> (\<lambda>rv rv'. rv = to_bool rv') cond_xf G G' hs (gets_the (C r)) setter"
|
"\<And>r. ccorresG srel \<Gamma> (\<lambda>rv rv'. rv = to_bool rv') cond_xf (G r) G' [] (gets_the (C r)) setter"
|
||||||
and nf: "\<And>r. no_fail (G and (\<lambda>s. the (C r s))) (B r)"
|
assumes nf: "\<And>r. no_fail (\<lambda>s. G r s \<and> C r s = Some True) (B r)"
|
||||||
and no_ofail: "\<And>r. no_ofail G (C r)"
|
assumes no_ofail: "\<And>r. no_ofail (G r) (C r)"
|
||||||
and body_inv: "\<And>r. \<lbrace>G and (\<lambda>s. the (C r s))\<rbrace> B r \<lbrace>\<lambda>_. G\<rbrace>"
|
assumes body_inv:
|
||||||
"\<Gamma> \<turnstile> (G' \<inter> C') B' G'"
|
"\<And>r. \<lbrace>\<lambda>s. G r s \<and> C r s = Some True\<rbrace> B r \<lbrace>G\<rbrace>"
|
||||||
and setter_inv_cond: "\<Gamma> \<turnstile> G' setter (G' \<inter> {s'. cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C'})"
|
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')
|
||||||
and setter_xf_inv: "\<And>val. \<Gamma> \<turnstile> {s'. xf s' = val} setter {s'. xf s' = val}"
|
\<and> s' \<in> C' \<and> C r s = Some True}
|
||||||
shows "ccorresG srel \<Gamma> (=) xf G (G' \<inter> {s'. xf s' = r}) hs
|
B' G'"
|
||||||
(whileLoop (\<lambda>r s. the (C r s)) B r)
|
assumes setter_inv_cond:
|
||||||
(Seq setter (While {s'. cond_xf s' \<noteq> 0} (Seq B' setter)))"
|
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
|
||||||
|
setter
|
||||||
|
{s'. s' \<in> G' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C')}"
|
||||||
|
assumes setter_rrel:
|
||||||
|
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
|
||||||
|
setter
|
||||||
|
{s'. rrel r (xf s')}"
|
||||||
|
shows
|
||||||
|
"ccorresG srel \<Gamma> rrel xf (G r) (G' \<inter> {s'. rrel r (xf s')}) hs
|
||||||
|
(whileLoop (\<lambda>r s. the (C r s)) B r)
|
||||||
|
(setter;; (While {s'. cond_xf s' \<noteq> 0} (B';; setter)))"
|
||||||
proof -
|
proof -
|
||||||
note unif_rrel_def[simp add] to_bool_def[simp add]
|
note unif_rrel_def[simp add] to_bool_def[simp add]
|
||||||
have helper:
|
have helper:
|
||||||
"\<And>state xstate'.
|
"\<And>state xstate'.
|
||||||
\<Gamma> \<turnstile> \<langle>While {s'. cond_xf s' \<noteq> 0} (Seq B' setter), Normal state\<rangle> \<Rightarrow> xstate' \<Longrightarrow>
|
\<Gamma> \<turnstile> \<langle>While {s'. cond_xf s' \<noteq> 0} (Seq B' setter), Normal state\<rangle> \<Rightarrow> xstate' \<Longrightarrow>
|
||||||
\<forall>st r s. Normal st = xstate' \<and> (s, state) \<in> srel
|
\<forall>st r s. Normal st = xstate' \<and> (s, state) \<in> srel
|
||||||
\<and> (cond_xf state \<noteq> 0) = the (C r s) \<and> xf state = r \<and> G s
|
\<and> (C r s \<noteq> None) \<and> (cond_xf state \<noteq> 0) = the (C r s)
|
||||||
\<and> state \<in> G' \<and> (cond_xf state \<noteq> 0 \<longrightarrow> state \<in> C')
|
\<and> rrel r (xf state) \<and> G r s \<and> state \<in> G' \<and> (cond_xf state \<noteq> 0 \<longrightarrow> state \<in> C')
|
||||||
\<longrightarrow> (\<exists>rv s'. (rv, s') \<in> fst (whileLoop (\<lambda>r s. the (C r s)) B r s)
|
\<longrightarrow> (\<exists>rv s'. (rv, s') \<in> fst (whileLoop (\<lambda>r s. the (C r s)) B r s)
|
||||||
\<and> (s', st) \<in> srel \<and> rv = xf st)"
|
\<and> (s', st) \<in> srel \<and> rrel rv (xf st))"
|
||||||
apply (erule exec_While_final_inv''; simp)
|
apply (erule_tac C="{s'. cond_xf s' \<noteq> 0}" in exec_While_final_inv''; simp)
|
||||||
apply (fastforce simp: whileLoop_cond_fail return_def)
|
apply (fastforce simp: whileLoop_cond_fail return_def)
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (rename_tac t t' t'' s)
|
apply (rename_tac t t' t'' r s y)
|
||||||
apply (frule intermediate_Normal_state[where P="G' \<inter> C'"])
|
apply (frule_tac P="{s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')
|
||||||
|
\<and> s' \<in> C' \<and> (C r s \<noteq> None) \<and> the (C r s)}"
|
||||||
|
in intermediate_Normal_state)
|
||||||
apply fastforce
|
apply fastforce
|
||||||
apply (fastforce intro: body_inv)
|
apply (fastforce intro: body_inv conseqPre)
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (rename_tac inter_t)
|
apply (rename_tac inter_t)
|
||||||
apply (prop_tac "\<exists>s'. (xf inter_t, s') \<in> fst (B (xf t) s) \<and> (s', inter_t) \<in> srel")
|
apply (prop_tac "\<exists>rv' s'. rrel rv' (xf inter_t) \<and> (rv', s') \<in> fst (B r s)
|
||||||
subgoal by (erule ccorresE[OF body_ccorres])
|
\<and> (s', inter_t) \<in> srel")
|
||||||
(fastforce simp: no_fail_def nf[simplified no_fail_def] dest: EHOther)+
|
apply (insert body_ccorres)[1]
|
||||||
|
apply (drule_tac x=r in meta_spec)
|
||||||
|
apply (erule (1) ccorresE)
|
||||||
|
apply fastforce
|
||||||
|
apply fastforce
|
||||||
|
using nf apply (fastforce simp: no_fail_def)
|
||||||
|
apply (fastforce dest!: EHOther)
|
||||||
|
apply fastforce
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (prop_tac "G s'")
|
apply (prop_tac "G rv' s'")
|
||||||
apply (fastforce dest: use_valid intro: body_inv)
|
apply (fastforce dest: use_valid intro: body_inv)
|
||||||
apply (prop_tac "inter_t \<in> G'")
|
apply (prop_tac "inter_t \<in> G'")
|
||||||
apply (fastforce dest: hoarep_exec[rotated] intro: body_inv)
|
apply (fastforce dest: hoarep_exec[rotated] intro: body_inv)
|
||||||
|
apply (drule_tac x=rv' in spec)
|
||||||
apply (drule_tac x=s' in spec)
|
apply (drule_tac x=s' in spec)
|
||||||
|
apply (prop_tac "rrel rv' (xf inter_t)")
|
||||||
|
apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated])
|
||||||
apply (elim impE)
|
apply (elim impE)
|
||||||
apply (drule_tac s'=inter_t and r1="xf t'" in ccorresE_gets_the[OF cond_ccorres]; assumption?)
|
apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF setter_ccorres]; assumption?)
|
||||||
apply (fastforce intro: no_ofail)
|
apply (fastforce intro: no_ofail)
|
||||||
apply (fastforce dest: EHOther)
|
apply (fastforce dest: EHOther)
|
||||||
subgoal by (fastforce dest: hoarep_exec intro: setter_inv_cond)
|
apply (intro conjI)
|
||||||
apply (prop_tac "xf inter_t = xf t'")
|
apply fastforce
|
||||||
apply (fastforce dest: hoarep_exec[rotated] intro: setter_xf_inv)
|
using no_ofail apply (fastforce elim!: no_ofailD)
|
||||||
|
apply fastforce
|
||||||
|
apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated])
|
||||||
|
apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated])
|
||||||
|
apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated])
|
||||||
|
apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated])
|
||||||
apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3))
|
apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3))
|
||||||
done
|
done
|
||||||
|
|
||||||
|
have setter_hoarep:
|
||||||
|
"\<And>r s s' n xstate.
|
||||||
|
\<Gamma>\<turnstile>\<^sub>h \<langle>(setter;; While {s'. cond_xf s' \<noteq> 0} (B';; setter)) # hs,s'\<rangle> \<Rightarrow> (n, xstate)
|
||||||
|
\<Longrightarrow> \<Gamma>\<turnstile> {s' \<in> G'. (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
|
||||||
|
setter
|
||||||
|
{s'. (s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s'))
|
||||||
|
\<and> (cond_xf s' \<noteq> 0 \<longrightarrow> (s' \<in> C' \<and> C r s = Some True))}"
|
||||||
|
apply (insert setter_ccorres)
|
||||||
|
apply (drule_tac x=r in meta_spec)
|
||||||
|
apply (frule_tac s=s in ccorres_to_vcg_gets_the)
|
||||||
|
apply (fastforce intro: no_ofail)
|
||||||
|
apply (insert setter_rrel)
|
||||||
|
apply (drule_tac x=s in meta_spec)
|
||||||
|
apply (drule_tac x=r in meta_spec)
|
||||||
|
apply (rule hoarep_conj_lift_pre_fix)
|
||||||
|
apply (rule hoarep_conj_lift_pre_fix)
|
||||||
|
apply (insert setter_inv_cond)[1]
|
||||||
|
apply (drule_tac x=s in meta_spec)
|
||||||
|
apply (drule_tac x=r in meta_spec)
|
||||||
|
apply (rule_tac Q'="{s' \<in> G'. cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C'}" in conseqPost; fastforce)
|
||||||
|
apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre)
|
||||||
|
apply (insert setter_inv_cond)
|
||||||
|
apply (drule_tac x=s in meta_spec)
|
||||||
|
apply (drule_tac x=r in meta_spec)
|
||||||
|
apply (simp add: imp_conjR)
|
||||||
|
apply (rule hoarep_conj_lift_pre_fix)
|
||||||
|
apply (simp add: Collect_mono conseq_under_new_pre)
|
||||||
|
apply (rule_tac Q'="{s'. C r s \<noteq> None \<and> the (C r s) = (cond_xf s' \<noteq> 0)}"
|
||||||
|
in conseqPost[rotated])
|
||||||
|
apply fastforce
|
||||||
|
apply fastforce
|
||||||
|
apply (simp add: Collect_mono conseq_under_new_pre)
|
||||||
|
done
|
||||||
|
|
||||||
show ?thesis
|
show ?thesis
|
||||||
apply (clarsimp simp: ccorres_underlying_def)
|
apply (clarsimp simp: ccorres_underlying_def)
|
||||||
apply (rename_tac s s' n xstate)
|
apply (rename_tac s s' n xstate)
|
||||||
apply (frule (1) exec_handlers_use_hoare_nothrow_hoarep)
|
apply (frule_tac R'="{s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}"
|
||||||
apply (rule_tac R="G' \<inter> {s'. s' \<in> {t. cond_xf t \<noteq> 0} \<longrightarrow> s' \<in> C'}" in HoarePartial.Seq)
|
and Q'="{s'. \<exists>rv s. s' \<in> G' \<and> (s, s') \<in> srel \<and> G rv s \<and> rrel rv (xf s')}"
|
||||||
apply (fastforce intro: setter_inv_cond)
|
in exec_handlers_use_hoare_nothrow_hoarep)
|
||||||
apply (fastforce intro: While_inv_from_body_setter setter_inv_cond body_inv)
|
apply fastforce
|
||||||
apply clarsimp
|
apply (rule HoarePartial.Seq)
|
||||||
apply (frule (1) intermediate_Normal_state)
|
apply (erule setter_hoarep)
|
||||||
apply (fastforce intro: setter_inv_cond)
|
apply (rule conseqPre)
|
||||||
|
apply (rule ccorres_While_Normal_helper)
|
||||||
|
apply (fastforce intro!: setter_hoarep hoarep_ex_lift)
|
||||||
|
apply (intro hoarep_ex_pre, rename_tac rv new_s)
|
||||||
|
apply (insert setter_inv_cond)[1]
|
||||||
|
apply (drule_tac x=new_s in meta_spec)
|
||||||
|
apply (drule_tac x=rv in meta_spec)
|
||||||
|
apply (insert body_ccorres)[1]
|
||||||
|
apply (drule_tac x=rv in meta_spec)
|
||||||
|
apply (insert body_inv(2))[1]
|
||||||
|
apply (drule_tac x=new_s in meta_spec)
|
||||||
|
apply (drule_tac x=rv in meta_spec)
|
||||||
|
apply (frule_tac s=new_s in ccorres_to_vcg_with_prop)
|
||||||
|
using nf apply fastforce
|
||||||
|
using body_inv apply fastforce
|
||||||
|
apply (rule_tac Q'="{s'. s' \<in> G'
|
||||||
|
\<and> (\<exists>(rv, s) \<in>fst (B rv new_s). (s, s') \<in> srel \<and> rrel rv (xf s')
|
||||||
|
\<and> G rv s)}"
|
||||||
|
in conseqPost;
|
||||||
|
fastforce?)
|
||||||
|
apply (rule hoarep_conj_lift_pre_fix;
|
||||||
|
fastforce simp: Collect_mono conseq_under_new_pre)
|
||||||
|
apply fastforce
|
||||||
|
apply (case_tac xstate; clarsimp)
|
||||||
|
apply (frule intermediate_Normal_state[OF _ _ setter_hoarep]; assumption?)
|
||||||
|
apply fastforce
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (rename_tac inter_t)
|
apply (rename_tac inter_t)
|
||||||
apply (drule (2) ccorresE_gets_the[OF cond_ccorres _ _ _ no_ofail])
|
apply (insert setter_ccorres)
|
||||||
|
apply (drule_tac x=r in meta_spec)
|
||||||
|
apply (drule (3) ccorresE_gets_the)
|
||||||
|
apply (fastforce intro: no_ofail)
|
||||||
apply (fastforce dest: EHOther)
|
apply (fastforce dest: EHOther)
|
||||||
apply (prop_tac "xf inter_t = xf s'")
|
apply (prop_tac "rrel r (xf inter_t)")
|
||||||
apply (fastforce dest: hoarep_exec[rotated] intro: setter_xf_inv)
|
apply (fastforce dest: hoarep_exec[rotated] intro: setter_rrel)
|
||||||
apply (clarsimp simp: isNormal_def)
|
apply (case_tac "\<not> the (C r s)")
|
||||||
apply (auto dest: hoarep_exec dest!: helper spec intro: setter_inv_cond)
|
apply (fastforce elim: exec_Normal_elim_cases simp: whileLoop_cond_fail return_def)
|
||||||
|
apply (insert no_ofail)
|
||||||
|
apply (fastforce dest!: helper hoarep_exec[OF _ _ setter_inv_cond, rotated] no_ofailD)
|
||||||
done
|
done
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue