Add some lemmas about bitvectors

Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy
index e7286fcf..e0d684ba 100644
--- a/lib/isabelle/State_monad_lemmas.thy
+++ b/lib/isabelle/State_monad_lemmas.thy
@@ -32,6 +32,9 @@ lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)"
 lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
   by (auto simp: bindS_def updateS_def returnS_def)
 
+lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()"
+  by (auto simp: assert_expS_def)
+
 
 lemma result_cases:
   fixes r :: "('a, 'e) result"
@@ -126,6 +129,13 @@ lemma try_catchS_intros:
   "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s"
   by (auto simp: try_catchS_def returnS_def intro: bexI[rotated])
 
+lemma no_Ex_basic_builtins[simp]:
+  "\<And>s e s' a. (Ex e, s') \<in> returnS a s \<longleftrightarrow> False"
+  "\<And>s e s' f. (Ex e, s') \<in> readS f s \<longleftrightarrow> False"
+  "\<And>s e s' f. (Ex e, s') \<in> updateS f s \<longleftrightarrow> False"
+  "\<And>s e s' xs. (Ex e, s') \<in> chooseS xs s \<longleftrightarrow> False"
+  by (auto simp: readS_def updateS_def returnS_def chooseS_def)
+
 fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where
   "ignore_throw_aux (Value a, s') = {(Value a, s')}"
 | "ignore_throw_aux (Ex (Throw e), s') = {}"