From 2214c0e266d4a57b09a7a6b010a8a5c98b32d77e Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 1 Feb 2024 10:25:00 +1100 Subject: [PATCH] squash into prefix_closed rule set: use auto 4 4 Signed-off-by: Corey Lewis --- lib/Monads/trace/Trace_Prefix_Closed.thy | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/lib/Monads/trace/Trace_Prefix_Closed.thy b/lib/Monads/trace/Trace_Prefix_Closed.thy index 931382f401d..cf1ac150fb9 100644 --- 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]: "\prefix_closed f; \x. prefix_closed (g x)\ \ 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]: