[STATEMENT]
lemma cycle_tl_is_path: "is_cycle xs \<and> walk_length xs \<ge> 3 \<Longrightarrow> is_path (tl xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle xs \<and> 3 \<le> walk_length xs \<Longrightarrow> is_path (tl xs)
[PROOF STEP]
proof (simp add: is_cycle_def is_path_def is_open_walk_def is_closed_walk_def walk_length_conv,
    elim conjE, intro conjI, simp add: is_walk_tl)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
assume w: "is_walk xs" and eq: "hd xs = last xs" and  "3 \<le> length xs - Suc 0" and
    dis: "distinct (tl xs)"
[PROOF STATE]
proof (state)
this:
is_walk xs
hd xs = last xs
3 \<le> length xs - Suc 0
distinct (tl xs)

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk xs
hd xs = last xs
3 \<le> length xs - Suc 0
distinct (tl xs)
[PROOF STEP]
have len: "4 \<le> length xs"
[PROOF STATE]
proof (prove)
using this:
is_walk xs
hd xs = last xs
3 \<le> length xs - Suc 0
distinct (tl xs)

goal (1 subgoal):
 1. 4 \<le> length xs
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
4 \<le> length xs

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
4 \<le> length xs
[PROOF STEP]
have lentl: "3 \<le> length (tl xs)"
[PROOF STATE]
proof (prove)
using this:
4 \<le> length xs

goal (1 subgoal):
 1. 3 \<le> length (tl xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
3 \<le> length (tl xs)

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
3 \<le> length (tl xs)
[PROOF STEP]
have lentltl: "2 \<le> length (tl (tl xs))"
[PROOF STATE]
proof (prove)
using this:
3 \<le> length (tl xs)

goal (1 subgoal):
 1. 2 \<le> length (tl (tl xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 \<le> length (tl (tl xs))

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
have "last (tl (tl xs)) = last (tl xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (tl (tl xs)) = last (tl xs)
[PROOF STEP]
by (metis One_nat_def Suc_1 \<open>3 \<le> length xs - Suc 0\<close> diff_is_0_eq' is_walk_def is_walk_tl last_tl
        lentl not_less_eq_eq numeral_le_one_iff one_le_numeral order.trans semiring_norm(70) w)
[PROOF STATE]
proof (state)
this:
last (tl (tl xs)) = last (tl xs)

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
last (tl (tl xs)) = last (tl xs)
[PROOF STEP]
have "last (tl xs) \<in> set (tl (tl xs))"
[PROOF STATE]
proof (prove)
using this:
last (tl (tl xs)) = last (tl xs)

goal (1 subgoal):
 1. last (tl xs) \<in> set (tl (tl xs))
[PROOF STEP]
using  last_in_list_tl_set lentltl
[PROOF STATE]
proof (prove)
using this:
last (tl (tl xs)) = last (tl xs)
2 \<le> length ?xs \<Longrightarrow> last ?xs \<in> set (tl ?xs)
2 \<le> length (tl (tl xs))

goal (1 subgoal):
 1. last (tl xs) \<in> set (tl (tl xs))
[PROOF STEP]
by (metis last_in_set list.sel(2))
[PROOF STATE]
proof (state)
this:
last (tl xs) \<in> set (tl (tl xs))

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last (tl xs) \<in> set (tl (tl xs))

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
have "hd (tl xs) \<notin> set (tl (tl xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (tl xs) \<notin> set (tl (tl xs))
[PROOF STEP]
using dis lentltl
[PROOF STATE]
proof (prove)
using this:
distinct (tl xs)
2 \<le> length (tl (tl xs))

goal (1 subgoal):
 1. hd (tl xs) \<notin> set (tl (tl xs))
[PROOF STEP]
by (metis distinct.simps(2) hd_Cons_tl list.sel(2) list.size(3) not_numeral_le_zero)
[PROOF STATE]
proof (state)
this:
hd (tl xs) \<notin> set (tl (tl xs))

goal (1 subgoal):
 1. \<lbrakk>is_walk xs; hd xs = last xs; Suc 0 \<le> length xs - Suc 0; distinct (tl xs); 3 \<le> length xs - Suc 0\<rbrakk> \<Longrightarrow> hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last (tl xs) \<in> set (tl (tl xs))
hd (tl xs) \<notin> set (tl (tl xs))
[PROOF STEP]
show "hd (tl xs) \<noteq> last (tl xs)"
[PROOF STATE]
proof (prove)
using this:
last (tl xs) \<in> set (tl (tl xs))
hd (tl xs) \<notin> set (tl (tl xs))

goal (1 subgoal):
 1. hd (tl xs) \<noteq> last (tl xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
hd (tl xs) \<noteq> last (tl xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_gen_path_path:
  assumes "is_gen_path p" and "walk_length p > 0" and "(\<not> is_cycle p)"
  shows "is_path p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path p
[PROOF STEP]
proof (simp add: is_gen_path_def is_path_def is_open_walk_def, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_walk p
 2. hd p \<noteq> last p
 3. distinct p
[PROOF STEP]
show "is_walk p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk p
[PROOF STEP]
using is_gen_path_def assms(1)
[PROOF STATE]
proof (prove)
using this:
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)
is_gen_path p

goal (1 subgoal):
 1. is_walk p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_walk p

goal (2 subgoals):
 1. hd p \<noteq> last p
 2. distinct p
[PROOF STEP]
show ne: "hd p \<noteq> last p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd p \<noteq> last p
[PROOF STEP]
using assms(1) assms(2) assms(3) is_cycle_alt_gen_path
[PROOF STATE]
proof (prove)
using this:
is_gen_path p
0 < walk_length p
\<not> is_cycle p
is_cycle ?xs = (is_gen_path ?xs \<and> 1 \<le> walk_length ?xs \<and> hd ?xs = last ?xs)

goal (1 subgoal):
 1. hd p \<noteq> last p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd p \<noteq> last p

goal (1 subgoal):
 1. distinct p
[PROOF STEP]
have "((distinct (tl p) \<and> hd p = last p) \<or> distinct p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (tl p) \<and> hd p = last p \<or> distinct p
[PROOF STEP]
using is_gen_path_def assms(1)
[PROOF STATE]
proof (prove)
using this:
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)
is_gen_path p

goal (1 subgoal):
 1. distinct (tl p) \<and> hd p = last p \<or> distinct p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (tl p) \<and> hd p = last p \<or> distinct p

goal (1 subgoal):
 1. distinct p
[PROOF STEP]
thus "distinct p"
[PROOF STATE]
proof (prove)
using this:
distinct (tl p) \<and> hd p = last p \<or> distinct p

goal (1 subgoal):
 1. distinct p
[PROOF STEP]
using ne
[PROOF STATE]
proof (prove)
using this:
distinct (tl p) \<and> hd p = last p \<or> distinct p
hd p \<noteq> last p

goal (1 subgoal):
 1. distinct p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_gen_path_options: "is_gen_path p \<longleftrightarrow> is_cycle p \<or> is_path p \<or> (\<exists> v \<in> V. p = [v])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_gen_path p = (is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]))
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_gen_path p \<Longrightarrow> is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])
 2. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
assume a: "is_gen_path p"
[PROOF STATE]
proof (state)
this:
is_gen_path p

goal (2 subgoals):
 1. is_gen_path p \<Longrightarrow> is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])
 2. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_gen_path p
[PROOF STEP]
have "p \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
is_gen_path p

goal (1 subgoal):
 1. p \<noteq> []
[PROOF STEP]
unfolding is_gen_path_def is_walk_def
[PROOF STATE]
proof (prove)
using this:
(set p \<subseteq> V \<and> set (walk_edges p) \<subseteq> E \<and> p \<noteq> []) \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p)

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

goal (2 subgoals):
 1. is_gen_path p \<Longrightarrow> is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])
 2. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> []
[PROOF STEP]
have "(\<forall> v \<in> V . p \<noteq> [v]) \<Longrightarrow> walk_length p > 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []

goal (1 subgoal):
 1. \<forall>v\<in>V. p \<noteq> [v] \<Longrightarrow> 0 < walk_length p
[PROOF STEP]
using walk_length_def
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
walk_length ?p \<equiv> length (walk_edges ?p)

goal (1 subgoal):
 1. \<forall>v\<in>V. p \<noteq> [v] \<Longrightarrow> 0 < walk_length p
[PROOF STEP]
by (metis a is_gen_path_def is_walk_wf_hd length_greater_0_conv list.collapse list.distinct(1) walk_edges.simps(3))
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>V. p \<noteq> [v] \<Longrightarrow> 0 < walk_length p

goal (2 subgoals):
 1. is_gen_path p \<Longrightarrow> is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])
 2. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>V. p \<noteq> [v] \<Longrightarrow> 0 < walk_length p
[PROOF STEP]
show "is_cycle p \<or> is_path p \<or> (\<exists> v \<in> V. p = [v])"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V. p \<noteq> [v] \<Longrightarrow> 0 < walk_length p

goal (1 subgoal):
 1. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])
[PROOF STEP]
using a is_gen_path_path
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V. p \<noteq> [v] \<Longrightarrow> 0 < walk_length p
is_gen_path p
\<lbrakk>is_gen_path ?p; 0 < walk_length ?p; \<not> is_cycle ?p\<rbrakk> \<Longrightarrow> is_path ?p

goal (1 subgoal):
 1. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v])

goal (1 subgoal):
 1. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
show "is_cycle p \<or> is_path p \<or> (\<exists> v \<in> V. p = [v]) \<Longrightarrow> is_gen_path p "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
using is_gen_path_cycle is_path_gen_path is_gen_path_trivial
[PROOF STATE]
proof (prove)
using this:
is_cycle ?p \<Longrightarrow> is_gen_path ?p
is_path ?p \<Longrightarrow> is_gen_path ?p
?x \<in> V \<Longrightarrow> is_gen_path [?x]

goal (1 subgoal):
 1. is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_cycle p \<or> is_path p \<or> (\<exists>v\<in>V. p = [v]) \<Longrightarrow> is_gen_path p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cycles_ss_gen_paths: "cycles \<subseteq> gen_paths"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cycles \<subseteq> gen_paths
[PROOF STEP]
unfolding cycles_def gen_paths_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect is_cycle \<subseteq> Collect is_gen_path
[PROOF STEP]
using is_gen_path_cycle
[PROOF STATE]
proof (prove)
using this:
is_cycle ?p \<Longrightarrow> is_gen_path ?p

goal (1 subgoal):
 1. Collect is_cycle \<subseteq> Collect is_gen_path
[PROOF STEP]
by auto


[STATEMENT]
lemma gen_paths_ss: "gen_paths \<subseteq> cycles \<union> paths \<union> {[v] | v. v \<in> V}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_paths \<subseteq> cycles \<union> paths \<union> {[v] |v. v \<in> V}
[PROOF STEP]
unfolding gen_paths_def cycles_def paths_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect is_gen_path \<subseteq> Collect is_cycle \<union> Collect is_path \<union> {[v] |v. v \<in> V}
[PROOF STEP]
using is_gen_path_options
[PROOF STATE]
proof (prove)
using this:
is_gen_path ?p = (is_cycle ?p \<or> is_path ?p \<or> (\<exists>v\<in>V. ?p = [v]))

goal (1 subgoal):
 1. Collect is_gen_path \<subseteq> Collect is_cycle \<union> Collect is_path \<union> {[v] |v. v \<in> V}
[PROOF STEP]
by auto


[STATEMENT]
lemma distinct_edgesI:
  assumes "distinct p" shows "distinct (walk_edges p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (walk_edges p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (walk_edges p)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
distinct p
[PROOF STEP]
have "?thesis" "\<And>u. u \<notin> set p \<Longrightarrow> (\<And>v. u \<noteq> v \<Longrightarrow> {u,v} \<notin> set (walk_edges p))"
[PROOF STATE]
proof (prove)
using this:
distinct p

goal (1 subgoal):
 1. distinct (walk_edges p) &&& (\<And>u. u \<notin> set p \<Longrightarrow> (\<And>v. u \<noteq> v \<Longrightarrow> {u, v} \<notin> set (walk_edges p)))
[PROOF STEP]
by (induct p rule: walk_edges.induct) auto
[PROOF STATE]
proof (state)
this:
distinct (walk_edges p)
\<lbrakk>?u \<notin> set p; ?u \<noteq> ?v\<rbrakk> \<Longrightarrow> {?u, ?v} \<notin> set (walk_edges p)

goal (1 subgoal):
 1. distinct (walk_edges p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (walk_edges p)
\<lbrakk>?u \<notin> set p; ?u \<noteq> ?v\<rbrakk> \<Longrightarrow> {?u, ?v} \<notin> set (walk_edges p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (walk_edges p)
\<lbrakk>?u \<notin> set p; ?u \<noteq> ?v\<rbrakk> \<Longrightarrow> {?u, ?v} \<notin> set (walk_edges p)

goal (1 subgoal):
 1. distinct (walk_edges p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (walk_edges p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scycles_distinct_edges:
  assumes "c \<in> cycles" "3 \<le> walk_length c" shows "distinct (walk_edges c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
c \<in> cycles
3 \<le> walk_length c
[PROOF STEP]
have c_props: "distinct (tl c)" "4 \<le> length c" "hd c = last c"
[PROOF STATE]
proof (prove)
using this:
c \<in> cycles
3 \<le> walk_length c

goal (1 subgoal):
 1. distinct (tl c) &&& 4 \<le> length c &&& hd c = last c
[PROOF STEP]
by (auto simp add: cycles_def is_cycle_def is_closed_walk_def walk_length_conv)
[PROOF STATE]
proof (state)
this:
distinct (tl c)
4 \<le> length c
hd c = last c

goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (tl c)
4 \<le> length c
hd c = last c
[PROOF STEP]
have "{hd c, hd (tl c)} \<notin> set (walk_edges (tl c))"
[PROOF STATE]
proof (prove)
using this:
distinct (tl c)
4 \<le> length c
hd c = last c

goal (1 subgoal):
 1. {hd c, hd (tl c)} \<notin> set (walk_edges (tl c))
[PROOF STEP]
proof (induct c rule: walk_edges.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
case (3 x y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys)))
distinct (tl (x # y # ys))
4 \<le> length (x # y # ys)
hd (x # y # ys) = last (x # y # ys)

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys)))
distinct (tl (x # y # ys))
4 \<le> length (x # y # ys)
hd (x # y # ys) = last (x # y # ys)
[PROOF STEP]
have "hd ys \<noteq> last ys"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys)))
distinct (tl (x # y # ys))
4 \<le> length (x # y # ys)
hd (x # y # ys) = last (x # y # ys)

goal (1 subgoal):
 1. hd ys \<noteq> last ys
[PROOF STEP]
by (cases ys) auto
[PROOF STATE]
proof (state)
this:
hd ys \<noteq> last ys

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hd ys \<noteq> last ys

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys)))
distinct (tl (x # y # ys))
4 \<le> length (x # y # ys)
hd (x # y # ys) = last (x # y # ys)
[PROOF STEP]
have "walk_edges (y # ys) = {y, hd ys} # walk_edges ys"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys)))
distinct (tl (x # y # ys))
4 \<le> length (x # y # ys)
hd (x # y # ys) = last (x # y # ys)

goal (1 subgoal):
 1. walk_edges (y # ys) = {y, hd ys} # walk_edges ys
[PROOF STEP]
by (cases ys) auto
[PROOF STATE]
proof (state)
this:
walk_edges (y # ys) = {y, hd ys} # walk_edges ys

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
walk_edges (y # ys) = {y, hd ys} # walk_edges ys

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
walk_edges (y # ys) = {y, hd ys} # walk_edges ys

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
have "set (walk_edges xs) \<subseteq> Pow (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges xs) \<subseteq> Pow (set xs)
[PROOF STEP]
by (induct xs rule: walk_edges.induct) auto
[PROOF STATE]
proof (state)
this:
set (walk_edges xs) \<subseteq> Pow (set xs)

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (walk_edges ?xs2) \<subseteq> Pow (set ?xs2)

goal (3 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
 3. \<And>x y ys. \<lbrakk>\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys))); distinct (tl (x # y # ys)); 4 \<le> length (x # y # ys); hd (x # y # ys) = last (x # y # ys)\<rbrakk> \<Longrightarrow> {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hd ys \<noteq> last ys
walk_edges (y # ys) = {y, hd ys} # walk_edges ys
set (walk_edges ?xs2) \<subseteq> Pow (set ?xs2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd ys \<noteq> last ys
walk_edges (y # ys) = {y, hd ys} # walk_edges ys
set (walk_edges ?xs2) \<subseteq> Pow (set ?xs2)

goal (1 subgoal):
 1. {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
hd ys \<noteq> last ys
walk_edges (y # ys) = {y, hd ys} # walk_edges ys
set (walk_edges ?xs2) \<subseteq> Pow (set ?xs2)
\<lbrakk>distinct (tl (y # ys)); 4 \<le> length (y # ys); hd (y # ys) = last (y # ys)\<rbrakk> \<Longrightarrow> {hd (y # ys), hd (tl (y # ys))} \<notin> set (walk_edges (tl (y # ys)))
distinct (tl (x # y # ys))
4 \<le> length (x # y # ys)
hd (x # y # ys) = last (x # y # ys)

goal (1 subgoal):
 1. {hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{hd (x # y # ys), hd (tl (x # y # ys))} \<notin> set (walk_edges (tl (x # y # ys)))

goal (2 subgoals):
 1. \<lbrakk>distinct (tl []); 4 \<le> length []; hd [] = last []\<rbrakk> \<Longrightarrow> {hd [], hd (tl [])} \<notin> set (walk_edges (tl []))
 2. \<And>x. \<lbrakk>distinct (tl [x]); 4 \<le> length [x]; hd [x] = last [x]\<rbrakk> \<Longrightarrow> {hd [x], hd (tl [x])} \<notin> set (walk_edges (tl [x]))
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
{hd c, hd (tl c)} \<notin> set (walk_edges (tl c))

goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{hd c, hd (tl c)} \<notin> set (walk_edges (tl c))

goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
c \<in> cycles
3 \<le> walk_length c
[PROOF STEP]
have "distinct (walk_edges (tl c))"
[PROOF STATE]
proof (prove)
using this:
c \<in> cycles
3 \<le> walk_length c

goal (1 subgoal):
 1. distinct (walk_edges (tl c))
[PROOF STEP]
by (intro distinct_edgesI) (simp add: cycles_def is_cycle_def)
[PROOF STATE]
proof (state)
this:
distinct (walk_edges (tl c))

goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{hd c, hd (tl c)} \<notin> set (walk_edges (tl c))
distinct (walk_edges (tl c))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{hd c, hd (tl c)} \<notin> set (walk_edges (tl c))
distinct (walk_edges (tl c))

goal (1 subgoal):
 1. distinct (walk_edges c)
[PROOF STEP]
by(cases c, simp_all)
      (metis distinct.simps(1) distinct.simps(2) list.sel(1) list.sel(3) walk_edges.elims)
[PROOF STATE]
proof (state)
this:
distinct (walk_edges c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_paths: "finite paths"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite paths
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite paths
[PROOF STEP]
have ss: "paths \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> (card (V))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paths \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> order}
[PROOF STEP]
proof (rule, simp, intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> paths \<Longrightarrow> set x \<subseteq> V
 2. \<And>x. x \<in> paths \<Longrightarrow> length x \<le> order
[PROOF STEP]
show 1: "\<And>x. x \<in> paths \<Longrightarrow> set x \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> paths \<Longrightarrow> set x \<subseteq> V
[PROOF STEP]
unfolding paths_def is_path_def is_open_walk_def is_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {p. ((set p \<subseteq> V \<and> set (walk_edges p) \<subseteq> E \<and> p \<noteq> []) \<and> hd p \<noteq> last p) \<and> distinct p} \<Longrightarrow> set x \<subseteq> V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> paths \<Longrightarrow> set ?x \<subseteq> V

goal (1 subgoal):
 1. \<And>x. x \<in> paths \<Longrightarrow> length x \<le> order
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> paths \<Longrightarrow> length x \<le> order
[PROOF STEP]
assume a: "x \<in> paths"
[PROOF STATE]
proof (state)
this:
x \<in> paths

goal (1 subgoal):
 1. \<And>x. x \<in> paths \<Longrightarrow> length x \<le> order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> paths
[PROOF STEP]
have "distinct x"
[PROOF STATE]
proof (prove)
using this:
x \<in> paths

goal (1 subgoal):
 1. distinct x
[PROOF STEP]
using paths_def is_path_def
[PROOF STATE]
proof (prove)
using this:
x \<in> paths
paths \<equiv> Collect is_path
is_path ?xs \<equiv> is_open_walk ?xs \<and> distinct ?xs

goal (1 subgoal):
 1. distinct x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
distinct x

goal (1 subgoal):
 1. \<And>x. x \<in> paths \<Longrightarrow> length x \<le> order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct x
[PROOF STEP]
have eq: "length x = card (set x)"
[PROOF STATE]
proof (prove)
using this:
distinct x

goal (1 subgoal):
 1. length x = card (set x)
[PROOF STEP]
by (simp add: distinct_card)
[PROOF STATE]
proof (state)
this:
length x = card (set x)

goal (1 subgoal):
 1. \<And>x. x \<in> paths \<Longrightarrow> length x \<le> order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length x = card (set x)
[PROOF STEP]
show "length x \<le> order"
[PROOF STATE]
proof (prove)
using this:
length x = card (set x)

goal (1 subgoal):
 1. length x \<le> order
[PROOF STEP]
using a 1
[PROOF STATE]
proof (prove)
using this:
length x = card (set x)
x \<in> paths
?x \<in> paths \<Longrightarrow> set ?x \<subseteq> V

goal (1 subgoal):
 1. length x \<le> order
[PROOF STEP]
by (simp add: card_mono finV)
[PROOF STATE]
proof (state)
this:
length x \<le> order

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
paths \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> order}

goal (1 subgoal):
 1. finite paths
[PROOF STEP]
have "finite {xs. set xs \<subseteq> V \<and> length xs \<le> (card (V))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {xs. set xs \<subseteq> V \<and> length xs \<le> order}
[PROOF STEP]
using finV
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite {xs. set xs \<subseteq> V \<and> length xs \<le> order}
[PROOF STEP]
by (simp add: finite_lists_length_le)
[PROOF STATE]
proof (state)
this:
finite {xs. set xs \<subseteq> V \<and> length xs \<le> order}

goal (1 subgoal):
 1. finite paths
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {xs. set xs \<subseteq> V \<and> length xs \<le> order}

goal (1 subgoal):
 1. finite paths
[PROOF STEP]
using ss finite_subset
[PROOF STATE]
proof (prove)
using this:
finite {xs. set xs \<subseteq> V \<and> length xs \<le> order}
paths \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> order}
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite paths
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite paths

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_cycles: "finite (cycles)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cycles
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite cycles
[PROOF STEP]
have "cycles \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> Suc (card (V))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cycles \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}
[PROOF STEP]
proof (rule, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
assume "p \<in> cycles"
[PROOF STATE]
proof (state)
this:
p \<in> cycles

goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> cycles
[PROOF STEP]
have "distinct (tl p)" and "set p \<subseteq> V"
[PROOF STATE]
proof (prove)
using this:
p \<in> cycles

goal (1 subgoal):
 1. distinct (tl p) &&& set p \<subseteq> V
[PROOF STEP]
unfolding cycles_def walks_def is_cycle_def is_closed_walk_def is_walk_def
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. ((set p \<subseteq> V \<and> set (walk_edges p) \<subseteq> E \<and> p \<noteq> []) \<and> hd p = last p) \<and> 1 \<le> walk_length p \<and> distinct (tl p)}

goal (1 subgoal):
 1. distinct (tl p) &&& set p \<subseteq> V
[PROOF STEP]
by (simp_all)
[PROOF STATE]
proof (state)
this:
distinct (tl p)
set p \<subseteq> V

goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (tl p)
set p \<subseteq> V
[PROOF STEP]
have "set (tl p) \<subseteq> V"
[PROOF STATE]
proof (prove)
using this:
distinct (tl p)
set p \<subseteq> V

goal (1 subgoal):
 1. set (tl p) \<subseteq> V
[PROOF STEP]
by (cases p) auto
[PROOF STATE]
proof (state)
this:
set (tl p) \<subseteq> V

goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
with finV
[PROOF STATE]
proof (chain)
picking this:
finite V
set (tl p) \<subseteq> V
[PROOF STEP]
have "card (set (tl p)) \<le> card (V)"
[PROOF STATE]
proof (prove)
using this:
finite V
set (tl p) \<subseteq> V

goal (1 subgoal):
 1. card (set (tl p)) \<le> order
[PROOF STEP]
by (rule card_mono)
[PROOF STATE]
proof (state)
this:
card (set (tl p)) \<le> order

goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (set (tl p)) \<le> order
[PROOF STEP]
have "length (p) \<le> 1 + card (V)"
[PROOF STATE]
proof (prove)
using this:
card (set (tl p)) \<le> order

goal (1 subgoal):
 1. length p \<le> 1 + order
[PROOF STEP]
using distinct_card[OF \<open>distinct (tl p)\<close>]
[PROOF STATE]
proof (prove)
using this:
card (set (tl p)) \<le> order
card (set (tl p)) = length (tl p)

goal (1 subgoal):
 1. length p \<le> 1 + order
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p \<le> 1 + order

goal (1 subgoal):
 1. \<And>x. x \<in> cycles \<Longrightarrow> set x \<subseteq> V \<and> length x \<le> Suc order
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length p \<le> 1 + order
[PROOF STEP]
show "set p \<subseteq> V \<and> length p \<le> Suc (card (V))"
[PROOF STATE]
proof (prove)
using this:
length p \<le> 1 + order

goal (1 subgoal):
 1. set p \<subseteq> V \<and> length p \<le> Suc order
[PROOF STEP]
by (simp add: \<open>set p \<subseteq> V\<close>)
[PROOF STATE]
proof (state)
this:
set p \<subseteq> V \<and> length p \<le> Suc order

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cycles \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}

goal (1 subgoal):
 1. finite cycles
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cycles \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}

goal (1 subgoal):
 1. finite cycles
[PROOF STEP]
have "finite {xs. set xs \<subseteq> V \<and> length xs \<le> Suc (card (V))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}
[PROOF STEP]
using finV
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}
[PROOF STEP]
by (rule finite_lists_length_le)
[PROOF STATE]
proof (state)
this:
finite {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}

goal (1 subgoal):
 1. finite cycles
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cycles \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}
finite {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cycles \<subseteq> {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}
finite {xs. set xs \<subseteq> V \<and> length xs \<le> Suc order}

goal (1 subgoal):
 1. finite cycles
[PROOF STEP]
by (rule finite_subset)
[PROOF STATE]
proof (state)
this:
finite cycles

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_gen_paths: "finite (gen_paths)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite gen_paths
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite gen_paths
[PROOF STEP]
have "finite ({[v] | v . v \<in> V})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {[v] |v. v \<in> V}
[PROOF STEP]
using finV
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite {[v] |v. v \<in> V}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {[v] |v. v \<in> V}

goal (1 subgoal):
 1. finite gen_paths
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {[v] |v. v \<in> V}

goal (1 subgoal):
 1. finite gen_paths
[PROOF STEP]
using gen_paths_ss finite_cycles finite_paths finite_subset
[PROOF STATE]
proof (prove)
using this:
finite {[v] |v. v \<in> V}
gen_paths \<subseteq> cycles \<union> paths \<union> {[v] |v. v \<in> V}
finite cycles
finite paths
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite gen_paths
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite gen_paths

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma suminf_comparison:
  assumes "summable f" and gf: "\<And>n. norm (g n) \<le> f n"
  shows "suminf g \<le> suminf f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suminf g \<le> suminf f
[PROOF STEP]
proof (rule suminf_le)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. g n \<le> f n
 2. summable g
 3. summable f
[PROOF STEP]
show "g n \<le> f n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g n \<le> f n
[PROOF STEP]
using gf[of n]
[PROOF STATE]
proof (prove)
using this:
norm (g n) \<le> f n

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

goal (2 subgoals):
 1. summable g
 2. summable f
[PROOF STEP]
show "summable g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable g
[PROOF STEP]
using assms summable_comparison_test'
[PROOF STATE]
proof (prove)
using this:
summable f
norm (g ?n) \<le> f ?n
\<lbrakk>summable ?g; \<And>n. ?N \<le> n \<Longrightarrow> norm (?f n) \<le> ?g n\<rbrakk> \<Longrightarrow> summable ?f

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

goal (1 subgoal):
 1. summable f
[PROOF STEP]
show "summable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
summable f

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tendsto_of_int_diff_0:
  assumes "(\<lambda>n. f n - of_int(g n)) \<longlonglongrightarrow> (0::real)" "\<forall>\<^sub>F n in sequentially. f n > 0"
  shows "\<forall>\<^sub>F n in sequentially. 0 \<le> g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> g n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> g n
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. \<bar>f n - of_int(g n)\<bar> < 1 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<bar>f n - real_of_int (g n)\<bar> < 1 / 2
[PROOF STEP]
using assms(1)[unfolded tendsto_iff,rule_format,of "1/2"]
[PROOF STATE]
proof (prove)
using this:
0 < 1 / 2 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. dist (f x - real_of_int (g x)) 0 < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<bar>f n - real_of_int (g n)\<bar> < 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. \<bar>f n - real_of_int (g n)\<bar> < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> g n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. \<bar>f n - real_of_int (g n)\<bar> < 1 / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. \<bar>f n - real_of_int (g n)\<bar> < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> g n
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. \<bar>f n - real_of_int (g n)\<bar> < 1 / 2
\<forall>\<^sub>F n in sequentially. 0 < f n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> g n
[PROOF STEP]
by eventually_elim linarith
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. 0 \<le> g n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eventually_mono_sequentially:
  assumes "eventually P sequentially"
  assumes "\<And>x. P (x+k) \<Longrightarrow> Q (x+k)"
  shows "eventually Q sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually Q sequentially
[PROOF STEP]
using sequentially_offset[OF assms(1),of k]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F i in sequentially. P (i + k)

goal (1 subgoal):
 1. eventually Q sequentially
[PROOF STEP]
apply (subst eventually_sequentially_seg[symmetric,of _ k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F i in sequentially. P (i + k) \<Longrightarrow> \<forall>\<^sub>F n in sequentially. Q (n + k)
[PROOF STEP]
apply (elim eventually_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. P (x + k) \<Longrightarrow> Q (x + k)
[PROOF STEP]
by fact


[STATEMENT]
lemma frequently_eventually_at_top:
  fixes P Q::"'a::linorder \<Rightarrow> bool"
  assumes "frequently P at_top" "eventually Q at_top"
  shows "frequently (\<lambda>x. P x \<and> (\<forall>y\<ge>x. Q y) ) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<^sub>F x in at_top. P x \<and> (\<forall>y\<ge>x. Q y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
frequently P at_top
eventually Q at_top

goal (1 subgoal):
 1. \<exists>\<^sub>F x in at_top. P x \<and> (\<forall>y\<ge>x. Q y)
[PROOF STEP]
unfolding frequently_def eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
\<nexists>N. \<forall>n\<ge>N. \<not> P n
\<exists>N. \<forall>n\<ge>N. Q n

goal (1 subgoal):
 1. \<nexists>N. \<forall>n\<ge>N. \<not> (P n \<and> (\<forall>y\<ge>n. Q y))
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) le_cases order_trans)


[STATEMENT]
lemma eventually_at_top_mono:
  fixes P Q::"'a::linorder \<Rightarrow> bool"
  assumes event_P:"eventually P at_top"
  assumes PQ_imp:"\<And>x. x\<ge>z \<Longrightarrow> \<forall>y\<ge>x. P y \<Longrightarrow> Q x"
  shows "eventually Q at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually Q at_top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eventually Q at_top
[PROOF STEP]
obtain N where "\<forall>n\<ge>N. P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. P n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson event_P eventually_at_top_linorder)
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. P n

goal (1 subgoal):
 1. eventually Q at_top
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<ge>N. P n
[PROOF STEP]
have "Q x" when "x \<ge> max N z" for x
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. P n

goal (1 subgoal):
 1. Q x
[PROOF STEP]
using PQ_imp that
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. P n
\<lbrakk>z \<le> ?x; \<forall>y\<ge>?x. P y\<rbrakk> \<Longrightarrow> Q ?x
max N z \<le> x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max N z \<le> ?x \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. eventually Q at_top
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max N z \<le> ?x \<Longrightarrow> Q ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
max N z \<le> ?x \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. eventually Q at_top
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
max N z \<le> ?x \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. Q n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eventually Q at_top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frequently_at_top_elim:
  fixes P Q::"'a::linorder \<Rightarrow> bool"
  assumes "\<exists>\<^sub>Fx in at_top. P x"
  assumes "\<And>i. P i \<Longrightarrow> \<exists>j>i. Q j"
  shows "\<exists>\<^sub>Fx in at_top. Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frequently Q at_top
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
frequently P at_top
P ?i \<Longrightarrow> \<exists>j>?i. Q j

goal (1 subgoal):
 1. frequently Q at_top
[PROOF STEP]
unfolding frequently_def eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
\<nexists>N. \<forall>n\<ge>N. \<not> P n
P ?i \<Longrightarrow> \<exists>j>?i. Q j

goal (1 subgoal):
 1. \<nexists>N. \<forall>n\<ge>N. \<not> Q n
[PROOF STEP]
by (meson leD le_cases less_le_trans)


[STATEMENT]
lemma less_Liminf_iff:
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
  shows "Liminf F X < C \<longleftrightarrow> (\<exists>y<C. frequently (\<lambda>x. y \<ge> X x) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Liminf F X < C) = (\<exists>y<C. \<exists>\<^sub>F x in F. X x \<le> y)
[PROOF STEP]
by (force simp: not_less not_frequently not_le le_Liminf_iff simp flip: Not_eq_iff)


[STATEMENT]
lemma sequentially_even_odd_imp:
  assumes "\<forall>\<^sub>F N in sequentially. P (2*N)" "\<forall>\<^sub>F N in sequentially. P (2*N+1)"
  shows "\<forall>\<^sub>F n in sequentially. P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P sequentially
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eventually P sequentially
[PROOF STEP]
obtain N where N_P:"\<forall>x\<ge>N.  P (2 * x) \<and> P (2 * x + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<forall>x\<ge>N. P (2 * x) \<and> P (2 * x + 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eventually_conj[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. P (2 * x) \<and> P (2 * x + 1)

goal (1 subgoal):
 1. (\<And>N. \<forall>x\<ge>N. P (2 * x) \<and> P (2 * x + 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. P (2 * n) \<and> P (2 * n + 1)

goal (1 subgoal):
 1. (\<And>N. \<forall>x\<ge>N. P (2 * x) \<and> P (2 * x + 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<ge>N. P (2 * x) \<and> P (2 * x + 1)

goal (1 subgoal):
 1. eventually P sequentially
[PROOF STEP]
have "P n" when "n \<ge> 2*N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P n
[PROOF STEP]
define n' where "n'= n div 2"
[PROOF STATE]
proof (state)
this:
n' = n div 2

goal (1 subgoal):
 1. P n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n' = n div 2
[PROOF STEP]
have "n' \<ge> N"
[PROOF STATE]
proof (prove)
using this:
n' = n div 2

goal (1 subgoal):
 1. N \<le> n'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n' = n div 2
2 * N \<le> n

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

goal (1 subgoal):
 1. P n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> n'
[PROOF STEP]
have "P (2 * n') \<and> P (2 * n' + 1)"
[PROOF STATE]
proof (prove)
using this:
N \<le> n'

goal (1 subgoal):
 1. P (2 * n') \<and> P (2 * n' + 1)
[PROOF STEP]
using N_P
[PROOF STATE]
proof (prove)
using this:
N \<le> n'
\<forall>x\<ge>N. P (2 * x) \<and> P (2 * x + 1)

goal (1 subgoal):
 1. P (2 * n') \<and> P (2 * n' + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (2 * n') \<and> P (2 * n' + 1)

goal (1 subgoal):
 1. P n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P (2 * n') \<and> P (2 * n' + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P (2 * n') \<and> P (2 * n' + 1)

goal (1 subgoal):
 1. P n
[PROOF STEP]
unfolding n'_def
[PROOF STATE]
proof (prove)
using this:
P (2 * (n div 2)) \<and> P (2 * (n div 2) + 1)

goal (1 subgoal):
 1. P n
[PROOF STEP]
by (cases "even n") auto
[PROOF STATE]
proof (state)
this:
P n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 * N \<le> ?n \<Longrightarrow> P ?n

goal (1 subgoal):
 1. eventually P sequentially
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * N \<le> ?n \<Longrightarrow> P ?n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * N \<le> ?n \<Longrightarrow> P ?n

goal (1 subgoal):
 1. eventually P sequentially
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
2 * N \<le> ?n \<Longrightarrow> P ?n

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. P n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eventually P sequentially

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aux_series_summable: "summable (\<lambda>n. b n / (\<Prod>k\<le>n. a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. \<bar>b x\<bar> / (a (x-1) * a x) < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < e
[PROOF STEP]
using ab_tendsto[unfolded tendsto_iff]
[PROOF STATE]
proof (prove)
using this:
\<forall>e>0. \<forall>\<^sub>F x in sequentially. dist (real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x)) 0 < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < e
[PROOF STEP]
apply (simp add: abs_mult flip: of_int_abs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>0 < e; \<forall>e>0. \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / (real_of_int \<bar>a (x - Suc 0)\<bar> * real_of_int \<bar>a x\<bar>) < e\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / (real_of_int (a (x - Suc 0)) * real_of_int (a x)) < e
[PROOF STEP]
by (subst (asm) (2) abs_of_pos,use \<open>\<forall> n. a n > 0\<close> in auto)+
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < ?e

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
from this[of 1]
[PROOF STATE]
proof (chain)
picking this:
0 < 1 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < 1
[PROOF STEP]
have "\<forall>\<^sub>F x in sequentially. \<bar>real_of_int(b x)\<bar> < (a (x-1) * a x)"
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < 1

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)
[PROOF STEP]
using \<open>\<forall> n. a n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < 1
\<forall>n. 0 < a n

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "\<forall>n. (\<Prod>k\<le>n. real_of_int (a k)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. \<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))
[PROOF STEP]
by (auto intro!:linordered_semidom_class.prod_pos)
[PROOF STATE]
proof (state)
this:
\<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in sequentially. \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)
\<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. \<bar>b n\<bar> / (\<Prod>k\<le>n. a k)
                        < (a (n-1) * a n) / (\<Prod>k\<le>n. a k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)
\<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
[PROOF STEP]
apply (elim eventually_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k)); \<bar>real_of_int (b x)\<bar> < real_of_int (a (x - 1) * a x)\<rbrakk> \<Longrightarrow> real_of_int \<bar>b x\<bar> / real_of_int (prod a {..x}) < real_of_int (a (x - 1) * a x) / real_of_int (prod a {..x})
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "\<bar>b n\<bar> / (\<Prod>k\<le>n. a k) = norm (b n / (\<Prod>k\<le>n. a k))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) = norm (real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
using \<open>\<forall>n. (\<Prod>k\<le>n. real_of_int (a k)) > 0\<close>[rule_format,of n]
[PROOF STATE]
proof (prove)
using this:
0 < (\<Prod>k\<le>n. real_of_int (a k))

goal (1 subgoal):
 1. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) = norm (real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>b ?n\<bar> / real_of_int (prod a {..?n}) = norm (real_of_int (b ?n) / real_of_int (prod a {..?n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
real_of_int \<bar>b ?n\<bar> / real_of_int (prod a {..?n}) = norm (real_of_int (b ?n) / real_of_int (prod a {..?n}))
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. norm (b n / (\<Prod>k\<le>n. a k))
                        < (a (n-1) * a n) / (\<Prod>k\<le>n. a k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (prod a {..n}) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
real_of_int \<bar>b ?n\<bar> / real_of_int (prod a {..?n}) = norm (real_of_int (b ?n) / real_of_int (prod a {..?n}))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "summable (\<lambda>n. (a (n-1) * a n) / (\<Prod>k\<le>n. a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
obtain s where a_gt_1:"\<forall> n\<ge>s. a n >1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<forall>n\<ge>s. 1 < a n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a_large[unfolded eventually_at_top_linorder]
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. 1 < a n

goal (1 subgoal):
 1. (\<And>s. \<forall>n\<ge>s. 1 < a n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>s. 1 < a n

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
define cc where "cc= (\<Prod>k<s. a k)"
[PROOF STATE]
proof (state)
this:
cc = prod a {..<s}

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "cc>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < cc
[PROOF STEP]
unfolding cc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < prod a {..<s}
[PROOF STEP]
by (meson a_pos prod_pos)
[PROOF STATE]
proof (state)
this:
0 < cc

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "(\<Prod>k\<le>n+s. a k) \<ge> cc * 2^n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
have "prod a {s..<Suc (s + n)} \<ge> 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n \<le> prod a {s..<Suc (s + n)}
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 ^ 0 \<le> prod a {s..<Suc (s + 0)}
 2. \<And>n. 2 ^ n \<le> prod a {s..<Suc (s + n)} \<Longrightarrow> 2 ^ Suc n \<le> prod a {s..<Suc (s + Suc n)}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. 2 ^ 0 \<le> prod a {s..<Suc (s + 0)}
 2. \<And>n. 2 ^ n \<le> prod a {s..<Suc (s + n)} \<Longrightarrow> 2 ^ Suc n \<le> prod a {s..<Suc (s + Suc n)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ 0 \<le> prod a {s..<Suc (s + 0)}
[PROOF STEP]
using a_gt_1
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>s. 1 < a n

goal (1 subgoal):
 1. 2 ^ 0 \<le> prod a {s..<Suc (s + 0)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ 0 \<le> prod a {s..<Suc (s + 0)}

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

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

goal (1 subgoal):
 1. \<And>n. 2 ^ n \<le> prod a {s..<Suc (s + n)} \<Longrightarrow> 2 ^ Suc n \<le> prod a {s..<Suc (s + Suc n)}
[PROOF STEP]
have "a (s + Suc n) \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> a (s + Suc n)
[PROOF STEP]
using a_gt_1
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>s. 1 < a n

goal (1 subgoal):
 1. 2 \<le> a (s + Suc n)
[PROOF STEP]
by (smt le_add1)
[PROOF STATE]
proof (state)
this:
2 \<le> a (s + Suc n)

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

goal (1 subgoal):
 1. 2 ^ Suc n \<le> prod a {s..<Suc (s + Suc n)}
[PROOF STEP]
apply (subst prod.atLeastLessThan_Suc,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n \<le> prod a {s..<Suc (s + n)}; 2 \<le> a (s + Suc n)\<rbrakk> \<Longrightarrow> 2 ^ Suc n \<le> prod a {s..<s + Suc n} * a (s + Suc n)
[PROOF STEP]
using mult_mono'[of 2 "a (Suc (s + n))" " 2 ^ n" "prod a {s..<Suc (s + n)}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> a (Suc (s + n)); 2 ^ n \<le> prod a {s..<Suc (s + n)}; 0 \<le> 2; 0 \<le> 2 ^ n\<rbrakk> \<Longrightarrow> 2 * 2 ^ n \<le> a (Suc (s + n)) * prod a {s..<Suc (s + n)}

goal (1 subgoal):
 1. \<lbrakk>2 ^ n \<le> prod a {s..<Suc (s + n)}; 2 \<le> a (s + Suc n)\<rbrakk> \<Longrightarrow> 2 ^ Suc n \<le> prod a {s..<s + Suc n} * a (s + Suc n)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
2 ^ Suc n \<le> prod a {s..<Suc (s + Suc n)}

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

goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
2 ^ n \<le> prod a {s..<Suc (s + n)}

goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
have "prod a {0..(n + s)} = prod a {..<s} * prod a {s..<Suc (s + n)} "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}
[PROOF STEP]
using prod.atLeastLessThan_concat[of 0 s "s+n+1" a]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> s; s \<le> s + n + 1\<rbrakk> \<Longrightarrow> prod a {0..<s} * prod a {s..<s + n + 1} = prod a {0..<s + n + 1}

goal (1 subgoal):
 1. prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}
[PROOF STEP]
by (simp add: add.commute lessThan_atLeast0 prod.atLeastLessThan_concat prod.head_if)
[PROOF STATE]
proof (state)
this:
prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}

goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
2 ^ n \<le> prod a {s..<Suc (s + n)}
prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> prod a {s..<Suc (s + n)}
prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}

goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
using \<open>cc>0\<close>
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> prod a {s..<Suc (s + n)}
prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}
0 < cc

goal (1 subgoal):
 1. cc * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
unfolding cc_def
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> prod a {s..<Suc (s + n)}
prod a {0..n + s} = prod a {..<s} * prod a {s..<Suc (s + n)}
0 < prod a {..<s}

goal (1 subgoal):
 1. prod a {..<s} * 2 ^ n \<le> prod a {..n + s}
[PROOF STEP]
by (simp add: atLeast0AtMost)
[PROOF STATE]
proof (state)
this:
cc * 2 ^ n \<le> prod a {..n + s}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cc * 2 ^ ?n \<le> prod a {..?n + s}

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cc * 2 ^ ?n \<le> prod a {..?n + s}
[PROOF STEP]
have "1/(\<Prod>k\<le>n+s. a k) \<le> 1/(cc * 2^n)" for n
[PROOF STATE]
proof (prove)
using this:
cc * 2 ^ ?n \<le> prod a {..?n + s}

goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. cc * 2 ^ n \<le> prod a {..n + s}) \<Longrightarrow> 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
assume asm:"\<And>n. cc * 2 ^ n \<le> prod a {..n + s}"
[PROOF STATE]
proof (state)
this:
cc * 2 ^ ?n \<le> prod a {..?n + s}

goal (1 subgoal):
 1. (\<And>n. cc * 2 ^ n \<le> prod a {..n + s}) \<Longrightarrow> 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cc * 2 ^ ?n \<le> prod a {..?n + s}
[PROOF STEP]
have "real_of_int (cc * 2 ^ n) \<le> prod a {..n + s}"
[PROOF STATE]
proof (prove)
using this:
cc * 2 ^ ?n \<le> prod a {..?n + s}

goal (1 subgoal):
 1. real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})
[PROOF STEP]
using of_int_le_iff
[PROOF STATE]
proof (prove)
using this:
cc * 2 ^ ?n \<le> prod a {..?n + s}
(of_int ?w \<le> of_int ?z) = (?w \<le> ?z)

goal (1 subgoal):
 1. real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})

goal (1 subgoal):
 1. (\<And>n. cc * 2 ^ n \<le> prod a {..n + s}) \<Longrightarrow> 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})

goal (1 subgoal):
 1. (\<And>n. cc * 2 ^ n \<le> prod a {..n + s}) \<Longrightarrow> 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
have "prod a {..n + s} >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < prod a {..n + s}
[PROOF STEP]
using \<open>cc>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < cc

goal (1 subgoal):
 1. 0 < prod a {..n + s}
[PROOF STEP]
by (simp add: a_pos prod_pos)
[PROOF STATE]
proof (state)
this:
0 < prod a {..n + s}

goal (1 subgoal):
 1. (\<And>n. cc * 2 ^ n \<le> prod a {..n + s}) \<Longrightarrow> 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})
0 < prod a {..n + s}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})
0 < prod a {..n + s}

goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
using \<open>cc>0\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_int (cc * 2 ^ n) \<le> real_of_int (prod a {..n + s})
0 < prod a {..n + s}
0 < cc

goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
by (auto simp:field_simps simp del:of_int_prod)
[PROOF STATE]
proof (state)
this:
1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 / real_of_int (prod a {..?n + s}) \<le> 1 / real_of_int (cc * 2 ^ ?n)

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 / real_of_int (prod a {..?n + s}) \<le> 1 / real_of_int (cc * 2 ^ ?n)

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
have "summable (\<lambda>n. 1/(cc * 2^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))
[PROOF STEP]
have "summable (\<lambda>n. 1/(2::int)^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (2 ^ n))
[PROOF STEP]
using summable_geometric[of "1/(2::int)"]
[PROOF STATE]
proof (prove)
using this:
norm (1 / real_of_int 2) < 1 \<Longrightarrow> summable ((^) (1 / real_of_int 2))

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (2 ^ n))
[PROOF STEP]
by (simp add:power_one_over)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 1 / real_of_int (2 ^ n))

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))
[PROOF STEP]
from summable_mult[OF this,of "1/cc"]
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. 1 / real_of_int cc * (1 / real_of_int (2 ^ n)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. 1 / real_of_int cc * (1 / real_of_int (2 ^ n)))

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 / real_of_int (prod a {..?n + s}) \<le> 1 / real_of_int (cc * 2 ^ ?n)
summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))
[PROOF STEP]
have "summable (\<lambda>n. 1 / (\<Prod>k\<le>n+s. a k))"
[PROOF STATE]
proof (prove)
using this:
1 / real_of_int (prod a {..?n + s}) \<le> 1 / real_of_int (cc * 2 ^ ?n)
summable (\<lambda>n. 1 / real_of_int (cc * 2 ^ n))

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (prod a {..n + s}))
[PROOF STEP]
apply (elim summable_comparison_test'[where N=0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<And>n. 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n); 0 \<le> n\<rbrakk> \<Longrightarrow> norm (1 / real_of_int (prod a {..n + s})) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
apply (unfold real_norm_def, subst abs_of_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<And>n. 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n); 0 \<le> n\<rbrakk> \<Longrightarrow> 0 < 1 / real_of_int (prod a {..n + s})
 2. \<And>n. \<lbrakk>\<And>n. 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n); 0 \<le> n\<rbrakk> \<Longrightarrow> 1 / real_of_int (prod a {..n + s}) \<le> 1 / real_of_int (cc * 2 ^ n)
[PROOF STEP]
by (auto simp add: \<open>\<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))\<close>)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n + s}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n + s}))
[PROOF STEP]
have "summable (\<lambda>n. 1 / (\<Prod>k\<le>n. a k))"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n + s}))

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (prod a {..n}))
[PROOF STEP]
apply (subst summable_iff_shift[where k=s,symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (prod a {..n + s})) \<Longrightarrow> summable (\<lambda>n. 1 / real_of_int (prod a {..n + s}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n}))
[PROOF STEP]
have "summable (\<lambda>n. (a (n+1) * a (n+2)) / (\<Prod>k\<le>n+2. a k))"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (prod a {..n})) \<Longrightarrow> summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
assume asm:"summable (\<lambda>n. 1 / real_of_int (prod a {..n}))"
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 1 / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (prod a {..n})) \<Longrightarrow> summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
have "1 / real_of_int (prod a {..n}) = (a (n+1) * a (n+2)) / (\<Prod>k\<le>n+2. a k)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n}) = real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n}) = real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2})
[PROOF STEP]
have "a (Suc (Suc n)) \<noteq> 0" "a (Suc n) \<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (Suc (Suc n)) \<noteq> 0 &&& a (Suc n) \<noteq> 0
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. a (Suc (Suc n)) \<noteq> 0 &&& a (Suc n) \<noteq> 0
[PROOF STEP]
by (metis less_irrefl)+
[PROOF STATE]
proof (state)
this:
a (Suc (Suc n)) \<noteq> 0
a (Suc n) \<noteq> 0

goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n}) = real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a (Suc (Suc n)) \<noteq> 0
a (Suc n) \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a (Suc (Suc n)) \<noteq> 0
a (Suc n) \<noteq> 0

goal (1 subgoal):
 1. 1 / real_of_int (prod a {..n}) = real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2})
[PROOF STEP]
by (simp add: atLeast0_atMost_Suc atMost_atLeast0)
[PROOF STATE]
proof (state)
this:
1 / real_of_int (prod a {..n}) = real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 / real_of_int (prod a {..?n}) = real_of_int (a (?n + 1) * a (?n + 2)) / real_of_int (prod a {..?n + 2})

goal (1 subgoal):
 1. summable (\<lambda>n. 1 / real_of_int (prod a {..n})) \<Longrightarrow> summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 / real_of_int (prod a {..?n}) = real_of_int (a (?n + 1) * a (?n + 2)) / real_of_int (prod a {..?n + 2})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 / real_of_int (prod a {..?n}) = real_of_int (a (?n + 1) * a (?n + 2)) / real_of_int (prod a {..?n + 2})

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
1 / real_of_int (prod a {..?n}) = real_of_int (a (?n + 1) * a (?n + 2)) / real_of_int (prod a {..?n + 2})
summable (\<lambda>n. 1 / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
show "summable (\<lambda>n. (a (n-1) * a n) / (\<Prod>k\<le>n. a k))"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
apply (subst summable_iff_shift[symmetric,of _ 2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (a (n + 1) * a (n + 2)) / real_of_int (prod a {..n + 2})) \<Longrightarrow> summable (\<lambda>n. real_of_int (a (n + 2 - 1) * a (n + 2)) / real_of_int (prod a {..n + 2}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
summable (\<lambda>n. real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
apply (elim summable_comparison_test_ev[rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) < real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n}) \<Longrightarrow> \<forall>\<^sub>F n in sequentially. norm (real_of_int (b n) / real_of_int (prod a {..n})) \<le> real_of_int (a (n - 1) * a n) / real_of_int (prod a {..n})
[PROOF STEP]
by (simp add: eventually_mono)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))

goal:
No subgoals!
[PROOF STEP]
qed