kings-crown/FVELER_Isabelle huggingface dataset:
theory LemmaBucket

lemma isRight_case_sum: "isRight x \<Longrightarrow> case_sum f g x = g (theRight x)" by (cases x; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isRight x \<Longrightarrow> (case x of Inl x \<Rightarrow> f x | Inr x \<Rightarrow> g x) = g (theRight x)
theory LemmaBucket

lemma enumerate_append:"enumerate i (xs @ ys) = enumerate i xs @ enumerate (i + length xs) ys" apply (induct xs arbitrary:ys i) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enumerate i (xs @ ys) = enumerate i xs @ enumerate (i + length xs) ys proof (prove)
goal (2 subgoals):
 1. \<And>ys i. enumerate i ([] @ ys) = enumerate i [] @ enumerate (i + length []) ys
 2. \<And>a xs ys i. (\<And>ys i. enumerate i (xs @ ys) = enumerate i xs @ enumerate (i + length xs) ys) \<Longrightarrow> enumerate i ((a # xs) @ ys) = enumerate i (a # xs) @ enumerate (i + length (a # xs)) ys proof (prove)
goal:
No subgoals!
theory LemmaBucket

lemma enumerate_bound:"(a, b) \<in> set (enumerate n xs) \<Longrightarrow> a < n + length xs" by (metis add.commute in_set_enumerate_eq prod.sel(1))

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

lemma enumerate_exceed:"(n + length xs, b) \<notin> set (enumerate n xs)" by (metis enumerate_bound less_not_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n + length xs, b) \<notin> set (enumerate n xs)
theory LemmaBucket

lemma all_pair_unwrap:"(\<forall>a. P (fst a) (snd a)) = (\<forall>a b. P a b)" by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. P (fst a) (snd a)) = (\<forall>a b. P a b)
theory LemmaBucket

lemma if_fold[simp]:"(if P then Q else if P then R else S) = (if P then Q else S)" by presburger

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then Q else if P then R else S) = (if P then Q else S)
theory LemmaBucket

lemma disjoint_subset_both:"\<lbrakk>A' \<subseteq> A; B' \<subseteq> B; A \<inter> B = {}\<rbrakk> \<Longrightarrow> A' \<inter> B' = {}" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A' \<subseteq> A; B' \<subseteq> B; A \<inter> B = {}\<rbrakk> \<Longrightarrow> A' \<inter> B' = {}
theory LemmaBucket

lemma union_split: "\<lbrakk>A \<inter> C = {}; B \<inter> C = {}\<rbrakk> \<Longrightarrow> (A \<union> B) \<inter> C = {}" by (simp add: inf_sup_distrib2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> C = {}; B \<inter> C = {}\<rbrakk> \<Longrightarrow> (A \<union> B) \<inter> C = {}
theory LemmaBucket

lemma dom_expand: "dom (\<lambda>x. if P x then Some y else None) = {x. P x}" using if_option_Some by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if P x then Some y else None) = {x. P x} proof (prove)
using this:
((if ?P then None else Some ?x) = Some ?y) = (\<not> ?P \<and> ?x = ?y)

goal (1 subgoal):
 1. dom (\<lambda>x. if P x then Some y else None) = {x. P x}
theory LemmaBucket

lemma range_translate: "(range f = range g) = ((\<forall>x. \<exists>y. f x = g y) \<and> (\<forall>x. \<exists>y. f y = g x))" by (rule iffI,
       rule conjI,
        clarsimp,
        blast,
       clarsimp,
       metis f_inv_into_f range_eqI,
      clarsimp,
      subst set_eq_subset,
      rule conjI,
       clarsimp,
       rename_tac arg,
       erule_tac x=arg and P="\<lambda>x. (\<exists>y. f x = g y)" in allE,
       clarsimp,
      clarsimp,
      rename_tac arg,
      erule_tac x=arg and P="\<lambda>x. (\<exists>y. f y = g x)" in allE,
      clarsimp,
      metis range_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (range f = range g) = ((\<forall>x. \<exists>y. f x = g y) \<and> (\<forall>x. \<exists>y. f y = g x))
theory LemmaBucket

lemma ran_expand: "\<exists>x. P x \<Longrightarrow> ran (\<lambda>x. if P x then Some y else None) = {y}" by (rule subset_antisym,
       (clarsimp simp:ran_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. P x \<Longrightarrow> ran (\<lambda>x. if P x then Some y else None) = {y}
theory LemmaBucket

lemma map_upd_expand: "f(x \<mapsto> y) = f ++ (\<lambda>z. if z = x then Some y else None)" by (rule ext, rename_tac w,
      case_tac "w = x",
       simp,
      simp add:map_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f(x \<mapsto> y) = f ++ (\<lambda>z. if z = x then Some y else None)
theory LemmaBucket

lemma map_upd_subI: "\<lbrakk>f \<subseteq>\<^sub>m g; f x = None\<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m g(x \<mapsto> y)" by (rule_tac f="\<lambda>i. if i = x then Some y else None" in map_add_le_mapE,
      simp add:map_le_def,
      rule ballI, rename_tac a,
      rule conjI,
       erule_tac x=x in ballE,
        clarsimp,
        erule disjE,
         clarsimp,
        clarsimp simp:map_add_def,
       clarsimp,
       erule disjE,
        clarsimp,
       clarsimp simp:map_add_def,
      clarsimp simp:map_add_def,
      erule_tac x=a in ballE,
       erule disjE,
        (case_tac "g a"; simp_all),
       clarsimp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<subseteq>\<^sub>m g; f x = None\<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m g(x \<mapsto> y)
theory LemmaBucket

lemma all_ext: "\<forall>x. f x = g x \<Longrightarrow> f = g" by presburger

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. f x = g x \<Longrightarrow> f = g
theory LemmaBucket

lemma conjI2: "\<lbrakk>B; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A \<and> B" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A \<and> B
theory LemmaBucket

lemma Least2: "\<lbrakk>\<not>P 0; \<not>P 1; P (2::nat)\<rbrakk> \<Longrightarrow> Least P = 2" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; P 2\<rbrakk> \<Longrightarrow> Least P = 2
theory LemmaBucket

lemma Least3: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; P (3::nat)\<rbrakk> \<Longrightarrow> Least P = 3" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; P 3\<rbrakk> \<Longrightarrow> Least P = 3
theory LemmaBucket

lemma Least4: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; P (4::nat)\<rbrakk> \<Longrightarrow> Least P = 4" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; P 4\<rbrakk> \<Longrightarrow> Least P = 4
theory LemmaBucket

lemma Least5: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; P (5::nat)\<rbrakk> \<Longrightarrow> Least P = 5" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; P 5\<rbrakk> \<Longrightarrow> Least P = 5
theory LemmaBucket

lemma Least6: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; P (6::nat)\<rbrakk> \<Longrightarrow> Least P = 6" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; P 6\<rbrakk> \<Longrightarrow> Least P = 6
theory LemmaBucket

lemma Least7: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; P (7::nat)\<rbrakk> \<Longrightarrow> Least P = 7" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; P 7\<rbrakk> \<Longrightarrow> Least P = 7
theory LemmaBucket

lemma Least8: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; P (8::nat)\<rbrakk> \<Longrightarrow> Least P = 8" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; P 8\<rbrakk> \<Longrightarrow> Least P = 8
theory LemmaBucket

lemma Least9: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; P (9::nat)\<rbrakk> \<Longrightarrow> Least P = 9" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; P 9\<rbrakk> \<Longrightarrow> Least P = 9
theory LemmaBucket

lemma Least10: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; P (10::nat)\<rbrakk> \<Longrightarrow> Least P
                 = 10" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; P 10\<rbrakk> \<Longrightarrow> Least P = 10
theory LemmaBucket

lemma Least11: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; P (11::nat)\<rbrakk> \<Longrightarrow>
                 Least P = 11" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; P 11\<rbrakk> \<Longrightarrow> Least P = 11
theory LemmaBucket

lemma Least12: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; P
                 (12::nat)\<rbrakk> \<Longrightarrow> Least P = 12" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; P 12\<rbrakk> \<Longrightarrow> Least P = 12
theory LemmaBucket

lemma Least13: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; P
                 (13::nat)\<rbrakk> \<Longrightarrow> Least P = 13" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; P 13\<rbrakk> \<Longrightarrow> Least P = 13
theory LemmaBucket

lemma Least15: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; P (15::nat)\<rbrakk> \<Longrightarrow> Least P = 15" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; P 15\<rbrakk> \<Longrightarrow> Least P = 15
theory LemmaBucket

lemma Least16: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; P (16::nat)\<rbrakk> \<Longrightarrow> Least P = 16" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; P 16\<rbrakk> \<Longrightarrow> Least P = 16
theory LemmaBucket

lemma Least17: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; P (17::nat)\<rbrakk> \<Longrightarrow> Least P = 17" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; P 17\<rbrakk> \<Longrightarrow> Least P = 17
theory LemmaBucket

lemma Least18: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; P (18::nat)\<rbrakk> \<Longrightarrow> Least P = 18" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; P 18\<rbrakk> \<Longrightarrow> Least P = 18
theory LemmaBucket

lemma Least19: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; P (19::nat)\<rbrakk> \<Longrightarrow> Least P = 19" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; P 19\<rbrakk> \<Longrightarrow> Least P = 19
theory LemmaBucket

lemma Least20: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; P (20::nat)\<rbrakk> \<Longrightarrow> Least P = 20" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; P 20\<rbrakk> \<Longrightarrow> Least P = 20
theory LemmaBucket

lemma Least21: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; P (21::nat)\<rbrakk> \<Longrightarrow> Least P = 21" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; P 21\<rbrakk> \<Longrightarrow> Least P = 21
theory LemmaBucket

lemma Least22: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; P (22::nat)\<rbrakk> \<Longrightarrow> Least P
                 = 22" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; \<not> P 21; P 22\<rbrakk> \<Longrightarrow> Least P = 22
theory LemmaBucket

lemma Least23: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; P (23::nat)\<rbrakk> \<Longrightarrow>
                 Least P = 23" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; \<not> P 21; \<not> P 22; P 23\<rbrakk> \<Longrightarrow> Least P = 23
theory LemmaBucket

lemma Least24: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; P
                 (24::nat)\<rbrakk> \<Longrightarrow> Least P = 24" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; \<not> P 21; \<not> P 22; \<not> P 23; P 24\<rbrakk> \<Longrightarrow> Least P = 24
theory LemmaBucket

lemma Least26: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; \<not>P
                 25; P (26::nat)\<rbrakk> \<Longrightarrow> Least P = 26" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; \<not> P 21; \<not> P 22; \<not> P 23; \<not> P 24; \<not> P 25; P 26\<rbrakk> \<Longrightarrow> Least P = 26
theory LemmaBucket

lemma Least27: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; \<not>P
                 25; \<not>P 26; P (27::nat)\<rbrakk> \<Longrightarrow> Least P = 27" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; \<not> P 21; \<not> P 22; \<not> P 23; \<not> P 24; \<not> P 25; \<not> P 26; P 27\<rbrakk> \<Longrightarrow> Least P = 27
theory LemmaBucket

lemma Least28: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P
                 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; \<not>P
                 25; \<not>P 26; \<not>P 27; P (28::nat)\<rbrakk> \<Longrightarrow> Least P = 28" by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P 0; \<not> P 1; \<not> P 2; \<not> P 3; \<not> P 4; \<not> P 5; \<not> P 6; \<not> P 7; \<not> P 8; \<not> P 9; \<not> P 10; \<not> P 11; \<not> P 12; \<not> P 13; \<not> P 14; \<not> P 15; \<not> P 16; \<not> P 17; \<not> P 18; \<not> P 19; \<not> P 20; \<not> P 21; \<not> P 22; \<not> P 23; \<not> P 24; \<not> P 25; \<not> P 26; \<not> P 27; P 28\<rbrakk> \<Longrightarrow> Least P = 28
theory LemmaBucket

lemma map_add_discard: "\<not> cond x \<Longrightarrow> (f ++ (\<lambda>x. if cond x then (g x) else None)) x = f x" by (simp add: map_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> cond x \<Longrightarrow> (f ++ (\<lambda>x. if cond x then g x else None)) x = f x
theory LemmaBucket

lemma dom_split:"\<lbrakk>\<forall>x \<in> S. \<exists>y. f x = Some y; \<forall>x. x \<notin> S \<longrightarrow> f x = None\<rbrakk> \<Longrightarrow> dom f = S" by (auto simp:dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>S. \<exists>y. f x = Some y; \<forall>x. x \<notin> S \<longrightarrow> f x = None\<rbrakk> \<Longrightarrow> dom f = S
theory LemmaBucket

lemma map_set_in: "x \<in> f ` S = (\<exists>y\<in>S. f y = x)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> f ` S) = (\<exists>y\<in>S. f y = x)
theory LemmaBucket

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

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

lemma sum_suc: "(\<Sum>x \<leftarrow> xs. Suc (f x)) = length xs + (\<Sum>x \<leftarrow> xs. f x)" apply (induct xs) by clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>xs. Suc (f x)) = length xs + sum_list (map f xs) proof (prove)
goal (2 subgoals):
 1. (\<Sum>x\<leftarrow>[]. Suc (f x)) = length [] + sum_list (map f [])
 2. \<And>a xs. (\<Sum>x\<leftarrow>xs. Suc (f x)) = length xs + sum_list (map f xs) \<Longrightarrow> (\<Sum>x\<leftarrow>a # xs. Suc (f x)) = length (a # xs) + sum_list (map f (a # xs))