Integrating scoping to the VCG!!
This commit is contained in:
nemouchi
parent
4cad6c33b6
commit
ab4cc6a38c
|
|
@ -330,6 +330,7 @@ text \<open>For UTP solve tactics see @{method utp_simp_tac}\<close>
|
|||
subsubsection \<open> UTP predicates tactics\<close>
|
||||
|
||||
method upreds_defs = (unfold upred_defs)[1]
|
||||
thm lens_defs
|
||||
method upreds_rewrites = (simp add: fun_eq_iff lens_defs upred_defs alpha_splits Product_Type.split_beta)
|
||||
|
||||
method upreds_simp = utp_tac_control upreds_defs fast_uexpr_transfer upreds_rewrites uexpr_interp_tac utp_simp_tac
|
||||
|
|
@ -361,9 +362,9 @@ subsection\<open>Auxiliary lemmas for VCG\<close>
|
|||
|
||||
lemma FRAME_TRIPLE_E: "FRAME_TRIPLE P \<Longrightarrow> P" by (auto simp: FRAME_TRIPLE_def)
|
||||
|
||||
definition DONT_TOUCH_E :: "bool \<Rightarrow> bool" where "DONT_TOUCH_E P = P"
|
||||
definition DONT_TOUCH :: "bool \<Rightarrow> bool" where "DONT_TOUCH P = P"
|
||||
|
||||
lemma DONT_TOUCH_E: "DONT_TOUCH_E P \<Longrightarrow> P" by (auto simp: DONT_TOUCH_E_def)
|
||||
lemma DONT_TOUCH_E: "DONT_TOUCH P \<Longrightarrow> P" by (auto simp: DONT_TOUCH_def)
|
||||
|
||||
subsection \<open>VCG first goal pre-processing\<close>
|
||||
|
||||
|
|
@ -428,6 +429,26 @@ method hoare_wp_rule_apply =
|
|||
| (match conclusion in "\<lbrace>_\<rbrace>FOR (_,_,_)DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>DO _ WHILE _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>FROM _ UNTIL _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
(*Annotated SCOPED loop patterns for total correctness*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>IN _ INVAR _ VRT _ WHILE _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
rule while_scp_invr_vrt_prog_hoare_wp[where e = "&\<Sigma>" and R = measure and
|
||||
g = fst_lens and l = snd_lens];
|
||||
rule FRAME_TRIPLE_E)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>IN _ FOR (_,_,_) INVAR _ VRT _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
subst for_lfp_scp_invr_vrt_prog_def_alt)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>IN _ DO _ INVAR _ VRT _ WHILE _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
subst do_while_lfp_scp_invr_vrt_prog_def_alt)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>IN _ FROM _ INVAR _ VRT _ UNTIL _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
subst from_until_lfp_scp_invr_vrt_prog_def_alt)
|
||||
(*Non-annotated SCOPED loop patterns fail the VCG... which requires a proof annotation *)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ INVAR _ WHILE _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ FOR (_,_,_)INVAR _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ DO _ INVAR _ WHILE _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ FROM _ INVAR _ UNTIL _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ WHILE _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ FOR (_,_,_)DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ DO _ WHILE _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ FROM _ UNTIL _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>)
|
||||
--\<open>WP Matching rules for partial correctness\<close>
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>\<langle>_\<rangle>\<^sub>a\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>succeed\<close>), rule assigns_backward_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>SKIP\<^sub>r\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>succeed\<close>), rule skip_hoare_rel)
|
||||
|
|
@ -599,13 +620,13 @@ method vcg_hol_post_processing =
|
|||
--\<open>The method in the sequel puts together SE step1 and SE step2.\<close>
|
||||
|
||||
method post_processing = ((unfold pr_var_def in_var_def out_var_def)?,
|
||||
((simp only: lens_indep_all_simplifier)+)?,
|
||||
((simp only: lens_indep_all_simplifier))?,
|
||||
clarsimp?,
|
||||
(vcg_upreds_post_processing+)?,
|
||||
(vcg_upreds_post_processing)?,
|
||||
vcg_hol_post_processing(*TODO: ADD SOLVING STEP HERE*))
|
||||
|
||||
method vcg_can_do_symbolic_execution =
|
||||
(match conclusion in "DONT_TOUCH_E _" \<Rightarrow> fail
|
||||
(match conclusion in "DONT_TOUCH _" \<Rightarrow> fail
|
||||
\<bar> "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>P"\<Rightarrow> fail
|
||||
\<bar> "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>G"\<Rightarrow> fail
|
||||
\<bar> "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>u"\<Rightarrow> fail
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ lemma add_prog_total:
|
|||
OD
|
||||
\<lbrace>&a =\<^sub>u \<guillemotleft>y\<guillemotright> + \<guillemotleft>x\<guillemotright>\<rbrace>\<^sub>P"
|
||||
apply (insert assms) (*Make this automatic *)
|
||||
apply (vcg wp_trace)
|
||||
apply (vcg wp)
|
||||
done
|
||||
|
||||
subsection \<open>Increment method\<close>
|
||||
|
|
@ -624,7 +624,7 @@ lemma
|
|||
(*additional post-processing for proving VCs related to the modify assumption
|
||||
TODO: automate this*)
|
||||
apply (insert assms)
|
||||
apply (simp_all add: DONT_TOUCH_E_def prog_rep_eq)
|
||||
apply (simp_all add: DONT_TOUCH_def prog_rep_eq)
|
||||
apply rel_auto+
|
||||
done
|
||||
|
||||
|
|
@ -651,7 +651,7 @@ lemma count_down_preserves_list_test:
|
|||
(*additional post-processing for proving VCs related to the modify assumption
|
||||
TODO: automate this*)
|
||||
apply (insert assms)
|
||||
apply (simp_all add: DONT_TOUCH_E_def prog_rep_eq)
|
||||
apply (simp_all add: DONT_TOUCH_def prog_rep_eq)
|
||||
apply rel_auto+
|
||||
done
|
||||
|
||||
|
|
@ -669,7 +669,7 @@ lemma swap_count_down_preserves_list:
|
|||
(*additional post-processing for proving VCs related to the modify assumption
|
||||
TODO: automate this*)
|
||||
apply (insert assms)
|
||||
apply (simp_all add: DONT_TOUCH_E_def prog_rep_eq)
|
||||
apply (simp_all add: DONT_TOUCH_def prog_rep_eq)
|
||||
apply rel_auto+
|
||||
done
|
||||
|
||||
|
|
@ -726,196 +726,82 @@ lemma blah:
|
|||
|
||||
declare blah[unfolded Product_Type.split_paired_All, unfolded Product_Type.prod.case,THEN spec, vcg_proved_specs]
|
||||
|
||||
lemma antiframe_prog_refinedBy_while_lfp:
|
||||
assumes WF:"wf R"
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
assumes induct_step: "\<And>st. g:[WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body ; passert_prog ((e, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright>) ; g:[WHILE b DO body OD]
|
||||
ELSE SKIP FI"
|
||||
shows "g:[WHILE b DO body OD] \<sqsubseteq> WHILE b DO body OD"
|
||||
proof -
|
||||
{
|
||||
fix st
|
||||
have " g:[WHILE b DO body OD] \<sqsubseteq> WHILE b DO body OD"
|
||||
using WF proof (induction rule: wf_induct_rule)
|
||||
case (less st)
|
||||
hence 0:"passert_prog ((e,\<guillemotleft>st\<guillemotright>)\<^sub>u\<in>\<^sub>u\<guillemotleft>R\<guillemotright>) ; g:[WHILE b DO body OD] \<sqsubseteq> WHILE b DO body OD"
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_simp
|
||||
apply (metis (no_types, lifting))
|
||||
done
|
||||
have 1: "IF b THEN body;WHILE b DO body OD ELSE SKIP FI \<sqsubseteq> WHILE b DO body OD"
|
||||
unfolding while_lfp_invr_vrt_prog_def
|
||||
by (metis order_refl while_lfp_prog_unfold)
|
||||
from 0 1 have 2: "passert_prog ((e,\<guillemotleft>st\<guillemotright>)\<^sub>u\<in>\<^sub>u\<guillemotleft>R\<guillemotright>) ; g:[WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body; WHILE b DO body OD ELSE SKIP FI"
|
||||
by (metis while_lfp_invr_vrt_prog_def while_lfp_prog_unfold)
|
||||
have 3: "IF b THEN body; passert_prog ((e,\<guillemotleft>st\<guillemotright>)\<^sub>u\<in>\<^sub>u\<guillemotleft>R\<guillemotright>) ; g:[WHILE b DO body OD] ELSE SKIP FI \<sqsubseteq>
|
||||
IF b THEN body; WHILE b DO body OD ELSE SKIP FI"
|
||||
by (rule Mono_progD[OF if_prog_mono[THEN mono_Monotone_prog], OF 0])
|
||||
have 4: " g:[WHILE b DO body OD] \<sqsubseteq> \<dots>"
|
||||
by (rule induct_step)
|
||||
then show ?case using order_trans[OF 3 4]
|
||||
by (metis while_lfp_invr_vrt_prog_def while_lfp_prog_unfold)
|
||||
qed
|
||||
}
|
||||
thus ?thesis
|
||||
apply (simp add: prog_rep_eq)
|
||||
|
||||
done
|
||||
qed
|
||||
|
||||
lemma while_lfp_prog_antiframe_prog_modifies:
|
||||
assumes WF:"wf R"
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
assumes modifies: "g:[body] = body"
|
||||
assumes induct_step: "\<And>st. g:[WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body ; passert_prog ((e, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright>) ; g:[WHILE b DO body OD]
|
||||
ELSE SKIP FI"
|
||||
shows "g:[WHILE b DO body OD] = WHILE b DO body OD"
|
||||
apply (rule antisym)
|
||||
apply (rule antiframe_prog_refines_while_lfp_prog[OF vwb_lens modifies])
|
||||
apply (rule antiframe_prog_refinedBy_while_lfp[OF WF vwb_lens induct_step])
|
||||
done
|
||||
|
||||
lemma while_lfp_prog_invar_vrt_antiframe_prog_modifies:
|
||||
assumes WF:"wf R"
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
assumes modifies: "g:[body] = body"
|
||||
assumes induct_step: "\<And>st. g:[INVAR I VRT \<guillemotleft>R\<guillemotright> WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body ; passert_prog ((e, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright>) ; g:[INVAR I VRT \<guillemotleft>R\<guillemotright> WHILE b DO body OD]
|
||||
ELSE SKIP FI"
|
||||
shows "g:[INVAR I VRT \<guillemotleft>R\<guillemotright> WHILE b DO body OD] = INVAR I VRT \<guillemotleft>R\<guillemotright> WHILE b DO body OD"
|
||||
using assms unfolding while_lfp_invr_vrt_prog_def
|
||||
using while_lfp_prog_antiframe_prog_modifies
|
||||
by blast
|
||||
|
||||
lemma while_lfp_prog_invar_vrt_measur_antiframe_prog_modifies:
|
||||
assumes WF:"wf (measure (Rep_uexpr (expression)))"
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
assumes modifies: "g:[body] = body"
|
||||
assumes induct_step: "\<And>st. g:[INVAR I VRT \<guillemotleft>measure (Rep_uexpr (expression))\<guillemotright> WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body ; passert_prog ((e, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>measure (Rep_uexpr (expression))\<guillemotright>) ; g:[INVAR I VRT \<guillemotleft>measure (Rep_uexpr (expression))\<guillemotright> WHILE b DO body OD]
|
||||
ELSE SKIP FI"
|
||||
shows "g:[INVAR I VRT expression WHILE b DO body OD] = INVAR I VRT expression WHILE b DO body OD"
|
||||
using assms unfolding while_lfp_invr_vrt_prog_def
|
||||
using while_lfp_prog_antiframe_prog_modifies
|
||||
by blast
|
||||
|
||||
(*lemma while_lfp_prog_vrt_invar_antiframe_prog_modifies:
|
||||
assumes WF:"\<And>z. wf (R z)"
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
assumes modifies: "g:[body] = body"
|
||||
assumes induct_step: "\<And>st z. (passert_prog (e =\<^sub>u \<guillemotleft>st\<guillemotright>)) ; g:[ VRT (\<lambda>z. \<guillemotleft>R z\<guillemotright>) INVAR I WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body ; passert_prog ((e, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R z\<guillemotright>) ; g:[VRT (\<lambda>z. \<guillemotleft>R z\<guillemotright>) INVAR I WHILE b DO body OD]
|
||||
ELSE SKIP FI"
|
||||
shows "g:[VRT (\<lambda>z. \<guillemotleft>R z\<guillemotright>) INVAR I WHILE b DO body OD] = VRT (\<lambda>z. \<guillemotleft>R z\<guillemotright>) INVAR I WHILE b DO body OD"
|
||||
using assms unfolding while_lfp_invr_vrt_prog_G_def
|
||||
using while_lfp_prog_antiframe_prog_modifies
|
||||
by blast
|
||||
|
||||
lemma while_lfp_prog_vrt_invar_antiframe_prog_modifies':
|
||||
assumes WF:"\<And>z. wf (R z)"
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
assumes modifies: "g:[body] = body"
|
||||
assumes induct_step: "\<And>st z. (passert_prog (e =\<^sub>u \<guillemotleft>st\<guillemotright>)) ; g:[ VRT (\<lambda>z. \<guillemotleft>R z\<guillemotright>) INVAR I WHILE b DO body OD] \<sqsubseteq>
|
||||
IF b THEN body ; passert_prog ((e, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R z\<guillemotright>) ; g:[VRT (\<lambda>z. \<guillemotleft>R z\<guillemotright>) INVAR I WHILE b DO body OD]
|
||||
ELSE SKIP FI"
|
||||
shows "g:[VRT vari INVAR I WHILE b DO body OD] = VRT vari INVAR I WHILE b DO body OD"
|
||||
using assms unfolding while_lfp_invr_vrt_prog_G_def
|
||||
using while_lfp_prog_antiframe_prog_modifies
|
||||
by blast*)
|
||||
|
||||
lemma assigns_prog_antiframe_prog_modifies:
|
||||
"[g \<mapsto>\<^sub>s \<langle>\<sigma>\<rangle>\<^sub>s g] = \<sigma> \<Longrightarrow>vwb_lens g \<Longrightarrow>g:[\<langle>\<sigma>\<rangle>\<^sub>a] = \<langle>\<sigma>\<rangle>\<^sub>a"
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_simp
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma If_prog_refines_prog:
|
||||
assumes "spec \<sqsubseteq> passert_prog b ; P"
|
||||
assumes "spec \<sqsubseteq> passert_prog (\<not>b) ; Q"
|
||||
shows " spec \<sqsubseteq> IF b THEN P ELSE Q FI"
|
||||
using assms
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_simp
|
||||
apply metis
|
||||
done
|
||||
|
||||
|
||||
lemma If_blah:
|
||||
"P ; IF b THEN Q1 ELSE Q2 FI =
|
||||
IF b THEN P ; IF b THEN Q1 ELSE Q2 FI ELSE P ; IF b THEN Q1 ELSE Q2 FI FI "
|
||||
by pauto
|
||||
lemma
|
||||
"passert_prog p ; IF b THEN Q1 ELSE Q2 FI =
|
||||
IF b \<and> p THEN Q1 ELSE Q2 FI "
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply pred_simp
|
||||
apply auto
|
||||
|
||||
apply blast
|
||||
oops
|
||||
lemma assumes "vwb_lens i" "vwb_lens r"
|
||||
shows
|
||||
"passert_prog (&\<Sigma> =\<^sub>u \<guillemotleft>st\<guillemotright>\<and>b)
|
||||
\<sqsubseteq> passert_prog b"
|
||||
apply (insert assms)
|
||||
apply pauto
|
||||
oops
|
||||
lemma assumes "vwb_lens i" "vwb_lens r"
|
||||
shows
|
||||
"passume_prog (&\<Sigma> =\<^sub>u \<guillemotleft>st\<guillemotright>\<and> (b \<or> \<not>b))
|
||||
\<sqsubseteq> passert_prog b "
|
||||
apply (insert assms)
|
||||
apply pauto
|
||||
|
||||
oops
|
||||
|
||||
lemma "\<And>aa st.
|
||||
`((&\<Sigma>, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>measure \<lbrakk>uop length \<guillemotleft>a\<guillemotright> - &i:fst_lens\<rbrakk>\<^sub>e\<guillemotright>) \<and> (\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>a\<guillemotright> \<and> \<guillemotleft>0\<guillemotright> <\<^sub>u (&i:fst_lens) \<and> (&i:fst_lens) \<le>\<^sub>u uop length \<guillemotleft>a\<guillemotright> \<and>
|
||||
(&r:fst_lens) =\<^sub>u uop Max (uop set (bop take (&i:fst_lens) \<guillemotleft>a\<guillemotright>)) \<and>
|
||||
bop op < &r:fst_lens (bop op ! \<guillemotleft>a\<guillemotright> &i:fst_lens)) \<Rightarrow>
|
||||
(\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>a\<guillemotright> \<and> \<guillemotleft>0\<guillemotright> <\<^sub>u (&i:fst_lens) \<and> (&i:fst_lens) \<le>\<^sub>u uop length \<guillemotleft>a\<guillemotright> \<and>
|
||||
(&r:fst_lens) =\<^sub>u uop Max (uop set (bop take (&i:fst_lens) \<guillemotleft>a\<guillemotright>)) \<and>
|
||||
bop op < &r:fst_lens (bop op ! \<guillemotleft>a\<guillemotright> &i:fst_lens))`"
|
||||
apply pred_simp
|
||||
subgoal for aa aaaa
|
||||
apply (cases "(get\<^bsub>i\<^esub> aa)")
|
||||
apply auto
|
||||
apply (cases "(get\<^bsub>i\<^esub> aaaa)")
|
||||
apply auto
|
||||
apply (subst (asm) take_Suc_conv_app_nth )
|
||||
|
||||
apply auto
|
||||
apply (subst (asm) take_Suc_conv_app_nth )
|
||||
|
||||
apply auto
|
||||
|
||||
lemma blah':
|
||||
assumes "r \<bowtie> i"
|
||||
assumes "vwb_lens i" "vwb_lens r"
|
||||
shows
|
||||
"\<lbrace> (\<lambda>(aa). (\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> uop length \<guillemotleft>aa\<guillemotright> \<ge>\<^sub>u\<guillemotleft>1\<guillemotright> \<and> (&i:fst_lens) =\<^sub>u \<guillemotleft>1\<guillemotright> \<and>
|
||||
(&r:fst_lens) =\<^sub>u bop nth \<guillemotleft>aa:: int list\<guillemotright> \<guillemotleft>0\<guillemotright>))\<rbrace>
|
||||
\<lambda>(aa).
|
||||
IN ((i;\<^sub>Lfst_lens) +\<^sub>L (r;\<^sub>Lfst_lens))
|
||||
INVAR ((\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> \<guillemotleft>0\<guillemotright> <\<^sub>u (&i:fst_lens) \<and> (&i:fst_lens) \<le>\<^sub>u uop length \<guillemotleft>aa\<guillemotright> \<and>
|
||||
(&r:fst_lens) =\<^sub>u uop Max (uop set (bop take (&i:fst_lens) \<guillemotleft>aa\<guillemotright>))))
|
||||
VRT (uop length \<guillemotleft>a\<guillemotright> - (&i:fst_lens))
|
||||
WHILE \<not>((&i:fst_lens) =\<^sub>u uop length \<guillemotleft>a\<guillemotright>)
|
||||
DO IF (&r:fst_lens) <\<^sub>u bop nth \<guillemotleft>a\<guillemotright> (&i:fst_lens)
|
||||
THEN (r:fst_lens) :== (bop nth \<guillemotleft>a\<guillemotright> (&i:fst_lens))
|
||||
ELSE SKIP
|
||||
FI;
|
||||
(i:fst_lens) :== ((&i:fst_lens) + \<guillemotleft>1\<guillemotright>)
|
||||
OD
|
||||
\<lbrace> (\<lambda>(aa). ((&r:fst_lens) =\<^sub>uuop Max (uop set \<guillemotleft>aa\<guillemotright>)))\<rbrace>\<^sub>G"
|
||||
apply (insert assms)
|
||||
apply ( vcg wp)
|
||||
subgoal for _
|
||||
by (cases a; auto)
|
||||
defer
|
||||
defer
|
||||
defer
|
||||
subgoal for _ i'
|
||||
apply (simp add: take_Suc_conv_app_nth )
|
||||
apply (subst (asm) Max_insert)
|
||||
apply auto
|
||||
unfolding Ball_def
|
||||
|
||||
apply auto
|
||||
oops
|
||||
lemma
|
||||
" \<And>aa st. r \<bowtie> i\<Longrightarrow> vwb_lens i\<Longrightarrow> vwb_lens r\<Longrightarrow>
|
||||
`(\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> \<guillemotleft>0\<guillemotright> <\<^sub>u (&i:fst_lens) \<and> (&i:fst_lens) \<le>\<^sub>u uop length \<guillemotleft>aa\<guillemotright> \<and> (&r:fst_lens) =\<^sub>u uop Max (uop set (bop take (&i:fst_lens) \<guillemotleft>aa\<guillemotright>)))` \<Longrightarrow>
|
||||
{&i:fst_lens , &r:fst_lens, &snd_lens}:[IF bop op < &r:fst_lens (bop op ! \<guillemotleft>a\<guillemotright> &i:fst_lens)
|
||||
THEN (r:fst_lens) :== (bop op ! \<guillemotleft>a\<guillemotright> &i:fst_lens) ELSE SKIP FI ;
|
||||
(i:fst_lens) :== (&i:fst_lens + \<guillemotleft>1\<guillemotright>)] \<sqsubseteq>
|
||||
(&\<Sigma>, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>measure \<lbrakk>uop length \<guillemotleft>a\<guillemotright> - &i:fst_lens\<rbrakk>\<^sub>e\<guillemotright>\<^sub>\<bottom>\<^sub>P"
|
||||
apply auto
|
||||
done
|
||||
subgoal for _ i'
|
||||
apply (clarsimp simp: take_Suc_conv_app_nth)
|
||||
apply (cases a, auto)
|
||||
done
|
||||
subgoal for _ i
|
||||
by (clarsimp simp: take_Suc_conv_app_nth)
|
||||
subgoal for _ i
|
||||
by (clarsimp simp: take_Suc_conv_app_nth)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_pred_sublens)
|
||||
apply (subst seq_prog_anti_frame_prog_modifies)
|
||||
defer
|
||||
apply (subst If_prog_anti_frame_prog_modifies )
|
||||
defer
|
||||
apply (subst assigns_prog_antiframe_prog_modifies)
|
||||
defer
|
||||
defer
|
||||
defer
|
||||
apply (subst SKIP_prog_anti_frame_prog_modifies)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (subst assigns_prog_antiframe_prog_modifies)
|
||||
using assms
|
||||
apply rel_simp
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply simp
|
||||
apply (simp add: DONT_TOUCH_def)
|
||||
using assms
|
||||
apply rel_simp
|
||||
apply simp
|
||||
done
|
||||
|
||||
declare blah'[unfolded Product_Type.split_paired_All, unfolded Product_Type.prod.case,THEN spec, vcg_proved_specs]
|
||||
|
||||
oops
|
||||
lemma
|
||||
assumes "r \<bowtie> i"
|
||||
assumes "vwb_lens i" "vwb_lens r"
|
||||
shows
|
||||
"\<lbrace>\<lambda>(aa). \<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> uop length \<guillemotleft>aa\<guillemotright> \<ge>\<^sub>u\<guillemotleft>1\<guillemotright> \<and> (&i:fst_lens) =\<^sub>u \<guillemotleft>1\<guillemotright> \<and> (&r:fst_lens) =\<^sub>u bop nth \<guillemotleft>aa:: int list\<guillemotright> \<guillemotleft>0\<guillemotright>\<rbrace>
|
||||
"\<lbrace>\<lambda>(aa). \<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> uop length \<guillemotleft>aa\<guillemotright> \<ge>\<^sub>u\<guillemotleft>1\<guillemotright> \<and> (&i:fst_lens) =\<^sub>u \<guillemotleft>1\<guillemotright> \<and>
|
||||
(&r:fst_lens) =\<^sub>u bop nth \<guillemotleft>aa:: int list\<guillemotright> \<guillemotleft>0\<guillemotright>\<rbrace>
|
||||
\<lambda>(aa). {&i:fst_lens, &r:fst_lens}:[
|
||||
|
||||
INVAR (\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> \<guillemotleft>0\<guillemotright> <\<^sub>u (&i:fst_lens) \<and> (&i:fst_lens) \<le>\<^sub>u uop length \<guillemotleft>aa\<guillemotright> \<and> (&r:fst_lens) =\<^sub>u uop Max (uop set (bop take (&i:fst_lens) \<guillemotleft>aa\<guillemotright>)))
|
||||
IN ((i;\<^sub>Lfst_lens) +\<^sub>L (r;\<^sub>Lfst_lens))
|
||||
INVAR (\<guillemotleft>a\<guillemotright> =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and> \<guillemotleft>0\<guillemotright> <\<^sub>u (&i:fst_lens) \<and> (&i:fst_lens) \<le>\<^sub>u uop length \<guillemotleft>aa\<guillemotright> \<and>
|
||||
(&r:fst_lens) =\<^sub>u uop Max (uop set (bop take (&i:fst_lens) \<guillemotleft>aa\<guillemotright>)))
|
||||
VRT(uop length \<guillemotleft>a\<guillemotright> - (&i:fst_lens))
|
||||
WHILE \<not>((&i:fst_lens) =\<^sub>u uop length \<guillemotleft>a\<guillemotright>)
|
||||
DO IF (&r:fst_lens) <\<^sub>u bop nth \<guillemotleft>a\<guillemotright> (&i:fst_lens)
|
||||
|
|
@ -926,72 +812,13 @@ lemma
|
|||
OD]
|
||||
\<lbrace>\<lambda>(aa). (&r:fst_lens) =\<^sub>uuop Max (uop set \<guillemotleft>aa\<guillemotright>)\<rbrace>\<^sub>G"
|
||||
apply (insert assms)
|
||||
apply (vcg wp_trace)
|
||||
apply (vcg wp)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (metis assms(1) assms(2) assms(3) fst_vwb_lens in_var_def in_var_indep lens_comp_lb lens_indep_sym plus_pred_sublens vwb_lens_def)
|
||||
unfolding DONT_TOUCH_E_def
|
||||
apply (rule while_lfp_prog_invar_vrt_measur_antiframe_prog_modifies[where e="&\<Sigma>"])
|
||||
apply pred_simp
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (subst seq_prog_anti_frame_prog_modifies)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (subst If_prog_anti_frame_prog_modifies)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (rule assigns_prog_antiframe_prog_modifies)
|
||||
apply rel_simp
|
||||
apply (simp add: assms(2) assms(3))
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (rule SKIP_prog_anti_frame_prog_modifies)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (rule refl)
|
||||
apply (rule assigns_prog_antiframe_prog_modifies)
|
||||
apply rel_simp
|
||||
apply (simp add: assms)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (rule refl)
|
||||
unfolding DONT_TOUCH_def while_lfp_scp_invr_vrt_prog_def
|
||||
|
||||
thm while_lfp_prog_unfold[unfolded while_lfp_invr_vrt_prog_def[THEN sym]]
|
||||
thm while_lfp_invr_vrt_prog_def[THEN sym]
|
||||
unfolding while_lfp_invr_vrt_prog_def
|
||||
|
||||
apply (subst (2) while_lfp_prog_unfold)
|
||||
|
||||
apply (subst If_prog_anti_frame_prog_distr[THEN sym])
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
apply (rule if_prog_monoI)
|
||||
apply (subst seq_prog_anti_frame_prog_distr[THEN sym])
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
defer
|
||||
apply (rule seq_prog_monoI)
|
||||
defer
|
||||
apply (subst (2) while_lfp_prog_unfold)
|
||||
apply (subst If_prog_anti_frame_prog_distr[THEN sym])
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
|
||||
apply (subst seq_prog_anti_frame_prog_distr[THEN sym])
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
defer
|
||||
apply (subst while_lfp_prog_unfold)
|
||||
apply (subst If_prog_anti_frame_prog_distr[THEN sym])
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
|
||||
apply (subst If_blah)
|
||||
apply (rule if_prog_monoI)
|
||||
|
||||
apply (rule seq_prog_monoI)
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_auto
|
||||
|
||||
apply (rule If_prog_refines_prog)
|
||||
apply (rule algebraic_laws_prog.seq_prog_monoI)
|
||||
|
||||
|
||||
|
||||
apply (subst (2) while_lfp_prog_unfold)
|
||||
apply (rule seq_prog_anti_frame_prog_refines)
|
||||
|
||||
thm If_prog_anti_frame_prog_modifies[THEN order.antisym]
|
||||
thm order.antisym[THEN If_prog_anti_frame_prog_modifies]
|
||||
apply (subst antiframe_prog_modifies_while_lfp_scp_prog)
|
||||
apply (subst If_prog_anti_frame_prog_modifies )
|
||||
oops
|
||||
term " \<guillemotleft>hd aa\<guillemotright>"
|
||||
|
||||
|
|
|
|||
|
|
@ -293,6 +293,16 @@ lemma assigns_prog_cond_prog[algebraic_laws_prog]:
|
|||
|
||||
section \<open>Laws for Conditional\<close>
|
||||
|
||||
lemma If_prog_refines_prog:
|
||||
assumes "spec \<sqsubseteq> passert_prog b ; P"
|
||||
assumes "spec \<sqsubseteq> passert_prog (\<not>b) ; Q"
|
||||
shows " spec \<sqsubseteq> IF b THEN P ELSE Q FI"
|
||||
using assms
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_simp
|
||||
apply metis
|
||||
done
|
||||
|
||||
lemma if_prog_pusbst_distr[usubst]:
|
||||
"\<sigma> \<dagger> (IF b THEN P ELSE Q FI) = IF \<sigma> \<dagger> b THEN \<sigma> \<dagger> P ELSE \<sigma> \<dagger> Q FI"
|
||||
by (simp add: prog_rep_eq usubst)
|
||||
|
|
@ -1220,6 +1230,12 @@ lemma If_prog_anti_frame_prog_modifies:
|
|||
shows "g:[IF b THEN P1 ELSE P2 FI] = IF b THEN P1 ELSE P2 FI"
|
||||
by (metis If_prog_anti_frame_prog_distr modifies1 modifies2 vwb_lens)
|
||||
|
||||
lemma assigns_prog_antiframe_prog_modifies:
|
||||
"[g \<mapsto>\<^sub>s \<langle>\<sigma>\<rangle>\<^sub>s g] = \<sigma> \<Longrightarrow>vwb_lens g \<Longrightarrow>g:[\<langle>\<sigma>\<rangle>\<^sub>a] = \<langle>\<sigma>\<rangle>\<^sub>a"
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_simp
|
||||
done
|
||||
|
||||
lemma SKIP_prog_anti_frame_prog_modifies:
|
||||
assumes vwb_lens: "vwb_lens g"
|
||||
shows "g:[SKIP] = SKIP"
|
||||
|
|
@ -1747,6 +1763,7 @@ proof -
|
|||
next
|
||||
case 2
|
||||
then show ?case
|
||||
apply auto[]
|
||||
by (simp add: If_prog_anti_frame_prog_modifies SKIP_prog_anti_frame_prog_modifies
|
||||
antiframe_prog_idemp modifies seq_prog_anti_frame_prog_modifies vwb_lens)
|
||||
qed
|
||||
|
|
@ -1759,7 +1776,7 @@ qed
|
|||
theorem while_lfp_scp_prog_true:
|
||||
"IN G WHILE true DO body OD = (\<mu>\<^bsub>G\<^esub> X \<bullet> body ; X)"
|
||||
unfolding while_lfp_scp_prog_mu_prog if_prog_true ..
|
||||
term "((\<lambda>x. SKIP ; x) (G:[ABORT]))"
|
||||
|
||||
lemma while_lfp_scp_prog_false:
|
||||
"(IN G WHILE false DO body OD) = SKIP"
|
||||
unfolding while_lfp_scp_prog_mu_prog if_prog_false
|
||||
|
|
@ -1792,14 +1809,19 @@ lemma from_until_lfp_scp_prog_def_alt:
|
|||
"IN G FROM init UNTIL b DO body OD = init ; IN G WHILE \<not>b DO body OD"
|
||||
unfolding from_until_lfp_scp_prog_def while_lfp_scp_prog_mu_prog ..
|
||||
|
||||
lemma from_until_lfp_SCP_prog_unfold:
|
||||
lemma from_until_lfp_scp_invr_vrt_prog_def_alt:
|
||||
"IN G FROM init INVAR invar VRT vari UNTIL b DO body OD =
|
||||
init ; IN G INVAR invar VRT vari WHILE \<not>b DO body OD"
|
||||
by (simp add: from_until_lfp_scp_invr_vrt_prog_def from_until_lfp_scp_prog_def_alt
|
||||
while_lfp_scp_invr_vrt_prog_def)
|
||||
|
||||
lemma from_until_lfp_scp_prog_unfold:
|
||||
"vwb_lens G \<Longrightarrow> G:[body] = body \<Longrightarrow>
|
||||
IN G FROM init UNTIL b DO body OD = init ; IF \<not>b THEN body ; IN G WHILE \<not>b DO body OD ELSE SKIP FI"
|
||||
unfolding from_until_lfp_scp_prog_def_alt
|
||||
using while_lfp_scp_prog_unfold[of G body "\<not>b"]
|
||||
by simp
|
||||
|
||||
|
||||
lemma from_until_lfp_scp_prog_true:
|
||||
"IN G FROM init UNTIL true DO body OD = init"
|
||||
unfolding from_until_lfp_scp_prog_def_alt
|
||||
|
|
@ -1815,6 +1837,12 @@ lemma do_while_lfp_scp_prog_def_alt:
|
|||
unfolding do_while_lfp_scp_prog_def from_until_lfp_scp_prog_def_alt
|
||||
by simp
|
||||
|
||||
lemma do_while_lfp_scp_invr_vrt_prog_def_alt:
|
||||
"IN G DO body INVAR invar VRT vari WHILE b OD =
|
||||
body ; IN G INVAR invar VRT vari WHILE b DO body OD"
|
||||
by (simp add: do_while_lfp_scp_invr_vrt_prog_def do_while_lfp_scp_prog_def_alt
|
||||
while_lfp_scp_invr_vrt_prog_def)
|
||||
|
||||
lemma do_while_lfp_scp_prog_unfold:
|
||||
"vwb_lens G \<Longrightarrow> G:[body] = body \<Longrightarrow>
|
||||
IN G DO body WHILE b OD = body ; IF b THEN body; IN G WHILE b DO body OD ELSE SKIP FI"
|
||||
|
|
@ -1827,8 +1855,7 @@ lemma do_while_lfp_scp_prog_false:
|
|||
unfolding do_while_lfp_scp_prog_def_alt
|
||||
by (simp add: while_lfp_scp_prog_false)
|
||||
|
||||
|
||||
lemma do_while_lfp_scp_prog_non_termination:(*should equal abort situation*)
|
||||
lemma do_while_lfp_scp_prog_non_termination:
|
||||
"vwb_lens G \<Longrightarrow> IN G DO SKIP WHILE true OD = G:[ABORT]"
|
||||
unfolding do_while_lfp_scp_prog_def_alt
|
||||
by (simp add: while_lfp_scp_prog_non_termination)
|
||||
|
|
@ -1839,6 +1866,12 @@ lemma for_lfp_scp_prog_def_alt:
|
|||
unfolding for_lfp_scp_prog_def from_until_lfp_scp_prog_def_alt
|
||||
by simp
|
||||
|
||||
lemma for_lfp_scp_invr_vrt_prog_def_alt:
|
||||
"IN G FOR (init, b, incr) INVAR invar VRT vari DO body OD =
|
||||
init ; IN G INVAR invar VRT vari WHILE b DO body ; incr OD"
|
||||
by (simp add: for_lfp_scp_invr_vrt_prog_def for_lfp_scp_prog_def_alt
|
||||
while_lfp_scp_invr_vrt_prog_def)
|
||||
|
||||
lemma for_lfp_scp_prog_unfold:
|
||||
" vwb_lens G \<Longrightarrow> G:[body; incr] = body; incr \<Longrightarrow>
|
||||
IN G FOR (init, b, incr) DO body OD =
|
||||
|
|
|
|||
Loading…
Reference in New Issue