Monads: refactor reader_option and nondet connection

lib/HaskellLib_H.thy

@@ -14,8 +14,7 @@ imports
   Lib
   More_Numeral_Type
   Monads.Nondet_VCG
-  Monads.Reader_Option_Monad
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 abbreviation (input) "flip \<equiv> swp"

lib/Monads/ROOT

@@ -36,8 +36,8 @@ session Monads (lib) = HOL +
     Nondet_Monad_Equations
     Nondet_While_Loop_Rules
     Nondet_While_Loop_Rules_Completeness
+    Nondet_Reader_Option
     Reader_Option_Monad
-    Reader_Option_ND
     Reader_Option_VCG
     Trace_Monad
     Trace_Lemmas
@@ -53,6 +53,7 @@ session Monads (lib) = HOL +
     Trace_In_Monad
     Trace_More_VCG
     Trace_No_Fail
+    Trace_Reader_Option
     Trace_Sat
     Strengthen
     Nondet_Strengthen_Setup

lib/Monads/reader_option/Reader_Option_ND.thy → lib/Monads/nondet/Nondet_Reader_Option.thy

@@ -1,15 +1,16 @@
 (*
+ * Copyright 2024, Proofcraft Pty Ltd
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (* Reader option monad syntax plus the connection between the reader option monad and the nondet monad *)
 
-theory Reader_Option_ND
+theory Nondet_Reader_Option
 imports
-  Nondet_Lemmas
-  Reader_Option_Monad
+  Nondet_No_Fail
+  Reader_Option_VCG
 begin
 
 (* FIXME: remove this syntax, standardise on do {..} instead *)
@@ -23,9 +24,34 @@ translations
   "DO x <- a; e OD"        == "a |>> (\<lambda>x. e)"
 
 
-lemma ogets_def:
-  "ogets f = (\<lambda>s. Some (f s))"
-  by (clarsimp simp: asks_def obind_def)
+lemma ovalid_K_bind_wp[wp]:
+  "ovalid P f Q \<Longrightarrow> ovalid P (K_bind f x) Q"
+  by simp
+
+lemma ovalidNF_K_bind_wp[wp]:
+  "ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q"
+  by simp
+
+lemma no_ofail_K_bind[wp]:
+  "no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)"
+  by simp
+
+lemma no_ofail_gets_the_eq:
+  "no_ofail P f \<longleftrightarrow> no_fail P (gets_the (f :: ('s, 'a) lookup))"
+  by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def
+                 get_def assert_opt_def bind_def return_def fail_def
+         split: option.split)
+
+lemmas no_ofail_gets_the =
+  no_ofail_gets_the_eq[THEN iffD1]
+
+
+(* Lemmas relating ovalid and valid *)
+lemma ovalid_gets_the:
+  "ovalid P f Q \<Longrightarrow> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
+  apply wpsimp
+  apply (fastforce dest: use_ovalid)
+  done
 
 
 lemmas monad_simps =
@@ -104,8 +130,6 @@ lemmas omonad_simps [simp] =
   gets_the_throwError gets_the_assert gets_the_Some
   gets_the_oapply_comp
 
-lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq in_opt_pred Let_def
-
 
 section "Relation between option monad loops and non-deterministic monad loops."
 
@@ -163,12 +187,12 @@ proof -
   note option_while'_None = this
 
   have "\<And>s. owhile C B r s = None
-      \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({}, True)"
+          \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({}, True)"
     by (auto simp: whileLoop_def owhile_def option_while_def option_while'_THE gets_the_loop_terminates
       split: if_split_asm dest: option_while'_None wl'_Inl option_while'_inj)
   moreover
   have "\<And>s r'. owhile C B r s = Some r'
-      \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({(r', s)}, False)"
+          \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({(r', s)}, False)"
     by (auto simp: whileLoop_def owhile_def option_while_def option_while'_THE gets_the_loop_terminates
       split: if_split_asm dest: wl'_Inl wl'_Inr option_while'_inj intro: option_while'_Some)
   ultimately

lib/Monads/reader_option/Reader_Option_Monad.thy

@@ -260,7 +260,11 @@ definition
 definition
   "oskip \<equiv> oreturn ()"
 
-lemmas omonad_defs = ofail_def oreturn_def oassert_def oassert_opt_def asks_def ounless_def
+lemma ogets_def:
+  "ogets f = (\<lambda>s. Some (f s))"
+  by (clarsimp simp: asks_def obind_def oreturn_def)
+
+lemmas omonad_defs = ofail_def oreturn_def oassert_def oassert_opt_def ogets_def ounless_def
                      owhen_def
 
 
@@ -478,6 +482,8 @@ lemma obindK_is_opt_map:
   "f \<bind> (\<lambda>x. K $ g x) = f |> g"
   by (simp add: obind_def opt_map_def)
 
+lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq in_opt_pred Let_def
+
 
 section \<open>"While" loops over option monad.\<close>
 
@@ -584,6 +590,7 @@ proof -
   qed
 qed
 
+
 section \<open>Lift @{term option_while} to the @{typ "('a,'s) lookup"} monad\<close>
 
 definition owhile :: "('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('s,'a) lookup) \<Rightarrow> 'a \<Rightarrow> ('s,'a) lookup" where

lib/Monads/reader_option/Reader_Option_VCG.thy

@@ -12,9 +12,8 @@ This list is almost certainly incomplete; add rules here as they are needed.
 
 theory Reader_Option_VCG
 imports
-  Reader_Option_ND
-  WP
-  Nondet_No_Fail
+  Reader_Option_Monad
+  WPSimp
 begin
 
 (* Hoare triples.
@@ -84,10 +83,6 @@ lemma ofail_wp[wp]:
   "ovalid (\<lambda>_. True) ofail Q"
   by (simp add: ovalid_def ofail_def)
 
-lemma ovalid_K_bind_wp[wp]:
-  "ovalid P f Q \<Longrightarrow> ovalid P (K_bind f x) Q"
-  by simp
-
 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)
@@ -159,7 +154,6 @@ lemma ovalid_wp_comb3[wp_comb]:
   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"
@@ -178,10 +172,6 @@ lemma ofail_NF_wp[wp]:
   "ovalidNF (\<lambda>_. False) ofail Q"
   by (simp add: ovalidNF_def ofail_def)
 
-lemma ovalidNF_K_bind_wp[wp]:
-  "ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q"
-  by simp
-
 lemma ogets_NF_wp[wp]:
   "ovalidNF (\<lambda>s. P (f s) s) (ogets f) P"
   by (simp add: ovalidNF_def ogets_def)
@@ -234,7 +224,6 @@ lemma ovalidNF_wp_comb3[wp_comb]:
   by (simp add: ovalidNF_def)
 
 
-
 (* FIXME: WP rules for no_ofail, which might not be correct. *)
 lemma no_ofailD:
   "\<lbrakk> no_ofail P m; P s \<rbrakk> \<Longrightarrow> \<exists>y. m s = Some y"
@@ -254,7 +243,7 @@ lemma no_ofail_ofail[wp]:
 
 lemma no_ofail_asks_simp[simp]:
   "no_ofail P (asks f)"
-  unfolding asks_def get_def oreturn_def obind_def no_ofail_def
+  unfolding asks_def oreturn_def obind_def no_ofail_def
   by simp
 
 lemma no_ofail_asks[wp]:
@@ -269,10 +258,6 @@ lemma no_ofail_obind[wp]:
   "\<lbrakk> \<And>r. no_ofail (R r) (g r); \<lblot>Q\<rblot> f \<lblot>R\<rblot>; no_ofail P f \<rbrakk> \<Longrightarrow> no_ofail (P and Q) (f |>> g)"
   by (auto simp: no_ofail_def obind_def ovalid_def)
 
-lemma no_ofail_K_bind[wp]:
-  "no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)"
-  by simp
-
 lemma no_ofail_oguard[wp]:
   "no_ofail (\<lambda>s. f s) (oguard f)"
   by (auto simp: no_ofail_def oguard_def)
@@ -311,15 +296,6 @@ lemma no_ofail_oassert[simp, wp]:
   "no_ofail (\<lambda>_. P) (oassert P)"
   by (simp add: oassert_def no_ofail_def)
 
-lemma no_ofail_gets_the_eq:
-  "no_ofail P f \<longleftrightarrow> no_fail P (gets_the (f :: ('s, 'a) lookup))"
-  by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def
-                 get_def assert_opt_def bind_def return_def fail_def
-         split: option.split)
-
-lemmas no_ofail_gets_the =
-  no_ofail_gets_the_eq[THEN iffD1]
-
 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)
@@ -333,14 +309,6 @@ lemma no_ofail_wp_comb2[wp_comb]:
   by (simp add: no_ofail_def)
 
 
-(* Lemmas relating ovalid and valid *)
-lemma ovalid_gets_the:
-  "ovalid P f Q \<Longrightarrow> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
-  apply wpsimp
-  apply (fastforce dest: use_ovalid)
-  done
-
-
 (* Some extra lemmas for our predicates. *)
 lemma ovalid_grab_asm:
   "(G \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid (\<lambda>s. G \<and> P s) f Q"

lib/Monads/trace/Trace_Monad.thy

@@ -694,8 +694,8 @@ inductive_set whileLoop_results ::
     "\<lbrakk> \<not> C r s \<rbrakk> \<Longrightarrow> ((r, s), ([], Result (r, s))) \<in> whileLoop_results C B"
   | "\<lbrakk> C r s; (ts, Failed) \<in> B r s \<rbrakk> \<Longrightarrow> ((r, s), (ts, Failed)) \<in> whileLoop_results C B"
   | "\<lbrakk> C r s; (ts, Incomplete) \<in> B r s \<rbrakk> \<Longrightarrow> ((r, s), (ts, Incomplete)) \<in> whileLoop_results C B"
-  | "\<lbrakk> C r s; (ts, Result (r', s')) \<in> B r s; ((r', s'), (ts',z)) \<in> whileLoop_results C B  \<rbrakk>
-       \<Longrightarrow> ((r, s), (ts'@ts,z)) \<in> whileLoop_results C B"
+  | "\<lbrakk> C r s; (ts, Result (r', s')) \<in> B r s; ((r', s'), (ts',z)) \<in> whileLoop_results C B; ts''=ts'@ts \<rbrakk>
+       \<Longrightarrow> ((r, s), (ts'',z)) \<in> whileLoop_results C B"
 
 \<comment> \<open>FIXME: there are fewer lemmas here than in NonDetMonad and I don't understand this well enough
   to know whether this is correct or not.\<close>