Add Print outcome to prompt monad for debugging and tracing

Currently ignored in the state monad

1 files changed, 3 insertions, 0 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index ffed5afb..2f2d43ef 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -42,6 +42,7 @@ datatype 'regval event =
   (* Request to write register *)
   | e_write_reg string 'regval
   | e_undefined bool
+  | e_print string
 
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
   Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T"
@@ -55,6 +56,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
 | Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T"
 | Undefined : "((Undefined k), e_undefined v, k v) \<in> T"
+| Print: "((Print msg k), e_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -85,6 +87,7 @@ lemma Traces_cases:
   | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces"
   | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
   | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
   then show ?thesis by (auto intro: that(1))