monads/reader_option: add ostate_assert

This adds ostate_assert and ohaskell_state_assert, which are versions of state_assert/stateAssert for the reader monad. Also adds several rules for basic reasoning about these functions. Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jul 11, 2024 · 5d78cd7 · 5d78cd7
1 parent 9646d32
commit 5d78cd7
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 18 deletions.
diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy
@@ -548,6 +548,9 @@ lemma gets_the_ohaskell_assert:
   "gets_the (ohaskell_assert P []) = assert P"
   by (clarsimp simp: ohaskell_assert_def split: if_splits)
 
-lemmas omonad_defs = omonad_defs ohaskell_assert_def ohaskell_fail_def
+definition ohaskell_state_assert :: "('s \<Rightarrow> bool) \<Rightarrow> unit list \<Rightarrow> ('s, unit) lookup" where
+  "ohaskell_state_assert P L \<equiv> ostate_assert P"
+
+lemmas omonad_defs = omonad_defs ohaskell_assert_def ohaskell_state_assert_def ohaskell_fail_def
 
 end
diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy
@@ -98,6 +98,11 @@ lemma gets_the_assert:
   "gets_the (oassert P) = assert P"
   by (simp add: oassert_def assert_def gets_the_fail gets_the_return)
 
+lemma gets_the_ostate_assert:
+  "gets_the (ostate_assert P) = state_assert P"
+  by (clarsimp simp: ostate_assert_def state_assert_def gets_the_Some_get gets_the_obind
+                     gets_the_assert)
+
 lemma gets_the_assert_opt:
   "gets_the (oassert_opt P) = assert_opt P"
   by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits)

diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy
@@ -216,6 +216,9 @@ definition oassert :: "bool \<Rightarrow> ('s, unit) lookup" where
 definition oassert_opt :: "'a option \<Rightarrow> ('s, 'a) lookup" where
   "oassert_opt r \<equiv> case r of None \<Rightarrow> ofail | Some x \<Rightarrow> oreturn x"
 
+definition ostate_assert :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, unit) lookup" where
+  "ostate_assert P \<equiv> do { s \<leftarrow> Some; oassert (P s)}"
+
 definition oapply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
   "oapply x \<equiv> \<lambda>s. s x"
 

diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy
@@ -58,6 +58,19 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric]
 
 
 (* WP rules for ovalid. *)
+
+lemma ovalid_wp_comb1[wp_comb]:
+  "\<lbrakk> ovalid P' f Q; ovalid P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalid P f (\<lambda>r s. Q r s \<and> Q' r s)"
+  by (simp add: ovalid_def)
+
+lemma ovalid_wp_comb2[wp_comb]:
+  "\<lbrakk> ovalid P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalid P' f Q"
+  by (auto simp: ovalid_def)
+
+lemma ovalid_wp_comb3[wp_comb]:
+  "\<lbrakk> ovalid P f Q; ovalid P' f Q' \<rbrakk> \<Longrightarrow> ovalid (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)"
+  by (auto simp: ovalid_def)
+
 lemma ovalid_post_taut[wp]:
   "\<lblot>P\<rblot> f \<lblot>\<top>\<top>\<rblot>"
   by (simp add: ovalid_def)
@@ -102,6 +115,15 @@ lemma oassert_wp[wp]:
   apply (intro conjI; wpsimp)
   done
 
+lemma ostate_assert_wp:
+  "\<lblot>\<lambda>s. f s \<longrightarrow> P () s\<rblot> ostate_assert f \<lblot>P\<rblot>"
+  unfolding ostate_assert_def
+  by (wpsimp wp: ask_wp)
+
+lemma ostate_assert_sp:
+  "\<lblot>P\<rblot> ostate_assert Q \<lblot>\<lambda>_ s. P s \<and> Q s\<rblot>"
+  by (wpsimp wp: ostate_assert_wp ovalid_wp_comb2)
+
 lemma ogets_wp[wp]:
   "ovalid (\<lambda>s. P (f s) s) (ogets f) P"
   by wp
@@ -150,19 +172,6 @@ lemma ovalid_is_triple[wp_trip]:
   by (auto simp: triple_judgement_def ovalid_def ovalid_property_def)
 
 
-lemma ovalid_wp_comb1[wp_comb]:
-  "\<lbrakk> ovalid P' f Q; ovalid P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalid P f (\<lambda>r s. Q r s \<and> Q' r s)"
-  by (simp add: ovalid_def)
-
-lemma ovalid_wp_comb2[wp_comb]:
-  "\<lbrakk> ovalid P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalid P' f Q"
-  by (auto simp: ovalid_def)
-
-lemma ovalid_wp_comb3[wp_comb]:
-  "\<lbrakk> ovalid P f Q; ovalid P' f Q' \<rbrakk> \<Longrightarrow> ovalid (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)"
-  by (auto simp: ovalid_def)
-
-
 (* WP rules for ovalidNF. *)
 lemma obind_NF_wp[wp]:
   "\<lbrakk> \<And>r. ovalidNF (R r) (g r) Q; ovalidNF P f R \<rbrakk> \<Longrightarrow> ovalidNF P (obind f g) Q"
@@ -234,6 +243,11 @@ lemma ovalidNF_wp_comb3[wp_comb]:
 
 
 (* FIXME: WP rules for no_ofail, which might not be correct. *)
+
+lemma no_ofail_pre_imp[wp_pre]:
+  "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f"
+  by (simp add: no_ofail_def)
+
 lemma no_ofailD:
   "\<lbrakk> no_ofail P m; P s \<rbrakk> \<Longrightarrow> \<exists>y. m s = Some y"
   by (simp add: no_ofail_def)
@@ -309,6 +323,11 @@ lemma no_ofail_oassert[simp, wp]:
   "no_ofail (\<lambda>_. P) (oassert P)"
   by (simp add: oassert_def no_ofail_def)
 
+lemma no_ofail_ostate_assert[wp]:
+  "no_ofail P (ostate_assert P)"
+  unfolding ostate_assert_def
+  by wpsimp
+
 lemma no_ofail_is_triple[wp_trip]:
   "no_ofail P f = triple_judgement P f (\<lambda>s f. f s \<noteq> None)"
   by (auto simp: triple_judgement_def no_ofail_def)
@@ -355,10 +374,6 @@ lemma ovalidNF_pre_imp:
   "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P' f Q"
   by (simp add: ovalidNF_def)
 
-lemma no_ofail_pre_imp[wp_pre]:
-  "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f"
-  by (simp add: no_ofail_def)
-
 lemma ovalid_post_imp:
   "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'"
   by (simp add: ovalid_def)