diff options
| author | Thomas Bauereiss | 2018-04-18 16:03:26 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-04-18 16:03:26 +0100 |
| commit | e1b2379f9058e858722f2bd9691c76d00c00dcaa (patch) | |
| tree | 635c9dfcf02772200796297f98aea114a118fda1 /lib/isabelle/State_lemmas.thy | |
| parent | 15f965c9e4bd39eb7fe97552b9ac9db51a3cdbfb (diff) | |
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.
Diffstat (limited to 'lib/isabelle/State_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 36fb987f..84b08e6c 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -19,6 +19,8 @@ lemma Value_liftState_Run: auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps; blast elim: Value_bindS_elim) +lemmas liftState_if_distrib[simp] = if_distrib[where f = "liftState ra" for ra] + lemma liftState_throw[simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def) lemma liftState_assert[simp]: "liftState r (assert_exp c msg) = assert_expS c msg" by (auto simp: assert_exp_def assert_expS_def) lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: exit0_def exitS_def) |