[STATEMENT]
lemma ln_minus_ln_floor_bigo: "(\<lambda>x. ln x - ln (real (nat \<lfloor>x\<rfloor>))) \<in> O(\<lambda>_. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. ln x - ln (real (nat \<lfloor>x\<rfloor>))) \<in> O(\<lambda>_. 1)
[PROOF STEP]
proof (intro le_imp_bigo_real[of 1] eventually_mono[OF eventually_ge_at_top[of 1]])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
fix x :: real
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
assume x: "x \<ge> 1"
[PROOF STATE]
proof (state)
this:
1 \<le> x

goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
1 \<le> x
[PROOF STEP]
have *: "x - real (nat \<lfloor>x\<rfloor>) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> x

goal (1 subgoal):
 1. x - real (nat \<lfloor>x\<rfloor>) \<le> 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
x - real (nat \<lfloor>x\<rfloor>) \<le> 1

goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
1 \<le> x
[PROOF STEP]
have "ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> (x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
1 \<le> x

goal (1 subgoal):
 1. ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> (x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
by (intro ln_diff_le) auto
[PROOF STATE]
proof (state)
this:
ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> (x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>)

goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> (x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>)

goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
have "\<dots> \<le> 1 / 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>) \<le> 1 / 1
[PROOF STEP]
using x *
[PROOF STATE]
proof (prove)
using this:
1 \<le> x
x - real (nat \<lfloor>x\<rfloor>) \<le> 1

goal (1 subgoal):
 1. (x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>) \<le> 1 / 1
[PROOF STEP]
by (intro frac_le) auto
[PROOF STATE]
proof (state)
this:
(x - real (nat \<lfloor>x\<rfloor>)) / real (nat \<lfloor>x\<rfloor>) \<le> 1 / 1

goal (3 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
 3. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 / 1
[PROOF STEP]
show "ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1"
[PROOF STATE]
proof (prove)
using this:
ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 / 1

goal (1 subgoal):
 1. ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ln x - ln (real (nat \<lfloor>x\<rfloor>)) \<le> 1 * 1

goal (2 subgoals):
 1. 0 \<le> 1
 2. \<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ln x - ln (real (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
qed auto


[STATEMENT]
lemma cos_geD:
  assumes "cos x \<ge> cos a" "0 \<le> a" "a \<le> pi" "-pi \<le> x" "x \<le> pi"
  shows   "x \<in> {-a..a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {- a..a}
[PROOF STEP]
proof (cases "x \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
 2. \<not> 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> x

goal (2 subgoals):
 1. 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
 2. \<not> 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cos a \<le> cos x
0 \<le> a
a \<le> pi
- pi \<le> x
x \<le> pi
0 \<le> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cos a \<le> cos x
0 \<le> a
a \<le> pi
- pi \<le> x
x \<le> pi
0 \<le> x

goal (1 subgoal):
 1. x \<in> {- a..a}
[PROOF STEP]
by (subst (asm) cos_mono_le_eq) auto
[PROOF STATE]
proof (state)
this:
x \<in> {- a..a}

goal (1 subgoal):
 1. \<not> 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> x

goal (1 subgoal):
 1. \<not> 0 \<le> x \<Longrightarrow> x \<in> {- a..a}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cos a \<le> cos x
0 \<le> a
a \<le> pi
- pi \<le> x
x \<le> pi
\<not> 0 \<le> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cos a \<le> cos x
0 \<le> a
a \<le> pi
- pi \<le> x
x \<le> pi
\<not> 0 \<le> x

goal (1 subgoal):
 1. x \<in> {- a..a}
[PROOF STEP]
using cos_mono_le_eq[of a "-x"]
[PROOF STATE]
proof (prove)
using this:
cos a \<le> cos x
0 \<le> a
a \<le> pi
- pi \<le> x
x \<le> pi
\<not> 0 \<le> x
\<lbrakk>0 \<le> a; a \<le> pi; 0 \<le> - x; - x \<le> pi\<rbrakk> \<Longrightarrow> (cos a \<le> cos (- x)) = (- x \<le> a)

goal (1 subgoal):
 1. x \<in> {- a..a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {- a..a}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_image_part_circlepath_same_Re:
  assumes "0 \<le> b" "b \<le> pi" "a = -b" "r \<ge> 0"
  shows   "path_image (part_circlepath c r a b) = sphere c r \<inter> {s. Re s \<ge> Re c + r * cos a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r a b) = sphere c r \<inter> {s. Re c + r * cos a \<le> Re s}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> x \<in> sphere c r
 2. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> Re c + r * cos a \<le> Re x
 3. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> x \<in> sphere c r
 2. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> Re c + r * cos a \<le> Re x
 3. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
assume "z \<in> path_image (part_circlepath c r a b)"
[PROOF STATE]
proof (state)
this:
z \<in> path_image (part_circlepath c r a b)

goal (3 subgoals):
 1. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> x \<in> sphere c r
 2. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> Re c + r * cos a \<le> Re x
 3. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
obtain t where t: "t \<in> {a..b}" "z = c + of_real r * cis t"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
z \<in> path_image (part_circlepath c r a b)

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {a..b}; z = c + complex_of_real r * cis t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: path_image_part_circlepath exp_eq_polar)
[PROOF STATE]
proof (state)
this:
t \<in> {a..b}
z = c + complex_of_real r * cis t

goal (3 subgoals):
 1. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> x \<in> sphere c r
 2. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> Re c + r * cos a \<le> Re x
 3. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
from t and assms
[PROOF STATE]
proof (chain)
picking this:
t \<in> {a..b}
z = c + complex_of_real r * cis t
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
[PROOF STEP]
show "z \<in> sphere c r"
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
z = c + complex_of_real r * cis t
0 \<le> b
b \<le> pi
a = - b
0 \<le> r

goal (1 subgoal):
 1. z \<in> sphere c r
[PROOF STEP]
by (auto simp: dist_norm norm_mult)
[PROOF STATE]
proof (state)
this:
z \<in> sphere c r

goal (2 subgoals):
 1. \<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> Re c + r * cos a \<le> Re x
 2. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
from t and assms
[PROOF STATE]
proof (chain)
picking this:
t \<in> {a..b}
z = c + complex_of_real r * cis t
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
[PROOF STEP]
show "Re z \<ge> Re c + r * cos a"
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
z = c + complex_of_real r * cis t
0 \<le> b
b \<le> pi
a = - b
0 \<le> r

goal (1 subgoal):
 1. Re c + r * cos a \<le> Re z
[PROOF STEP]
using cos_monotone_0_pi_le[of t b] cos_monotone_minus_pi_0'[of a t]
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
z = c + complex_of_real r * cis t
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
\<lbrakk>0 \<le> t; t \<le> b; b \<le> pi\<rbrakk> \<Longrightarrow> cos b \<le> cos t
\<lbrakk>- pi \<le> a; a \<le> t; t \<le> 0\<rbrakk> \<Longrightarrow> cos a \<le> cos t

goal (1 subgoal):
 1. Re c + r * cos a \<le> Re z
[PROOF STEP]
by (cases "t \<ge> 0") (auto intro!: mult_left_mono)
[PROOF STATE]
proof (state)
this:
Re c + r * cos a \<le> Re z

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
assume z: "z \<in> sphere c r" "Re z \<ge> Re c + r * cos a"
[PROOF STATE]
proof (state)
this:
z \<in> sphere c r
Re c + r * cos a \<le> Re z

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> sphere c r; Re c + r * cos a \<le> Re x\<rbrakk> \<Longrightarrow> x \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
show "z \<in> path_image (part_circlepath c r a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
proof (cases "r = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<noteq> 0

goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
r \<noteq> 0
[PROOF STEP]
have r: "r > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
r \<noteq> 0

goal (1 subgoal):
 1. 0 < r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < r

goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> sphere c r
Re c + r * cos a \<le> Re z
0 < r
[PROOF STEP]
have z_eq: "z = c + r * cis (Arg (z - c))"
[PROOF STATE]
proof (prove)
using this:
z \<in> sphere c r
Re c + r * cos a \<le> Re z
0 < r

goal (1 subgoal):
 1. z = c + complex_of_real r * cis (Arg (z - c))
[PROOF STEP]
using Arg_eq[of "z - c"]
[PROOF STATE]
proof (prove)
using this:
z \<in> sphere c r
Re c + r * cos a \<le> Re z
0 < r
z - c \<noteq> 0 \<Longrightarrow> z - c = complex_of_real (cmod (z - c)) * exp (\<i> * complex_of_real (Arg (z - c)))

goal (1 subgoal):
 1. z = c + complex_of_real r * cis (Arg (z - c))
[PROOF STEP]
by (auto simp: dist_norm exp_eq_polar norm_minus_commute)
[PROOF STATE]
proof (state)
this:
z = c + complex_of_real r * cis (Arg (z - c))

goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z = c + complex_of_real r * cis (Arg (z - c))

goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
from z(2) r assms
[PROOF STATE]
proof (chain)
picking this:
Re c + r * cos a \<le> Re z
0 < r
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
[PROOF STEP]
have "cos b \<le> cos (Arg (z - c))"
[PROOF STATE]
proof (prove)
using this:
Re c + r * cos a \<le> Re z
0 < r
0 \<le> b
b \<le> pi
a = - b
0 \<le> r

goal (1 subgoal):
 1. cos b \<le> cos (Arg (z - c))
[PROOF STEP]
by (subst (asm) z_eq) auto
[PROOF STATE]
proof (state)
this:
cos b \<le> cos (Arg (z - c))

goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
cos b \<le> cos (Arg (z - c))
[PROOF STEP]
have "Arg (z - c) \<in> {-b..b}"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
cos b \<le> cos (Arg (z - c))

goal (1 subgoal):
 1. Arg (z - c) \<in> {- b..b}
[PROOF STEP]
using Arg_le_pi[of "z - c"] mpi_less_Arg[of "z - c"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> b
b \<le> pi
a = - b
0 \<le> r
cos b \<le> cos (Arg (z - c))
Arg (z - c) \<le> pi
- pi < Arg (z - c)

goal (1 subgoal):
 1. Arg (z - c) \<in> {- b..b}
[PROOF STEP]
by (intro cos_geD) auto
[PROOF STATE]
proof (state)
this:
Arg (z - c) \<in> {- b..b}

goal (2 subgoals):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
 2. r \<noteq> 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z = c + complex_of_real r * cis (Arg (z - c))
Arg (z - c) \<in> {- b..b}
[PROOF STEP]
show "z \<in> path_image (part_circlepath c r a b)"
[PROOF STATE]
proof (prove)
using this:
z = c + complex_of_real r * cis (Arg (z - c))
Arg (z - c) \<in> {- b..b}

goal (1 subgoal):
 1. z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z = c + complex_of_real r * cis (Arg (z - c))
Arg (z - c) \<in> {- b..b}
0 \<le> b
b \<le> pi
a = - b
0 \<le> r

goal (1 subgoal):
 1. z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
by (subst path_image_part_circlepath) (auto simp: exp_eq_polar)
[PROOF STATE]
proof (state)
this:
z \<in> path_image (part_circlepath c r a b)

goal (1 subgoal):
 1. r = 0 \<Longrightarrow> z \<in> path_image (part_circlepath c r a b)
[PROOF STEP]
qed (insert assms z, auto simp: path_image_part_circlepath)
[PROOF STATE]
proof (state)
this:
z \<in> path_image (part_circlepath c r a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma part_circlepath_rotate_left:
  "part_circlepath c r (x + a) (x + b) = (\<lambda>z. c + cis x * (z - c)) \<circ> part_circlepath c r a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c r (x + a) (x + b) = (\<lambda>z. c + cis x * (z - c)) \<circ> part_circlepath c r a b
[PROOF STEP]
by (simp add: part_circlepath_def exp_eq_polar fun_eq_iff
                linepath_translate_left linepath_translate_right cis_mult add_ac)


[STATEMENT]
lemma part_circlepath_rotate_right:
  "part_circlepath c r (a + x) (b + x) = (\<lambda>z. c + cis x * (z - c)) \<circ> part_circlepath c r a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c r (a + x) (b + x) = (\<lambda>z. c + cis x * (z - c)) \<circ> part_circlepath c r a b
[PROOF STEP]
by (simp add: part_circlepath_def exp_eq_polar fun_eq_iff
                linepath_translate_left linepath_translate_right cis_mult add_ac)


[STATEMENT]
lemma path_image_semicircle_Re_ge:
  assumes "r \<ge> 0"
  shows   "path_image (part_circlepath c r (-pi/2) (pi/2)) =
             sphere c r \<inter> {s. Re s \<ge> Re c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r (- pi / 2) (pi / 2)) = sphere c r \<inter> {s. Re c \<le> Re s}
[PROOF STEP]
by (subst path_image_part_circlepath_same_Re) (simp_all add: assms)


[STATEMENT]
lemma sphere_rotate: "(\<lambda>z. c + cis x * (z - c)) ` sphere c r = sphere c r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis x * (z - c)) ` sphere c r = sphere c r
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa z. z \<in> sphere c r \<Longrightarrow> c + cis x * (z - c) \<in> sphere c r
 2. \<And>xa. xa \<in> sphere c r \<Longrightarrow> xa \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa z. z \<in> sphere c r \<Longrightarrow> c + cis x * (z - c) \<in> sphere c r
 2. \<And>xa. xa \<in> sphere c r \<Longrightarrow> xa \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r
[PROOF STEP]
assume z: "z \<in> sphere c r"
[PROOF STATE]
proof (state)
this:
z \<in> sphere c r

goal (2 subgoals):
 1. \<And>xa z. z \<in> sphere c r \<Longrightarrow> c + cis x * (z - c) \<in> sphere c r
 2. \<And>xa. xa \<in> sphere c r \<Longrightarrow> xa \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r
[PROOF STEP]
hence "z = c + cis x * (c + cis (-x) * (z - c) - c)"
        "c + cis (-x) * (z - c) \<in> sphere c r"
[PROOF STATE]
proof (prove)
using this:
z \<in> sphere c r

goal (1 subgoal):
 1. z = c + cis x * (c + cis (- x) * (z - c) - c) &&& c + cis (- x) * (z - c) \<in> sphere c r
[PROOF STEP]
by (auto simp: dist_norm norm_mult norm_minus_commute
                   cis_conv_exp exp_minus field_simps norm_divide)
[PROOF STATE]
proof (state)
this:
z = c + cis x * (c + cis (- x) * (z - c) - c)
c + cis (- x) * (z - c) \<in> sphere c r

goal (2 subgoals):
 1. \<And>xa z. z \<in> sphere c r \<Longrightarrow> c + cis x * (z - c) \<in> sphere c r
 2. \<And>xa. xa \<in> sphere c r \<Longrightarrow> xa \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> sphere c r
z = c + cis x * (c + cis (- x) * (z - c) - c)
c + cis (- x) * (z - c) \<in> sphere c r
[PROOF STEP]
show "z \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r"
[PROOF STATE]
proof (prove)
using this:
z \<in> sphere c r
z = c + cis x * (c + cis (- x) * (z - c) - c)
c + cis (- x) * (z - c) \<in> sphere c r

goal (1 subgoal):
 1. z \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> (\<lambda>z. c + cis x * (z - c)) ` sphere c r

goal (1 subgoal):
 1. \<And>xa z. z \<in> sphere c r \<Longrightarrow> c + cis x * (z - c) \<in> sphere c r
[PROOF STEP]
qed (auto simp: dist_norm norm_minus_commute norm_mult)


[STATEMENT]
lemma path_image_semicircle_Re_le:
  assumes "r \<ge> 0"
  shows   "path_image (part_circlepath c r (pi/2) (3/2*pi)) =
             sphere c r \<inter> {s. Re s \<le> Re c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
let ?f = "(\<lambda>z. c + cis pi * (z - c))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
have *: "part_circlepath c r (pi/2) (3/2*pi) = part_circlepath c r (pi + (-pi/2)) (pi + pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c r (pi / 2) (3 / 2 * pi) = part_circlepath c r (pi + - pi / 2) (pi + pi / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
part_circlepath c r (pi / 2) (3 / 2 * pi) = part_circlepath c r (pi + - pi / 2) (pi + pi / 2)

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
have "path_image (part_circlepath c r (pi/2) (3/2*pi)) =
          ?f ` sphere c r \<inter> ?f ` {s. Re c \<le> Re s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = (\<lambda>z. c + cis pi * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis pi * (z - c)) ` {s. Re c \<le> Re s}
[PROOF STEP]
unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis pi * (z - c)) ` (sphere c r \<inter> {s. Re c \<le> Re s}) = (\<lambda>z. c + cis pi * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis pi * (z - c)) ` {s. Re c \<le> Re s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = (\<lambda>z. c + cis pi * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis pi * (z - c)) ` {s. Re c \<le> Re s}

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = (\<lambda>z. c + cis pi * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis pi * (z - c)) ` {s. Re c \<le> Re s}

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
have "?f ` sphere c r = sphere c r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis pi * (z - c)) ` sphere c r = sphere c r
[PROOF STEP]
by (rule sphere_rotate)
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis pi * (z - c)) ` sphere c r = sphere c r

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis pi * (z - c)) ` sphere c r = sphere c r

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
have "?f ` {s. Re c \<le> Re s} = {s. Re c \<ge> Re s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis pi * (z - c)) ` {s. Re c \<le> Re s} = {s. Re s \<le> Re c}
[PROOF STEP]
by (auto simp: image_iff intro!: exI[of _ "2 * c - x" for x])
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis pi * (z - c)) ` {s. Re c \<le> Re s} = {s. Re s \<le> Re c}

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}

goal (1 subgoal):
 1. path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r (pi / 2) (3 / 2 * pi)) = sphere c r \<inter> {s. Re s \<le> Re c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_image_semicircle_Im_ge:
  assumes "r \<ge> 0"
  shows   "path_image (part_circlepath c r 0 pi) =
             sphere c r \<inter> {s. Im s \<ge> Im c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
let ?f = "(\<lambda>z. c + cis (pi/2) * (z - c))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
have *: "part_circlepath c r 0 pi = part_circlepath c r (pi / 2 + (-pi/2)) (pi / 2 + pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c r 0 pi = part_circlepath c r (pi / 2 + - pi / 2) (pi / 2 + pi / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
part_circlepath c r 0 pi = part_circlepath c r (pi / 2 + - pi / 2) (pi / 2 + pi / 2)

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
have "path_image (part_circlepath c r 0 pi) =
          ?f ` sphere c r \<inter> ?f ` {s. Re c \<le> Re s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = (\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (pi / 2) * (z - c)) ` {s. Re c \<le> Re s}
[PROOF STEP]
unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis (pi / 2) * (z - c)) ` (sphere c r \<inter> {s. Re c \<le> Re s}) = (\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (pi / 2) * (z - c)) ` {s. Re c \<le> Re s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r 0 pi) = (\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (pi / 2) * (z - c)) ` {s. Re c \<le> Re s}

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r 0 pi) = (\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (pi / 2) * (z - c)) ` {s. Re c \<le> Re s}

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
have "?f ` sphere c r = sphere c r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r = sphere c r
[PROOF STEP]
by (rule sphere_rotate)
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r = sphere c r

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis (pi / 2) * (z - c)) ` sphere c r = sphere c r

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
have "?f ` {s. Re c \<le> Re s} = {s. Im c \<le> Im s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis (pi / 2) * (z - c)) ` {s. Re c \<le> Re s} = {s. Im c \<le> Im s}
[PROOF STEP]
by (auto simp: image_iff intro!: exI[of _ "c - \<i> * (x - c)" for x])
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis (pi / 2) * (z - c)) ` {s. Re c \<le> Re s} = {s. Im c \<le> Im s}

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}

goal (1 subgoal):
 1. path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r 0 pi) = sphere c r \<inter> {s. Im c \<le> Im s}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_image_semicircle_Im_le:
  assumes "r \<ge> 0"
  shows   "path_image (part_circlepath c r pi (2 * pi)) =
             sphere c r \<inter> {s. Im s \<le> Im c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
let ?f = "(\<lambda>z. c + cis (3*pi/2) * (z - c))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
have *: "part_circlepath c r pi (2*pi) = part_circlepath c r (3*pi/2 + (-pi/2)) (3*pi/2 + pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c r pi (2 * pi) = part_circlepath c r (3 * pi / 2 + - pi / 2) (3 * pi / 2 + pi / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
part_circlepath c r pi (2 * pi) = part_circlepath c r (3 * pi / 2 + - pi / 2) (3 * pi / 2 + pi / 2)

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
have "path_image (part_circlepath c r pi (2 * pi)) =
          ?f ` sphere c r \<inter> ?f ` {s. Re c \<le> Re s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` {s. Re c \<le> Re s}
[PROOF STEP]
unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` (sphere c r \<inter> {s. Re c \<le> Re s}) = (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` {s. Re c \<le> Re s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r pi (2 * pi)) = (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` {s. Re c \<le> Re s}

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r pi (2 * pi)) = (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r \<inter> (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` {s. Re c \<le> Re s}

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
have "?f ` sphere c r = sphere c r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r = sphere c r
[PROOF STEP]
by (rule sphere_rotate)
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r = sphere c r

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` sphere c r = sphere c r

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
have "cis (3 * pi / 2) = -\<i>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (3 * pi / 2) = - \<i>
[PROOF STEP]
using cis_mult[of pi "pi / 2"]
[PROOF STATE]
proof (prove)
using this:
cis pi * cis (pi / 2) = cis (pi + pi / 2)

goal (1 subgoal):
 1. cis (3 * pi / 2) = - \<i>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis (3 * pi / 2) = - \<i>

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
hence "?f ` {s. Re c \<le> Re s} = {s. Im c \<ge> Im s}"
[PROOF STATE]
proof (prove)
using this:
cis (3 * pi / 2) = - \<i>

goal (1 subgoal):
 1. (\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` {s. Re c \<le> Re s} = {s. Im s \<le> Im c}
[PROOF STEP]
by (auto simp: image_iff intro!: exI[of _ "c + \<i> * (x - c)" for x])
[PROOF STATE]
proof (state)
this:
(\<lambda>z. c + cis (3 * pi / 2) * (z - c)) ` {s. Re c \<le> Re s} = {s. Im s \<le> Im c}

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}

goal (1 subgoal):
 1. path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
path_image (part_circlepath c r pi (2 * pi)) = sphere c r \<inter> {s. Im s \<le> Im c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powr_numeral [simp]: "x \<ge> 0 \<Longrightarrow> (x::real) powr numeral y = x ^ numeral y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x \<Longrightarrow> x powr numeral y = x ^ numeral y
[PROOF STEP]
using powr_numeral[of x y]
[PROOF STATE]
proof (prove)
using this:
0 \<le> x \<Longrightarrow> x powr numeral y = x ^ numeral y

goal (1 subgoal):
 1. 0 \<le> x \<Longrightarrow> x powr numeral y = x ^ numeral y
[PROOF STEP]
by (cases "x = 0") auto


[STATEMENT]
lemma eval_fds_logderiv_zeta_real:
  assumes "x > (1 :: real)"
  shows  "(\<lambda>p. ln (real p) / (p powr x - 1)) abs_summable_on {p. prime p}" (is ?th1)
    and  "deriv zeta (of_real x) / zeta (of_real x) =
            -of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (p powr x - 1))" (is ?th2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p} &&& deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}
 2. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
have "(\<lambda>p. Re (of_real (ln (real p)) / (of_nat p powr of_real x - 1)))
          abs_summable_on {p. prime p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. Re (complex_of_real (ln (real p)) / (of_nat p powr complex_of_real x - 1))) abs_summable_on {p. prime p}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < x

goal (1 subgoal):
 1. (\<lambda>p. Re (complex_of_real (ln (real p)) / (of_nat p powr complex_of_real x - 1))) abs_summable_on {p. prime p}
[PROOF STEP]
by (intro abs_summable_Re eval_fds_logderiv_zeta) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>p. Re (complex_of_real (ln (real p)) / (of_nat p powr complex_of_real x - 1))) abs_summable_on {p. prime p}

goal (2 subgoals):
 1. (\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}
 2. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>p. Re (complex_of_real (ln (real p)) / (of_nat p powr complex_of_real x - 1))) abs_summable_on {p. prime p}

goal (2 subgoals):
 1. (\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}
 2. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
have "?this \<longleftrightarrow> ?th1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>p. Re (complex_of_real (ln (real p)) / (of_nat p powr complex_of_real x - 1))) abs_summable_on {p. prime p}) = ((\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p})
[PROOF STEP]
by (intro abs_summable_on_cong) (auto simp: powr_Reals_eq)
[PROOF STATE]
proof (state)
this:
((\<lambda>p. Re (complex_of_real (ln (real p)) / (of_nat p powr complex_of_real x - 1))) abs_summable_on {p. prime p}) = ((\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p})

goal (2 subgoals):
 1. (\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}
 2. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}
[PROOF STEP]
show ?th1
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}

goal (1 subgoal):
 1. (\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>p. ln (real p) / (real p powr x - 1)) abs_summable_on {p. prime p}

goal (1 subgoal):
 1. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
show ?th2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < x

goal (1 subgoal):
 1. deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))
[PROOF STEP]
by (subst eval_fds_logderiv_zeta) (auto simp: infsetsum_of_real [symmetric] powr_Reals_eq)
[PROOF STATE]
proof (state)
this:
deriv zeta (complex_of_real x) / zeta (complex_of_real x) = - complex_of_real (\<Sum>\<^sub>ap | prime p. ln (real p) / (real p powr x - 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ln_fact_conv_sum_upto: "ln (fact n) = sum_upto ln n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (fact n) = sum_upto (\<lambda>x. ln (real x)) (real n)
[PROOF STEP]
by (induction n) (auto simp: sum_upto_plus1 add.commute[of 1] ln_mult)


[STATEMENT]
lemma sum_upto_ln_conv_ln_fact: "sum_upto ln x = ln (fact (nat \<lfloor>x\<rfloor>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>x. ln (real x)) x = ln (fact (nat \<lfloor>x\<rfloor>))
[PROOF STEP]
by (simp add: ln_fact_conv_sum_upto sum_upto_altdef)


[STATEMENT]
lemma real_of_nat_div: "real (a div b) = real_of_int \<lfloor>real a / real b\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (a div b) = real_of_int \<lfloor>real a / real b\<rfloor>
[PROOF STEP]
by (subst floor_divide_of_nat_eq) auto


[STATEMENT]
lemma integral_subset_negligible:
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
  assumes "S \<subseteq> T" "negligible (T - S)"
  shows   "integral S f = integral T f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
have "integral T f = integral T (\<lambda>x. if x \<in> S then f x else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral T f = integral T (\<lambda>x. if x \<in> S then f x else (0::'b))
[PROOF STEP]
by (rule integral_spike[of "T - S"]) (use assms in auto)
[PROOF STATE]
proof (state)
this:
integral T f = integral T (\<lambda>x. if x \<in> S then f x else (0::'b))

goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral T f = integral T (\<lambda>x. if x \<in> S then f x else (0::'b))

goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
have "\<dots> = integral (S \<inter> T) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral T (\<lambda>x. if x \<in> S then f x else (0::'b)) = integral (S \<inter> T) f
[PROOF STEP]
by (subst integral_restrict_Int) auto
[PROOF STATE]
proof (state)
this:
integral T (\<lambda>x. if x \<in> S then f x else (0::'b)) = integral (S \<inter> T) f

goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral T (\<lambda>x. if x \<in> S then f x else (0::'b)) = integral (S \<inter> T) f

goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
have "S \<inter> T = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> T
negligible (T - S)

goal (1 subgoal):
 1. S \<inter> T = S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<inter> T = S

goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral T f = integral S f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
integral T f = integral S f

goal (1 subgoal):
 1. integral S f = integral T f
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
integral S f = integral T f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma integrable_on_cong [cong]:
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x" "A = B"
  shows   "f integrable_on A \<longleftrightarrow> g integrable_on B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f integrable_on A) = (g integrable_on B)
[PROOF STEP]
using has_integral_cong[of A f g, OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> A \<Longrightarrow> x \<in> A) \<Longrightarrow> (f has_integral ?i) A = (g has_integral ?i) A
A = B

goal (1 subgoal):
 1. (f integrable_on A) = (g integrable_on B)
[PROOF STEP]
by (auto simp: integrable_on_def)


[STATEMENT]
lemma measurable_sum_upto [measurable]:
  fixes f :: "'a \<Rightarrow> nat \<Rightarrow> real"
  assumes [measurable]: "\<And>y. (\<lambda>t. f t y) \<in> M \<rightarrow>\<^sub>M borel"
  assumes [measurable]: "x \<in> M \<rightarrow>\<^sub>M borel"
  shows "(\<lambda>t. sum_upto (f t) (x t)) \<in> M \<rightarrow>\<^sub>M borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
have meas: "(\<lambda>t. set_lebesgue_integral lborel {y. y \<ge> 0 \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} (\<lambda>y. f t (nat \<lceil>y\<rceil>)))
          \<in> M \<rightarrow>\<^sub>M borel" (is "?f \<in> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>)) \<in> borel_measurable M
[PROOF STEP]
unfolding set_lebesgue_integral_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. LBINT xa. indicat_real {y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} xa *\<^sub>R f t (nat \<lceil>xa\<rceil>)) \<in> borel_measurable M
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
(\<lambda>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>)) \<in> borel_measurable M

goal (1 subgoal):
 1. (\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>)) \<in> borel_measurable M

goal (1 subgoal):
 1. (\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
have "?f = (\<lambda>t. sum_upto (f t) (x t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>)) = (\<lambda>t. sum_upto (f t) (x t))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
fix t :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
show "?f t = sum_upto (f t) (x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
proof (cases "x t < 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
 2. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x t < 1

goal (2 subgoals):
 1. x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
 2. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
hence "{y. y \<ge> 0 \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} = {0}"
[PROOF STATE]
proof (prove)
using this:
x t < 1

goal (1 subgoal):
 1. {y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} = {0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} = {0}

goal (2 subgoals):
 1. x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
 2. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} = {0}

goal (1 subgoal):
 1. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0} = {0}
x t < 1

goal (1 subgoal):
 1. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
by (simp add: set_integral_at_point sum_upto_altdef)
[PROOF STATE]
proof (state)
this:
LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x t < 1

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
define n where "n = nat \<lfloor>x t\<rfloor>"
[PROOF STATE]
proof (state)
this:
n = nat \<lfloor>x t\<rfloor>

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> x t < 1
[PROOF STEP]
have "n > 0"
[PROOF STATE]
proof (prove)
using this:
\<not> x t < 1

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by (auto simp: n_def)
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
have *: "((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral sum (f t) {0<..n}) {real 0..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral sum (f t) {0<..n}) {real 0..real n}
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. ((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral sum (f t) {0<..n}) {real 0..real n}
[PROOF STEP]
by (intro nat_sum_has_integral_ceiling) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral sum (f t) {0<..n}) {real 0..real n}

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
have **: "(\<lambda>x. f t (nat \<lceil>x\<rceil>)) absolutely_integrable_on {real 0..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f t (nat \<lceil>x\<rceil>)) absolutely_integrable_on {real 0..real n}
[PROOF STEP]
proof (rule absolutely_integrable_absolutely_integrable_ubound)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<lambda>x. f t (nat \<lceil>x\<rceil>)) integrable_on {real 0..real n}
 2. ?g absolutely_integrable_on {real 0..real n}
 3. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> ?g x
[PROOF STEP]
show "(\<lambda>_. MAX n\<in>{0..n}. \<bar>f t n\<bar>) absolutely_integrable_on {real 0..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. MAX n\<in>{0..n}. \<bar>f t n\<bar>) absolutely_integrable_on {real 0..real n}
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<lambda>_. MAX n\<in>{0..n}. \<bar>f t n\<bar>) absolutely_integrable_on {real 0..real n}
[PROOF STEP]
by (subst absolutely_integrable_on_iff_nonneg)
                           (auto simp: Max_ge_iff intro!: exI[of _ "f t 0"])
[PROOF STATE]
proof (state)
this:
(\<lambda>_. MAX n\<in>{0..n}. \<bar>f t n\<bar>) absolutely_integrable_on {real 0..real n}

goal (2 subgoals):
 1. (\<lambda>x. f t (nat \<lceil>x\<rceil>)) integrable_on {real 0..real n}
 2. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
show "(\<lambda>x. f t (nat \<lceil>x\<rceil>)) integrable_on {real 0..real n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f t (nat \<lceil>x\<rceil>)) integrable_on {real 0..real n}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral sum (f t) {0<..n}) {real 0..real n}

goal (1 subgoal):
 1. (\<lambda>x. f t (nat \<lceil>x\<rceil>)) integrable_on {real 0..real n}
[PROOF STEP]
by (simp add: has_integral_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f t (nat \<lceil>x\<rceil>)) integrable_on {real 0..real n}

goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
fix y :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
assume y: "y \<in> {real 0..real n}"
[PROOF STATE]
proof (state)
this:
y \<in> {real 0..real n}

goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
have "f t (nat \<lceil>y\<rceil>) \<le> \<bar>f t (nat \<lceil>y\<rceil>)\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f t (nat \<lceil>y\<rceil>) \<le> \<bar>f t (nat \<lceil>y\<rceil>)\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f t (nat \<lceil>y\<rceil>) \<le> \<bar>f t (nat \<lceil>y\<rceil>)\<bar>

goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f t (nat \<lceil>y\<rceil>) \<le> \<bar>f t (nat \<lceil>y\<rceil>)\<bar>

goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
have "\<dots> \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>f t (nat \<lceil>y\<rceil>)\<bar> \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
y \<in> {real 0..real n}

goal (1 subgoal):
 1. \<bar>f t (nat \<lceil>y\<rceil>)\<bar> \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
by (intro Max.coboundedI) auto
[PROOF STATE]
proof (state)
this:
\<bar>f t (nat \<lceil>y\<rceil>)\<bar> \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)

goal (1 subgoal):
 1. \<And>x. x \<in> {real 0..real n} \<Longrightarrow> f t (nat \<lceil>x\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f t (nat \<lceil>y\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
show "f t (nat \<lceil>y\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)"
[PROOF STATE]
proof (prove)
using this:
f t (nat \<lceil>y\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)

goal (1 subgoal):
 1. f t (nat \<lceil>y\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f t (nat \<lceil>y\<rceil>) \<le> (MAX n\<in>{0..n}. \<bar>f t n\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f t (nat \<lceil>x\<rceil>)) absolutely_integrable_on {real 0..real n}

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
have "sum (f t) {0<..n} = (\<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>) \<partial>lebesgue)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (f t) {0<..n} = \<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue
[PROOF STEP]
using has_integral_set_lebesgue[OF **] *
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral \<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue) {real 0..real n}
((\<lambda>x. f t (nat \<lceil>x\<rceil>)) has_integral sum (f t) {0<..n}) {real 0..real n}

goal (1 subgoal):
 1. sum (f t) {0<..n} = \<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue
[PROOF STEP]
by (simp add: has_integral_iff)
[PROOF STATE]
proof (state)
this:
sum (f t) {0<..n} = \<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (f t) {0<..n} = \<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
have "\<dots> = (\<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue = LBINT x:{real 0..real n}. f t (nat \<lceil>x\<rceil>)
[PROOF STEP]
unfolding set_lebesgue_integral_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|lebesgue. indicat_real {real 0..real n} x *\<^sub>R f t (nat \<lceil>x\<rceil>) = LBINT x. indicat_real {real 0..real n} x *\<^sub>R f t (nat \<lceil>x\<rceil>)
[PROOF STEP]
by (subst integral_completion) auto
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue = LBINT x:{real 0..real n}. f t (nat \<lceil>x\<rceil>)

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>{real 0..real n}. f t (nat \<lceil>x\<rceil>)\<partial>lebesgue = LBINT x:{real 0..real n}. f t (nat \<lceil>x\<rceil>)

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
have "{real 0..real n} = {y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {real 0..real n} = {y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}
[PROOF STEP]
by (auto simp: n_def)
[PROOF STATE]
proof (state)
this:
{real 0..real n} = {y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{real 0..real n} = {y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
have "sum (f t) {0<..n} = sum_upto (f t) (x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (f t) {0<..n} = sum_upto (f t) (x t)
[PROOF STEP]
by (simp add: sum_upto_altdef n_def)
[PROOF STATE]
proof (state)
this:
sum (f t) {0<..n} = sum_upto (f t) (x t)

goal (1 subgoal):
 1. \<not> x t < 1 \<Longrightarrow> LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_upto (f t) (x t) = LBINT x:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>x\<rceil>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_upto (f t) (x t) = LBINT x:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>x\<rceil>)

goal (1 subgoal):
 1. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>) = sum_upto (f t) (x t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>t. LBINT y:{y. 0 \<le> y \<and> y - real (nat \<lfloor>x t\<rfloor>) \<le> 0}. f t (nat \<lceil>y\<rceil>)) = (\<lambda>t. sum_upto (f t) (x t))

goal (1 subgoal):
 1. (\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M

goal (1 subgoal):
 1. (\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>t. sum_upto (f t) (x t)) \<in> borel_measurable M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift:
  assumes fin: "finite C \<and> finite D"
  assumes apart: "vars\<^sub>l\<^sub>s C \<inter> vars\<^sub>l\<^sub>s D = {}"
  assumes inst\<^sub>1: "instance_of\<^sub>l\<^sub>s C' C"
  assumes inst\<^sub>2: "instance_of\<^sub>l\<^sub>s D' D"
  assumes appl: "applicable C' D' L' M' \<sigma>"
  shows "\<exists>L M \<tau>. applicable C D L M \<tau> \<and>
                   instance_of\<^sub>l\<^sub>s (resolution C' D' L' M' \<sigma>) (resolution C D L M \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L M \<tau>. applicable C D L M \<tau> \<and> instance_of\<^sub>l\<^sub>s (resolution C' D' L' M' \<sigma>) (resolution C D L M \<tau>)
[PROOF STEP]
using assms lifting
[PROOF STATE]
proof (prove)
using this:
finite C \<and> finite D
vars\<^sub>l\<^sub>s C \<inter> vars\<^sub>l\<^sub>s D = {}
instance_of\<^sub>l\<^sub>s C' C
instance_of\<^sub>l\<^sub>s D' D
applicable C' D' L' M' \<sigma>
\<lbrakk>finite ?C\<^sub>1 \<and> finite ?C\<^sub>2; vars\<^sub>l\<^sub>s ?C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s ?C\<^sub>2 = {}; instance_of\<^sub>l\<^sub>s ?C\<^sub>1' ?C\<^sub>1 \<and> instance_of\<^sub>l\<^sub>s ?C\<^sub>2' ?C\<^sub>2; applicable ?C\<^sub>1' ?C\<^sub>2' ?L\<^sub>1' ?L\<^sub>2' ?\<sigma>\<rbrakk> \<Longrightarrow> \<exists>L\<^sub>1 L\<^sub>2 \<tau>. applicable ?C\<^sub>1 ?C\<^sub>2 L\<^sub>1 L\<^sub>2 \<tau> \<and> instance_of\<^sub>l\<^sub>s (resolution ?C\<^sub>1' ?C\<^sub>2' ?L\<^sub>1' ?L\<^sub>2' ?\<sigma>) (resolution ?C\<^sub>1 ?C\<^sub>2 L\<^sub>1 L\<^sub>2 \<tau>)

goal (1 subgoal):
 1. \<exists>L M \<tau>. applicable C D L M \<tau> \<and> instance_of\<^sub>l\<^sub>s (resolution C' D' L' M' \<sigma>) (resolution C D L M \<tau>)
[PROOF STEP]
by metis


[STATEMENT]
theorem complete:
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  assumes unsat: "\<forall>(F::hterm fun_denot) (G::hterm pred_denot) . \<not>eval\<^sub>c\<^sub>s F G Cs"
  shows "\<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
using assms completeness
[PROOF STATE]
proof (prove)
using this:
finite Cs
\<forall>C\<in>Cs. finite C
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
\<lbrakk>finite ?Cs; \<forall>C\<in>?Cs. finite C; \<forall>F G. \<not> eval\<^sub>c\<^sub>s F G ?Cs\<rbrakk> \<Longrightarrow> \<exists>Cs'. resolution_deriv ?Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
by -


[STATEMENT]
theorem complete_countable:
  assumes inf_uni: "infinite (UNIV :: ('u :: countable) set)"
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  assumes unsat: "\<forall>(F::'u fun_denot) (G::'u pred_denot). \<not>eval\<^sub>c\<^sub>s F G Cs"
  shows "\<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
using assms completeness_countable
[PROOF STATE]
proof (prove)
using this:
infinite UNIV
finite Cs
\<forall>C\<in>Cs. finite C
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
\<lbrakk>infinite UNIV; finite ?Cs; \<forall>C\<in>?Cs. finite C; \<forall>F G. \<not> eval\<^sub>c\<^sub>s F G ?Cs\<rbrakk> \<Longrightarrow> \<exists>Cs'. resolution_deriv ?Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
by -


[STATEMENT]
theorem complete_nat:
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  assumes unsat: "\<forall>(F::nat fun_denot) (G::nat pred_denot) . \<not>eval\<^sub>c\<^sub>s F G Cs"
  shows "\<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
using assms completeness_nat
[PROOF STATE]
proof (prove)
using this:
finite Cs
\<forall>C\<in>Cs. finite C
\<forall>F G. \<not> eval\<^sub>c\<^sub>s F G Cs
\<lbrakk>finite ?Cs; \<forall>C\<in>?Cs. finite C; \<forall>F G. \<not> eval\<^sub>c\<^sub>s F G ?Cs\<rbrakk> \<Longrightarrow> \<exists>Cs'. resolution_deriv ?Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. \<exists>Cs'. resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
by -


[STATEMENT]
lemma Vfrom_Ord_bundle:
  assumes "A = A" and "i = i"
  shows "Vfrom A i = Vfrom A (rank i)" and "Ord (rank i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A i = Vfrom A (rank i) &&& Ord (rank i)
[PROOF STEP]
by (simp_all add: Vfrom_rank_eq )


[STATEMENT]
lemma Vfrom_in_bundle:
  assumes "i \<in>\<^sub>\<circ> j" and "A = A" and "B = B"
  shows "Vfrom A i = Vfrom A (rank i)"
    and "Ord (rank i)"
    and "Vfrom B j = Vfrom B (rank j)"
    and "Ord (rank j)"
    and "rank i \<in>\<^sub>\<circ> rank j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Vfrom A i = Vfrom A (rank i) &&& Ord (rank i)) &&& Vfrom B j = Vfrom B (rank j) &&& Ord (rank j) &&& rank i \<in>\<^sub>\<circ> rank j
[PROOF STEP]
by (simp_all add: assms(1) Vfrom_rank_eq Ord_mem_iff_lt rank_lt)


[STATEMENT]
lemma Ord_Vset_in_Vset_succI[intro]:
  assumes "Ord \<alpha>"
  shows "Vset \<alpha> \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset \<alpha> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (simp add: Vset_succ assms)


[STATEMENT]
lemma Ord_in_in_VsetI[intro]:
  assumes "Ord \<alpha>" and "a \<in>\<^sub>\<circ> \<alpha>"
  shows "a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (metis assms Ord_VsetI Ord_iff_rank rank_lt)


[STATEMENT]
lemma Vfrom_trans[intro]:
  assumes "Transset A" and "x \<in>\<^sub>\<circ> X" and "X \<in>\<^sub>\<circ> Vfrom A i"
  shows "x \<in>\<^sub>\<circ> Vfrom A i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> Vfrom A i
[PROOF STEP]
using Transset_def
[PROOF STATE]
proof (prove)
using this:
Transset ?x \<equiv> \<forall>y\<in>elts ?x. y \<subseteq>\<^sub>\<circ> ?x

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> Vfrom A i
[PROOF STEP]
by (blast intro: assms Transset_Vfrom)


[STATEMENT]
lemma Vset_trans[intro]:
  assumes "x \<in>\<^sub>\<circ> X" and "X \<in>\<^sub>\<circ> Vset i"
  shows "x \<in>\<^sub>\<circ> Vset i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
by (auto intro: assms)


[STATEMENT]
lemma Vfrom_in_mono:
  assumes "A \<subseteq>\<^sub>\<circ> B" and "i \<in>\<^sub>\<circ> j"
  shows "Vfrom A i \<in>\<^sub>\<circ> Vfrom B j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A i \<in>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Vfrom A i \<in>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
define i' where "i' = rank i"
[PROOF STATE]
proof (state)
this:
i' = rank i

goal (1 subgoal):
 1. Vfrom A i \<in>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
define j' where "j' = rank j"
[PROOF STATE]
proof (state)
this:
j' = rank j

goal (1 subgoal):
 1. Vfrom A i \<in>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
note rank_conv =
    Vfrom_in_bundle[
      OF assms(2) HOL.refl[of A] HOL.refl[of B], folded i'_def j'_def
      ]
[PROOF STATE]
proof (state)
this:
Vfrom A i = Vfrom A i'
Ord i'
Vfrom B j = Vfrom B j'
Ord j'
i' \<in>\<^sub>\<circ> j'

goal (1 subgoal):
 1. Vfrom A i \<in>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A i \<in>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
unfolding rank_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> Vfrom B j'
[PROOF STEP]
using rank_conv(4,5)
[PROOF STATE]
proof (prove)
using this:
Ord j'
i' \<in>\<^sub>\<circ> j'

goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> Vfrom B j'
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; i' \<in>\<^sub>\<circ> \<alpha> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<alpha>; i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ \<alpha>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
case (succ j')
[PROOF STATE]
proof (state)
this:
Ord j'
i' \<in>\<^sub>\<circ> j' \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B j'
i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ j'

goal (3 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; i' \<in>\<^sub>\<circ> \<alpha> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<alpha>; i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ \<alpha>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
from succ
[PROOF STATE]
proof (chain)
picking this:
Ord j'
i' \<in>\<^sub>\<circ> j' \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B j'
i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ j'
[PROOF STEP]
have "Ord (succ j')"
[PROOF STATE]
proof (prove)
using this:
Ord j'
i' \<in>\<^sub>\<circ> j' \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B j'
i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ j'

goal (1 subgoal):
 1. Ord (ZFC_in_HOL.succ j')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord (ZFC_in_HOL.succ j')

goal (3 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; i' \<in>\<^sub>\<circ> \<alpha> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<alpha>; i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ \<alpha>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
from succ(3) succ.hyps
[PROOF STATE]
proof (chain)
picking this:
i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ j'
Ord j'
[PROOF STEP]
have "i' \<subseteq>\<^sub>\<circ> j'"
[PROOF STATE]
proof (prove)
using this:
i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ j'
Ord j'

goal (1 subgoal):
 1. i' \<subseteq>\<^sub>\<circ> j'
[PROOF STEP]
by (auto simp: Ord_def Transset_def)
[PROOF STATE]
proof (state)
this:
i' \<subseteq>\<^sub>\<circ> j'

goal (3 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; i' \<in>\<^sub>\<circ> \<alpha> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<alpha>; i' \<in>\<^sub>\<circ> ZFC_in_HOL.succ \<alpha>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
from Vfrom_mono[OF \<open>Ord i'\<close> assms(1) this]
[PROOF STATE]
proof (chain)
picking this:
Vfrom A i' \<subseteq>\<^sub>\<circ> Vfrom B j'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Vfrom A i' \<subseteq>\<^sub>\<circ> Vfrom B j'

goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (ZFC_in_HOL.succ j')
[PROOF STEP]
unfolding Vfrom_succ_Ord[OF \<open>Ord j'\<close>, of B]
[PROOF STATE]
proof (prove)
using this:
Vfrom A i' \<subseteq>\<^sub>\<circ> Vfrom B j'

goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> B \<union>\<^sub>\<circ> VPow (Vfrom B j')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (ZFC_in_HOL.succ j')

goal (2 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
case (Limit j')
[PROOF STATE]
proof (state)
this:
Limit j'
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> j'; i' \<in>\<^sub>\<circ> ?\<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B ?\<xi>
i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>j'. \<xi>) `\<^sub>\<circ> j')

goal (2 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
from Limit(3)
[PROOF STATE]
proof (chain)
picking this:
i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>j'. \<xi>) `\<^sub>\<circ> j')
[PROOF STEP]
obtain \<xi> where "i' \<in>\<^sub>\<circ> \<xi>" and "\<xi> \<in>\<^sub>\<circ> j'"
[PROOF STATE]
proof (prove)
using this:
i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>j'. \<xi>) `\<^sub>\<circ> j')

goal (1 subgoal):
 1. (\<And>\<xi>. \<lbrakk>i' \<in>\<^sub>\<circ> \<xi>; \<xi> \<in>\<^sub>\<circ> j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' \<in>\<^sub>\<circ> \<xi>
\<xi> \<in>\<^sub>\<circ> j'

goal (2 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
with vifunionI
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i \<in>\<^sub>\<circ> ?I; ?a \<in>\<^sub>\<circ> ?f ?i\<rbrakk> \<Longrightarrow> ?a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda ?I ?f `\<^sub>\<circ> ?I)
i' \<in>\<^sub>\<circ> \<xi>
\<xi> \<in>\<^sub>\<circ> j'
[PROOF STEP]
have "Vfrom A i' \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>\<xi>\<in>\<^sub>\<circ>j'. Vfrom B \<xi>)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in>\<^sub>\<circ> ?I; ?a \<in>\<^sub>\<circ> ?f ?i\<rbrakk> \<Longrightarrow> ?a \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda ?I ?f `\<^sub>\<circ> ?I)
i' \<in>\<^sub>\<circ> \<xi>
\<xi> \<in>\<^sub>\<circ> j'

goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda j' (Vfrom B) `\<^sub>\<circ> j')
[PROOF STEP]
by (auto simp: Limit.IH)
[PROOF STATE]
proof (state)
this:
Vfrom A i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda j' (Vfrom B) `\<^sub>\<circ> j')

goal (2 subgoals):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; i' \<in>\<^sub>\<circ> \<xi>\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B \<xi>; i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>)\<rbrakk> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vfrom A i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda j' (Vfrom B) `\<^sub>\<circ> j')
[PROOF STEP]
show "Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ>\<xi>\<in>\<^sub>\<circ>j'. \<xi>)"
[PROOF STATE]
proof (prove)
using this:
Vfrom A i' \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda j' (Vfrom B) `\<^sub>\<circ> j')

goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>j'. a) `\<^sub>\<circ> j'))
[PROOF STEP]
unfolding Limit_Vfrom_eq[symmetric, OF Limit(1)]
[PROOF STATE]
proof (prove)
using this:
Vfrom A i' \<in>\<^sub>\<circ> Vfrom B j'

goal (1 subgoal):
 1. Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>j'. a) `\<^sub>\<circ> j'))
[PROOF STEP]
by (simp add: SUP_vifunion[symmetric] Limit.hyps)
[PROOF STATE]
proof (state)
this:
Vfrom A i' \<in>\<^sub>\<circ> Vfrom B (\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>j'. a) `\<^sub>\<circ> j'))

goal (1 subgoal):
 1. i' \<in>\<^sub>\<circ> []\<^sub>\<circ> \<Longrightarrow> Vfrom A i' \<in>\<^sub>\<circ> Vfrom B []\<^sub>\<circ>
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
Vfrom A i \<in>\<^sub>\<circ> Vfrom B j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Vfrom_vsubset_mono:
  assumes "A \<subseteq>\<^sub>\<circ> B" and "i \<subseteq>\<^sub>\<circ> j"
  shows "Vfrom A i \<subseteq>\<^sub>\<circ> Vfrom B j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A i \<subseteq>\<^sub>\<circ> Vfrom B j
[PROOF STEP]
by (metis assms Vfrom_Ord_bundle(1,2) Vfrom_mono rank_mono)


[STATEMENT]
lemma arg1_vsubset_Vfrom: "a \<subseteq>\<^sub>\<circ> Vfrom a i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<subseteq>\<^sub>\<circ> Vfrom a i
[PROOF STEP]
using Vfrom
[PROOF STATE]
proof (prove)
using this:
Vfrom ?a ?i = ?a \<union>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>j\<in>\<^sub>\<circ>?i. VPow (Vfrom ?a j)) `\<^sub>\<circ> ?i)

goal (1 subgoal):
 1. a \<subseteq>\<^sub>\<circ> Vfrom a i
[PROOF STEP]
by blast


[STATEMENT]
lemma VPow_vsubset_Vset:
  \<comment>\<open>Based on Theorem 9.10 from \cite{takeuti_introduction_1971}\<close>
  assumes "X \<in>\<^sub>\<circ> Vset i"
  shows "VPow X \<subseteq>\<^sub>\<circ> Vset i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i
[PROOF STEP]
define i' where "i' = rank i"
[PROOF STATE]
proof (state)
this:
i' = rank i

goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i
[PROOF STEP]
note rank_conv = Vfrom_Ord_bundle[OF refl[of 0] refl[of i], folded i'_def]
[PROOF STATE]
proof (state)
this:
Vset i = Vset i'
Ord i'

goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i
[PROOF STEP]
using rank_conv(2) assms
[PROOF STATE]
proof (prove)
using this:
Ord i'
X \<in>\<^sub>\<circ> Vset i

goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i
[PROOF STEP]
unfolding rank_conv
[PROOF STATE]
proof (prove)
using this:
Ord i'
X \<in>\<^sub>\<circ> Vset i'

goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset i'
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; X \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<alpha>; X \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<xi>; X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
case (Limit \<alpha>)
[PROOF STATE]
proof (state)
this:
Limit \<alpha>
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset ?\<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset ?\<xi>
X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))

goal (3 subgoals):
 1. X \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; X \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<alpha>; X \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<xi>; X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
from Limit
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset ?\<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset ?\<xi>
X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
have "X \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>\<alpha>. Vset i)"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
\<lbrakk>?\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset ?\<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset ?\<xi>
X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))

goal (1 subgoal):
 1. X \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
by (simp add: SUP_vifunion[symmetric] Limit_Vfrom_eq)
[PROOF STATE]
proof (state)
this:
X \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (3 subgoals):
 1. X \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; X \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<alpha>; X \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<xi>; X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
have "VPow X \<subseteq>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>\<alpha>. Vset i)"
[PROOF STATE]
proof (prove)
using this:
X \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
by (intro vsubsetI) (metis Limit.IH vifunionE vifunionI vsubsetE)
[PROOF STATE]
proof (state)
this:
VPow X \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (3 subgoals):
 1. X \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; X \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<alpha>; X \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
 3. \<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<lbrakk>\<xi> \<in>\<^sub>\<circ> \<alpha>; X \<in>\<^sub>\<circ> Vset \<xi>\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<xi>; X \<in>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
VPow X \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
VPow X \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (VLambda \<alpha> Vset `\<^sub>\<circ> \<alpha>)

goal (1 subgoal):
 1. VPow X \<subseteq>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))
[PROOF STEP]
by (simp add: SUP_vifunion[symmetric] Limit.hyps Limit_Vfrom_eq)
[PROOF STATE]
proof (state)
this:
VPow X \<subseteq>\<^sub>\<circ> Vset (\<Union>\<^sub>\<circ> ((\<lambda>\<xi>\<in>\<^sub>\<circ>\<alpha>. \<xi>) `\<^sub>\<circ> \<alpha>))

goal (2 subgoals):
 1. X \<in>\<^sub>\<circ> Vset []\<^sub>\<circ> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset []\<^sub>\<circ>
 2. \<And>\<alpha>. \<lbrakk>Ord \<alpha>; X \<in>\<^sub>\<circ> Vset \<alpha> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset \<alpha>; X \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> VPow X \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
qed (simp_all add: Vset_succ)
[PROOF STATE]
proof (state)
this:
VPow X \<subseteq>\<^sub>\<circ> Vset i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Vfrom_vsubset_VPow_Vfrom:
  assumes "Transset A"
  shows "Vfrom A i \<subseteq>\<^sub>\<circ> VPow (Vfrom A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vfrom A i \<subseteq>\<^sub>\<circ> VPow (Vfrom A i)
[PROOF STEP]
using assms Transset_VPow Transset_Vfrom
[PROOF STATE]
proof (prove)
using this:
Transset A
Transset ?i \<Longrightarrow> Transset (VPow ?i)
Transset ?A \<Longrightarrow> Transset (Vfrom ?A ?i)

goal (1 subgoal):
 1. Vfrom A i \<subseteq>\<^sub>\<circ> VPow (Vfrom A i)
[PROOF STEP]
by (auto simp: Transset_def)


[STATEMENT]
lemma arg1_vsubset_VPow_Vfrom:
  assumes "Transset A"
  shows "A \<subseteq>\<^sub>\<circ> VPow (Vfrom A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq>\<^sub>\<circ> VPow (Vfrom A i)
[PROOF STEP]
by (meson assms Vfrom_vsubset_VPow_Vfrom arg1_vsubset_Vfrom dual_order.trans)


[STATEMENT]
lemma Limit_vempty_in_VsetI:
  assumes "Limit \<alpha>"
  shows "0 \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: Limit_def)


[STATEMENT]
lemma vsubset_in_VsetI[intro]:
  assumes "a \<subseteq>\<^sub>\<circ> A" and "A \<in>\<^sub>\<circ> Vset i"
  shows "a \<in>\<^sub>\<circ> Vset i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<subseteq>\<^sub>\<circ> A
A \<in>\<^sub>\<circ> Vset i

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
by (auto dest: VPow_vsubset_Vset)


[STATEMENT]
lemma Ord_vsubset_in_Vset_succI:
  assumes "Ord \<alpha>" and "A \<subseteq>\<^sub>\<circ> Vset \<alpha>"
  shows "A \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
using assms Ord_Vset_in_Vset_succI
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
A \<subseteq>\<^sub>\<circ> Vset \<alpha>
Ord ?\<alpha> \<Longrightarrow> Vset ?\<alpha> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ ?\<alpha>)

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by auto


[STATEMENT]
lemma Limit_VPow_in_VsetI[intro]:
  assumes "Limit \<alpha>" and "A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "VPow A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VPow A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
[PROOF STEP]
have "Ord \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>

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

goal (1 subgoal):
 1. VPow A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha>
Ord \<alpha>
[PROOF STEP]
obtain i where "A \<in>\<^sub>\<circ> Vset i" and "i \<in>\<^sub>\<circ> \<alpha>" and "Ord i"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
A \<in>\<^sub>\<circ> Vset \<alpha>
Ord \<alpha>

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A \<in>\<^sub>\<circ> Vset i; i \<in>\<^sub>\<circ> \<alpha>; Ord i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: Ord_in_Ord Limit_Vfrom_eq)
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> Vset i
i \<in>\<^sub>\<circ> \<alpha>
Ord i

goal (1 subgoal):
 1. VPow A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "Vset i \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset i \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule Vset_in_mono) (auto intro: \<open>i \<in>\<^sub>\<circ> \<alpha>\<close>)
[PROOF STATE]
proof (state)
this:
Vset i \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VPow A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from VPow_vsubset_Vset[OF \<open>A \<in>\<^sub>\<circ> Vset i\<close>] this
[PROOF STATE]
proof (chain)
picking this:
VPow A \<subseteq>\<^sub>\<circ> Vset i
Vset i \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
VPow A \<subseteq>\<^sub>\<circ> Vset i
Vset i \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VPow A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule vsubset_in_VsetI)
[PROOF STATE]
proof (state)
this:
VPow A \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma VPow_in_Vset_revD:
  assumes "VPow A \<in>\<^sub>\<circ> Vset i"
  shows "A \<in>\<^sub>\<circ> Vset i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
using assms Vset_trans
[PROOF STATE]
proof (prove)
using this:
VPow A \<in>\<^sub>\<circ> Vset i
\<lbrakk>?x \<in>\<^sub>\<circ> ?X; ?X \<in>\<^sub>\<circ> Vset ?i\<rbrakk> \<Longrightarrow> ?x \<in>\<^sub>\<circ> Vset ?i

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset i
[PROOF STEP]
by blast


[STATEMENT]
lemma Ord_VPow_in_Vset_succI:
  assumes "Ord \<alpha>" and "a \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "VPow a \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VPow a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
using VPow_vsubset_Vset[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
VPow a \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VPow a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (auto intro: Ord_Vset_in_Vset_succI[OF assms(1)])


[STATEMENT]
lemma Ord_VPow_in_Vset_succD:
  assumes "Ord \<alpha>" and "VPow a \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
  shows "a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
VPow a \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (fastforce dest: Vset_succ)