From 68c4283501ff0bf9b7b9604a6118258f2c2baba5 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Fri, 13 Oct 2023 10:50:44 +1100 Subject: [PATCH] squash lib/monads: remove another _tac Signed-off-by: Corey Lewis --- lib/Monads/trace/Trace_RG.thy | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy index ce39dc9af0..bac4c822bb 100644 --- a/lib/Monads/trace/Trace_RG.thy +++ b/lib/Monads/trace/Trace_RG.thy @@ -734,13 +734,16 @@ lemmas modify_prefix_closed[simp] = modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed] lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed] +lemma repeat_n_prefix_closed[intro!]: + "prefix_closed f \ prefix_closed (repeat_n n f)" + apply (induct n; simp) + apply (auto intro: prefix_closed_bind) + done + lemma repeat_prefix_closed[intro!]: "prefix_closed f \ prefix_closed (repeat f)" apply (simp add: repeat_def) apply (rule prefix_closed_bind; clarsimp) - apply (rename_tac n) - apply (induct_tac n; simp) - apply (auto intro: prefix_closed_bind) done lemma rely_cond_True[simp]: