squash into prefix_closed rule set: use auto 4 4

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Jan 31, 2024 · 2214c0e · 2214c0e
1 parent 4cdfa4e
commit 2214c0e
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/lib/Monads/trace/Trace_Prefix_Closed.thy b/lib/Monads/trace/Trace_Prefix_Closed.thy
@@ -60,9 +60,8 @@ lemmas [prefix_closed_terminal] = no_trace_terminal[THEN no_trace_prefix_closed]
 lemma prefix_closed_bind[wp_split]:
   "\<lbrakk>prefix_closed f; \<And>x. prefix_closed (g x)\<rbrakk> \<Longrightarrow> prefix_closed (f >>= g)"
   apply (subst prefix_closed_def, clarsimp simp: bind_def)
-  apply (auto simp: Cons_eq_append_conv split: tmres.split_asm
-             dest!: prefix_closedD[rotated];
-         fastforce elim: rev_bexI)
+  apply (auto 4 4 simp: Cons_eq_append_conv split: tmres.split_asm
+                 dest!: prefix_closedD[rotated] elim: rev_bexI)
   done
 
 lemma prefix_closed_case_option[prefix_closed_cond]: