Some rules for Lib and CLib

lib/Corres_UL.thy

@@ -1298,6 +1298,16 @@ lemmas corres_split_noop_rhs2
 
 lemmas corres_split_dc = corres_split[where r'=dc, simplified]
 
+lemma corres_add_noop_rhs:
+  "corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> return (); g od)
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  by simp
+
+lemma corres_add_noop_rhs2:
+  "corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> g; return () od)
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  by simp
+
 lemma isLeft_case_sum:
   "isLeft v \<Longrightarrow> (case v of Inl v' \<Rightarrow> f v' | Inr v' \<Rightarrow> g v') = f (theLeft v)"
   by (clarsimp split: sum.splits)

lib/ExtraCorres.thy

@@ -288,11 +288,11 @@ lemma corres_noop_ex_abs:
 lemma corres_symb_exec_r_conj_ex_abs:
   assumes z: "\<And>rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)"
   assumes y: "\<lbrace>Q'\<rbrace> m \<lbrace>R'\<rbrace>"
-  assumes x: "\<And>s. Q s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr\<rbrace>"
-  assumes nf: "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying sr Q) m"
-  shows      "corres_underlying sr nf nf' r Q (P' and Q') x (m >>= (\<lambda>rv. y rv))"
+  assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr\<rbrace>"
+  assumes nf: "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying sr P) m"
+  shows      "corres_underlying sr nf nf' r (P and Q) (P' and Q') x (m >>= (\<lambda>rv. y rv))"
 proof -
-  have P: "corres_underlying sr nf nf' dc Q P' (return undefined) m"
+  have P: "corres_underlying sr nf nf' dc P P' (return undefined) m"
     apply (rule corres_noop_ex_abs)
      apply (simp add: x)
     apply (erule nf)

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

lib/Monads/nondet/Nondet_Reader_Option.thy

@@ -70,6 +70,10 @@ lemma gets_the_obind:
   "gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))"
   by (rule ext) (simp add: monad_simps obind_def split: option.splits)
 
+lemma gets_the_Some_get[simp]:
+  "gets_the Some = get"
+  by (clarsimp simp: gets_the_def gets_def assert_opt_Some)
+
 lemma gets_the_return:
   "gets_the (oreturn x) = return x"
   by (simp add: monad_simps oreturn_def)
@@ -94,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)

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"
 

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)
@@ -83,6 +96,10 @@ lemma ofail_wp[wp]:
   "ovalid (\<lambda>_. True) ofail Q"
   by (simp add: ovalid_def ofail_def)
 
+lemma ask_wp[wp]:
+  "\<lblot>\<lambda>s. P s s\<rblot> ask \<lblot>P\<rblot>"
+  by (clarsimp simp: ovalid_def)
+
 lemma asks_wp[wp]:
   "ovalid (\<lambda>s. P (f s) s) (asks f) P"
   by (simp add: split_def asks_def oreturn_def obind_def ovalid_def)
@@ -98,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
@@ -146,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"
@@ -230,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)
@@ -246,6 +264,10 @@ lemma no_ofail_ofail[wp]:
   "no_ofail \<bottom> ofail"
   by (simp add: no_ofail_def)
 
+lemma no_ofail_ask[wp]:
+  "no_ofail \<top> ask"
+  by (simp add: no_ofail_def)
+
 lemma no_ofail_asks_simp[simp]:
   "no_ofail P (asks f)"
   unfolding asks_def oreturn_def obind_def no_ofail_def
@@ -301,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)
@@ -347,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)