Generalise seq_none and add skip_elim to simp

HOL-Theorem-Prover · Oct 28, 2024 · b7caab9 · b7caab9
1 parent 68350b8
commit b7caab9
Showing 1 changed file with 9 additions and 5 deletions.
diff --git 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] >>