From ea8ab81aa41e7c40caca5d67c4dcd202c378b996 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolffburkhart@gmail.com>
Date: Wed, 9 Oct 2024 13:02:39 +0200
Subject: [PATCH] Bu's Symbolic execution rules for assertions
---
C11-BackEnds/Clean/src/Symbex_MonadSE.thy | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/C11-BackEnds/Clean/src/Symbex_MonadSE.thy b/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
index b163bf17c..773c299c3 100644
--- a/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
+++ b/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
@@ -547,8 +547,7 @@ next
exec_mbindFStop_success list.set_intros(1) list.set_intros(2) valid_bind_cong)
qed
-
-
+text\<open>Symbolic execution rules for assertions.\<close>
lemma assert_suffix_seq :
"\<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p xs iostep; assert\<^sub>S\<^sub>E (P))
\<Longrightarrow> \<forall>\<sigma>. P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p ys iostep; assert\<^sub>S\<^sub>E (Q)))
--
GitLab