4 files changed, 69 insertions, 16 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 50e6d471..1cff8f61 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,7 +1,7 @@
 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
-EXTRA_THYS = State_monad_extras.thy Prompt_monad_extras.thy
+EXTRA_THYS = State_monad_extras.thy State_extras.thy Prompt_monad_extras.thy
 
 .PHONY: all heap-img clean
 
@@ -29,16 +29,16 @@ Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_oper
 Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_operators.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy
+Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-State.thy: ../../src/gen_lib/state.lem State_monad.thy State_monad_extras.thy
+Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_extras.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy
+State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_extras.thy
+State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_extras.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
 clean:
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index c798447e..d826ea08 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -2,8 +2,8 @@ session "Sail" = "LEM" +
   options [document = false]
   theories
     Sail_values
-    State
     Prompt
+    State_extras
     Sail_operators_mwords
     Sail_operators_bitlists
 
diff --git a/lib/isabelle/State_extras.thy b/lib/isabelle/State_extras.thy
new file mode 100644
index 00000000..096fb19b
--- /dev/null
+++ b/lib/isabelle/State_extras.thy
@@ -0,0 +1,35 @@
+theory State_extras
+  imports State
+begin
+
+lemma All_liftState_dom: "liftState_dom (r, m)"
+  by (induction m) (auto intro: liftState.domintros)
+
+termination liftState using All_liftState_dom by auto
+
+lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def)
+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_bind[simp]:
+  "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)"
+  by (induction m f rule: bind.induct) auto
+
+lemma liftState_read_reg[intro]:
+  assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
+  shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg"
+proof
+  fix s :: "'a sequential_state"
+  obtain rv v where "get_regval' (name reg) (regstate s) = Some rv"
+    and "of_regval reg rv = Some v" and "read_from reg (regstate s) = v"
+    using assms unfolding bind_eq_Some_conv by blast
+  then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s"
+    by (auto simp: read_reg_def bindS_def returnS_def read_regS_def)
+qed
+
+lemma liftState_write_reg[intro]:
+  assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg s v)"
+  shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v"
+  using assms by (auto simp: write_reg_def bindS_def returnS_def write_regS_def)
+
+end
diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy
index cf042a02..eb8ed678 100644
--- a/lib/isabelle/State_monad_extras.thy
+++ b/lib/isabelle/State_monad_extras.thy
@@ -2,24 +2,42 @@ theory State_monad_extras
   imports State_monad
 begin
 
-lemma bind_ext_cong[fundef_cong]:
+abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> [(Ex e, s')])"
+
+lemma bindS_ext_cong[fundef_cong]:
   assumes m: "m1 s = m2 s"
     and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
-  shows "(bind m1 f1) s = (bind m2 f2) s"
+  shows "(bindS m1 f1) s = (bindS m2 f2) s"
 proof -
-  have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s)) =
-        List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s))"
+  have "List.concat (map (bindS_aux f1) (m2 s)) = List.concat (map (bindS_aux f2) (m2 s))"
     using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits)
-  then show ?thesis using m by (auto simp: bind_def)
+  then show ?thesis using m by (auto simp: bindS_def)
 qed
 
-lemma bind_cong[fundef_cong]:
+lemma bindS_cong[fundef_cong]:
   assumes m: "m1 = m2"
     and f: "\<And>s a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
-  shows "bind m1 f1 = bind m2 f2"
-  using assms by (blast intro: bind_ext_cong)
+  shows "bindS m1 f1 = bindS m2 f2"
+  using assms by (blast intro: bindS_ext_cong)
+
+lemma bindS_returnS[simp]: "bindS (returnS x) m = m x"
+  by (auto simp add: bindS_def returnS_def)
+
+lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)"
+proof -
+  have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) =
+        List.concat (map (bindS_aux (\<lambda>x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs
+    by (induction xs) (auto split: result.splits)
+  then show ?thesis unfolding bindS_def by auto
+qed
+
+lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def failS_def)
+lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def throwS_def)
+declare seqS_def[simp]
 
-lemma bind_return[simp]: "bind (return x) m = m x"
-  by (auto simp add: bind_def return_def)
+lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a"
+  and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg"
+  and try_catchS_throwS[simp]: "try_catchS (throwS e) h = h e"
+  by (auto simp: returnS_def failS_def throwS_def try_catchS_def)
 
 end