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_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_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index e230bd37..9c5dd8af 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -25,6 +25,7 @@ lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: e lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def) lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def) lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def) +lemma liftState_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def) lemma liftState_try_catch[simp]: "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)" |