squash lib/monads: remove another _tac

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Oct 12, 2023 · 68c4283 · 68c4283
1 parent c17e165
commit 68c4283
Showing 1 changed file with 6 additions and 3 deletions.
diff --git 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 \<Longrightarrow> 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 \<Longrightarrow> 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]: