Skip to content

Commit

Permalink
lib: improve corres rules for whileLoop
Browse files Browse the repository at this point in the history 
This generalises the corres rules for whileLoop by allowing the
guards to be predicates of the initial value given to the
whileLoop (written r and r' in these rules), in addition to the state.

Signed-off-by: Michael McInerney <[email protected]>
  • Loading branch information
@michaelmcinerney
michaelmcinerney committed Jun 23, 2023
1 parent e54d727 commit 3d50d01
Showing 1 changed file with 72 additions and 54 deletions.
126 changes: 72 additions & 54 deletions lib/ExtraCorres.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -241,17 +241,19 @@ lemma hoare_from_abs_inv:
lemma in_whileLoop_corres:
assumes body_corres:
"\<And>r r'. rrel r r' \<Longrightarrow>
corres_underlying srel False nf' rrel (P and C r) (P' and C' r') (B r) (B' r')"
and body_inv: "\<And>r. \<lbrace>P and C r\<rbrace> B r \<lbrace>\<lambda>_. P\<rbrace>"
"\<And>r'. \<lbrace>P' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>_. P'\<rbrace>"
and cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P s; P' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
and cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
and result: "(rv', t') \<in> fst (whileLoop C' B' r' s')"
shows "\<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P s \<and> P' s'
and nf: "nf \<Longrightarrow> (\<And>r. no_fail (P r and C r) (B r))"
shows "\<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s'
\<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C B r s) \<and> (t, t') \<in> srel \<and> rrel rv rv')"
apply (rule in_whileLoop_induct[OF result])
apply (force simp: cond whileLoop_def)
apply clarsimp
apply (frule (1) corres_underlyingD2[OF body_corres]; (fastforce simp: cond)?)
apply (frule (1) corres_underlyingD2[OF body_corres];
(fastforce dest: nf simp: cond no_fail_def)?)
apply clarsimp
apply (frule use_valid[OF _ body_inv(1)])
apply (fastforce dest: cond)
Expand All @@ -260,21 +262,21 @@ lemma in_whileLoop_corres:
apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3) dest: cond)
done

lemma corres_whileLoop:
assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P s; P' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
lemma corres_whileLoop_ret:
assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
and body_corres:
"\<And>r r'. rrel r r' \<Longrightarrow>
corres_underlying srel False nf' rrel (P and C r) (P' and C' r') (B r) (B' r')"
and body_inv: "\<And>r. \<lbrace>P and C r\<rbrace> B r \<lbrace>\<lambda>_. P\<rbrace>"
"\<And>r'. \<lbrace>P' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>_. P'\<rbrace>"
corres_underlying srel False nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
and rel: "rrel r r'"
and nf': "\<And>r'. no_fail (P' and C' r') (B' r')"
and termin: "\<And>r' s'. \<lbrakk>P' s'; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'"
shows "corres_underlying srel False nf' rrel P P' (whileLoop C B r) (whileLoop C' B' r')"
and nf': "\<And>r'. no_fail (P' r' and C' r') (B' r')"
and termin: "\<And>r' s'. \<lbrakk>P' r' s'; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'"
shows "corres_underlying srel False nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')"
apply (rule corres_no_failI)
apply (simp add: no_fail_def)
apply (intro impI allI)
apply (erule_tac I="\<lambda>_ s. P' s"
apply (erule_tac I="\<lambda>r' s'. P' r' s'"
and R="{((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s)
\<and> whileLoop_terminates C' B' r s}"
in not_snd_whileLoop)
Expand All @@ -293,82 +295,98 @@ lemma corres_whileLoop:
apply (fastforce intro: assms)
done

lemmas corres_whileLoop =
corres_whileLoop_ret[where P="\<lambda>_. P" for P, where P'="\<lambda>_. P'" for P', simplified]

lemma whileLoop_terminates_cross:
assumes body_corres:
"\<And>r r'. rrel r r' \<Longrightarrow>
corres_underlying srel False nf' rrel (P and C r) (P' and C' r') (B r) (B' r')"
and cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P s; P' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
and body_inv: "\<And>r. \<lbrace>P and C r\<rbrace> B r \<lbrace>\<lambda>_. P\<rbrace>"
"\<And>r'. \<lbrace>P' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>_. P'\<rbrace>"
and abs_termination: "\<And>r s. P s \<Longrightarrow> whileLoop_terminates C B r s"
and ex_abs: "ex_abs_underlying srel P s'"
corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
and cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
and abs_termination: "\<And>r s. (P r s \<and> C r s) \<Longrightarrow> whileLoop_terminates C B r s"
and ex_abs: "ex_abs_underlying srel (P r) s'"
and rrel: "rrel r r'"
and P': "P' s'"
and P': "P' r' s'"
and nf: "nf \<Longrightarrow> (\<And>r. no_fail (P r and C r) (B r))"
shows "whileLoop_terminates C' B' r' s'"
proof -
have helper: "\<And>s. P s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P s \<and> P' s'
\<longrightarrow> whileLoop_terminates C' B' r' s'"
have helper: "\<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s'
\<longrightarrow> whileLoop_terminates C' B' r' s'"
(is "\<And>s. _ \<Longrightarrow> ?I r s")
apply (rule_tac P="?I" in whileLoop_terminates.induct)
apply (fastforce intro: abs_termination)
apply (fastforce simp: whileLoop_terminates.intros dest: cond)
apply (subst whileLoop_terminates.simps)
apply clarsimp
apply (frule (1) corres_underlyingD2[OF body_corres], fastforce+)
apply (frule (1) corres_underlyingD2[OF body_corres], (fastforce dest: nf simp: no_fail_def)+)
apply (fastforce dest: use_valid intro: body_inv)
done

show ?thesis
apply (insert assms helper)
apply (clarsimp simp: ex_abs_underlying_def)
apply (cases "C' r' s'")
apply (fastforce simp: ex_abs_underlying_def)
apply (simp add: whileLoop_terminates.intros(1))
done
qed

lemma corres_whileLoop_abs:
assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P s; P' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
lemma corres_whileLoop_abs_ret:
assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
and body_corres:
"\<And>r r'. rrel r r' \<Longrightarrow>
corres_underlying srel False nf' rrel (P and C r) (P' and C' r') (B r) (B' r')"
and nf: "\<And>r. no_fail (P and C r) (B r)"
corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
and rrel: "rrel r r'"
and rrel2: "\<forall>r'. \<exists>r. rrel r r'"
and body_inv: "\<And>r. \<lbrace>P and C r\<rbrace> B r \<lbrace>\<lambda>_. P\<rbrace>"
"\<And>r'. \<lbrace>P' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>_. P'\<rbrace>"
and abs_termination: "\<And>r s. P s \<Longrightarrow> whileLoop_terminates C B r s"
shows "corres_underlying srel False nf' rrel P P' (whileLoop C B r) (whileLoop C' B' r')"
and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
and abs_termination: "\<And>r s. (P r s \<and> C r s) \<Longrightarrow> whileLoop_terminates C B r s"
and nf: "nf \<Longrightarrow> (\<And>r. no_fail (P r and C r) (B r))"
shows "corres_underlying srel nf nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')"
apply (rule corres_underlyingI)
apply (frule in_whileLoop_corres[OF body_corres body_inv];
(fastforce intro: body_corres body_inv rrel dest: cond))
apply (rule_tac I="\<lambda>rv' s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv rv' \<and> P s \<and> P' s'"
and R="{((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s)
\<and> whileLoop_terminates C' B' r s}"
in not_snd_whileLoop)
(fastforce intro: body_corres body_inv rrel dest: nf cond))
apply (rule_tac I="\<lambda>rv' s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv rv' \<and> P rv s \<and> P' rv' s'"
and R="{((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s)
\<and> whileLoop_terminates C' B' r s}"
in not_snd_whileLoop)
apply (fastforce intro: rrel)
apply (rename_tac conc_r s)
apply (rename_tac s s' conc_r new_s)
apply (clarsimp simp: validNF_def)
apply (rule conjI)
apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?)
apply (prop_tac "\<exists>abs_r. rrel abs_r conc_r")
apply (fastforce simp: rrel2)
apply clarsimp
apply (rule_tac Q="\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r
\<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s"
in hoare_weaken_pre[rotated])
apply clarsimp
apply (rule hoare_ex_pre)
apply (rename_tac abs_r)
apply (rule hoare_weaken_pre)
apply (fastforce intro!: wp_from_corres_u body_inv body_corres)
apply (rule_tac G="rrel abs_r conc_r" in hoare_grab_asm)
apply (wpsimp wp: wp_from_corres_u[OF body_corres] body_inv)
apply (fastforce dest: nf)
apply (fastforce dest: cond)
apply (fastforce simp: valid_def)
apply wpsimp
apply (rule whileLoop_terminates_cross[OF body_corres];
(fastforce dest: cond intro: body_inv abs_termination))
apply (prop_tac "\<exists>abs_r. rrel abs_r conc_r")
apply (fastforce simp: rrel2)
apply clarsimp
apply (rule_tac P="\<lambda>s'. \<exists>s. (s, s') \<in> srel \<and> (P and C abs_r) s \<and> P' s' \<and> C' conc_r s'"
in no_fail_pre)
apply (insert cond body_corres)
apply (fastforce intro: corres_u_nofail simp: pred_conj_def)
apply fastforce
(fastforce dest: nf cond intro: body_inv abs_termination))
apply (rule_tac P="\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r
\<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s"
in no_fail_pre[rotated])
apply fastforce
apply (rule no_fail_ex_pre)
apply (rename_tac abs_r)
apply (rule no_fail_pre)
apply (rule_tac G="rrel abs_r conc_r" in no_fail_grab_asm)
apply (rule corres_u_nofail)
apply (fastforce dest: body_corres)
apply (fastforce dest: nf)
apply (fastforce simp: cond)
apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']])
done

lemmas corres_whileLoop_abs =
corres_whileLoop_abs_ret[where P="\<lambda>_. P" for P, where P'="\<lambda>_. P'" for P', simplified]

text \<open>Some corres_underlying rules for monadic combinators\<close>

Expand Down

0 comments on commit 3d50d01

Please sign in to comment.