two other common lemmas

HOL-Theorem-Prover · Jun 12, 2024 · 511c529 · 511c529
1 parent 3b07de4
commit 511c529
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml
@@ -880,6 +880,12 @@ Proof
   metis_tac[itree_wbisim_coind_upto_equiv]
 QED
 
+Theorem itree_wbisim_vis:
+  !e k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==> itree_wbisim (Vis e k1) (Vis e k2)
+Proof
+  metis_tac[strip_tau_cases, itree_wbisim_cases]
+QED
+
 Theorem itree_wbisim_tau:
   !t t'. itree_wbisim (Tau t) t' ==> itree_wbisim t t'
 Proof
@@ -960,6 +966,13 @@ Proof
             itree_wbisim_sym]
 QED
 
+(* common bind base case *)
+Theorem itree_bind_ret_inv:
+  itree_bind t k = Ret r ==> ?r'. t = Ret r' /\ (k r') = Ret r
+Proof
+  Cases_on ‘t’ >> fs[itree_bind_thm]
+QED
+
 (* combinators respect weak bisimilarity *)
 Theorem itree_bind_strip_tau_wbisim:
   !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k)