From 22883e5222a1a35cdca7177cdbefec8dec6d715d Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 5 Mar 2018 15:54:45 +0000 Subject: Add Print outcome to prompt monad for debugging and tracing Currently ignored in the state monad --- lib/isabelle/Prompt_monad_lemmas.thy | 3 +++ 1 file changed, 3 insertions(+) (limited to 'lib') 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 \ 'rv event \ ('rv, 'a, 'e) monad) set" where Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \ T" @@ -55,6 +56,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \ 'rv event \ ('rv, 'a, ' | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \ T" | Write_reg: "((Write_reg r v k), e_write_reg r v, k) \ T" | Undefined : "((Undefined k), e_undefined v, k v) \ T" +| Print: "((Print msg k), e_print msg, k) \ T" inductive_set Traces :: "(('rv, 'a, 'e) monad \ 'rv event list \ ('rv, 'a, 'e) monad) set" where Nil: "(s, [], s) \ Traces" @@ -85,6 +87,7 @@ lemma Traces_cases: | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \ 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') \ Traces" | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \ Traces" + | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \ Traces" proof (use Run in \cases m t m' set: Traces\) case Nil then show ?thesis by (auto intro: that(1)) -- cgit v1.2.3