Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improve corres rules whileLoop #650

Merged
merged 2 commits into from
Oct 5, 2023
Merged

Improve corres rules whileLoop #650

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
02c2914
lib/monads: add no_fail_ex_lift and no_fail_grab_asm
michaelmcinerney Oct 5, 2023
7170ef1
lib: improve corres_underlying rules for whileLoop
michaelmcinerney Oct 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
140 changes: 80 additions & 60 deletions lib/ExtraCorres.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,17 +254,20 @@ 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'"
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'
corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
assumes body_inv:
"\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
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'"
assumes result: "(rv', t') \<in> fst (whileLoop C' B' r' s')"
assumes nf: "\<And>r. nf \<Longrightarrow> 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 @@ -273,21 +276,22 @@ 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'"
and body_corres:
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'"
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 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')"
corres_underlying srel False nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
assumes body_inv:
"\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
assumes rel: "rrel r r'"
assumes nf': "\<And>r'. no_fail (P' r' and C' r') (B' r')"
assumes 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 @@ -306,82 +310,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'"
and rrel: "rrel r r'"
and P': "P' s'"
corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
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'"
assumes body_inv:
"\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
assumes abs_termination: "\<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s"
assumes ex_abs: "ex_abs_underlying srel (P r) s'"
assumes rrel: "rrel r r'"
assumes P': "P' r' s'"
assumes nf: "\<And>r. nf \<Longrightarrow> 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'
michaelmcinerney marked this conversation as resolved.
Show resolved Hide resolved
\<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))
michaelmcinerney marked this conversation as resolved.
Show resolved Hide resolved
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'"
and body_corres:
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'"
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 nf: "\<And>r. no_fail (P and C 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')"
corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
assumes rrel: "rrel r r'"
assumes body_inv:
"\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
"\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
assumes abs_termination: "\<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s"
assumes nf: "\<And>r. nf \<Longrightarrow> 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_lift)
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 (fastforce intro: corres_u_nofail dest: body_corres nf)
apply (fastforce simp: cond)
apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']])
done

lemmas corres_whileLoop_abs =
michaelmcinerney marked this conversation as resolved.
Show resolved Hide resolved
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
8 changes: 8 additions & 0 deletions lib/Monads/nondet/Nondet_No_Fail.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,4 +225,12 @@ lemma no_fail_condition:
unfolding condition_def no_fail_def
by clarsimp

lemma no_fail_ex_lift:
"(\<And>x. no_fail (P x) f) \<Longrightarrow> no_fail (\<lambda>s. \<exists>x. P x s) f"
by (clarsimp simp: no_fail_def)

lemma no_fail_grab_asm:
"(G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f"
by (cases G, simp+)

end