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.

3 files changed, 10 insertions, 7 deletions

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index f8786321..b10dde78 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,6 +1,6 @@
 THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \
   Sail_operators_mwords.thy Sail_operators_bitlists.thy \
-  State_monad.thy State.thy Prompt_monad.thy Prompt.thy
+  State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy
 EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \
   Sail_operators_mwords_lemmas.thy Hoare.thy
 
@@ -51,5 +51,8 @@ State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy
 State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy
 	lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
+State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy
+	lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
 clean:
 	-rm $(THYS)
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"
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy
index 53175ec9..90d65320 100644
--- a/lib/isabelle/manual/Manual.thy
+++ b/lib/isabelle/manual/Manual.thy
@@ -288,7 +288,7 @@ exception handler as arguments.
 The exception mechanism is also used to implement early returns by throwing and catching return
 values:  A function body with one or more early returns of type @{typ 'a} (and exception type
 @{typ 'e}) is lifted to a monadic expression with exception type @{typ "('a + 'e)"} using
-@{term liftSR}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a
+@{term liftRS}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a
 regular exception @{term e} is thrown as @{term "Inr e"}.  The function body is then wrapped in
 @{term catch_early_returnS} to lower it back to the default monad and exception type.  These
 liftings and lowerings are automatically inserted by Sail for functions with early returns.\<^footnote>\<open>To be