kings-crown/FVELER_Isabelle huggingface dataset:
theory LemmaBucket

lemma sum_suc_pair: "(\<Sum>(a, b) \<leftarrow> xs. Suc (f a b)) = length xs + (\<Sum>(a, b) \<leftarrow> xs. f a b)" apply (induct xs) by clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(a, b)\<leftarrow>xs. Suc (f a b)) = length xs + (\<Sum>(a, b)\<leftarrow>xs. f a b) proof (prove)
goal (2 subgoals):
 1. (\<Sum>a\<leftarrow>[]. case a of (a, b) \<Rightarrow> Suc (f a b)) = length [] + (\<Sum>a\<leftarrow>[]. case a of (a, b) \<Rightarrow> f a b)
 2. \<And>a xs. (\<Sum>a\<leftarrow>xs. case a of (a, b) \<Rightarrow> Suc (f a b)) = length xs + (\<Sum>a\<leftarrow>xs. case a of (a, b) \<Rightarrow> f a b) \<Longrightarrow> (\<Sum>a\<leftarrow>a # xs. case a of (a, b) \<Rightarrow> Suc (f a b)) = length (a # xs) + (\<Sum>a\<leftarrow>a # xs. case a of (a, b) \<Rightarrow> f a b)
theory LemmaBucket

lemma fold_add_sum: "fold (+) ((map (\<lambda>(a, b). f a b) xs)::nat list) 0 = (\<Sum>(a, b) \<leftarrow> xs. f a b)" apply (subst fold_plus_sum_list_rev) apply (subst sum_list_rev) by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (+) (map (\<lambda>(a, b). f a b) xs) 0 = (\<Sum>(a, b)\<leftarrow>xs. f a b) proof (prove)
goal (1 subgoal):
 1. sum_list (rev (map (\<lambda>(x, y). f x y) xs)) + 0 = (\<Sum>(x, y)\<leftarrow>xs. f x y) proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<leftarrow>xs. f x y) + 0 = (\<Sum>(x, y)\<leftarrow>xs. f x y)
theory LemmaBucket

lemma set_of_enumerate:"card (set (enumerate n xs)) = length xs" by (metis distinct_card distinct_enumerate length_enumerate)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. card (set (enumerate n xs)) = length xs
theory LemmaBucket

lemma collapse_fst: "fst ` (\<lambda>x. (f x, g x)) ` s = f ` s" by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst ` (\<lambda>x. (f x, g x)) ` s = f ` s
theory LemmaBucket

lemma collapse_fst2: "fst ` (\<lambda>(x, y). (f x, g y)) ` s = (\<lambda>x. f (fst x)) ` s" by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst ` (\<lambda>(x, y). (f x, g y)) ` s = (\<lambda>x. f (fst x)) ` s
theory LemmaBucket

lemma card_of_dom_bounded:
  fixes f :: "'a \<Rightarrow> 'b option"
  assumes "finite (UNIV::'a set)"
  shows "card (dom f) \<le> CARD('a)" by (simp add: assms card_mono)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. card (dom f) \<le> CARD('a)
theory LemmaBucket

lemma third_in: "(a, b, c) \<in> S \<Longrightarrow> c \<in> (snd \<circ> snd) ` S" by (metis (erased, opaque_lifting) map_set_in image_comp snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b, c) \<in> S \<Longrightarrow> c \<in> (snd \<circ> snd) ` S
theory LemmaBucket

lemma third_in2: "(a \<in> (snd \<circ> snd) ` (set (enumerate i xs))) = (a \<in> snd ` (set xs))" by (metis map_map map_snd_enumerate set_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<in> (snd \<circ> snd) ` set (enumerate i xs)) = (a \<in> snd ` set xs)
theory LemmaBucket

lemma map_of_enum: "map_of (enumerate n xs) x = Some y \<Longrightarrow> y \<in> set xs" apply (clarsimp) by (metis enumerate_eq_zip in_set_zipE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_of (enumerate n xs) x = Some y \<Longrightarrow> y \<in> set xs proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> set (enumerate n xs) \<Longrightarrow> y \<in> set xs
theory LemmaBucket

lemma map_of_append:
  "(map_of xs ++ map_of ys) x = (case map_of ys x of None \<Rightarrow> map_of xs x | Some x' \<Rightarrow> Some x')" by (simp add: map_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map_of xs ++ map_of ys) x = (case map_of ys x of None \<Rightarrow> map_of xs x | Some x' \<Rightarrow> Some x')
theory LemmaBucket

lemma map_of_append2:
  "(map_of xs ++ map_of ys ++ map_of zs) x =
     (case map_of zs x of None \<Rightarrow> (case map_of ys x of None \<Rightarrow> map_of xs x
                                                     | Some x' \<Rightarrow> Some x')
                        | Some x' \<Rightarrow> Some x')" by (simp add: map_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map_of xs ++ map_of ys ++ map_of zs) x = (case map_of zs x of None \<Rightarrow> case map_of ys x of None \<Rightarrow> map_of xs x | Some x' \<Rightarrow> Some x' | Some x' \<Rightarrow> Some x')
theory LemmaBucket

lemma map_of_in_set_map: "map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z \<Longrightarrow> z \<in> snd ` set xs" proof - assume "map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z" hence "(x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs" using map_of_SomeD by fastforce thus "z \<in> snd ` set xs" using map_set_in by fastforce qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z \<Longrightarrow> z \<in> snd ` set xs proof (state)
goal (1 subgoal):
 1. map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z \<Longrightarrow> z \<in> snd ` set xs proof (state)
this:
map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z

goal (1 subgoal):
 1. map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z \<Longrightarrow> z \<in> snd ` set xs proof (prove)
using this:
map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z

goal (1 subgoal):
 1. (x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs proof (prove)
using this:
map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z
map_of ?xs ?k = Some ?y \<Longrightarrow> (?k, ?y) \<in> set ?xs

goal (1 subgoal):
 1. (x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs proof (state)
this:
(x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs

goal (1 subgoal):
 1. map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z \<Longrightarrow> z \<in> snd ` set xs proof (prove)
using this:
(x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs

goal (1 subgoal):
 1. z \<in> snd ` set xs proof (prove)
using this:
(x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs
(?x \<in> ?f ` ?S) = (\<exists>y\<in>?S. ?f y = ?x)

goal (1 subgoal):
 1. z \<in> snd ` set xs proof (state)
this:
z \<in> snd ` set xs

goal:
No subgoals!
theory LemmaBucket

lemma pair_in_enum: "(a, b) \<in> set (enumerate x ys) \<Longrightarrow> b \<in> set ys" by (metis enumerate_eq_zip in_set_zip2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> set (enumerate x ys) \<Longrightarrow> b \<in> set ys
theory LemmaBucket

lemma distinct_inj:
  "inj f \<Longrightarrow> distinct xs = distinct (map f xs)" apply (induct xs) apply simp apply (simp add: inj_image_mem_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj f \<Longrightarrow> distinct xs = distinct (map f xs) proof (prove)
goal (2 subgoals):
 1. inj f \<Longrightarrow> distinct [] = distinct (map f [])
 2. \<And>a xs. \<lbrakk>inj f \<Longrightarrow> distinct xs = distinct (map f xs); inj f\<rbrakk> \<Longrightarrow> distinct (a # xs) = distinct (map f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>inj f \<Longrightarrow> distinct xs = distinct (map f xs); inj f\<rbrakk> \<Longrightarrow> distinct (a # xs) = distinct (map f (a # xs)) proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma distinct_map_via_ran: "distinct (map fst xs) \<Longrightarrow> ran (map_of xs) = set (map snd xs)" apply (cut_tac xs="map fst xs" and ys="map snd xs" in ran_map_of_zip[symmetric]) apply clarsimp+ by (simp add: ran_distinct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs) \<Longrightarrow> ran (map_of xs) = set (map snd xs) proof (prove)
goal (3 subgoals):
 1. distinct (map fst xs) \<Longrightarrow> length (map fst xs) = length (map snd xs)
 2. distinct (map fst xs) \<Longrightarrow> distinct (map fst xs)
 3. \<lbrakk>distinct (map fst xs); set (map snd xs) = ran (map_of (zip (map fst xs) (map snd xs)))\<rbrakk> \<Longrightarrow> ran (map_of xs) = set (map snd xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst xs); snd ` set xs = ran (map_of (zip (map fst xs) (map snd xs)))\<rbrakk> \<Longrightarrow> ran (map_of xs) = ran (map_of (zip (map fst xs) (map snd xs)))
theory LemmaBucket

lemma in_ran_in_set: "x \<in> ran (map_of xs) \<Longrightarrow> x \<in> set (map snd xs)" by (metis (mono_tags) map_set_in map_of_SomeD ranE set_map snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> ran (map_of xs) \<Longrightarrow> x \<in> set (map snd xs)
theory LemmaBucket

lemma none_some_map2: "the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) = ran f" apply (rule subset_antisym) apply clarsimp apply (case_tac "f x", simp_all) apply (simp add: ranI) apply clarsimp apply (subst none_some_map[symmetric]) apply clarsimp+ apply (erule ranE) by (metis range_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) = ran f proof (prove)
goal (2 subgoals):
 1. the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) \<subseteq> ran f
 2. ran f \<subseteq> the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<not> Option.is_none (f x) \<Longrightarrow> the (f x) \<in> ran f
 2. ran f \<subseteq> the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) proof (prove)
goal (2 subgoals):
 1. \<And>x a. f x = Some a \<Longrightarrow> a \<in> ran f
 2. ran f \<subseteq> the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) proof (prove)
goal (1 subgoal):
 1. ran f \<subseteq> the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> ran f \<Longrightarrow> x \<in> the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> ran f \<Longrightarrow> None \<notin> Set.filter (\<lambda>s. \<not> Option.is_none s) (range f)
 2. \<And>x. x \<in> ran f \<Longrightarrow> Some x \<in> Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> ran f \<Longrightarrow> Some x \<in> range f proof (prove)
goal (1 subgoal):
 1. \<And>x xa. f xa = Some x \<Longrightarrow> Some x \<in> range f
theory LemmaBucket

lemma prop_map_of_prop:"\<lbrakk>\<forall>z \<in> set xs. P (g z); map_of (map (\<lambda>x. (f x, g x)) xs) y = Some a\<rbrakk> \<Longrightarrow> P a" using map_of_SomeD by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>z\<in>set xs. P (g z); map_of (map (\<lambda>x. (f x, g x)) xs) y = Some a\<rbrakk> \<Longrightarrow> P a proof (prove)
using this:
map_of ?xs ?k = Some ?y \<Longrightarrow> (?k, ?y) \<in> set ?xs

goal (1 subgoal):
 1. \<lbrakk>\<forall>z\<in>set xs. P (g z); map_of (map (\<lambda>x. (f x, g x)) xs) y = Some a\<rbrakk> \<Longrightarrow> P a
theory LemmaBucket

lemma insert_strip: "x \<noteq> y \<Longrightarrow> (x \<in> insert y S) = (x \<in> S)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (x \<in> insert y S) = (x \<in> S)
theory LemmaBucket

lemma dom_map_add: "dom ys = A \<Longrightarrow> dom (xs ++ ys) = A \<union> dom xs" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom ys = A \<Longrightarrow> dom (xs ++ ys) = A \<union> dom xs
theory LemmaBucket

lemma set_compre_unwrap: "({x. P x} \<subseteq> S) = (\<forall>x. P x \<longrightarrow> x \<in> S)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({x. P x} \<subseteq> S) = (\<forall>x. P x \<longrightarrow> x \<in> S)
theory LemmaBucket

lemma map_add_same: "\<lbrakk>xs = ys; zs = ws\<rbrakk> \<Longrightarrow> xs ++ zs = ys ++ ws" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = ys; zs = ws\<rbrakk> \<Longrightarrow> xs ++ zs = ys ++ ws
theory LemmaBucket

lemma map_add_find_left: "n k = None \<Longrightarrow> (m ++ n) k = m k" by (simp add:map_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n k = None \<Longrightarrow> (m ++ n) k = m k
theory LemmaBucket

lemma map_length_split_triple:
  "map (length \<circ> (\<lambda>(a, b, c). P a b c # map (f a b c) (Q a b c))) xs =
     map (\<lambda>(a, b, c). 1 + length (Q a b c)) xs" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map (length \<circ> (\<lambda>(a, b, c). P a b c # map (f a b c) (Q a b c))) xs = map (\<lambda>(a, b, c). 1 + length (Q a b c)) xs
theory LemmaBucket

lemma sum_suc_triple: "(\<Sum>(a, b, c)\<leftarrow>xs. Suc (f a b c)) = length xs + (\<Sum>(a, b, c)\<leftarrow>xs. f a b c)" by (induct xs; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(a, b, c)\<leftarrow>xs. Suc (f a b c)) = length xs + (\<Sum>(a, b, c)\<leftarrow>xs. f a b c)
theory LemmaBucket

lemma sum_enumerate: "(\<Sum>(a, b)\<leftarrow>enumerate n xs. P b) = (\<Sum>b\<leftarrow>xs. P b)" by (induct xs arbitrary:n; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(a, b)\<leftarrow>enumerate n xs. P b) = sum_list (map P xs)
theory LemmaBucket

lemma dom_map_fold:"dom (fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) ms) = dom ms \<union> set (map f xs)" by (induct xs arbitrary:f g ms; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) ms) = dom ms \<union> set (map f xs)
theory LemmaBucket

lemma list_ran_prop:"map_of (map (\<lambda>x. (f x, g x)) xs) i = Some t \<Longrightarrow> \<exists>x \<in> set xs. g x = t" by (induct xs arbitrary:f g t i; clarsimp split:if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>x. (f x, g x)) xs) i = Some t \<Longrightarrow> \<exists>x\<in>set xs. g x = t
theory LemmaBucket

lemma in_set_enumerate_eq2:"(a, b) \<in> set (enumerate n xs) \<Longrightarrow> (b = xs ! (a - n))" by (simp add: in_set_enumerate_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> set (enumerate n xs) \<Longrightarrow> b = xs ! (a - n)
theory LemmaBucket

lemma subset_eq_notI: "\<lbrakk>a\<in> B;a\<notin> C\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> C" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> B; a \<notin> C\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> C
theory LemmaBucket

lemma nat_divide_less_eq:
  fixes b :: nat
  shows "0 < c \<Longrightarrow> (b div c < a) = (b < a * c)" using td_gal_lt by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (b div c < a) = (b < a * c) proof (prove)
using this:
0 < ?c \<Longrightarrow> (?a < ?b * ?c) = (?a div ?c < ?b)

goal (1 subgoal):
 1. 0 < c \<Longrightarrow> (b div c < a) = (b < a * c)
theory LemmaBucket

lemma strengthen_imp_same_first_conj:
  "(b \<and> (a \<longrightarrow> c) \<and> (a' \<longrightarrow> c')) \<Longrightarrow> ((a \<longrightarrow> b \<and> c) \<and> (a' \<longrightarrow> b \<and> c'))" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<and> (a \<longrightarrow> c) \<and> (a' \<longrightarrow> c') \<Longrightarrow> (a \<longrightarrow> b \<and> c) \<and> (a' \<longrightarrow> b \<and> c')
theory LemmaBucket

lemma conj_impD:
  "a \<and> b \<Longrightarrow> a \<longrightarrow> b" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<and> b \<Longrightarrow> a \<longrightarrow> b
theory LemmaBucket

lemma set_list_mem_nonempty:
  "x \<in> set xs \<Longrightarrow> xs \<noteq> []" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> xs \<noteq> []
theory LemmaBucket

lemma strenghten_False_imp:
  "\<not>P \<Longrightarrow> P \<longrightarrow> Q" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> P \<longrightarrow> Q
theory LemmaBucket

lemma None_in_range_Some [simp]:
  "(None \<in> range Some) = False" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (None \<in> range Some) = False
theory LemmaBucket

lemma foldl_fun_or_alt:
  "foldl (\<lambda>x y. x \<or> f y) b ls = foldl (\<or>) b (map f ls)" apply (induct ls) apply clarsimp apply clarsimp by (simp add: foldl_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>x y. x \<or> f y) b ls = foldl (\<or>) b (map f ls) proof (prove)
goal (2 subgoals):
 1. foldl (\<lambda>x y. x \<or> f y) b [] = foldl (\<or>) b (map f [])
 2. \<And>a ls. foldl (\<lambda>x y. x \<or> f y) b ls = foldl (\<or>) b (map f ls) \<Longrightarrow> foldl (\<lambda>x y. x \<or> f y) b (a # ls) = foldl (\<or>) b (map f (a # ls)) proof (prove)
goal (1 subgoal):
 1. \<And>a ls. foldl (\<lambda>x y. x \<or> f y) b ls = foldl (\<or>) b (map f ls) \<Longrightarrow> foldl (\<lambda>x y. x \<or> f y) b (a # ls) = foldl (\<or>) b (map f (a # ls)) proof (prove)
goal (1 subgoal):
 1. \<And>a ls. foldl (\<lambda>x y. x \<or> f y) b ls = foldl (\<or>) b (map f ls) \<Longrightarrow> foldl (\<lambda>x y. x \<or> f y) (b \<or> f a) ls = foldl (\<or>) (b \<or> f a) (map f ls)
theory LemmaBucket

lemma sorted_imp_sorted_filter:
  "sorted xs \<Longrightarrow> sorted (filter P xs)" by (metis filter_sort sorted_sort sorted_sort_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sorted xs \<Longrightarrow> sorted (filter P xs)
theory LemmaBucket

lemma sorted_list_of_set_already_sorted:
  "\<lbrakk> distinct xs; sorted xs \<rbrakk> \<Longrightarrow> sorted_list_of_set (set xs) = xs" by (simp add: sorted_list_of_set_sort_remdups distinct_remdups_id sorted_sort_id)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; sorted xs\<rbrakk> \<Longrightarrow> sorted_list_of_set (set xs) = xs
theory LemmaBucket

lemma inj_on_domD: "\<lbrakk>inj_on f (dom f); f x = Some z; f y = Some z\<rbrakk> \<Longrightarrow> x = y" by (erule inj_onD) clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f x = Some z; f y = Some z\<rbrakk> \<Longrightarrow> x = y
theory LemmaBucket

lemma not_emptyI:
  "\<And>x A B. \<lbrakk>x\<in>A; x\<in>B\<rbrakk> \<Longrightarrow> A \<inter> B \<noteq> {}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x A B. \<lbrakk>x \<in> A; x \<in> B\<rbrakk> \<Longrightarrow> A \<inter> B \<noteq> {}
theory LemmaBucket

lemma add_mask_lower_bits2:
  "\<lbrakk>is_aligned (x :: 'a :: len word) n; p && ~~ mask n = 0\<rbrakk> \<Longrightarrow> x + p && ~~ mask n = x" apply (subst word_plus_and_or_coroll) apply (simp add: aligned_mask_disjoint and_mask_0_iff_le_mask) apply (clarsimp simp: bit.conj_disj_distrib2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; p && ~~ mask n = 0\<rbrakk> \<Longrightarrow> x + p && ~~ mask n = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; p && ~~ mask n = 0\<rbrakk> \<Longrightarrow> x && p = 0
 2. \<lbrakk>is_aligned x n; p && ~~ mask n = 0\<rbrakk> \<Longrightarrow> (x || p) && ~~ mask n = x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; p && ~~ mask n = 0\<rbrakk> \<Longrightarrow> (x || p) && ~~ mask n = x proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma if3_fold2:
  "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" by (rule z3_rule)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then x else if Q then x else y) = (if P \<or> Q then x else y)
theory LemmaBucket

lemma inter_UNIV_minus[simp]:
  "x \<inter> (UNIV - y) = x-y" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<inter> (UNIV - y) = x - y
theory LemmaBucket

lemma imp_and_strg: "Q \<and> C \<longrightarrow> (A \<longrightarrow> Q \<and> C) \<and> C" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q \<and> C \<longrightarrow> (A \<longrightarrow> Q \<and> C) \<and> C
theory LemmaBucket

lemma cases_conj_strg: "A \<and> B \<longrightarrow> (P \<and> A) \<or> (\<not> P \<and> B)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<and> B \<longrightarrow> P \<and> A \<or> \<not> P \<and> B
theory ListLibLemmas

lemma psorted_Cons: "psorted (x#xs) = (psorted xs & (\<forall> y \<in> set xs. less x y))" apply (rule iffI) apply (erule psorted.cases,simp) apply clarsimp apply (rule psorted.Cons,clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. psorted (x # xs) = (psorted xs \<and> (\<forall>y\<in>set xs. less x y)) proof (prove)
goal (2 subgoals):
 1. psorted (x # xs) \<Longrightarrow> psorted xs \<and> (\<forall>y\<in>set xs. less x y)
 2. psorted xs \<and> (\<forall>y\<in>set xs. less x y) \<Longrightarrow> psorted (x # xs) proof (prove)
goal (2 subgoals):
 1. \<And>xsa xa. \<lbrakk>x # xs = xa # xsa; \<forall>y\<in>set xsa. less xa y; psorted xsa\<rbrakk> \<Longrightarrow> psorted xs \<and> (\<forall>y\<in>set xs. less x y)
 2. psorted xs \<and> (\<forall>y\<in>set xs. less x y) \<Longrightarrow> psorted (x # xs) proof (prove)
goal (1 subgoal):
 1. psorted xs \<and> (\<forall>y\<in>set xs. less x y) \<Longrightarrow> psorted (x # xs) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma pinsort_set: "set (pinsort a xs) = insert a (set xs)" apply (induct xs) apply simp apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (pinsort a xs) = insert a (set xs) proof (prove)
goal (2 subgoals):
 1. set (pinsort a []) = insert a (set [])
 2. \<And>aa xs. set (pinsort a xs) = insert a (set xs) \<Longrightarrow> set (pinsort a (aa # xs)) = insert a (set (aa # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. set (pinsort a xs) = insert a (set xs) \<Longrightarrow> set (pinsort a (aa # xs)) = insert a (set (aa # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. set (pinsort a xs) = insert a (set xs) \<Longrightarrow> \<not> less a aa \<longrightarrow> insert aa (insert a (set xs)) = insert a (insert aa (set xs)) proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma all_comp': "R x y \<Longrightarrow> \<not>less x y \<Longrightarrow> less y x" apply (cut_tac x=x and y=y in all_comp,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R x y; \<not> less x y\<rbrakk> \<Longrightarrow> less y x proof (prove)
goal:
No subgoals!
theory ListLibLemmas

lemma psort_set: "set (psort xs) = set xs" apply (simp add: psort_def) apply (induct xs) apply simp apply (simp add: pinsort_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (psort xs) = set xs proof (prove)
goal (1 subgoal):
 1. set (foldr pinsort xs []) = set xs proof (prove)
goal (2 subgoals):
 1. set (foldr pinsort [] []) = set []
 2. \<And>a xs. set (foldr pinsort xs []) = set xs \<Longrightarrow> set (foldr pinsort (a # xs) []) = set (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. set (foldr pinsort xs []) = set xs \<Longrightarrow> set (foldr pinsort (a # xs) []) = set (a # xs) proof (prove)
goal:
No subgoals!