From 4cdfa4e69099c929786114e12f18549bb3f42925 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 1 Feb 2024 10:21:49 +1100 Subject: [PATCH] squash into no_trace rule set: remove FIXME Signed-off-by: Corey Lewis --- lib/Monads/trace/Trace_No_Trace.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/Monads/trace/Trace_No_Trace.thy b/lib/Monads/trace/Trace_No_Trace.thy index a5d2bbbcec2..de836f3cbf1 100644 --- a/lib/Monads/trace/Trace_No_Trace.thy +++ b/lib/Monads/trace/Trace_No_Trace.thy @@ -348,8 +348,8 @@ lemma no_trace_andM[no_trace_cond]: unfolding andM_def by (wpsimp wp: no_trace_terminal no_trace_cond) -\ \FIXME: This is true but is it useful to even state? - The parallel composition of traceless functions doesn't make much sense\ +\ \While the parallel composition of traceless functions doesn't make much sense, this + still might be useful to handle trivial goals as part of a proof by contradiction.\ lemma no_trace_parallel[no_trace_cond]: "\ no_trace f; no_trace g \ \ no_trace (parallel f g)" by (fastforce simp: parallel_def2 no_trace_def)