Cleanups!
This commit is contained in:
parent
195be89bf9
commit
d3265eb492
|
@ -377,12 +377,12 @@ method vcg_first_goal_preprocessing =
|
|||
|(match conclusion in "_" \<Rightarrow> \<open>fail\<close> -- \<open>fail for any other goal with different syntax\<close>)
|
||||
|
||||
method precondition_strengthening =
|
||||
(match conclusion in "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>rule pre_str_prog_hoare\<close>)
|
||||
(match conclusion in "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>rule pre_weak_prog_hoare\<close>)
|
||||
|(match conclusion in "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>rule pre_str_hoare_rel\<close>)
|
||||
|(match conclusion in "_" \<Rightarrow> \<open>fail\<close> -- \<open>fail for any other goal with different syntax\<close>)
|
||||
|
||||
method postcondition_weakening =
|
||||
(match conclusion in "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>rule post_weak_prog_hoare\<close>)
|
||||
(match conclusion in "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>rule post_str_prog_hoare\<close>)
|
||||
|(match conclusion in "\<lbrace>_\<rbrace>_\<lbrace>_\<rbrace>\<^sub>u" \<Rightarrow> \<open>rule post_weak_hoare_rel\<close>)
|
||||
|(match conclusion in "_" \<Rightarrow> \<open>fail\<close> -- \<open>fail for any other goal with different syntax\<close>)
|
||||
|
||||
|
@ -402,7 +402,7 @@ method hoare_wp_rule_apply_total =
|
|||
|((match conclusion in "\<lbrace>_\<rbrace>_;_\<lbrace>_\<rbrace>\<^sub>P"\<Rightarrow> succeed), rule seq_prog_hoare)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>IF _ THEN _ ELSE _ FI\<lbrace>_\<rbrace>\<^sub>P"\<Rightarrow> succeed), rule cond_prog_hoare_wp)
|
||||
(*Scoping programming construct!*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>g:[_]\<lbrace>_\<rbrace>\<^sub>P" for g \<Rightarrow> succeed),
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>MODIFY g DO _ OD\<lbrace>_\<rbrace>\<^sub>P" for g \<Rightarrow> succeed),
|
||||
rule antiframe_prog_hoare_wp_weak[where g= fst_lens and l= snd_lens]; rule FRAME_TRIPLE_E)
|
||||
(*Special handling for the VCs generated from scoping construct*)
|
||||
|((match conclusion in "FRAME_TRIPLE (g:[_] = _)"for g \<Rightarrow> \<open>succeed\<close>),
|
||||
|
@ -412,7 +412,7 @@ method hoare_wp_rule_apply_total =
|
|||
|((match conclusion in "FRAME_TRIPLE _" \<Rightarrow> \<open>succeed\<close>), (simp only: FRAME_TRIPLE_def))
|
||||
(*Annotated loop patterns for total correctness*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>INVAR _ VRT _ WHILE _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
rule while_invr_vrt_hoare_prog_wp[where R= measure and e = "&\<Sigma>"])
|
||||
rule while_invr_vrt_hoare_prog_wp[where R= measure and st' = "&\<Sigma>"])
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>FOR (_,_,_) INVAR _ VRT _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
subst for_lfp_invar_vrt_prog_def_alt)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>DO _ INVAR _ VRT _ WHILE _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
|
@ -430,7 +430,7 @@ method hoare_wp_rule_apply_total =
|
|||
| (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
|
||||
rule while_scp_invr_vrt_prog_hoare_wp[where st' = "&\<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>),
|
||||
|
@ -506,7 +506,7 @@ method hoare_sp_rule_apply =
|
|||
|((match conclusion in "FRAME_TRIPLE _" \<Rightarrow> \<open>succeed\<close>), (simp only: FRAME_TRIPLE_def))
|
||||
(*Annotated loop patterns for total correctness*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>INVAR _ VRT _ WHILE _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
rule while_invr_vrt_hoare_prog_sp[where R= measure and e = "&\<Sigma>"])
|
||||
rule while_invr_vrt_hoare_prog_sp[where R= measure and st' = "&\<Sigma>"])
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>FOR (_,_,_) INVAR _ VRT _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
subst for_lfp_invar_vrt_prog_def_alt)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>DO _ INVAR _ VRT _ WHILE _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>succeed\<close>),
|
||||
|
@ -796,8 +796,8 @@ method precondition_strengthening_trace =
|
|||
(match conclusion
|
||||
in "\<lbrace>REQUIRES\<rbrace>PROGRAM\<lbrace>ENSURES\<rbrace>\<^sub>P" for REQUIRES PROGRAM ENSURES \<Rightarrow>
|
||||
\<open>print_string \<open>++Application of the INTRO rule:\<close>,
|
||||
print_fact pre_str_prog_hoare,
|
||||
rule pre_str_prog_hoare,
|
||||
print_fact pre_weak_prog_hoare,
|
||||
rule pre_weak_prog_hoare,
|
||||
print_string \<open>==================================================\<close>,
|
||||
print_string \<open>====End of the Preprocessing of the First Goal====\<close>,
|
||||
print_string \<open>==================================================\<close>\<close>)
|
||||
|
@ -852,8 +852,7 @@ 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]\<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 process for the VCs of the frame rule-->>\<close>,
|
||||
|
@ -873,11 +872,11 @@ method hoare_wp_rule_apply_trace =
|
|||
(simp only: FRAME_TRIPLE_def),
|
||||
print_string \<open><<--FRAME RULE: VCG ends removing the TAG for the normale VCs-->>\<close>)
|
||||
(*Annotated loop patterns for total correctness*)
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>INVAR invar VRT vari WHILE b DO _ OD\<lbrace>Q\<rbrace>\<^sub>P" for invar vari b Q \<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
|
||||
|((match conclusion in "\<lbrace>_\<rbrace>INVAR invar VRT vari WHILE b DO _ OD\<lbrace>Q\<rbrace>\<^sub>P" for invar vari b Q \<Rightarrow> \<open>succeed\<close>),
|
||||
(print_fact while_invr_vrt_hoare_prog_wp[where st' = "&\<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 R= measure and e = "&\<Sigma>"]))
|
||||
rule while_invr_vrt_hoare_prog_wp[where R= measure and st' = "&\<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>succeed\<close>),
|
||||
print_fact
|
||||
|
@ -893,7 +892,7 @@ method hoare_wp_rule_apply_trace =
|
|||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>FROM init INVAR invar VRT vari UNTIL b DO body OD\<lbrace>_\<rbrace>\<^sub>P" for init invar vari b body \<Rightarrow> \<open>succeed\<close>),
|
||||
print_fact from_until_lfp_invr_vrt_prog_def_alt[where b = b and body = body and
|
||||
vari = vari and invar = invar],
|
||||
vari = vari and invar = invar],
|
||||
subst from_until_lfp_invr_vrt_prog_def_alt)
|
||||
(*Non-annotated loop patterns fail the VCG... which requires a proof annotation *)
|
||||
| (match conclusion in "\<lbrace>_\<rbrace>INVAR _ WHILE _ DO _ OD\<lbrace>_\<rbrace>\<^sub>P" \<Rightarrow> \<open>fail\<close>),
|
||||
|
@ -915,8 +914,8 @@ method hoare_wp_rule_apply_trace =
|
|||
(*Annotated SCOPED loop patterns for total correctness*)
|
||||
|((match conclusion in
|
||||
"\<lbrace>_\<rbrace>IN G INVAR invar VRT vari WHILE b DO body OD\<lbrace>Q\<rbrace>\<^sub>P" for G invar vari b body Q \<Rightarrow> \<open>succeed\<close>),
|
||||
rule while_scp_invr_vrt_prog_hoare_wp[where e = "&\<Sigma>" and R = measure and
|
||||
q = Q and invar = invar and
|
||||
rule while_scp_invr_vrt_prog_hoare_wp[where st' = "&\<Sigma>" and R = measure and
|
||||
Q = Q and invar = invar and
|
||||
expression = vari and
|
||||
b = b and
|
||||
g = fst_lens and l = snd_lens];
|
||||
|
|
|
@ -812,7 +812,7 @@ lemma blah':
|
|||
OD
|
||||
\<lbrace> (\<lambda>(aa). ((&r:fst_lens) =\<^sub>uuop Max (uop set \<guillemotleft>aa\<guillemotright>)))\<rbrace>\<^sub>G"
|
||||
apply (insert assms)
|
||||
apply ( vcg wp)
|
||||
apply (vcg wp)
|
||||
subgoal for _
|
||||
by (cases a; auto)
|
||||
defer
|
||||
|
@ -863,7 +863,7 @@ lemma
|
|||
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). {&i:fst_lens, &r:fst_lens}:[
|
||||
\<lambda>(aa). MODIFY i ;\<^sub>L fst_lens +\<^sub>L r ;\<^sub>Lfst_lens DO
|
||||
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>)))
|
||||
|
@ -874,13 +874,16 @@ lemma
|
|||
ELSE SKIP
|
||||
FI;
|
||||
(i:fst_lens) :== ((&i:fst_lens) + \<guillemotleft>1\<guillemotright>)
|
||||
OD]
|
||||
OD
|
||||
OD
|
||||
\<lbrace>\<lambda>(aa). (&r:fst_lens) =\<^sub>uuop Max (uop set \<guillemotleft>aa\<guillemotright>)\<rbrace>\<^sub>G"
|
||||
apply (insert assms)
|
||||
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_def while_lfp_scp_invr_vrt_prog_def
|
||||
|
||||
unfolding DONT_TOUCH_def while_lfp_scp_invr_vrt_prog_def
|
||||
thm modifies_indep
|
||||
apply (subst modifies_indep)
|
||||
(**)
|
||||
apply (simp add: assms(1) assms(2) assms(3) lens_indep_sym plus_vwb_lens)
|
||||
|
|
|
@ -487,7 +487,7 @@ lemma EXAMPLE_vcg_step_by_step_proof_annotation:
|
|||
apply (hoare_wp_rule_apply)
|
||||
apply (hoare_wp_rule_apply)
|
||||
apply (hoare_wp_rule_apply)
|
||||
apply (rule while_hoare_prog_wp[where R= measure and e = "&\<Sigma>" and
|
||||
apply (rule while_hoare_prog_wp[where R= measure and st' = "&\<Sigma>" and
|
||||
invar = "utp_expr.var r >\<^sub>u0 \<and> utp_expr.var x >\<^sub>u 0 \<and>
|
||||
bop gcd (utp_expr.var r) (utp_expr.var x) =\<^sub>u bop gcd \<guillemotleft>a\<guillemotright> \<guillemotleft>b\<guillemotright>" and
|
||||
expression = "uop nat (bop max (utp_expr.var r) (utp_expr.var x))"])
|
||||
|
|
|
@ -1480,7 +1480,7 @@ lemma modifies_indep':
|
|||
done
|
||||
|
||||
lemma modifies_indep:
|
||||
"vwb_lens G \<Longrightarrow> vwb_lens l \<Longrightarrow> G \<bowtie> l \<Longrightarrow> G:[P] = P \<Longrightarrow> {&G, &l}:[P] = P"
|
||||
"vwb_lens G \<Longrightarrow> vwb_lens l \<Longrightarrow> G \<bowtie> l \<Longrightarrow> G:[P] = P \<Longrightarrow> MODIFY G +\<^sub>L l DO P OD = P"
|
||||
unfolding pr_var_def
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_auto
|
||||
|
|
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue