[STATEMENT]
lemma list_slice_nth_nth: "
  \<lbrakk> m < length xs div k; n < k \<rbrakk> \<Longrightarrow>
  (list_slice xs k) ! m ! n = xs ! (m * k + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length xs div k; n < k\<rbrakk> \<Longrightarrow> list_slice xs k ! m ! n = xs ! (m * k + n)
[PROOF STEP]
apply (frule list_slice_nth_length[of m xs k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length xs div k; n < k; length (list_slice xs k ! m) = k\<rbrakk> \<Longrightarrow> list_slice xs k ! m ! n = xs ! (m * k + n)
[PROOF STEP]
apply (simp add: list_slice_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_nth_nth_rev: "
  n < length xs div k * k \<Longrightarrow>
  (list_slice xs k) ! (n div k) ! (n mod k) = xs ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs div k * k \<Longrightarrow> list_slice xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (case_tac "k = 0", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs div k * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (simp add: list_slice_nth_nth div_less_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_eq_list_slice_take: "
  list_slice (xs \<down> (length xs div k * k)) k = list_slice xs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice (xs \<down> (length xs div k * k)) k = list_slice xs k
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> list_slice (xs \<down> (length xs div k * k)) k = list_slice xs k
 2. k \<noteq> 0 \<Longrightarrow> list_slice (xs \<down> (length xs div k * k)) k = list_slice xs k
[PROOF STEP]
apply (simp add: list_slice_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> list_slice (xs \<down> (length xs div k * k)) k = list_slice xs k
[PROOF STEP]
apply (simp add: list_eq_iff list_slice_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<forall>i<length xs div k. length (list_slice (xs \<down> (length xs div k * k)) k ! i) = length (list_slice xs k ! i) \<and> (\<forall>ia<length (list_slice (xs \<down> (length xs div k * k)) k ! i). list_slice (xs \<down> (length xs div k * k)) k ! i ! ia = list_slice xs k ! i ! ia)
[PROOF STEP]
apply (simp add: div_mult_le min_eqR list_slice_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<forall>i<length xs div k. min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (clarify, rename_tac i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (subgoal_tac "k \<le> length xs div k * k - i * k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
 2. \<And>i. \<lbrakk>0 < k; i < length xs div k\<rbrakk> \<Longrightarrow> k \<le> length xs div k * k - i * k
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k\<rbrakk> \<Longrightarrow> k \<le> length xs div k * k - i * k
 2. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (drule_tac m=i in Suc_leI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; Suc i \<le> length xs div k\<rbrakk> \<Longrightarrow> k \<le> length xs div k * k - i * k
 2. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (drule mult_le_mono1[of _ _ k])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; Suc i * k \<le> length xs div k * k\<rbrakk> \<Longrightarrow> k \<le> length xs div k * k - i * k
 2. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (subgoal_tac "length xs div k * k - i * k \<le> length xs - i * k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k; length xs div k * k - i * k \<le> length xs - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
 2. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> length xs div k * k - i * k \<le> length xs - i * k
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k\<rbrakk> \<Longrightarrow> length xs div k * k - i * k \<le> length xs - i * k
 2. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k; length xs div k * k - i * k \<le> length xs - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (simp add: div_mult_cancel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k; length xs div k * k - i * k \<le> length xs - i * k\<rbrakk> \<Longrightarrow> min (length xs div k * k - i * k) k = min (length xs - i * k) k \<and> (\<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs \<up> (i * k) ! ia)
[PROOF STEP]
apply (simp add: min_eqR)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k; i < length xs div k; k \<le> length xs div k * k - i * k; length xs div k * k - i * k \<le> length xs - i * k\<rbrakk> \<Longrightarrow> \<forall>ia. ia < length xs div k * k - i * k \<and> ia < k \<longrightarrow> xs \<down> (length xs div k * k) ! (i * k + ia) = xs ! (i * k + ia)
[PROOF STEP]
by (simp add: less_diff_conv)


[STATEMENT]
lemma list_slice_append_mult: "
  \<And>xs. length xs = m * k \<Longrightarrow>
  list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. length xs = m * k \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>length xs = m * k; k = 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
 2. \<And>xs. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
[PROOF STEP]
apply (simp add: list_slice_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
[PROOF STEP]
apply (induct m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>length xs = 0 * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
 2. \<And>m xs. \<lbrakk>\<And>xs. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k; length xs = Suc m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
[PROOF STEP]
apply (simp add: list_slice_Nil)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m xs. \<lbrakk>\<And>xs. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k; length xs = Suc m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
[PROOF STEP]
apply (simp add: list_slice_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m xs. \<lbrakk>\<And>xs. length xs = m * k \<Longrightarrow> list_slice_aux (xs @ ys) k (m + length ys div k) = list_slice_aux xs k m @ list_slice_aux ys k (length ys div k); length xs = k + m * k; 0 < k\<rbrakk> \<Longrightarrow> list_slice_aux (xs @ ys) k ((k + m * k + length ys) div k) = xs \<down> k # list_slice_aux (xs \<up> k) k m @ list_slice_aux ys k (length ys div k)
[PROOF STEP]
apply (simp add: list_slice_def add.commute[of _ "length ys"] add.assoc[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_append_mod: "
  length xs mod k = 0 \<Longrightarrow>
  list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs mod k = 0 \<Longrightarrow> list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k
[PROOF STEP]
by (auto intro: list_slice_append_mult elim!: dvdE)


[STATEMENT]
lemma list_slice_div_eq_1[rule_format]: "
  length xs div k = Suc 0 \<Longrightarrow> list_slice xs k = [take k xs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs div k = Suc 0 \<Longrightarrow> list_slice xs k = [xs \<down> k]
[PROOF STEP]
by (simp add: list_slice_def)


[STATEMENT]
lemma list_slice_div_eq_Suc[rule_format]: "
  length xs div k = Suc n \<Longrightarrow>
  list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs div k = Suc n \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (case_tac "k = 0", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs div k = Suc n; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (subgoal_tac "n * k < length xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; n * k < length xs\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
 2. \<lbrakk>length xs div k = Suc n; k \<noteq> 0\<rbrakk> \<Longrightarrow> n * k < length xs
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs div k = Suc n; k \<noteq> 0\<rbrakk> \<Longrightarrow> n * k < length xs
 2. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; n * k < length xs\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (case_tac "length xs = 0", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; length xs \<noteq> 0\<rbrakk> \<Longrightarrow> n * k < length xs
 2. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; n * k < length xs\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (drule_tac arg_cong[where f="\<lambda>x. x - Suc 0"], drule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k \<noteq> 0; length xs \<noteq> 0; Suc n - Suc 0 = length xs div k - Suc 0\<rbrakk> \<Longrightarrow> n * k < length xs
 2. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; n * k < length xs\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (simp add: diff_mult_distrib div_mult_cancel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; n * k < length xs\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (insert list_slice_append_mult[of "take (n * k) xs" n k "drop (n * k) xs"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs div k = Suc n; k \<noteq> 0; n * k < length xs; length (xs \<down> (n * k)) = n * k \<Longrightarrow> list_slice (xs \<down> (n * k) @ xs \<up> (n * k)) k = list_slice (xs \<down> (n * k)) k @ list_slice (xs \<up> (n * k)) k\<rbrakk> \<Longrightarrow> list_slice xs k = list_slice (xs \<down> (n * k)) k @ [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (simp add: min_eqR)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs div k = Suc n; 0 < k; n * k < length xs; list_slice xs k = list_slice (xs \<down> (n * k)) k @ list_slice (xs \<up> (n * k)) k\<rbrakk> \<Longrightarrow> list_slice (xs \<up> (n * k)) k = [xs \<up> (n * k) \<down> k]
[PROOF STEP]
apply (rule list_slice_div_eq_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs div k = Suc n; 0 < k; n * k < length xs; list_slice xs k = list_slice (xs \<down> (n * k)) k @ list_slice (xs \<up> (n * k)) k\<rbrakk> \<Longrightarrow> length (xs \<up> (n * k)) div k = Suc 0
[PROOF STEP]
apply (simp add: div_diff_mult_self1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice2_mod_0: "
  length xs mod k = 0 \<Longrightarrow> list_slice2 xs k = list_slice xs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs mod k = 0 \<Longrightarrow> list_slice2 xs k = list_slice xs k
[PROOF STEP]
by (simp add: list_slice2_def)


[STATEMENT]
lemma list_slice2_mod_gr0: "
  0 < length xs mod k \<Longrightarrow> list_slice2 xs k = list_slice xs k @ [xs \<up> (length xs div k * k)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length xs mod k \<Longrightarrow> list_slice2 xs k = list_slice xs k @ [xs \<up> (length xs div k * k)]
[PROOF STEP]
by (simp add: list_slice2_def)


[STATEMENT]
lemma list_slice2_length: "
  length (list_slice2 xs k) = (
  if length xs mod k = 0 then length xs div k else Suc (length xs div k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list_slice2 xs k) = (if length xs mod k = 0 then length xs div k else Suc (length xs div k))
[PROOF STEP]
by (simp add: list_slice2_def list_slice_length)


[STATEMENT]
lemma list_slice2_0: "
  list_slice2 xs 0 = (if (length xs = 0) then [] else [xs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice2 xs 0 = (if length xs = 0 then [] else [xs])
[PROOF STEP]
by (simp add: list_slice2_def list_slice_0)


[STATEMENT]
lemma list_slice2_1: "list_slice2 xs (Suc 0) = map (\<lambda>x. [x]) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice2 xs (Suc 0) = map (\<lambda>x. [x]) xs
[PROOF STEP]
by (simp add: list_slice2_def list_slice_1)


[STATEMENT]
lemma list_slice2_le: "
  length xs \<le> k \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> k \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs \<le> k; k = 0\<rbrakk> \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
 2. \<lbrakk>length xs \<le> k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
[PROOF STEP]
apply (simp add: list_slice2_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs \<le> k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
[PROOF STEP]
apply (drule order_le_less[THEN iffD1], erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k \<noteq> 0; length xs < k\<rbrakk> \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
 2. \<lbrakk>k \<noteq> 0; length xs = k\<rbrakk> \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
[PROOF STEP]
apply (simp add: list_slice2_def list_slice_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k \<noteq> 0; length xs = k\<rbrakk> \<Longrightarrow> list_slice2 xs k = (if length xs = 0 then [] else [xs])
[PROOF STEP]
apply (simp add: list_slice2_def list_slice_div_eq_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice2_Nil: "list_slice2 [] k = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice2 [] k = []
[PROOF STEP]
by (simp add: list_slice2_def list_slice_Nil)


[STATEMENT]
lemma list_slice2_list_slice_nth: "
  m < length xs div k \<Longrightarrow> list_slice2 xs k ! m = list_slice xs k ! m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> list_slice2 xs k ! m = list_slice xs k ! m
[PROOF STEP]
by (simp add: list_slice2_def list_slice_length nth_append)


[STATEMENT]
lemma list_slice2_last: "
  \<lbrakk> length xs mod k > 0; m = length xs div k \<rbrakk> \<Longrightarrow>
  list_slice2 xs k ! m = xs \<up> (length xs div k * k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < length xs mod k; m = length xs div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! m = xs \<up> (length xs div k * k)
[PROOF STEP]
by (simp add: list_slice2_def nth_append list_slice_length)


[STATEMENT]
lemma list_slice2_nth: "
  \<lbrakk> m < length xs div k \<rbrakk> \<Longrightarrow>
  list_slice2 xs k ! m = xs \<up> (m * k) \<down> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> list_slice2 xs k ! m = xs \<up> (m * k) \<down> k
[PROOF STEP]
by (simp add: list_slice2_def list_slice_length nth_append list_slice_nth)


[STATEMENT]
lemma list_slice2_nth_length_eq1: "
  m < length xs div k \<Longrightarrow> length (list_slice2 xs k ! m) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> length (list_slice2 xs k ! m) = k
[PROOF STEP]
by (simp add: list_slice2_def nth_append list_slice_length list_slice_nth_length)


[STATEMENT]
lemma list_slice2_nth_length_eq2: "
  \<lbrakk> length xs mod k > 0; m = length xs div k \<rbrakk> \<Longrightarrow>
  length (list_slice2 xs k ! m) = length xs mod k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < length xs mod k; m = length xs div k\<rbrakk> \<Longrightarrow> length (list_slice2 xs k ! m) = length xs mod k
[PROOF STEP]
by (simp add: list_slice2_def list_slice_length nth_append minus_div_mult_eq_mod [symmetric])


[STATEMENT]
lemma list_slice2_nth_nth_eq1: "
  \<lbrakk> m < length xs div k; n < k \<rbrakk> \<Longrightarrow>
  (list_slice2 xs k) ! m ! n = xs ! (m * k + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length xs div k; n < k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! m ! n = xs ! (m * k + n)
[PROOF STEP]
by (simp add: list_slice2_list_slice_nth list_slice_nth_nth)


[STATEMENT]
lemma list_slice2_nth_nth_eq2: "
  \<lbrakk> m = length xs div k; n < length xs mod k \<rbrakk> \<Longrightarrow>
  (list_slice2 xs k) ! m ! n = xs ! (m * k + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = length xs div k; n < length xs mod k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! m ! n = xs ! (m * k + n)
[PROOF STEP]
by (simp add: mult.commute[of _ k] minus_mod_eq_mult_div [symmetric] list_slice2_last)


[STATEMENT]
lemma list_slice2_nth_nth_rev: "
  n < length xs \<Longrightarrow> (list_slice2 xs k) ! (n div k) ! (n mod k) = xs ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; k = 0\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
 2. \<lbrakk>n < length xs; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (clarsimp simp: list_slice2_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (case_tac "n div k < length xs div k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; k \<noteq> 0; n div k < length xs div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
 2. \<lbrakk>n < length xs; k \<noteq> 0; \<not> n div k < length xs div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (simp add: list_slice2_nth_nth_eq1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; k \<noteq> 0; \<not> n div k < length xs div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (frule div_le_mono[OF less_imp_le, of _ _ k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; k \<noteq> 0; \<not> n div k < length xs div k; n div k \<le> length xs div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; 0 < k; n div k = length xs div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (length xs div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (length xs div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (subgoal_tac "n mod k < length xs mod k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; n mod k < length xs mod k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (length xs div k) ! (n mod k) = xs ! n
 2. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k\<rbrakk> \<Longrightarrow> n mod k < length xs mod k
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k\<rbrakk> \<Longrightarrow> n mod k < length xs mod k
 2. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; n mod k < length xs mod k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (length xs div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; \<not> n mod k < length xs mod k\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; n mod k < length xs mod k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (length xs div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (simp add: linorder_not_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; length xs mod k \<le> n mod k\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; n mod k < length xs mod k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (length xs div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (drule less_mod_ge_imp_div_less[of n "length xs" k], simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; 0 < k; length xs div k = n div k; n mod k < length xs mod k\<rbrakk> \<Longrightarrow> list_slice2 xs k ! (n div k) ! (n mod k) = xs ! n
[PROOF STEP]
apply (simp add: list_slice2_nth_nth_eq2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice2_append_mult: "
  length xs = m * k \<Longrightarrow>
  list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = m * k \<Longrightarrow> list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs = m * k; k = 0\<rbrakk> \<Longrightarrow> list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k
 2. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k
[PROOF STEP]
apply (simp add: list_slice2_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k
[PROOF STEP]
apply (clarsimp simp: list_slice2_def list_slice_append_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = m * k; 0 < k; 0 < length ys mod k\<rbrakk> \<Longrightarrow> ys \<up> ((m + length ys div k) * k - m * k) = ys \<up> (length ys div k * k)
[PROOF STEP]
apply (simp add: add.commute[of "m * k"] add_mult_distrib)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice2_append_mod: "
  length xs mod k = 0 \<Longrightarrow>
  list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs mod k = 0 \<Longrightarrow> list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k
[PROOF STEP]
by (auto intro: list_slice2_append_mult elim!: dvdE)


[STATEMENT]
lemma ilist_slice_nth: "
  (ilist_slice f k) m = map f [m * k..<Suc m * k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ilist_slice f k m = map f [m * k..<Suc m * k]
[PROOF STEP]
by (simp add: ilist_slice_def)


[STATEMENT]
lemma ilist_slice_nth_length: "length ((ilist_slice f k) m) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (ilist_slice f k m) = k
[PROOF STEP]
by (simp add: ilist_slice_def)


[STATEMENT]
lemma ilist_slice_nth_nth: "
  n < k \<Longrightarrow> (ilist_slice f k) m ! n = f (m * k + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < k \<Longrightarrow> ilist_slice f k m ! n = f (m * k + n)
[PROOF STEP]
by (simp add: ilist_slice_def)


[STATEMENT]
lemma ilist_slice_nth_nth_rev: "
  0 < k \<Longrightarrow> (ilist_slice f k) (n div k) ! (n mod k) = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> ilist_slice f k (n div k) ! (n mod k) = f n
[PROOF STEP]
by (simp add: ilist_slice_nth_nth)


[STATEMENT]
lemma list_slice_concat: "
  concat (list_slice xs k) = xs \<down> (length xs div k * k)"
  (is "?P xs k")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
 2. k \<noteq> 0 \<Longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (simp add: list_slice_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (subgoal_tac "\<And>m. \<forall>xs. length xs div k = m \<longrightarrow> ?P xs k", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. 0 < k \<Longrightarrow> \<forall>xs. length xs div k = m \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. 0 < k \<Longrightarrow> \<forall>xs. length xs div k = 0 \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
 2. \<And>m n. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)\<rbrakk> \<Longrightarrow> \<forall>xs. length xs div k = Suc n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m xs. \<lbrakk>0 < k; length xs div k = 0\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
 2. \<And>m n. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)\<rbrakk> \<Longrightarrow> \<forall>xs. length xs div k = Suc n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (simp add: in_set_conv_nth div_eq_0_conv' list_slice_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)\<rbrakk> \<Longrightarrow> \<forall>xs. length xs div k = Suc n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k); length xs div k = Suc n\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs \<down> (length xs div k * k)
[PROOF STEP]
apply (simp add: add.commute[of k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs \<down> (n * k + k)
[PROOF STEP]
apply (subgoal_tac "n * k + k \<le> length xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n; n * k + k \<le> length xs\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs \<down> (n * k + k)
 2. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n\<rbrakk> \<Longrightarrow> n * k + k \<le> length xs
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n\<rbrakk> \<Longrightarrow> n * k + k \<le> length xs
 2. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n; n * k + k \<le> length xs\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs \<down> (n * k + k)
[PROOF STEP]
apply (simp add: le_less_div_conv[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n; n * k + k \<le> length xs\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs \<down> (n * k + k)
[PROOF STEP]
apply (simp add: list_slice_div_eq_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>0 < k; \<forall>xs. length xs div k = n \<longrightarrow> concat (list_slice xs k) = xs \<down> (n * k); length xs div k = Suc n; n * k + k \<le> length xs\<rbrakk> \<Longrightarrow> xs \<down> (n * k) @ xs \<up> (n * k) \<down> k = xs \<down> (n * k + k)
[PROOF STEP]
apply (drule_tac x="xs \<down> (n * k)" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>0 < k; length xs div k = Suc n; n * k + k \<le> length xs; length (xs \<down> (n * k)) div k = n \<longrightarrow> concat (list_slice (xs \<down> (n * k)) k) = xs \<down> (n * k) \<down> (n * k)\<rbrakk> \<Longrightarrow> xs \<down> (n * k) @ xs \<up> (n * k) \<down> k = xs \<down> (n * k + k)
[PROOF STEP]
apply (simp add: min_eqR)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>0 < k; length xs div k = Suc n; n * k + k \<le> length xs; concat (list_slice (xs \<down> (n * k)) k) = xs \<down> (n * k)\<rbrakk> \<Longrightarrow> xs \<down> (n * k) @ xs \<up> (n * k) \<down> k = xs \<down> (n * k + k)
[PROOF STEP]
apply (simp add: take_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_unslice_mult: "
  length xs = m * k \<Longrightarrow> concat (list_slice xs k) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = m * k \<Longrightarrow> concat (list_slice xs k) = xs
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs = m * k; k = 0\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs
 2. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs
[PROOF STEP]
apply (simp add: list_slice_Nil)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = m * k; k \<noteq> 0\<rbrakk> \<Longrightarrow> concat (list_slice xs k) = xs
[PROOF STEP]
apply (simp add: list_slice_concat)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ilist_slice_unslice: "0 < k \<Longrightarrow> ilist_unslice (ilist_slice f k) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> ilist_unslice (ilist_slice f k) = f
[PROOF STEP]
by (simp add: ilist_unslice_def ilist_slice_nth_length ilist_slice_nth_nth)


[STATEMENT]
lemma i_take_ilist_slice_eq_list_slice: "
  0 < k \<Longrightarrow> ilist_slice f k \<Down> n = list_slice (f \<Down> (n * k)) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> ilist_slice f k \<Down> n = list_slice (f \<Down> (n * k)) k
[PROOF STEP]
apply (simp add: list_eq_iff list_slice_length ilist_slice_nth list_slice_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> \<forall>i<n. k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
[PROOF STEP]
apply (clarify, rename_tac i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k; i < n\<rbrakk> \<Longrightarrow> k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
[PROOF STEP]
apply (subgoal_tac "k \<le> n * k - i * k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
 2. \<And>i. \<lbrakk>0 < k; i < n\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; i < n\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 2. \<And>i. \<lbrakk>0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
[PROOF STEP]
apply (drule_tac m=i in Suc_leI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; Suc i \<le> n\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 2. \<And>i. \<lbrakk>0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
[PROOF STEP]
apply (drule mult_le_mono1[of _ _ k])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 < k; Suc i * k \<le> n * k\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 2. \<And>i. \<lbrakk>0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> k = min (n * k - i * k) k \<and> (\<forall>ia<k. f (i * k + ia) = f \<Down> (n * k) ! (i * k + ia))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_i_take_eq_i_take_ilist_slice: "
  list_slice (f \<Down> n) k = ilist_slice f k \<Down> (n div k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice (f \<Down> n) k = ilist_slice f k \<Down> (n div k)
[PROOF STEP]
apply (case_tac "k = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> list_slice (f \<Down> n) k = ilist_slice f k \<Down> (n div k)
 2. k \<noteq> 0 \<Longrightarrow> list_slice (f \<Down> n) k = ilist_slice f k \<Down> (n div k)
[PROOF STEP]
apply (simp add: list_slice_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> list_slice (f \<Down> n) k = ilist_slice f k \<Down> (n div k)
[PROOF STEP]
apply (simp add: i_take_ilist_slice_eq_list_slice)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> list_slice (f \<Down> n) k = list_slice (f \<Down> (n div k * k)) k
[PROOF STEP]
apply (subst list_slice_eq_list_slice_take[of "f \<Down> n", symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> list_slice (f \<Down> n \<down> (length (f \<Down> n) div k * k)) k = list_slice (f \<Down> (n div k * k)) k
[PROOF STEP]
apply (simp add: div_mult_le min_eqR)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ilist_slice_i_append_mod: "
  length xs mod k = 0 \<Longrightarrow>
  ilist_slice (xs \<frown> f) k = list_slice xs k \<frown> ilist_slice f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs mod k = 0 \<Longrightarrow> ilist_slice (xs \<frown> f) k = list_slice xs k \<frown> ilist_slice f k
[PROOF STEP]
apply (simp add: ilist_eq_iff ilist_slice_nth i_append_nth list_slice_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs mod k = 0 \<Longrightarrow> \<forall>x. (x < length xs div k \<longrightarrow> map (xs \<frown> f) [x * k..<k + x * k] = list_slice xs k ! x) \<and> (\<not> x < length xs div k \<longrightarrow> map (xs \<frown> f) [x * k..<k + x * k] = map f [(x - length xs div k) * k..<k + (x - length xs div k) * k])
[PROOF STEP]
apply (clarsimp simp: mult.commute[of k] elim!: dvdE, rename_tac n i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k\<rbrakk> \<Longrightarrow> (i < n \<longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = list_slice xs k ! i) \<and> (\<not> i < n \<longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k])
[PROOF STEP]
apply (intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = list_slice xs k ! i
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply (simp add: list_slice_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = xs \<up> (i * k) \<down> k
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply (subgoal_tac "k \<le> n * k - i * k")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = xs \<up> (i * k) \<down> k
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 3. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = xs \<up> (i * k) \<down> k
 3. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply (drule_tac m=i in Suc_leI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; Suc i \<le> n\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = xs \<up> (i * k) \<down> k
 3. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply (drule mult_le_mono1[of _ _ k])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; Suc i * k \<le> n * k\<rbrakk> \<Longrightarrow> k \<le> n * k - i * k
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = xs \<up> (i * k) \<down> k
 3. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; i < n; k \<le> n * k - i * k\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = xs \<up> (i * k) \<down> k
 2. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply (fastforce simp: list_eq_iff i_append_nth min_eqR)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; \<not> i < n\<rbrakk> \<Longrightarrow> map (xs \<frown> f) [i * k..<k + i * k] = map f [(i - n) * k..<k + (i - n) * k]
[PROOF STEP]
apply (simp add: ilist_eq_iff list_eq_iff i_append_nth linorder_not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i. \<lbrakk>length xs = n * k; 0 < k; n \<le> i\<rbrakk> \<Longrightarrow> \<forall>ia. (i * k + ia < n * k \<longrightarrow> ia < k \<longrightarrow> xs ! (i * k + ia) = f ((i - n) * k + ia)) \<and> (n * k \<le> i * k + ia \<longrightarrow> ia < k \<longrightarrow> f (i * k + ia - n * k) = f ((i - n) * k + ia))
[PROOF STEP]
apply (clarify, rename_tac j)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>length xs = n * k; 0 < k; n \<le> i\<rbrakk> \<Longrightarrow> (i * k + j < n * k \<longrightarrow> j < k \<longrightarrow> xs ! (i * k + j) = f ((i - n) * k + j)) \<and> (n * k \<le> i * k + j \<longrightarrow> j < k \<longrightarrow> f (i * k + j - n * k) = f ((i - n) * k + j))
[PROOF STEP]
apply (subgoal_tac "n * k \<le> i * k + j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n i j. \<lbrakk>length xs = n * k; 0 < k; n \<le> i; n * k \<le> i * k + j\<rbrakk> \<Longrightarrow> (i * k + j < n * k \<longrightarrow> j < k \<longrightarrow> xs ! (i * k + j) = f ((i - n) * k + j)) \<and> (n * k \<le> i * k + j \<longrightarrow> j < k \<longrightarrow> f (i * k + j - n * k) = f ((i - n) * k + j))
 2. \<And>n i j. \<lbrakk>length xs = n * k; 0 < k; n \<le> i\<rbrakk> \<Longrightarrow> n * k \<le> i * k + j
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n i j. \<lbrakk>length xs = n * k; 0 < k; n \<le> i\<rbrakk> \<Longrightarrow> n * k \<le> i * k + j
 2. \<And>n i j. \<lbrakk>length xs = n * k; 0 < k; n \<le> i; n * k \<le> i * k + j\<rbrakk> \<Longrightarrow> (i * k + j < n * k \<longrightarrow> j < k \<longrightarrow> xs ! (i * k + j) = f ((i - n) * k + j)) \<and> (n * k \<le> i * k + j \<longrightarrow> j < k \<longrightarrow> f (i * k + j - n * k) = f ((i - n) * k + j))
[PROOF STEP]
apply (simp add: trans_le_add1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>length xs = n * k; 0 < k; n \<le> i; n * k \<le> i * k + j\<rbrakk> \<Longrightarrow> (i * k + j < n * k \<longrightarrow> j < k \<longrightarrow> xs ! (i * k + j) = f ((i - n) * k + j)) \<and> (n * k \<le> i * k + j \<longrightarrow> j < k \<longrightarrow> f (i * k + j - n * k) = f ((i - n) * k + j))
[PROOF STEP]
apply (simp add: diff_mult_distrib)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma filterlim_sequentially_iff:
  "filterlim f F1 sequentially \<longleftrightarrow> filterlim (\<lambda>x. f (x+k)) F1 sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim f F1 sequentially = (LIM x sequentially. f (x + k) :> F1)
[PROOF STEP]
unfolding filterlim_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>P. eventually P F1 \<longrightarrow> (\<forall>\<^sub>F x in sequentially. P (f x))) = (\<forall>P. eventually P F1 \<longrightarrow> (\<forall>\<^sub>F x in sequentially. P (f (x + k))))
[PROOF STEP]
by (metis eventually_at_top_linorder eventually_sequentially_seg)


[STATEMENT]
lemma filterlim_realpow_sequentially_at_top:
  "(x::real) > 1 \<Longrightarrow> filterlim (power x) at_top sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < x \<Longrightarrow> filterlim ((^) x) at_top sequentially
[PROOF STEP]
apply (rule LIMSEQ_divide_realpow_zero[THEN filterlim_inverse_at_top,of _ 1,simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1 < x \<Longrightarrow> 1 < x
 2. 1 < x \<Longrightarrow> \<forall>\<^sub>F xa in sequentially. 0 < x ^ xa
[PROOF STEP]
by auto


[STATEMENT]
lemma filterlim_at_top_powr_real:
  fixes g::"'b \<Rightarrow> real"
  assumes "filterlim f at_top F" "(g \<longlongrightarrow> g') F" "g'>1"
  shows "LIM x F. g x powr f x :> at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
have "LIM x F. ((g' + 1) / 2) powr f x :> at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x F. ((g' + 1) / 2) powr f x :> at_top
[PROOF STEP]
proof (subst filterlim_at_top_gt[of _ _ 1],rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Z. 1 < Z \<Longrightarrow> \<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
fix Z::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Z. 1 < Z \<Longrightarrow> \<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
assume "Z > 1"
[PROOF STATE]
proof (state)
this:
1 < Z

goal (1 subgoal):
 1. \<And>Z. 1 < Z \<Longrightarrow> \<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
have "\<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x
[PROOF STEP]
using assms(1) filterlim_at_top
[PROOF STATE]
proof (prove)
using this:
filterlim f at_top F
filterlim ?f at_top ?F = (\<forall>Z. \<forall>\<^sub>F x in ?F. Z \<le> ?f x)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x

goal (1 subgoal):
 1. \<And>Z. 1 < Z \<Longrightarrow> \<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x
[PROOF STEP]
have "\<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
proof (eventually_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ln Z / ln ((g' + 1) / 2) \<le> f x \<Longrightarrow> ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
ln Z / ln ((g' + 1) / 2) \<le> f x

goal (1 subgoal):
 1. \<And>x. ln Z / ln ((g' + 1) / 2) \<le> f x \<Longrightarrow> ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ln Z / ln ((g' + 1) / 2) \<le> f x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ln Z / ln ((g' + 1) / 2) \<le> f x

goal (1 subgoal):
 1. ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
using \<open>g'>1\<close>
[PROOF STATE]
proof (prove)
using this:
ln Z / ln ((g' + 1) / 2) \<le> f x
1 < g'

goal (1 subgoal):
 1. ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
by (auto simp:ln_powr divide_simps)
[PROOF STATE]
proof (state)
this:
ln Z \<le> ln (((g' + 1) / 2) powr f x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)

goal (1 subgoal):
 1. \<And>Z. 1 < Z \<Longrightarrow> \<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
show "\<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
proof (eventually_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ln Z \<le> ln (((g' + 1) / 2) powr f x) \<Longrightarrow> Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
ln Z \<le> ln (((g' + 1) / 2) powr f x)

goal (1 subgoal):
 1. \<And>x. ln Z \<le> ln (((g' + 1) / 2) powr f x) \<Longrightarrow> Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ln Z \<le> ln (((g' + 1) / 2) powr f x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ln Z \<le> ln (((g' + 1) / 2) powr f x)

goal (1 subgoal):
 1. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
using \<open>1 < Z\<close> \<open>g'>1\<close>
[PROOF STATE]
proof (prove)
using this:
ln Z \<le> ln (((g' + 1) / 2) powr f x)
1 < Z
1 < g'

goal (1 subgoal):
 1. Z \<le> ((g' + 1) / 2) powr f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Z \<le> ((g' + 1) / 2) powr f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LIM x F. ((g' + 1) / 2) powr f x :> at_top

goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
LIM x F. ((g' + 1) / 2) powr f x :> at_top

goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
have "\<forall>\<^sub>F x in F. ((g'+1)/2) powr f x \<le> g x powr f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
have "\<forall>\<^sub>F x in F. g x > (g'+1)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. (g' + 1) / 2 < g x
[PROOF STEP]
apply (rule order_tendstoD[OF assms(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g' + 1) / 2 < g'
[PROOF STEP]
using \<open>g'>1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < g'

goal (1 subgoal):
 1. (g' + 1) / 2 < g'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. (g' + 1) / 2 < g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. (g' + 1) / 2 < g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
have "\<forall>\<^sub>F x in F. f x>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. 0 < f x
[PROOF STEP]
using assms(1) filterlim_at_top_dense
[PROOF STATE]
proof (prove)
using this:
filterlim f at_top F
filterlim ?f at_top ?F = (\<forall>Z. \<forall>\<^sub>F x in ?F. Z < ?f x)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. 0 < f x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. 0 < f x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in F. (g' + 1) / 2 < g x
\<forall>\<^sub>F x in F. 0 < f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. (g' + 1) / 2 < g x
\<forall>\<^sub>F x in F. 0 < f x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(g' + 1) / 2 < g x; 0 < f x\<rbrakk> \<Longrightarrow> ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
(g' + 1) / 2 < g x
0 < f x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(g' + 1) / 2 < g x; 0 < f x\<rbrakk> \<Longrightarrow> ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g' + 1) / 2 < g x
0 < f x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(g' + 1) / 2 < g x
0 < f x

goal (1 subgoal):
 1. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
using \<open>g'>1\<close>
[PROOF STATE]
proof (prove)
using this:
(g' + 1) / 2 < g x
0 < f x
1 < g'

goal (1 subgoal):
 1. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
by (auto intro!: powr_mono2)
[PROOF STATE]
proof (state)
this:
((g' + 1) / 2) powr f x \<le> g x powr f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x

goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
LIM x F. ((g' + 1) / 2) powr f x :> at_top
\<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LIM x F. ((g' + 1) / 2) powr f x :> at_top
\<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x

goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
using filterlim_at_top_mono
[PROOF STATE]
proof (prove)
using this:
LIM x F. ((g' + 1) / 2) powr f x :> at_top
\<forall>\<^sub>F x in F. ((g' + 1) / 2) powr f x \<le> g x powr f x
\<lbrakk>filterlim ?f at_top ?F; \<forall>\<^sub>F x in ?F. ?f x \<le> ?g x\<rbrakk> \<Longrightarrow> filterlim ?g at_top ?F

goal (1 subgoal):
 1. LIM x F. g x powr f x :> at_top
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
LIM x F. g x powr f x :> at_top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powrfinitesum:
  fixes a::real and s::nat assumes  "s \<le> n"
  shows " (\<Prod>j=s..(n::nat).(a powr (2^j)))  = a powr (\<Sum>j=s..(n::nat).(2^j)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}
[PROOF STEP]
using \<open>s \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<le> 0 \<Longrightarrow> (\<Prod>j = s..0. a powr 2 ^ j) = a powr sum ((^) 2) {s..0}
 2. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
s \<le> 0

goal (2 subgoals):
 1. s \<le> 0 \<Longrightarrow> (\<Prod>j = s..0. a powr 2 ^ j) = a powr sum ((^) 2) {s..0}
 2. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<le> 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s \<le> 0

goal (1 subgoal):
 1. (\<Prod>j = s..0. a powr 2 ^ j) = a powr sum ((^) 2) {s..0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Prod>j = s..0. a powr 2 ^ j) = a powr sum ((^) 2) {s..0}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}
s \<le> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
have ?case when "s\<le>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
by (metis Suc.prems add.commute linorder_not_le powr_add prod.nat_ivl_Suc' sum.cl_ivl_Suc that)
[PROOF STATE]
proof (state)
this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
have ?case when "s=Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
have "(\<Prod>j = s..Suc n. a powr 2 ^ j) =(a powr 2 ^(Suc n))  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n
[PROOF STEP]
using \<open>s=Suc n\<close>
[PROOF STATE]
proof (prove)
using this:
s = Suc n

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
have "a powr 2 ^ Suc n = a powr sum (power 2) {s..Suc n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a powr 2 ^ Suc n = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
s = Suc n

goal (1 subgoal):
 1. a powr 2 ^ Suc n = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a powr 2 ^ Suc n = a powr sum ((^) 2) {s..Suc n}

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n
a powr 2 ^ Suc n = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
show "(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum (power 2) {s..Suc n}"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n
a powr 2 ^ Suc n = a powr sum ((^) 2) {s..Suc n}

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
using \<open>s\<le>Suc n\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr 2 ^ Suc n
a powr 2 ^ Suc n = a powr sum ((^) 2) {s..Suc n}
s \<le> Suc n

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = Suc n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> (\<Prod>j = s..n. a powr 2 ^ j) = a powr sum ((^) 2) {s..n}; s \<le> Suc n\<rbrakk> \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
s = Suc n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
s = Suc n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
using \<open>s\<le>Suc n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
s = Suc n \<Longrightarrow> (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
s \<le> Suc n

goal (1 subgoal):
 1. (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma summable_ratio_test_tendsto:
  fixes f :: "nat \<Rightarrow> 'a::banach"
  assumes "c < 1" and "\<forall>n. f n\<noteq>0" and "(\<lambda>n. norm (f (Suc n)) / norm (f n)) \<longlonglongrightarrow> c"
  shows "summable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
obtain N where N_dist:"\<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1-c)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1 - c) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c < 1
\<forall>n. f n \<noteq> (0::'a)
(\<lambda>n. norm (f (Suc n)) / norm (f n)) \<longlonglongrightarrow> c

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1 - c) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding tendsto_iff eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
c < 1
\<forall>n. f n \<noteq> (0::'a)
\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < e

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1 - c) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson diff_gt_0_iff_gt zero_less_divide_iff zero_less_numeral)
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1 - c) / 2

goal (1 subgoal):
 1. summable f
[PROOF STEP]
have "norm (f (Suc n)) / norm (f n) \<le> (1+c)/2" when "n\<ge>N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (f (Suc n)) / norm (f n) \<le> (1 + c) / 2
[PROOF STEP]
using N_dist[rule_format,OF that] \<open>c<1\<close>
[PROOF STATE]
proof (prove)
using this:
dist (norm (f (Suc n)) / norm (f n)) c < (1 - c) / 2
c < 1

goal (1 subgoal):
 1. norm (f (Suc n)) / norm (f n) \<le> (1 + c) / 2
[PROOF STEP]
apply (auto simp add:field_simps dist_norm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c + 2 * \<bar>norm (f (Suc n)) / norm (f n) - c\<bar> < 1; c < 1\<rbrakk> \<Longrightarrow> 2 * norm (f (Suc n)) / norm (f n) \<le> 1 + c
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) / norm (f ?n) \<le> (1 + c) / 2

goal (1 subgoal):
 1. summable f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) / norm (f ?n) \<le> (1 + c) / 2
[PROOF STEP]
have "norm (f (Suc n))  \<le> (1+c)/2 * norm (f n)" when "n\<ge>N" for n
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) / norm (f ?n) \<le> (1 + c) / 2

goal (1 subgoal):
 1. norm (f (Suc n)) \<le> (1 + c) / 2 * norm (f n)
[PROOF STEP]
using that assms(2)[rule_format, of n]
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) / norm (f ?n) \<le> (1 + c) / 2
N \<le> n
f n \<noteq> (0::'a)

goal (1 subgoal):
 1. norm (f (Suc n)) \<le> (1 + c) / 2 * norm (f n)
[PROOF STEP]
by (auto simp add:divide_simps)
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) \<le> (1 + c) / 2 * norm (f ?n)

goal (1 subgoal):
 1. summable f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) \<le> (1 + c) / 2 * norm (f ?n)

goal (1 subgoal):
 1. summable f
[PROOF STEP]
have "(1+c)/2 < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + c) / 2 < 1
[PROOF STEP]
using \<open>c<1\<close>
[PROOF STATE]
proof (prove)
using this:
c < 1

goal (1 subgoal):
 1. (1 + c) / 2 < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 + c) / 2 < 1

goal (1 subgoal):
 1. summable f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) \<le> (1 + c) / 2 * norm (f ?n)
(1 + c) / 2 < 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) \<le> (1 + c) / 2 * norm (f ?n)
(1 + c) / 2 < 1

goal (1 subgoal):
 1. summable f
[PROOF STEP]
using summable_ratio_test[of _ N f]
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> norm (f (Suc ?n)) \<le> (1 + c) / 2 * norm (f ?n)
(1 + c) / 2 < 1
\<lbrakk>?c < 1; \<And>n. N \<le> n \<Longrightarrow> norm (f (Suc n)) \<le> ?c * norm (f n)\<rbrakk> \<Longrightarrow> summable f

goal (1 subgoal):
 1. summable f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
summable f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma summable_ln_plus:
  fixes f::"nat \<Rightarrow> real"
  assumes "summable f" "\<forall>n. f n>0"
  shows "summable (\<lambda>n. ln (1+f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. ln (1 + f n))
[PROOF STEP]
proof (rule summable_comparison_test_ev[OF _ assms(1)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n
[PROOF STEP]
have "ln (1 + f n) > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < ln (1 + f n)
[PROOF STEP]
by (simp add: assms(2) ln_gt_zero)
[PROOF STATE]
proof (state)
this:
0 < ln (1 + f ?n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < ln (1 + f ?n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n
[PROOF STEP]
have "ln (1 + f n) \<le> f n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (1 + f n) \<le> f n
[PROOF STEP]
apply (rule ln_add_one_self_le_self2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 < f n
[PROOF STEP]
using assms(2)[rule_format,of n]
[PROOF STATE]
proof (prove)
using this:
0 < f n

goal (1 subgoal):
 1. - 1 < f n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ln (1 + f ?n) \<le> f ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < ln (1 + f ?n)
ln (1 + f ?n) \<le> f ?n
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n"
[PROOF STATE]
proof (prove)
using this:
0 < ln (1 + f ?n)
ln (1 + f ?n) \<le> f ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n
[PROOF STEP]
by (auto intro!: eventuallyI simp add:less_imp_le)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma suminf_real_offset_le:
  fixes f :: "nat \<Rightarrow> real"
  assumes f: "\<And>i. 0 \<le> f i" and "summable f"
  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
have "(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))
[PROOF STEP]
using summable_sums[OF \<open>summable f\<close>]
[PROOF STATE]
proof (prove)
using this:
f sums suminf f

goal (1 subgoal):
 1. (\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))
[PROOF STEP]
by (simp add: assms(2) summable_LIMSEQ summable_ignore_initial_segment)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))

goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))

goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
have "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> (\<Sum>i. f i)
[PROOF STEP]
using summable_sums[OF \<open>summable f\<close>]
[PROOF STATE]
proof (prove)
using this:
f sums suminf f

goal (1 subgoal):
 1. (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> (\<Sum>i. f i)
[PROOF STEP]
by (simp add: sums_def atLeast0LessThan f)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> (\<Sum>i. f i)

goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> (\<Sum>i. f i)
[PROOF STEP]
have "(\<lambda>n. \<Sum>i<n + k. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> (\<Sum>i. f i)

goal (1 subgoal):
 1. (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i)
[PROOF STEP]
by (rule LIMSEQ_ignore_initial_segment)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i)

goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))
(\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))
(\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i)

goal (1 subgoal):
 1. (\<Sum>i. f (i + k)) \<le> suminf f
[PROOF STEP]
proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
assume "k \<le> n"
[PROOF STATE]
proof (state)
this:
k \<le> n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. f (i + k)) = sum (f \<circ> (\<lambda>i. i + k)) {..<n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. f (i + k)) = sum (f \<circ> (\<lambda>i. i + k)) {..<n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. f (i + k)) = sum (f \<circ> (\<lambda>i. i + k)) {..<n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (f \<circ> (\<lambda>i. i + k)) {..<n} = sum f ((\<lambda>i. i + k) ` {..<n})
[PROOF STEP]
by (subst sum.reindex) auto
[PROOF STATE]
proof (state)
this:
sum (f \<circ> (\<lambda>i. i + k)) {..<n} = sum f ((\<lambda>i. i + k) ` {..<n})

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (f \<circ> (\<lambda>i. i + k)) {..<n} = sum f ((\<lambda>i. i + k) ` {..<n})

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
have "\<dots> \<le> sum f {..<n + k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f ((\<lambda>i. i + k) ` {..<n}) \<le> sum f {..<n + k}
[PROOF STEP]
by (intro sum_mono2) (auto simp: f)
[PROOF STATE]
proof (state)
this:
sum f ((\<lambda>i. i + k) ` {..<n}) \<le> sum f {..<n + k}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k)); (\<lambda>n. sum f {..<n + k}) \<longlonglongrightarrow> (\<Sum>i. f i); k \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}

goal (1 subgoal):
 1. (\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i. f (i + k)) \<le> suminf f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma factt:
  fixes s n ::nat assumes "s \<le> n"
  shows " (\<Sum>i=s..n. 2^i) < (2^(n+1) :: real) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..n} < 2 ^ (n + 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. sum ((^) 2) {s..n} < 2 ^ (n + 1)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<le> 0 \<Longrightarrow> sum ((^) 2) {s..0} < 2 ^ (0 + 1)
 2. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
s \<le> 0

goal (2 subgoals):
 1. s \<le> 0 \<Longrightarrow> sum ((^) 2) {s..0} < 2 ^ (0 + 1)
 2. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..0} < 2 ^ (0 + 1)
[PROOF STEP]
by  auto
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..0} < 2 ^ (0 + 1)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1)
s \<le> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
have ?case when  "s=n+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
s = n + 1

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s = n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
have ?case when  "s \<noteq> n+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
have"(\<Sum>i=s..(n+1). 2^i ) = (\<Sum>i=s..n. 2^i ) + (2::real)^(n+1) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..n + 1} = sum ((^) 2) {s..n} + 2 ^ (n + 1)
[PROOF STEP]
using sum.cl_ivl_Suc \<open>s \<le> Suc n \<close>
[PROOF STATE]
proof (prove)
using this:
sum ?g {?m..Suc ?n} = (if Suc ?n < ?m then 0::?'a else sum ?g {?m..?n} + ?g (Suc ?n))
s \<le> Suc n

goal (1 subgoal):
 1. sum ((^) 2) {s..n + 1} = sum ((^) 2) {s..n} + 2 ^ (n + 1)
[PROOF STEP]
by (auto simp add:add.commute)
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n + 1} = sum ((^) 2) {s..n} + 2 ^ (n + 1)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n + 1} = sum ((^) 2) {s..n} + 2 ^ (n + 1)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
have "... < (2) ^ (n +1) + (2)^(n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)
[PROOF STEP]
have "s \<le>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> n
[PROOF STEP]
using that  \<open>s \<le> Suc n \<close>
[PROOF STATE]
proof (prove)
using this:
s \<noteq> n + 1
s \<le> Suc n

goal (1 subgoal):
 1. s \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<le> n

goal (1 subgoal):
 1. sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)
[PROOF STEP]
using Suc.hyps \<open>s \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n
s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1)
s \<le> n

goal (1 subgoal):
 1. sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n} + 2 ^ (n + 1) < 2 ^ (n + 1) + 2 ^ (n + 1)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
have "... = 2^(n+2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (n + 1) + 2 ^ (n + 1) = 2 ^ (n + 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (n + 1) + 2 ^ (n + 1) = 2 ^ (n + 2)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum ((^) 2) {s..n + 1} < 2 ^ (n + 2)
[PROOF STEP]
show "(\<Sum>i=s..(Suc n). 2^i )< (2::real)^(Suc n+1)"
[PROOF STATE]
proof (prove)
using this:
sum ((^) 2) {s..n + 1} < 2 ^ (n + 2)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<noteq> n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>s \<le> n \<Longrightarrow> sum ((^) 2) {s..n} < 2 ^ (n + 1); s \<le> Suc n\<rbrakk> \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s = n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
s \<noteq> n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s = n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
s \<noteq> n + 1 \<Longrightarrow> sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)

goal (1 subgoal):
 1. sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..Suc n} < 2 ^ (Suc n + 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma showpre7:
  fixes a b ::"nat\<Rightarrow>int " and q p::int
  assumes "q>0" and "p>0"and a: "\<forall>n. a n>0" and "\<forall>n. b n>0" and
    assumerational:"(\<lambda> n. b (n+1) / a (n+1) )  sums (p/q)"
  shows "q*((\<Prod>j=1..n. of_int( a j)))*(suminf (\<lambda>(j::nat). (b (j+n+1)/ a (j+n+1 ))))
        = ((\<Prod>j=1..n. of_int( a j)))*(p -q* (\<Sum>j=1..n. b j / a j))       "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
define aa where "aa=(\<Prod>j = 1..n. real_of_int (a j))"
[PROOF STATE]
proof (state)
this:
aa = (\<Prod>j = 1..n. real_of_int (a j))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
define ff where "ff=(\<lambda>i. real_of_int (b (i+1)) / real_of_int (a (i+1)))"
[PROOF STATE]
proof (state)
this:
ff = (\<lambda>i. real_of_int (b (i + 1)) / real_of_int (a (i + 1)))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
have "(\<Sum>j. ff (j+n)) =  (\<Sum>n. ff n) - sum ff {..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j. ff (j + n)) = (\<Sum>n. ff n) - sum ff {..<n}
[PROOF STEP]
apply (rule suminf_minus_initial_segment)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable ff
[PROOF STEP]
using assumerational
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)

goal (1 subgoal):
 1. summable ff
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))
[PROOF STEP]
by (simp add: sums_summable)
[PROOF STATE]
proof (state)
this:
(\<Sum>j. ff (j + n)) = (\<Sum>n. ff n) - sum ff {..<n}

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j. ff (j + n)) = (\<Sum>n. ff n) - sum ff {..<n}

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
have "... = p/q - sum ff {..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. ff n) - sum ff {..<n} = real_of_int p / real_of_int q - sum ff {..<n}
[PROOF STEP]
using assumerational
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)

goal (1 subgoal):
 1. (\<Sum>n. ff n) - sum ff {..<n} = real_of_int p / real_of_int q - sum ff {..<n}
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) - (\<Sum>i<n. real_of_int (b (i + 1)) / real_of_int (a (i + 1))) = real_of_int p / real_of_int q - (\<Sum>i<n. real_of_int (b (i + 1)) / real_of_int (a (i + 1)))
[PROOF STEP]
by (simp add: sums_iff)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ff n) - sum ff {..<n} = real_of_int p / real_of_int q - sum ff {..<n}

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ff n) - sum ff {..<n} = real_of_int p / real_of_int q - sum ff {..<n}

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
have "... = p/q - (\<Sum>j=1..n. ff (j-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int p / real_of_int q - sum ff {..<n} = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int p / real_of_int q - sum ff {..<n} = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
have "sum ff {..<n} = (\<Sum>j=1..n. ff (j-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ff {..<n} = (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
apply (subst sum_bounds_lt_plus1[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ff {..<n} = (\<Sum>k<n. ff (Suc k - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum ff {..<n} = (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. real_of_int p / real_of_int q - sum ff {..<n} = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum ff {..<n} = (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum ff {..<n} = (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. real_of_int p / real_of_int q - sum ff {..<n} = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<n. real_of_int (b (i + 1)) / real_of_int (a (i + 1))) = (\<Sum>j = 1..n. real_of_int (b (j - 1 + 1)) / real_of_int (a (j - 1 + 1)))

goal (1 subgoal):
 1. real_of_int p / real_of_int q - (\<Sum>i<n. real_of_int (b (i + 1)) / real_of_int (a (i + 1))) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. real_of_int (b (j - 1 + 1)) / real_of_int (a (j - 1 + 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int p / real_of_int q - sum ff {..<n} = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int p / real_of_int q - sum ff {..<n} = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
have "(\<Sum>j. ff (j + n)) = p / q - (\<Sum>j = 1..n. ff (j - 1))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. (\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
have "q*(\<Sum>j. ff (j + n)) = p - q*(\<Sum>j = 1..n. ff (j - 1))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. real_of_int q * (\<Sum>j. ff (j + n)) = real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
using \<open>q>0\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j. ff (j + n)) = real_of_int p / real_of_int q - (\<Sum>j = 1..n. ff (j - 1))
0 < q

goal (1 subgoal):
 1. real_of_int q * (\<Sum>j. ff (j + n)) = real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Sum>j. ff (j + n)) = real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int q * (\<Sum>j. ff (j + n)) = real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1))
[PROOF STEP]
have "aa*q*(\<Sum>j. ff (j + n)) = aa*(p - q*(\<Sum>j = 1..n. ff (j - 1)))"
[PROOF STATE]
proof (prove)
using this:
real_of_int q * (\<Sum>j. ff (j + n)) = real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1))

goal (1 subgoal):
 1. aa * real_of_int q * (\<Sum>j. ff (j + n)) = aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
aa * real_of_int q * (\<Sum>j. ff (j + n)) = aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1)))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aa * real_of_int q * (\<Sum>j. ff (j + n)) = aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aa * real_of_int q * (\<Sum>j. ff (j + n)) = aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. ff (j - 1)))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
unfolding aa_def ff_def
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j = 1..n. real_of_int (a j)) * real_of_int q * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b (j - 1 + 1)) / real_of_int (a (j - 1 + 1))))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))

goal:
No subgoals!
[PROOF STEP]
qed