[STATEMENT]
lemma sum_Pinfty:
  fixes f :: "'a \<Rightarrow> ereal"
  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum f P = \<infinity>) = (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sum f P = \<infinity> \<Longrightarrow> finite P
 2. sum f P = \<infinity> \<Longrightarrow> \<exists>i\<in>P. f i = \<infinity>
 3. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
assume *: "sum f P = \<infinity>"
[PROOF STATE]
proof (state)
this:
sum f P = \<infinity>

goal (3 subgoals):
 1. sum f P = \<infinity> \<Longrightarrow> finite P
 2. sum f P = \<infinity> \<Longrightarrow> \<exists>i\<in>P. f i = \<infinity>
 3. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
show "finite P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite P
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite P \<Longrightarrow> False
[PROOF STEP]
assume "\<not> finite P"
[PROOF STATE]
proof (state)
this:
infinite P

goal (1 subgoal):
 1. infinite P \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
sum f P = \<infinity>
infinite P
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sum f P = \<infinity>
infinite P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite P

goal (2 subgoals):
 1. sum f P = \<infinity> \<Longrightarrow> \<exists>i\<in>P. f i = \<infinity>
 2. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
show "\<exists>i\<in>P. f i = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>P. f i = \<infinity>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<in>P. f i = \<infinity>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<in>P. f i = \<infinity>)
[PROOF STEP]
have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<in>P. f i = \<infinity>)

goal (1 subgoal):
 1. \<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in> P \<Longrightarrow> f ?i \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
with \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
finite P
?i \<in> P \<Longrightarrow> f ?i \<noteq> \<infinity>
[PROOF STEP]
have "sum f P \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
finite P
?i \<in> P \<Longrightarrow> f ?i \<noteq> \<infinity>

goal (1 subgoal):
 1. sum f P \<noteq> \<infinity>
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
sum f P \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
sum f P = \<infinity>
sum f P \<noteq> \<infinity>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sum f P = \<infinity>
sum f P \<noteq> \<infinity>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>P. f i = \<infinity>

goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
assume "finite P" and "i \<in> P" and "f i = \<infinity>"
[PROOF STATE]
proof (state)
this:
finite P
i \<in> P
f i = \<infinity>

goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite P
i \<in> P
f i = \<infinity>
[PROOF STEP]
show "sum f P = \<infinity>"
[PROOF STATE]
proof (prove)
using this:
finite P
i \<in> P
f i = \<infinity>

goal (1 subgoal):
 1. sum f P = \<infinity>
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<in> {}; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f {} = \<infinity>
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>i \<in> F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f F = \<infinity>; i \<in> insert x F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f (insert x F) = \<infinity>
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
\<lbrakk>i \<in> A; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f A = \<infinity>
i \<in> insert x A
f i = \<infinity>

goal (2 subgoals):
 1. \<lbrakk>i \<in> {}; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f {} = \<infinity>
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>i \<in> F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f F = \<infinity>; i \<in> insert x F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f (insert x F) = \<infinity>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (insert x A) = \<infinity>
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
\<lbrakk>i \<in> A; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f A = \<infinity>
i \<in> insert x A
f i = \<infinity>

goal (1 subgoal):
 1. sum f (insert x A) = \<infinity>
[PROOF STEP]
by (cases "x = i") auto
[PROOF STATE]
proof (state)
this:
sum f (insert x A) = \<infinity>

goal (1 subgoal):
 1. \<lbrakk>i \<in> {}; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f {} = \<infinity>
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
sum f P = \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed