diff options
| author | Thomas Bauereiss | 2018-03-05 12:13:16 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-03-05 15:44:58 +0000 |
| commit | 21bb415d3c148361033576af6093f72f49d92866 (patch) | |
| tree | 53d87a289a6b089c4da9644a16e43086f17c05b3 /lib/isabelle/State_monad_lemmas.thy | |
| parent | ea2ff78cf675298df64e8ebacca7156b68f3c5c8 (diff) | |
Add support for undefined bit oracle to Lem shallow embedding
Add an Undefined outcome to the prompt monad that asks the environment for a
Boolean value. For the state monad, add fields for a random generator and a
seed (currently of type nat) to the state.
Diffstat (limited to 'lib/isabelle/State_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index fe827c66..d8730421 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -126,8 +126,11 @@ lemma no_throw_mem_builtins: "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" "\<And>t s. ignore_throw (write_tagS t) s = write_tagS t s" "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" - unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def write_mem_valS_def write_mem_bytesS_def write_tagS_def excl_resultS_def - by (auto simp: bindS_def chooseS_def Let_def split: option.splits)+ + "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" + unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def + unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def + unfolding excl_resultS_def undefined_boolS_def + by (auto simp: bindS_def chooseS_def Let_def split: option.splits prod.splits)+ lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s" by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_cong) |