Simplify treating of undefined_bool in Lem library

Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.

7 files changed, 83 insertions, 31 deletions

diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem
index edbd3752..3597fa06 100644
--- a/lib/hol/prompt.lem
+++ b/lib/hol/prompt.lem
@@ -3,12 +3,12 @@ open import State_monad
 open import State
 
 let inline undefined_bool = undefined_boolS
-let inline bool_of_bitU_oracle = bool_of_bitU_oracleS
+let inline bool_of_bitU_nondet = bool_of_bitU_nondetS
 let inline bool_of_bitU_fail = bool_of_bitU_fail
-let inline bools_of_bits_oracle = bools_of_bits_oracleS
-let inline of_bits_oracle = of_bits_oracleS
+let inline bools_of_bits_nondet = bools_of_bits_nondetS
+let inline of_bits_nondet = of_bits_nondetS
 let inline of_bits_fail = of_bits_failS
-let inline mword_oracle = mword_oracleS
+let inline mword_nondet = mword_nondetS
 let inline reg_deref = read_regS
 
 let inline foreachM = foreachS
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index 5c77c5e7..afa953be 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -363,4 +363,24 @@ lemma PrePostE_foreachS_invariant:
   using assms unfolding PrePostE_def
   by (intro PrePost_foreachS_invariant[THEN PrePost_strengthen_pre]) auto
 
+lemma PrePostE_bool_of_bitU_nondetS_any:
+  "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E"
+  unfolding bool_of_bitU_nondetS_def undefined_boolS_def
+  by (cases b; simp; rule PrePostE_strengthen_pre, rule PrePostE_atomI) auto
+
+lemma PrePostE_bools_of_bits_nondetS_any:
+  "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (bools_of_bits_nondetS bs) Q E"
+  unfolding bools_of_bits_nondetS_def
+  by (rule PrePostE_weaken_post[where B = "\<lambda>_ s. \<forall>bs. Q bs s"], rule PrePostE_strengthen_pre,
+      (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS
+            PrePostE_bool_of_bitU_nondetS_any)+)
+     auto
+
+lemma PrePostE_internal_pick:
+  "xs \<noteq> [] \<Longrightarrow> PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (internal_pickS xs) Q E"
+  unfolding internal_pickS_def Let_def
+  by (rule PrePostE_strengthen_pre,
+      (rule PrePostE_compositeI PrePostE_atomI PrePostE_bools_of_bits_nondetS_any)+)
+     (auto split: option.splits)
+
 end
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
index ae8802f2..2a6272c2 100644
--- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy
+++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
@@ -2,14 +2,14 @@ theory Sail2_operators_mwords_lemmas
   imports Sail2_operators_mwords
 begin
 
-lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def
-lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_oracle_def
+lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_nondet_def
+lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_nondet_def
 
-lemma bools_of_bits_oracle_just_list[simp]:
+lemma bools_of_bits_nondet_just_list[simp]:
   assumes "just_list (map bool_of_bitU bus) = Some bs"
-  shows "bools_of_bits_oracle bus = return bs"
+  shows "bools_of_bits_nondet bus = return bs"
 proof -
-  have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_oracle b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)"
+  have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_nondet b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)"
     if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools
   proof (use that in \<open>induction bus arbitrary: bs bools\<close>)
     case (Cons bu bus bs)
@@ -17,26 +17,26 @@ proof -
       using Cons.prems by (cases bu) (auto split: option.splits)
     then show ?case
       using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"]
-      by (cases bu) (auto simp: bool_of_bitU_oracle_def split: option.splits)
+      by (cases bu) (auto simp: bool_of_bitU_nondet_def split: option.splits)
   qed auto
-  then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def
+  then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_nondet_def
     by auto
 qed
 
 lemma of_bits_mword_return_of_bl[simp]:
   assumes "just_list (map bool_of_bitU bus) = Some bs"
-  shows "of_bits_oracle BC_mword bus = return (of_bl bs)"
+  shows "of_bits_nondet BC_mword bus = return (of_bl bs)"
     and "of_bits_fail BC_mword bus = return (of_bl bs)"
-  by (auto simp: of_bits_oracle_def of_bits_fail_def maybe_fail_def assms BC_mword_defs)
+  by (auto simp: of_bits_nondet_def of_bits_fail_def maybe_fail_def assms BC_mword_defs)
 
 lemma vec_of_bits_of_bl[simp]:
   assumes "just_list (map bool_of_bitU bus) = Some bs"
   shows "vec_of_bits_maybe bus = Some (of_bl bs)"
     and "vec_of_bits_fail bus = return (of_bl bs)"
-    and "vec_of_bits_oracle bus = return (of_bl bs)"
+    and "vec_of_bits_nondet bus = return (of_bl bs)"
     and "vec_of_bits_failwith bus = of_bl bs"
     and "vec_of_bits bus = of_bl bs"
-  unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_oracle_def
+  unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_nondet_def
             vec_of_bits_failwith_def vec_of_bits_def
   by (auto simp: assms)
 
@@ -53,10 +53,10 @@ lemma bool_of_bitU_monadic_simps[simp]:
   "bool_of_bitU_fail B0 = return False"
   "bool_of_bitU_fail B1 = return True"
   "bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
-  "bool_of_bitU_oracle B0 = return False"
-  "bool_of_bitU_oracle B1 = return True"
-  "bool_of_bitU_oracle BU = undefined_bool ()"
-  unfolding bool_of_bitU_fail_def bool_of_bitU_oracle_def
+  "bool_of_bitU_nondet B0 = return False"
+  "bool_of_bitU_nondet B1 = return True"
+  "bool_of_bitU_nondet BU = undefined_bool ()"
+  unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def
   by auto
 
 lemma update_vec_dec_simps[simp]:
@@ -66,12 +66,12 @@ lemma update_vec_dec_simps[simp]:
   "update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)"
   "update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)"
   "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
-  "update_vec_dec_oracle w i B0 = return (set_bit w (nat i) False)"
-  "update_vec_dec_oracle w i B1 = return (set_bit w (nat i) True)"
-  "update_vec_dec_oracle w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
+  "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)"
+  "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)"
+  "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
   "update_vec_dec w i B0 = set_bit w (nat i) False"
   "update_vec_dec w i B1 = set_bit w (nat i) True"
-  unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_oracle_def update_vec_dec_def
+  unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_nondet_def update_vec_dec_def
   by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def)
 
 lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]:
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 08c9b33c..3ca1729f 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -64,7 +64,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T"
 | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
 | Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T"
-| Undefined : "((Undefined k), e_undefined v, k v) \<in> T"
+| Undefined: "((Undefined k), e_undefined v, k v) \<in> T"
 | Print: "((Print msg k), e_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
@@ -95,7 +95,7 @@ lemma Traces_cases:
   | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = e_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
   | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces"
   | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
-  | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Undefined) xs v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
   | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 124722ab..8f04e850 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -23,6 +23,22 @@ lemma Value_liftState_Run:
 
 lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
 
+lemma member_set_nth:
+  assumes "x \<in> set xs"
+  obtains n where "x = xs ! n" and "n < length xs"
+proof (use assms in \<open>induction xs arbitrary: thesis\<close>)
+  case (Cons a xs) print_cases
+  show ?case proof cases
+    assume "x = a"
+    then show ?thesis using Cons(2)[where n = 0] Cons(3) by auto
+  next
+    assume "x \<noteq> a"
+    then obtain n where "x = xs ! n" and "n < length xs" using Cons by auto
+    then show ?thesis using Cons(2)[of "Suc n"] by auto
+  qed
+qed auto
+
+
 lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e"
   by (auto simp: throw_def)
 lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg"
@@ -66,6 +82,10 @@ lemma liftState_try_catchR[liftState_simp]:
   "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)"
   by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong)
 
+lemma liftState_bool_of_bitU_nondet[liftState_simp]:
+  "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b"
+  by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
+
 lemma liftState_read_mem_BC:
   assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
   shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
@@ -87,7 +107,7 @@ lemma liftState_write_mem_ea[liftState_simp]:
   "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)"
   by (auto simp: liftState_write_mem_ea_BC)
 
-lemma liftState_write_mem_val:
+lemma liftState_write_mem_val[liftState_simp]:
   "liftState r (write_mem_val BC v) = write_mem_valS BC v"
   by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits)
 
@@ -126,6 +146,18 @@ lemma liftState_foreachM[liftState_simp]:
   by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
      (auto simp: liftState_simp cong: bindS_cong)
 
+lemma liftState_bools_of_bits_nondet[liftState_simp]:
+  "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs"
+  unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def
+  by (auto simp: liftState_simp comp_def)
+
+lemma liftState_internal_pick[liftState_simp]:
+  "liftState r (internal_pick xs) = internal_pickS xs"
+  by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def
+                 option.case_distrib[where h = "liftState r"]
+           simp del: repeat.simps
+           cong: option.case_cong)
+
 lemma whileS_dom_step:
   assumes "whileS_dom (vars, cond, body, s)"
     and "(Value True, s') \<in> cond vars s"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index b705de4c..91e4c17e 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -35,6 +35,9 @@ lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
 lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()"
   by (auto simp: assert_expS_def)
 
+lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (f ` xs)"
+  by (intro ext) (auto simp: bindS_def chooseS_def returnS_def)
+
 
 lemma result_cases:
   fixes r :: "('a, 'e) result"
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy
index 6cd90a9a..0d67f6c5 100644
--- a/lib/isabelle/manual/Manual.thy
+++ b/lib/isabelle/manual/Manual.thy
@@ -168,8 +168,8 @@ following variants:
   \<^item> @{term quot_vec_maybe} returns an option type, with
     @{lemma "quot_vec_maybe w 0 = None" by (auto simp: quot_vec_maybe_def quot_bv_def arith_op_bv_no0_def)}.
   \<^item> @{term quot_vec_fail} is monadic and either returns the result or raises an exception.
-  \<^item> @{term quot_vec_oracle} is monadic and uses the @{term Undefined} effect in the exception case
-    to fill the result with bits drawn from a bitstream oracle.
+  \<^item> @{term quot_vec_nondet} is monadic and uses the @{term Undefined} effect in the exception case
+    to fill the result with bits chosen nondeterministically.
   \<^item> @{term quot_vec} is pure and returns an arbitrary (but fixed) value in the exception case,
     currently defined as follows:  For the bitlist representation of bitvectors,
     @{term "quot_vec w 0"} returns a list filled with @{term BU}, while for the machine word
@@ -263,9 +263,6 @@ The @{type sequential_state} record has the following fields:
     of the last announced memory write, if any.
   \<^item> The @{term last_exclusive_operation_was_load} flag is used to determine whether exclusive
     operations can succeed.
-  \<^item> The function stored in the @{term next_bool} field together with the seed in the @{term seed}
-    field are used as a random bit generator for undefined values.  The @{term next_bool}
-    function takes the current seed as an argument and returns a @{type bool} and the next seed.
 
 The library defines several combinators and wrappers in addition to the standard monadic bind and
 return (called @{term bindS} and @{term returnS} here, where the suffix @{term S} differentiates them