kings-crown/FVELER_Isabelle huggingface dataset:
theory NonDetMonadLemmaBucket

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (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)
theory NonDetMonadLemmaBucket

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>
     \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (isLeft rv) (theRight rv) s\<rbrace>" apply (simp add: validE_def) apply (erule hoare_strengthen_post) apply (simp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q False\<rbrace>, \<lbrace>\<lambda>e s. \<forall>v. Q True v s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q (isLeft rv) (theRight rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> \<forall>v. Q True v s | Inr r \<Rightarrow> Q False r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q (isLeft rv) (theRight rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> \<forall>v. Q True v s | Inr r \<Rightarrow> Q False r s \<Longrightarrow> Q (isLeft rv) (theRight rv) s proof (prove)
goal:
No subgoals!
theory NonDetMonadLemmaBucket

lemma gets_the_exs_valid_no_ofail:
  "\<lbrakk>no_ofail P h; ovalid P h Q\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace>" apply (rule exs_valid_weaken_pre) apply (rule gets_the_exs_valid) apply (fastforce simp: ovalid_def no_ofail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P h; \<lblot>P\<rblot> h \<lblot>Q\<rblot>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_ofail P h; \<lblot>P\<rblot> h \<lblot>Q\<rblot>\<rbrakk> \<Longrightarrow> \<lbrace>?P'\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace>
 2. \<And>s. \<lbrakk>no_ofail P h; \<lblot>P\<rblot> h \<lblot>Q\<rblot>; P s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_ofail P h; \<lblot>P\<rblot> h \<lblot>Q\<rblot>; P s\<rbrakk> \<Longrightarrow> \<exists>x. h s = Some x \<and> Q x s proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma map_bits_to_bl:
  "map ((!!) x) [0..<size x] = reverse (to_bl x)" by (simp add: map_bits_rev_to_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map ((!!) x) [0..<size x] = reverse (to_bl x)
theory HaskellLemmaBucket

lemma andList_Cons:
  assumes al: "andList $ map P (y # ys)"
  shows   "P y" using al unfolding andList_def by simp (induct rule: rev_induct, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P y proof (prove)
using this:
andList $ map P (y # ys)

goal (1 subgoal):
 1. P y proof (prove)
using this:
foldl (\<and>) True $ map P (y # ys)

goal (1 subgoal):
 1. P y
theory HaskellLemmaBucket

lemma andList_mapE:
  assumes al: "andList $ map P xs"
  and     xv: "x \<in> set xs"
  shows   "P x" using al xv proof (induct xs arbitrary: x rule: rev_induct) case Nil thus ?case by simp next case (snoc y ys) show ?case proof (cases "x = y") case True with snoc.prems show ?thesis by (simp add: andList_def) next case False with snoc.prems show ?thesis by (auto simp: andList_def intro!: snoc.hyps) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x proof (prove)
using this:
andList $ map P xs
x \<in> set xs

goal (1 subgoal):
 1. P x proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>andList $ map P []; x \<in> set []\<rbrakk> \<Longrightarrow> P x
 2. \<And>x xs xa. \<lbrakk>\<And>x. \<lbrakk>andList $ map P xs; x \<in> set xs\<rbrakk> \<Longrightarrow> P x; andList $ map P (xs @ [x]); xa \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> P xa proof (state)
this:
andList $ map P []
x \<in> set []

goal (2 subgoals):
 1. \<And>x. \<lbrakk>andList $ map P []; x \<in> set []\<rbrakk> \<Longrightarrow> P x
 2. \<And>x xs xa. \<lbrakk>\<And>x. \<lbrakk>andList $ map P xs; x \<in> set xs\<rbrakk> \<Longrightarrow> P x; andList $ map P (xs @ [x]); xa \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> P xa proof (prove)
using this:
andList $ map P []
x \<in> set []

goal (1 subgoal):
 1. P x proof (state)
this:
P x

goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. \<lbrakk>andList $ map P xs; x \<in> set xs\<rbrakk> \<Longrightarrow> P x; andList $ map P (xs @ [x]); xa \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> P xa proof (state)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. \<lbrakk>andList $ map P xs; x \<in> set xs\<rbrakk> \<Longrightarrow> P x; andList $ map P (xs @ [x]); xa \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> P xa proof (state)
this:
\<lbrakk>andList $ map P ys; ?x \<in> set ys\<rbrakk> \<Longrightarrow> P ?x
andList $ map P (ys @ [y])
x \<in> set (ys @ [y])

goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. \<lbrakk>andList $ map P xs; x \<in> set xs\<rbrakk> \<Longrightarrow> P x; andList $ map P (xs @ [x]); xa \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> P xa proof (prove)
goal (1 subgoal):
 1. P x proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> P x
 2. x \<noteq> y \<Longrightarrow> P x proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> P x
 2. x \<noteq> y \<Longrightarrow> P x proof (chain)
picking this:
andList $ map P (ys @ [y])
x \<in> set (ys @ [y])
x = y proof (prove)
using this:
andList $ map P (ys @ [y])
x \<in> set (ys @ [y])
x = y

goal (1 subgoal):
 1. P x proof (state)
this:
P x

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> P x proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> P x proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> P x proof (chain)
picking this:
andList $ map P (ys @ [y])
x \<in> set (ys @ [y])
x \<noteq> y proof (prove)
using this:
andList $ map P (ys @ [y])
x \<in> set (ys @ [y])
x \<noteq> y

goal (1 subgoal):
 1. P x proof (state)
this:
P x

goal:
No subgoals! proof (state)
this:
P x

goal:
No subgoals!
theory HaskellLemmaBucket

lemma andList_to_aligned:
  assumes al: "andList $ map (\<lambda>x. x && mask pageBits = 0) xs"
  and     xv: "x \<in> set xs"
  shows   "is_aligned x pageBits" proof (subst is_aligned_mask) from al show "x && mask pageBits = 0" by (rule andList_mapE) fact qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x pageBits proof (state)
goal (1 subgoal):
 1. x && mask pageBits = 0 proof (chain)
picking this:
andList $ map (\<lambda>x. x && mask pageBits = 0) xs proof (prove)
using this:
andList $ map (\<lambda>x. x && mask pageBits = 0) xs

goal (1 subgoal):
 1. x && mask pageBits = 0 proof (state)
this:
x && mask pageBits = 0

goal:
No subgoals!
theory HaskellLemmaBucket

lemma maximum_ge: "x \<in> set b \<Longrightarrow> x \<le> maximum b" unfolding maximum_def by (auto intro: Max_ge)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set b \<Longrightarrow> x \<le> maximum b proof (prove)
goal (1 subgoal):
 1. x \<in> set b \<Longrightarrow> x \<le> Max (set b)
theory HaskellLemmaBucket

lemma less_minimum_not_in:
  "\<lbrakk> ls \<noteq> []; x < minimum ls \<rbrakk> \<Longrightarrow> x \<notin> set ls" unfolding minimum_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<noteq> []; x < minimum ls\<rbrakk> \<Longrightarrow> x \<notin> set ls proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<noteq> []; x < Min (set ls)\<rbrakk> \<Longrightarrow> x \<notin> set ls
theory HaskellLemmaBucket

lemma minimum_le_member:
  "\<lbrakk> x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> minimum ls \<le> x" unfolding minimum_def apply (rule Min_le) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> minimum ls \<le> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> Min (set ls) \<le> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> finite (set ls)
 2. \<lbrakk>x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> x \<in> set ls proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> x \<in> set ls proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma minimum_enum_upto:
  fixes x :: "'a::len word"
  assumes le: "x \<le> y"
  shows   "minimum [x .e. y] = x" unfolding minimum_def using le by (auto intro!: MinI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. minimum [x .e. y] = x proof (prove)
goal (1 subgoal):
 1. Min (set [x .e. y]) = x proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. Min (set [x .e. y]) = x
theory HaskellLemmaBucket

lemma break_subsetsD:
  "break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs" apply (induct xs arbitrary: ys zs) apply simp apply (case_tac "break f xs") apply (elim meta_allE, drule(1) meta_mp) apply (fastforce simp: split_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs proof (prove)
goal (2 subgoals):
 1. \<And>ys zs. break f [] = (ys, zs) \<Longrightarrow> set ys \<subseteq> set [] \<and> set zs \<subseteq> set []
 2. \<And>a xs ys zs. \<lbrakk>\<And>ys zs. break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs; break f (a # xs) = (ys, zs)\<rbrakk> \<Longrightarrow> set ys \<subseteq> set (a # xs) \<and> set zs \<subseteq> set (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys zs. \<lbrakk>\<And>ys zs. break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs; break f (a # xs) = (ys, zs)\<rbrakk> \<Longrightarrow> set ys \<subseteq> set (a # xs) \<and> set zs \<subseteq> set (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys zs aa b. \<lbrakk>\<And>ys zs. break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs; break f (a # xs) = (ys, zs); break f xs = (aa, b)\<rbrakk> \<Longrightarrow> set ys \<subseteq> set (a # xs) \<and> set zs \<subseteq> set (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys zs aa b. \<lbrakk>break f (a # xs) = (ys, zs); break f xs = (aa, b); set aa \<subseteq> set xs \<and> set b \<subseteq> set xs\<rbrakk> \<Longrightarrow> set ys \<subseteq> set (a # xs) \<and> set zs \<subseteq> set (a # xs) proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma distinct_prop_breakD:
  "\<lbrakk> distinct_prop P xs; break f xs = (ys, zs) \<rbrakk>
    \<Longrightarrow> \<forall>y \<in> set ys. \<forall>z \<in> set zs. P y z" apply (induct xs arbitrary: ys zs) apply simp apply (simp add: split_def split: if_split_asm) apply (case_tac "break f xs") apply (elim meta_allE, drule(1) meta_mp) apply (frule break_subsetsD) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_prop P xs; break f xs = (ys, zs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<forall>z\<in>set zs. P y z proof (prove)
goal (2 subgoals):
 1. \<And>ys zs. \<lbrakk>distinct_prop P []; break f [] = (ys, zs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. Ball (set zs) (P y)
 2. \<And>a xs ys zs. \<lbrakk>\<And>ys zs. \<lbrakk>distinct_prop P xs; break f xs = (ys, zs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. Ball (set zs) (P y); distinct_prop P (a # xs); break f (a # xs) = (ys, zs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. Ball (set zs) (P y) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys zs. \<lbrakk>\<And>ys zs. \<lbrakk>distinct_prop P xs; break f xs = (ys, zs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. Ball (set zs) (P y); distinct_prop P (a # xs); break f (a # xs) = (ys, zs)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. Ball (set zs) (P y) proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys zs. break f xs = (ys, zs) \<Longrightarrow> \<forall>y\<in>set ys. \<forall>x\<in>set zs. P y x; \<not> f a; \<forall>x\<in>set xs. P a x; distinct_prop P xs; a # fst (break f xs) = ys\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<forall>x\<in>set (snd (break f xs)). P y x proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys aa b. \<lbrakk>\<And>ys zs. break f xs = (ys, zs) \<Longrightarrow> \<forall>y\<in>set ys. \<forall>x\<in>set zs. P y x; \<not> f a; \<forall>x\<in>set xs. P a x; distinct_prop P xs; a # fst (break f xs) = ys; break f xs = (aa, b)\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<forall>x\<in>set (snd (break f xs)). P y x proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys aa b. \<lbrakk>\<not> f a; \<forall>x\<in>set xs. P a x; distinct_prop P xs; a # fst (break f xs) = ys; break f xs = (aa, b); \<forall>y\<in>set aa. \<forall>x\<in>set b. P y x\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<forall>x\<in>set (snd (break f xs)). P y x proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys aa b. \<lbrakk>\<not> f a; \<forall>x\<in>set xs. P a x; distinct_prop P xs; a # fst (break f xs) = ys; break f xs = (aa, b); \<forall>y\<in>set aa. \<forall>x\<in>set b. P y x; set aa \<subseteq> set xs \<and> set b \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<forall>x\<in>set (snd (break f xs)). P y x proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma stateAssert_wp:
  "\<lbrace>\<lambda>s. P s \<longrightarrow> Q () s\<rbrace> stateAssert P e \<lbrace>Q\<rbrace>" by (clarsimp simp: stateAssert_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<longrightarrow> Q () s\<rbrace> stateAssert P e \<lbrace>Q\<rbrace>
theory HaskellLemmaBucket

lemma empty_fail_stateAssert[intro!, simp]:
  "empty_fail (stateAssert P l)" unfolding stateAssert_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (stateAssert P l) proof (prove)
goal (1 subgoal):
 1. empty_fail (state_assert P)
theory HaskellLemmaBucket

lemma haskell_assert_wp:
  "\<lbrace>\<lambda>s. Q \<longrightarrow> P s\<rbrace> haskell_assert Q xs \<lbrace>\<lambda>_. P\<rbrace>" by simp wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q \<longrightarrow> P s\<rbrace> haskell_assert Q xs \<lbrace>\<lambda>_. P\<rbrace>
theory HaskellLemmaBucket

lemma init_append_last:
  "xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs" apply (induct xs rule: rev_induct) apply simp apply (simp add: init_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs proof (prove)
goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> init [] @ [last []] = []
 2. \<And>x xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> init (xs @ [x]) @ [last (xs @ [x])] = xs @ [x] proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> init (xs @ [x]) @ [last (xs @ [x])] = xs @ [x] proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma init_Snoc[simp]:
  "init (xs @ [x]) = xs" by (induct xs) (auto simp: init_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. init (xs @ [x]) = xs
theory HaskellLemmaBucket

lemma init_upto_enum_upt[simp]:
  "init [0.e.n] = [0..<n]" by (induct n) (auto simp: init_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. init [0 .e. n] = [0..<n]
theory HaskellLemmaBucket

lemma no_fail_stateAssert:
  "no_fail P (stateAssert P xs)" apply (simp add: stateAssert_def) apply (rule no_fail_pre, wp no_fail_bind) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (stateAssert P xs) proof (prove)
goal (1 subgoal):
 1. no_fail P (state_assert P) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma haskell_fail_wp:
  "\<lbrace>\<top>\<rbrace> haskell_fail x \<lbrace>P\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> haskell_fail x \<lbrace>P\<rbrace>
theory HaskellLemmaBucket

lemma no_fail_haskell_fail [simp, wp]:
  "no_fail \<bottom> (haskell_fail xs)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) (haskell_fail xs)
theory HaskellLemmaBucket

lemma fun_is_in_assocs:
  "(f x = y) = ((x,y) \<in> set (assocs f))" by (simp add: in_assocs_is_fun)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f x = y) = ((x, y) \<in> set (assocs f))
theory HaskellLemmaBucket

lemma assert_into_when:
  "(assert P) = (when (\<not> P) (haskell_fail []))" by (simp add: assert_def when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert P = when (\<not> P) (haskell_fail [])
theory HaskellLemmaBucket

lemma const_None_empty:
  "const None = Map.empty" by (rule ext, simp add: const_apply)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. const None = (\<lambda>x. None)
theory HaskellLemmaBucket

lemma headM_tailM_Cons:
  "headM (x # xs) = return x"
  "tailM (x # xs) = return xs" by (simp add: headM_def tailM_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. headM (x # xs) = return x &&& tailM (x # xs) = return xs
theory HaskellLemmaBucket

lemma replicateM_mapM:
  "replicateM n f = mapM (\<lambda>x. f) (replicate n ())" by (simp add: replicateM_def mapM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replicateM n f = mapM (\<lambda>x. f) (replicate n ())
theory HaskellLemmaBucket

lemma orList_False:
  "(\<not> orList bs) = (set bs \<subseteq> {False})" apply (induct bs) apply (simp_all add: orList_def foldl_True) apply (case_tac a) apply (simp_all add: orList_def foldl_True) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> orList bs) = (set bs \<subseteq> {False}) proof (prove)
goal (2 subgoals):
 1. (\<not> orList []) = (set [] \<subseteq> {False})
 2. \<And>a bs. (\<not> orList bs) = (set bs \<subseteq> {False}) \<Longrightarrow> (\<not> orList (a # bs)) = (set (a # bs) \<subseteq> {False}) proof (prove)
goal (1 subgoal):
 1. \<And>a bs. foldl (\<or>) False bs = (True \<in> set bs) \<Longrightarrow> (\<not> foldl (\<or>) a bs) = (\<not> a \<and> True \<notin> set bs) proof (prove)
goal (2 subgoals):
 1. \<And>a bs. \<lbrakk>foldl (\<or>) False bs = (True \<in> set bs); a\<rbrakk> \<Longrightarrow> (\<not> foldl (\<or>) a bs) = (\<not> a \<and> True \<notin> set bs)
 2. \<And>a bs. \<lbrakk>foldl (\<or>) False bs = (True \<in> set bs); \<not> a\<rbrakk> \<Longrightarrow> (\<not> foldl (\<or>) a bs) = (\<not> a \<and> True \<notin> set bs) proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma Cons_eq_tails:
  "((xs # xxs) = tails ys) = (ys = xs \<and> xxs = tl (tails ys))" by (case_tac ys, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (xs # xxs = tails ys) = (ys = xs \<and> xxs = tl (tails ys))
theory HaskellLemmaBucket

lemma findM_on_outcome':
  assumes x: "\<And>x xs. \<lbrace>\<lambda>s. Q None s \<and> x \<in> fn s \<and> set xs \<subseteq> fn s\<rbrace> f x
                     \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xs \<subseteq> fn s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace>" apply (induct xs) apply (simp, wp) apply (simp, wp) apply (rule x) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. Q None s \<and> set [] \<subseteq> fn s\<rbrace> findM f [] \<lbrace>Q\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> set (a # xs) \<subseteq> fn s\<rbrace> findM f (a # xs) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> set (a # xs) \<subseteq> fn s\<rbrace> findM f (a # xs) \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>?Q6 a xs\<rbrace> f a \<lbrace>\<lambda>x s. (x \<longrightarrow> Q (Some a) s) \<and> (\<not> x \<longrightarrow> Q None s \<and> set xs \<subseteq> fn s)\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace>; Q None s \<and> a \<in> fn s \<and> set xs \<subseteq> fn s\<rbrakk> \<Longrightarrow> ?Q6 a xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace>; Q None s \<and> a \<in> fn s \<and> set xs \<subseteq> fn s\<rbrakk> \<Longrightarrow> Q None s \<and> a \<in> fn s \<and> set xs \<subseteq> fn s proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma in_set_tailsD: "xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys" apply (induct ys) apply simp apply simp apply (erule disjE) apply simp apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys proof (prove)
goal (2 subgoals):
 1. xs \<in> set (tails []) \<Longrightarrow> set xs \<subseteq> set []
 2. \<And>a ys. \<lbrakk>xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys; xs \<in> set (tails (a # ys))\<rbrakk> \<Longrightarrow> set xs \<subseteq> set (a # ys) proof (prove)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys; xs \<in> set (tails (a # ys))\<rbrakk> \<Longrightarrow> set xs \<subseteq> set (a # ys) proof (prove)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys; xs = a # ys \<or> xs \<in> set (tails ys)\<rbrakk> \<Longrightarrow> set xs \<subseteq> insert a (set ys) proof (prove)
goal (2 subgoals):
 1. \<And>a ys. \<lbrakk>xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys; xs = a # ys\<rbrakk> \<Longrightarrow> set xs \<subseteq> insert a (set ys)
 2. \<And>a ys. \<lbrakk>xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys; xs \<in> set (tails ys)\<rbrakk> \<Longrightarrow> set xs \<subseteq> insert a (set ys) proof (prove)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys; xs \<in> set (tails ys)\<rbrakk> \<Longrightarrow> set xs \<subseteq> insert a (set ys) proof (prove)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>set xs \<subseteq> set ys; xs \<in> set (tails ys)\<rbrakk> \<Longrightarrow> set xs \<subseteq> insert a (set ys) proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma notin_set_tails_set:
  "x \<notin> set xs \<Longrightarrow> \<forall>xs' \<in> set (tails xs). \<forall>x' \<in> set xs'. x \<noteq> x'" by (fastforce dest!: in_set_tailsD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> \<forall>xs'\<in>set (tails xs). \<forall>x'\<in>set xs'. x \<noteq> x'