Adding messages for the VCG debugger + regression tests on the examples + modifying the way of dealing with variables when modularity is used in the reasonning
This commit is contained in:
parent
f6b160a674
commit
332b6d7d6d
|
@ -848,13 +848,13 @@ method hoare_wp_rule_apply_trace =
|
|||
(*Scoping programming construct!*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>g:[_]\<lbrace>Q\<rbrace>\<^sub>P" for g Q \<Rightarrow>
|
||||
\<open>print_string \<open><||||>--FRAME RULE: VCG starts applying FRAME RULE--<||||>\<close>,
|
||||
print_fact antiframe_prog_hoare_wp_weak[where g = fst_lens and l= snd_lens and
|
||||
g'= "g;\<^sub>L fst_lens" and r = "\<lceil>Q\<rceil>\<^sub><"]\<close>),
|
||||
print_fact antiframe_prog_hoare_wp_weak[where g = fst_lens and l= snd_lens (*and
|
||||
g'= "g;\<^sub>L fst_lens" and r = "\<lceil>Q\<rceil>\<^sub><"*)]\<close>),
|
||||
(rule antiframe_prog_hoare_wp_weak[where g= fst_lens and l= snd_lens]);
|
||||
(print_string \<open><||||>--FRAME RULE: VCG ends applying FRAME RULE--<||||>\<close>,
|
||||
print_string \<open><<--FRAME RULE: VCG starts the TAG precess for the VCs of the frame rule-->>\<close>,
|
||||
print_string \<open><<--FRAME RULE: VCG starts the TAG process for the VCs of the frame rule-->>\<close>,
|
||||
(rule FRAME_TRIPLE_E),
|
||||
print_string \<open><<--FRAME RULE: VCG ends the TAG precess for the VCs of the frame rule-->>\<close>))
|
||||
print_string \<open><<--FRAME RULE: VCG ends the TAG process for the VCs of the frame rule-->>\<close>))
|
||||
(*Special handling for the VCs generated from scoping construct*)
|
||||
|((match conclusion in "FRAME_TRIPLE (g:[_] = _)"for g \<Rightarrow> \<open>succeed\<close>),
|
||||
print_string \<open><<--FRAME RULE: VCG starts changing the TAG for the MODIFIES condition-->>\<close>,
|
||||
|
@ -914,24 +914,30 @@ method hoare_wp_rule_apply_trace =
|
|||
rule while_scp_invr_vrt_prog_hoare_wp[where e = "&\<Sigma>" and R = measure and
|
||||
q = Q and invar = invar and
|
||||
expression = vari and
|
||||
b = b and G = "G;\<^sub>L fst_lens" and
|
||||
b = b 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>),
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>IN G FOR (init,b,incr) INVAR invar VRT vari DO body OD\<lbrace>_\<rbrace>\<^sub>P" for G init b incr invar vari body \<Rightarrow> \<open>succeed\<close>),
|
||||
print_fact
|
||||
for_lfp_scp_invr_vrt_prog_def_alt [where init = init and b = b and
|
||||
incr = incr and body = body and
|
||||
vari= vari and invar = invar],
|
||||
for_lfp_scp_invr_vrt_prog_def_alt [where G = "G;\<^sub>L fst_lens" and
|
||||
init = init and b = b and incr = incr and
|
||||
body = body and vari= vari and invar = invar],
|
||||
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>),
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>IN G DO body INVAR invar VRT vari WHILE b OD\<lbrace>_\<rbrace>\<^sub>P" for G body invar vari b \<Rightarrow> \<open>succeed\<close>),
|
||||
print_fact
|
||||
for_lfp_scp_invr_vrt_prog_def_alt[where b = b and body = body and
|
||||
vari = vari and invar = invar],
|
||||
for_lfp_scp_invr_vrt_prog_def_alt[where G = "G;\<^sub>L fst_lens" and
|
||||
b = b and body = body and
|
||||
vari = vari and invar = invar],
|
||||
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>),
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>IN G FROM init INVAR invar VRT vari UNTIL b DO body OD\<lbrace>_\<rbrace>\<^sub>P" for G init invar vari b body \<Rightarrow> \<open>succeed\<close>),
|
||||
print_fact
|
||||
from_until_lfp_scp_invr_vrt_prog_def_alt[where b = b and body = body and
|
||||
vari = vari and invar = invar],
|
||||
from_until_lfp_scp_invr_vrt_prog_def_alt[where G = "G;\<^sub>L fst_lens" and
|
||||
b = b and body = body and
|
||||
vari = vari and invar = invar and
|
||||
init = init],
|
||||
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>),
|
||||
|
@ -951,10 +957,14 @@ method hoare_wp_rule_apply_trace =
|
|||
| (match conclusion in "\<lbrace>_\<rbrace>IN _ FROM _ UNTIL _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>),
|
||||
print_string \<open>Non-Annotated loop: This loop is not annotated a variant and invariant are missing\<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)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>_;;_\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>succeed\<close>), rule seq_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>if\<^sub>u _ then _ else _\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>succeed\<close>), rule cond_hoare_rel_wp)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>a\<lbrace>Q\<rbrace>\<^sub>u" for \<sigma> Q \<Rightarrow> \<open>succeed\<close>),
|
||||
print_fact assigns_backward_hoare_rel[where \<sigma> = \<sigma> and p = Q],
|
||||
rule assigns_backward_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>SKIP\<^sub>r\<lbrace>Q\<rbrace>\<^sub>u" for Q \<Rightarrow> \<open>succeed\<close>), print_fact skip_hoare_rel[where p = Q], rule skip_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>_;;_\<lbrace>Q\<rbrace>\<^sub>u"for Q \<Rightarrow> \<open>succeed\<close>), print_fact seq_hoare_rel[where r = Q], rule seq_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>if\<^sub>u b then _ else _\<lbrace>Q\<rbrace>\<^sub>u" for b Q \<Rightarrow> \<open>succeed\<close>),
|
||||
print_fact cond_hoare_rel_wp [where b = b and q = Q],rule cond_hoare_rel_wp)
|
||||
(*CONTINUE FROM HERE!! ADDING DEBUG MESSAGES TO HOARE CONSTRUCTS IN PARTIAL CORRECTNESS!!*)
|
||||
(*Scoping programming construct for relations!*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>antiframe _ _\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>succeed\<close>), rule cond_hoare_rel_wp; rule FRAME_TRIPLE_E)
|
||||
(*Special handling for the VCs generated from scoping construct*)
|
||||
|
@ -982,106 +992,14 @@ method hoare_wp_rule_apply_trace =
|
|||
--{*For any goal which is not a Hoare triple*}
|
||||
|((match conclusion in "_" \<Rightarrow> \<open>succeed\<close>), vcg_defer)
|
||||
|
||||
(*method wp_trace = hoare_wp_vcg_preprocessing, hoare_wp_rule_apply+, (unfold DEFERRED_def)*)
|
||||
method hoare_wp_rule_apply_trace' =
|
||||
--\<open>WP Matching rules for total correctness\<close>
|
||||
((match conclusion in "\<lbrace>_\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>p\<lbrace>Q\<rbrace>\<^sub>P" for Q \<sigma> \<Rightarrow>
|
||||
\<open>print_fact assigns_prog_hoare_backward[where \<sigma> = \<sigma> and p = Q]\<close>),
|
||||
rule assigns_prog_hoare_backward)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>SKIP\<lbrace>Q\<rbrace>\<^sub>P" for Q \<Rightarrow> \<open>print_fact skip_prog_hoare[where p = Q]\<close>), rule skip_prog_hoare)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>_;_\<lbrace>Q\<rbrace>\<^sub>P" for Q \<Rightarrow> \<open>print_fact seq_prog_hoare[where r = Q]\<close>), rule seq_prog_hoare)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>IF b THEN _ ELSE _ FI\<lbrace>Q\<rbrace>\<^sub>P" for b Q \<Rightarrow>
|
||||
\<open>print_fact cond_prog_hoare_wp [where b = b and q = Q]\<close>),
|
||||
rule cond_prog_hoare_wp)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>g:[PROG]\<lbrace>Q\<rbrace>\<^sub>P" for g Q PROG \<Rightarrow>
|
||||
\<open>print_fact antiframe_prog_hoare_wp_weak[where g = fst_lens and l= snd_lens and
|
||||
g' = "g;\<^sub>L fst_lens" and r = "\<lceil>Q\<rceil>\<^sub><"]\<close>),
|
||||
rule antiframe_prog_hoare_wp_weak[where g= fst_lens and l= snd_lens]; rule FRAME_TRIPLE_E)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>INVAR invar VRT vari WHILE b DO body OD\<lbrace>Q\<rbrace>\<^sub>P" for Q invar vari b body \<Rightarrow>
|
||||
\<open>succeed\<close>), (print_fact while_invr_vrt_hoare_prog_wp[where e = "&\<Sigma>" and R= measure and
|
||||
q= Q and b = b and invar= invar and
|
||||
expression = vari and body = body],
|
||||
rule while_invr_vrt_hoare_prog_wp[where e = "&\<Sigma>" and R= measure]))
|
||||
(*|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>VRT vari INVAR invar WHILE b DO body OD\<lbrace>_\<rbrace>\<^sub>P" for invar vari b body \<Rightarrow>
|
||||
\<open>print_fact while_vrt_invr_hoare_prog_wp[where e = "&\<Sigma>"]\<close>),
|
||||
rule while_vrt_invr_hoare_prog_wp[where e = "&\<Sigma>"])*)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>FOR (init,b,incr) INVAR invar VRT vari DO body OD\<lbrace>_\<rbrace>\<^sub>P" for init b incr invar vari body \<Rightarrow>
|
||||
\<open>print_fact for_lfp_invar_vrt_prog_def_alt[where init = init and b = b and incr = incr and
|
||||
body = body and vari= vari and invar = invar]\<close>),
|
||||
(subst for_lfp_invar_vrt_prog_def_alt))
|
||||
(*|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>FOR (init,b,incr) VRT vari INVAR invar DO body OD\<lbrace>_\<rbrace>\<^sub>P" for init b incr invar vari body \<Rightarrow>
|
||||
\<open>print_fact for_vrt_invr_hoare_prog_wp[where e = "&\<Sigma>"]\<close>),
|
||||
rule for_vrt_invr_hoare_prog_wp[where e = "&\<Sigma>"])*)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>DO body INVAR invar VRT vari WHILE b OD\<lbrace>_\<rbrace>\<^sub>P" for body invar vari b \<Rightarrow>
|
||||
\<open>print_fact do_while_invar_vrt_lfp_prog_def_alt[where b = b and body = body and
|
||||
vari = vari and invar = invar]\<close>),
|
||||
subst do_while_invar_vrt_lfp_prog_def_alt)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>FROM init INVAR invar VRT vari UNTIL exit DO body OD\<lbrace>_\<rbrace>\<^sub>P" for init invar vari body exit \<Rightarrow>
|
||||
\<open>print_fact from_until_lfp_invr_vrt_prog_def_alt[where b = b and body = body and
|
||||
vari = vari and invar = invar]\<close>),
|
||||
subst from_until_lfp_invr_vrt_prog_def_alt)
|
||||
|((match conclusion in "FRAME_TRIPLE (g:[PROG] = PROG)" for g PROG \<Rightarrow> \<open>succeed\<close>),
|
||||
print_string \<open><<--Start processing the modifies condition-->>\<close>,
|
||||
(simp only: FRAME_TRIPLE_def), (rule DONT_TOUCH_E),
|
||||
print_string \<open><<--End processing the modifies condition-->>\<close>)
|
||||
|((match conclusion in "FRAME_TRIPLE \<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
print_string \<open>|||||||--Start Applying Already Proved Specs--|||||||\<close>,
|
||||
(simp only: FRAME_TRIPLE_def, rule vcg_proved_specs),
|
||||
print_string \<open>|||||||--End Applying Already Proved Specs--|||||||\<close>)
|
||||
(*TODO: add the cases where the loops are not annotated*)
|
||||
|
||||
--\<open>WP Matching rules for partial correctness\<close>
|
||||
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>\<langle>\<sigma>\<rangle>\<^sub>a\<lbrace>Q\<rbrace>\<^sub>u" for Q \<sigma> \<Rightarrow>
|
||||
\<open>print_fact assisgns_true_hoare_rel[where \<sigma> = \<sigma> and p = Q]\<close>), rule assigns_backward_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>SKIP\<^sub>r\<lbrace>Q\<rbrace>\<^sub>u" for Q \<Rightarrow> \<open>print_fact skip_hoare_rel[where p = Q]\<close>), rule skip_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>_;;_\<lbrace>Q\<rbrace>\<^sub>u" for Q \<Rightarrow> \<open>print_fact seq_hoare_rel[where r = Q]\<close>), rule seq_hoare_rel)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>if\<^sub>u b then _ else _ \<lbrace>Q\<rbrace>\<^sub>u" for b Q \<Rightarrow>
|
||||
\<open>print_fact cond_hoare_rel_wp[where b = b and q = Q]\<close>), rule cond_hoare_rel_wp)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>antiframe g _\<lbrace>Q\<rbrace>\<^sub>u" for g Q \<Rightarrow>
|
||||
\<open>print_fact antiframe_hoare_rel_wp[where g = fst_lens and l= snd_lens and
|
||||
g' = "g;\<^sub>L fst_lens" and r = "\<lceil>Q\<rceil>\<^sub><"]\<close>),
|
||||
rule antiframe_hoare_rel_wp)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>invr invar while\<^sup>\<top> b do _ od\<lbrace>Q\<rbrace>\<^sub>u" for invar b Q \<Rightarrow>
|
||||
\<open>print_fact while_gfp_invr_hoare_rel_wp_partial[where invar = invar and q=Q and b =b]\<close>),
|
||||
rule while_gfp_invr_hoare_rel_wp_partial)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>do body invr invar while\<^sup>\<top> b od\<lbrace>_\<rbrace>\<^sub>u" for body b invar \<Rightarrow>
|
||||
\<open>print_fact do_while_invar_vrt_gfp_rel_def_alt[where b =b and invar = invar]\<close>),
|
||||
subst do_while_invar_vrt_gfp_rel_def_alt)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>for\<^sup>\<top> (init, b, incr) invr invar do _ od\<lbrace>_\<rbrace>\<^sub>u" for init b incr invar \<Rightarrow>
|
||||
\<open>print_fact for_gfp_invar_vrt_rel_def_alt[where init=init and b=b and incr = incr and invar =invar]\<close>),
|
||||
subst for_gfp_invar_vrt_rel_def_alt)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>from\<^sup>\<top> init invr invar until exit do _ od\<lbrace>_\<rbrace>\<^sub>u" for init invar exit \<Rightarrow>
|
||||
\<open>print_fact from_until_gfp_invr_vrt_rel_def_alt\<close>),
|
||||
subst from_until_gfp_invr_vrt_rel_def_alt)
|
||||
|(match conclusion in
|
||||
"\<lbrace>_\<rbrace>invr _ vrt _ while\<^sub>\<bottom> _ do _ od\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow>
|
||||
\<open>print_error \<open>ERROR: this is relational paradigm! For total correctness use the lifted theory of designs\<close>,fail\<close>)
|
||||
|((match conclusion in "FRAME_TRIPLE _" \<Rightarrow> \<open>succeed\<close>),
|
||||
(simp only: FRAME_TRIPLE_def))
|
||||
|((match conclusion in "_" \<Rightarrow> \<open>succeed\<close>),vcg_defer_trace)
|
||||
|
||||
|
||||
method wp_trace' =
|
||||
method wp_trace =
|
||||
vcg_pre_processing_print_method wp_mode_print_method-- \<open>Printing useful information on the VCG\<close>,
|
||||
hoare_wp_vcg_preprocessing_trace,
|
||||
print_string \<open>+++++++++++++++++++++++++++++++++++++++++++++++\<close>,
|
||||
print_string \<open>++++Begin Application of Hoare Logic Rules+++++\<close>,
|
||||
print_string \<open>+++++++++++++++++++++++++++++++++++++++++++++++\<close>,
|
||||
hoare_wp_rule_apply_trace'+,
|
||||
hoare_wp_rule_apply_trace+,
|
||||
print_string \<open>+++++++++++++++++++++++++++++++++++++++++++++++\<close>,
|
||||
print_string \<open>++++End of Application of Hoare Logic Rules++++\<close>,
|
||||
print_string \<open>+++++++++++++++++++++++++++++++++++++++++++++++\<close>,
|
||||
|
|
|
@ -597,54 +597,58 @@ lemma max_program_correct_wp_rel:
|
|||
done
|
||||
|
||||
section \<open>Modular reasoning\<close>
|
||||
|
||||
abbreviation
|
||||
"swaping a j \<equiv> (((a:fst_lens) :== (trop swap (\<guillemotleft>j\<guillemotright>) (\<guillemotleft>j\<guillemotright>-1) \<lceil>&a\<rceil>\<^sub><))::_ prog)"
|
||||
"swaping a j \<equiv> ((a :== (trop swap (\<guillemotleft>j\<guillemotright>) (\<guillemotleft>j\<guillemotright>-1) (&a)))::_ prog)"
|
||||
|
||||
lemma swap_preserves_list:
|
||||
assumes "vwb_lens a"
|
||||
shows
|
||||
"\<lbrace>\<lambda>aa. ((&a:fst_lens) =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and>\<guillemotleft>j\<guillemotright> <\<^sub>u uop length \<guillemotleft>aa\<guillemotright>)\<rbrace>
|
||||
"\<lbrace>\<lambda>aa. ((&a) =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and>\<guillemotleft>j\<guillemotright> <\<^sub>u uop length \<guillemotleft>aa\<guillemotright>)\<rbrace>
|
||||
\<lambda>aa. swaping a j
|
||||
\<lbrace>\<lambda>aa. (mset\<^sub>u((&a:fst_lens)) =\<^sub>u mset\<^sub>u(\<guillemotleft>aa\<guillemotright>))\<rbrace>\<^sub>G"
|
||||
\<lbrace>\<lambda>aa. (mset\<^sub>u((&a)) =\<^sub>u mset\<^sub>u(\<guillemotleft>aa\<guillemotright>))\<rbrace>\<^sub>G"
|
||||
by (insert assms, rule allI,vcg wp)
|
||||
|
||||
(*declare swap_preserves_list[THEN spec, vcg_proved_specs]*)
|
||||
lemmas swap_preserves_list' =
|
||||
swap_preserves_list[simplified, THEN spec, vcg_proved_specs]
|
||||
lemma
|
||||
(*we add 2 massaging of the same proved spec to the VCG since depending on the situation
|
||||
the VCG may use one or another. Namely, there is a unification problem that needs to be solved*)
|
||||
|
||||
declare swap_preserves_list[THEN spec, vcg_proved_specs]
|
||||
declare swap_preserves_list[simplified, THEN spec, vcg_proved_specs]
|
||||
|
||||
lemma swap_preserves_list_test:
|
||||
assumes "vwb_lens a"
|
||||
assumes "vwb_lens b"
|
||||
assumes "a \<bowtie> b"
|
||||
shows
|
||||
"\<lbrace>\<lambda>aa. ((&a:fst_lens) =\<^sub>u \<guillemotleft>aa\<guillemotright> \<and>\<guillemotleft>j\<guillemotright> <\<^sub>u uop length \<guillemotleft>aa\<guillemotright>)\<rbrace>
|
||||
\<lambda>aa. (&a:fst_lens):[swaping a j];
|
||||
(b:snd_lens):== (\<guillemotleft>0\<guillemotright>)
|
||||
\<lbrace>\<lambda>aa. (mset\<^sub>u((&a:fst_lens)) =\<^sub>u mset\<^sub>u(\<guillemotleft>aa\<guillemotright>))\<rbrace>\<^sub>G"
|
||||
\<lambda>aa. (&a:fst_lens):[swaping (a;\<^sub>L fst_lens) j];
|
||||
(b:fst_lens):== (\<guillemotleft>0\<guillemotright>)
|
||||
\<lbrace>\<lambda>aa. (mset\<^sub>u(&a:fst_lens) =\<^sub>u mset\<^sub>u(\<guillemotleft>aa\<guillemotright>))\<rbrace>\<^sub>G"
|
||||
apply (insert assms)
|
||||
apply (vcg wp_trace')
|
||||
(*additional post-processing for proving VCs related to the modify assumption
|
||||
TODO: automate this*)
|
||||
apply (vcg wp_trace)
|
||||
apply (insert assms)
|
||||
apply (simp_all add: DONT_TOUCH_def prog_rep_eq)
|
||||
apply rel_auto+
|
||||
done
|
||||
|
||||
abbreviation
|
||||
"count_down j \<equiv> ((j :== ((&j) - \<guillemotleft>1\<guillemotright>))::_ prog)"
|
||||
|
||||
lemma count_down_preserves_list:
|
||||
assumes "vwb_lens j"
|
||||
shows
|
||||
"\<lbrace>\<lambda>n. (&j:fst_lens) =\<^sub>u \<guillemotleft>n::nat\<guillemotright> \<and> (&j:fst_lens) \<noteq>\<^sub>u \<guillemotleft>0::nat\<guillemotright>\<rbrace>
|
||||
\<lambda>aa. (j:fst_lens) :== ((&j:fst_lens) - \<guillemotleft>1\<guillemotright>)
|
||||
\<lbrace>\<lambda>n. (&j:fst_lens) \<le>\<^sub>u \<guillemotleft>n\<guillemotright>\<rbrace>\<^sub>G"
|
||||
"\<lbrace>\<lambda>n. (&j) =\<^sub>u \<guillemotleft>n::nat\<guillemotright> \<and> (&j) \<noteq>\<^sub>u \<guillemotleft>0::nat\<guillemotright>\<rbrace>
|
||||
\<lambda>aa. count_down j
|
||||
\<lbrace>\<lambda>n. (&j) \<le>\<^sub>u \<guillemotleft>n\<guillemotright>\<rbrace>\<^sub>G"
|
||||
by (insert assms, rule allI, vcg wp)
|
||||
|
||||
declare count_down_preserves_list[THEN spec, vcg_proved_specs]
|
||||
lemmas count_down_preserves_list' =
|
||||
count_down_preserves_list[simplified,THEN spec, vcg_proved_specs]
|
||||
declare count_down_preserves_list[ THEN spec, vcg_proved_specs]
|
||||
declare count_down_preserves_list[simplified,THEN spec, vcg_proved_specs]
|
||||
|
||||
lemma count_down_preserves_list_test:
|
||||
assumes "vwb_lens j"
|
||||
shows
|
||||
"\<lbrace>\<lambda>n. (&j:fst_lens) =\<^sub>u \<guillemotleft>n::nat\<guillemotright> \<and> (&j:fst_lens) \<noteq>\<^sub>u \<guillemotleft>0::nat\<guillemotright>\<rbrace>
|
||||
\<lambda>aa. (&j:fst_lens):[(j:fst_lens) :== ((&j:fst_lens) - \<guillemotleft>1\<guillemotright>)]
|
||||
\<lambda>aa. (&j:fst_lens):[count_down (j;\<^sub>Lfst_lens)]
|
||||
\<lbrace>\<lambda>n. (&j:fst_lens) \<le>\<^sub>u \<guillemotleft>n\<guillemotright>\<rbrace>\<^sub>G"
|
||||
apply (insert assms)
|
||||
apply (vcg wp)
|
||||
|
|
|
@ -1452,6 +1452,16 @@ lemma mu_scp_antiframe_modifies[closure]:
|
|||
apply (simp_all add: assms mu_scp_antiframe_refinedBy mu_scp_antiframe_refines)
|
||||
done
|
||||
|
||||
lemma modifies_indep':
|
||||
"vwb_lens G \<Longrightarrow> vwb_lens l \<Longrightarrow> G \<bowtie> l \<Longrightarrow> G:[P] = P \<Longrightarrow> {&G, &l}:[P] = G:[P]"
|
||||
unfolding pr_var_def
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_auto
|
||||
unfolding lens_indep_def
|
||||
apply simp
|
||||
apply (metis lens_override_def lens_override_idem)+
|
||||
done
|
||||
|
||||
lemma modifies_indep:
|
||||
"vwb_lens G \<Longrightarrow> vwb_lens l \<Longrightarrow> G \<bowtie> l \<Longrightarrow> G:[P] = P \<Longrightarrow> {&G, &l}:[P] = P"
|
||||
unfolding pr_var_def
|
||||
|
|
|
@ -569,25 +569,7 @@ proof -
|
|||
apply rel_simp
|
||||
done
|
||||
qed
|
||||
lemma
|
||||
"vwb_lens G \<Longrightarrow> vwb_lens l \<Longrightarrow> G \<bowtie> l \<Longrightarrow> {&G, &l}:[P] = G:[P]"
|
||||
|
||||
unfolding pr_var_def
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_auto
|
||||
unfolding lens_indep_def
|
||||
apply simp
|
||||
sledgehammer
|
||||
oops
|
||||
lemma "vwb_lens g \<Longrightarrow> vwb_lens g' \<Longrightarrow> vwb_lens l \<Longrightarrow>g \<bowtie> l \<Longrightarrow> g' \<subseteq>\<^sub>L g \<Longrightarrow> g':[P] = {&g',&l}:[P]"
|
||||
apply auto[]
|
||||
apply (subst (asm) Pi_iff)
|
||||
apply auto[]
|
||||
thm modifies_indep
|
||||
apply (rule modifies_indep)
|
||||
using lens_indep_g_l region sublens_pres_indep apply auto[1]
|
||||
apply auto[]
|
||||
oops
|
||||
lemma lfp_scp_prog_wf_region_refine_intro_strong:
|
||||
assumes vwb_lens1: "vwb_lens g"
|
||||
assumes vwb_lens2: "vwb_lens G"
|
||||
|
|
Loading…
Reference in New Issue