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

@@ -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)

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>