From 1893d00f8303f90b24e709a8e0499f67c807414f Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Wed, 25 Jan 2023 09:26:10 +1100
Subject: [PATCH] lib: move general lemma to Lib

lifted_if_collapse has no dependencies that require it to be in
NonDetMonadLemmaBucket.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 lib/Lib.thy                    | 4 ++++
 lib/NonDetMonadLemmaBucket.thy | 6 +-----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/lib/Lib.thy b/lib/Lib.thy
index c3c0bdd89..800a7e2c7 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -1472,6 +1472,10 @@ lemma list_case_If:
   "(case xs of [] \<Rightarrow> P | _ \<Rightarrow> Q) = (if xs = [] then P else Q)"
   by (rule list.case_eq_if)
 
+lemma lifted_if_collapse:
+  "(if P then \<top> else f) = (\<lambda>s. \<not>P \<longrightarrow> f s)"
+  by auto
+
 lemma remove1_Nil_in_set:
   "\<lbrakk> remove1 x xs = []; xs \<noteq> [] \<rbrakk> \<Longrightarrow> x \<in> set xs"
   by (induct xs) (auto split: if_split_asm)
diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy
index 791874866..7afb9d2d4 100644
--- a/lib/NonDetMonadLemmaBucket.thy
+++ b/lib/NonDetMonadLemmaBucket.thy
@@ -42,15 +42,11 @@ lemma return_bindE:
   "isRight v \<Longrightarrow> return v >>=E f = f (theRight v)"
   by (cases v; clarsimp simp: return_returnOk)
 
-lemma list_case_return: (* FIXME lib: move to Lib *)
+lemma list_case_return: (* not in Lib, because "return" is not in scope there *)
   "(case xs of [] \<Rightarrow> return v | y # ys \<Rightarrow> return (f y ys))
     = return (case xs of [] \<Rightarrow> v | y # ys \<Rightarrow> f y ys)"
   by (simp split: list.split)
 
-lemma lifted_if_collapse: (* FIXME lib: move to Lib *)
-  "(if P then \<top> else f) = (\<lambda>s. \<not>P \<longrightarrow> f s)"
-  by auto
-
 (* We use isLeft, because isLeft=isl is the primitive concept; isRight=\<not>isl matches on isl. *)
 lemma valid_isLeft_theRight_split:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q False rv s\<rbrace>,\<lbrace>\<lambda>e s. \<forall>v. Q True v s\<rbrace> \<Longrightarrow>