From b7caab9d734cac4d4c7c5d7050008447a08f5878 Mon Sep 17 00:00:00 2001
From: Adam Stucci <a.stucci@unsw.edu.au>
Date: Fri, 25 Oct 2024 18:56:27 +1100
Subject: [PATCH] Generalise seq_none and add skip_elim to simp

---
 examples/fun-op-sem/imp/impScript.sml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/examples/fun-op-sem/imp/impScript.sml b/examples/fun-op-sem/imp/impScript.sml
index 4120a887da..e18bedb7ac 100644
--- a/examples/fun-op-sem/imp/impScript.sml
+++ b/examples/fun-op-sem/imp/impScript.sml
@@ -105,15 +105,19 @@ val cval_ind = prove(
 Theorem cval_ind[allow_rebind] = cval_ind
 
 Theorem seq_none:
-  cval (Seq c c') s t <> NONE ==> cval c s t <> NONE
+  cval (Seq c c') s t = NONE <=>
+    cval c s t = NONE \/
+    ?s' t'. cval c s t = SOME (s', t') /\ cval c' s' t' = NONE
 Proof
-  rw[] >>
-  fs[cval_def] >>
-  Cases_on `cval c s t` >>
+  simp[EQ_IMP_THM] >>
+  conj_tac >>
+  rw[cval_def, CaseEq"option"] >>
+  simp[] >>
+  Cases_on `v` >>
   fs[]
 QED
 
-Theorem skip_elim:
+Theorem skip_elim[simp]:
   cval (Seq c1 SKIP) s t = cval c1 s t
 Proof
   simp[cval_def] >>