diff options
| author | Thomas Bauereiss | 2018-05-04 20:29:19 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-04 20:29:19 +0100 |
| commit | f469001209e0333dbdd8fe42c7232c92a6c1be6f (patch) | |
| tree | 0673f2b58eef0efc16da0219dde61328b1ef22b9 /lib/isabelle/State_lemmas.thy | |
| parent | 05a4a75d328d3bd8469167f6f23dda918146117a (diff) | |
Add back purely sequential Lem generation
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
Diffstat (limited to 'lib/isabelle/State_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 84b08e6c..253c21b9 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -1,5 +1,5 @@ theory State_lemmas - imports State + imports State State_lifting begin lemma All_liftState_dom: "liftState_dom (r, m)" @@ -44,12 +44,12 @@ lemma liftState_catch_early_return[simp]: by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong) lemma liftState_liftR[simp]: - "liftState r (liftR m) = liftSR (liftState r m)" - by (auto simp: liftR_def liftSR_def) + "liftState r (liftR m) = liftRS (liftState r m)" + by (auto simp: liftR_def liftRS_def) lemma liftState_try_catchR[simp]: - "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)" - by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong) + "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 cong: sum.case_cong) lemma liftState_read_mem_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" |