[STATEMENT]
lemma inv_step:
  assumes "S' \<noteq> {}"
and IH: "inv S' C r"
defines[simp]: "s \<equiv> (SOME s. s \<in> S')"
shows "inv (S' - {s' . s' \<in> S' \<and> dist s s' \<le> 2*r}) (C \<union> {s}) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have s_def: "s \<in> S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S'
[PROOF STEP]
using assms(1) some_in_eq
[PROOF STATE]
proof (prove)
using this:
S' \<noteq> {}
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

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

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "finite (C \<union> {s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (C \<union> {s})
[PROOF STEP]
using IH finite_subset[OF _ finite_sites]
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
?A \<subseteq> S \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (C \<union> {s})
[PROOF STEP]
by (simp add: inv_def)
[PROOF STATE]
proof (state)
this:
finite (C \<union> {s})

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (C \<union> {s})

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "(\<forall>s' \<in> (S - (S' - {s' . s' \<in> S' \<and> dist s s' \<le> 2*r})). distance (C \<union> {s}) s' \<le> 2*r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s'\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) s' \<le> 2 * r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s'. s' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) \<Longrightarrow> distance (C \<union> {s}) s' \<le> 2 * r
[PROOF STEP]
fix s''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s'. s' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) \<Longrightarrow> distance (C \<union> {s}) s' \<le> 2 * r
[PROOF STEP]
assume "s'' \<in> S - (S' - {s' . s' \<in> S' \<and> dist s s' \<le> 2*r})"
[PROOF STATE]
proof (state)
this:
s'' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r})

goal (1 subgoal):
 1. \<And>s'. s' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) \<Longrightarrow> distance (C \<union> {s}) s' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s'' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r})
[PROOF STEP]
have "s'' \<in> S - S' \<or> s'' \<in> {s' . s' \<in> S' \<and> dist s s' \<le> 2*r}"
[PROOF STATE]
proof (prove)
using this:
s'' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r})

goal (1 subgoal):
 1. s'' \<in> S - S' \<or> s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s'' \<in> S - S' \<or> s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}

goal (1 subgoal):
 1. \<And>s'. s' \<in> S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) \<Longrightarrow> distance (C \<union> {s}) s' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s'' \<in> S - S' \<or> s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}
[PROOF STEP]
show "distance (C \<union> {s}) s'' \<le> 2 * r"
[PROOF STATE]
proof (prove)
using this:
s'' \<in> S - S' \<or> s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s'' \<in> S - S' \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
 2. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
assume local_assm: "s'' \<in> S - S'"
[PROOF STATE]
proof (state)
this:
s'' \<in> S - S'

goal (2 subgoals):
 1. s'' \<in> S - S' \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
 2. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
have "S' = S \<or> C \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' = S \<or> C \<noteq> {}
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r

goal (1 subgoal):
 1. S' = S \<or> C \<noteq> {}
[PROOF STEP]
by (simp add: inv_def)
[PROOF STATE]
proof (state)
this:
S' = S \<or> C \<noteq> {}

goal (2 subgoals):
 1. s'' \<in> S - S' \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
 2. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' = S \<or> C \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S' = S \<or> C \<noteq> {}

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S' = S \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
 2. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
assume "S' = S"
[PROOF STATE]
proof (state)
this:
S' = S

goal (2 subgoals):
 1. S' = S \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
 2. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' = S
[PROOF STEP]
have "s'' \<in> {}"
[PROOF STATE]
proof (prove)
using this:
S' = S

goal (1 subgoal):
 1. s'' \<in> {}
[PROOF STEP]
using local_assm
[PROOF STATE]
proof (prove)
using this:
S' = S
s'' \<in> S - S'

goal (1 subgoal):
 1. s'' \<in> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s'' \<in> {}

goal (2 subgoals):
 1. S' = S \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
 2. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s'' \<in> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s'' \<in> {}

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
assume C_not_empty: "C \<noteq> {}"
[PROOF STATE]
proof (state)
this:
C \<noteq> {}

goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
have "finite C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C
[PROOF STEP]
using IH finite_subset[OF _ finite_sites]
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
?A \<subseteq> S \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite C
[PROOF STEP]
by (simp add: inv_def)
[PROOF STATE]
proof (state)
this:
finite C

goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
have "distance (C \<union> {s}) s'' \<le> distance C s''"
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> distance C s''
[PROOF STEP]
using distance_mono C_not_empty
[PROOF STATE]
proof (prove)
using this:
finite C
\<lbrakk>?C\<^sub>1 \<subseteq> ?C\<^sub>2; ?C\<^sub>1 \<noteq> {}; finite ?C\<^sub>2\<rbrakk> \<Longrightarrow> distance ?C\<^sub>2 ?s \<le> distance ?C\<^sub>1 ?s
C \<noteq> {}

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> distance C s''
[PROOF STEP]
by (meson Un_upper1 calculation)
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> distance C s''

goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> distance C s''

goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
have " ...  \<le> 2 * r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C s'' \<le> 2 * r
[PROOF STEP]
using IH local_assm inv_def
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
s'' \<in> S - S'
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))

goal (1 subgoal):
 1. distance C s'' \<le> 2 * r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distance C s'' \<le> 2 * r

goal (1 subgoal):
 1. C \<noteq> {} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal (1 subgoal):
 1. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
assume local_assm: "s'' \<in> {s' . s' \<in> S' \<and> dist s s' \<le> 2*r}"
[PROOF STATE]
proof (state)
this:
s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}

goal (1 subgoal):
 1. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}
[PROOF STEP]
have "distance (C \<union> {s}) s'' \<le> dist s'' s"
[PROOF STATE]
proof (prove)
using this:
s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> dist s'' s
[PROOF STEP]
using Min.coboundedI distance_def dist_lemmas calculation
[PROOF STATE]
proof (prove)
using this:
s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}
\<lbrakk>finite ?A; ?a \<in> ?A\<rbrakk> \<Longrightarrow> Min ?A \<le> ?a
distance ?C ?s = Min (dist ?s ` ?C)
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> finite (dist ?s ` ?C)
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> distance ?C ?s \<in> dist ?s ` ?C
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>c\<in>?C. dist ?s c = distance ?C ?s
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> 0 \<le> distance ?C ?s
finite (C \<union> {s})

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> dist s'' s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> dist s'' s

goal (1 subgoal):
 1. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> dist s'' s

goal (1 subgoal):
 1. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
have " ... \<le> 2 * r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist s'' s \<le> 2 * r
[PROOF STEP]
using local_assm
[PROOF STATE]
proof (prove)
using this:
s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r}

goal (1 subgoal):
 1. dist s'' s \<le> 2 * r
[PROOF STEP]
by (smt dist_self dist_triangle2 mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
dist s'' s \<le> 2 * r

goal (1 subgoal):
 1. s'' \<in> {s' \<in> S'. dist s s' \<le> 2 * r} \<Longrightarrow> distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal (1 subgoal):
 1. distance (C \<union> {s}) s'' \<le> 2 * r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distance (C \<union> {s}) s'' \<le> 2 * r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>s'\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) s' \<le> 2 * r

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>s'\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) s' \<le> 2 * r

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "S' - {s' . s' \<in> S' \<and> dist s s' \<le> 2*r} \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r

goal (1 subgoal):
 1. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S
[PROOF STEP]
by (auto simp: inv_def)
[PROOF STATE]
proof (state)
this:
S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
using IH inv_def s_def
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))
s \<in> S'

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

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
[PROOF STEP]
have "C \<union> {s} \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. C \<union> {s} \<subseteq> S
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
s \<in> S
local.inv S' C r

goal (1 subgoal):
 1. C \<union> {s} \<subseteq> S
[PROOF STEP]
by (simp add: inv_def)
[PROOF STATE]
proof (state)
this:
C \<union> {s} \<subseteq> S

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
C \<union> {s} \<subseteq> S

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<union> {s} \<subseteq> S

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "(\<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2
[PROOF STEP]
proof (rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c c\<^sub>2. \<lbrakk>c \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> 2 * r < dist c c\<^sub>2
[PROOF STEP]
fix c\<^sub>1 c\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c c\<^sub>2. \<lbrakk>c \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> 2 * r < dist c c\<^sub>2
[PROOF STEP]
assume local_assms: "c\<^sub>1 \<in> C \<union> {s}" "c\<^sub>2 \<in> C \<union> {s}" "c\<^sub>1 \<noteq> c\<^sub>2"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2

goal (1 subgoal):
 1. \<And>c c\<^sub>2. \<lbrakk>c \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> 2 * r < dist c c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2
[PROOF STEP]
have "(c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C) \<or> (c\<^sub>1 = s \<and> c\<^sub>2 \<in> C) \<or> (c\<^sub>1 \<in> C \<and> c\<^sub>2 = s) \<or> (c\<^sub>1 = s \<and> c\<^sub>2 = s)"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2

goal (1 subgoal):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<or> c\<^sub>1 = s \<and> c\<^sub>2 = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2
S' \<noteq> {}
local.inv S' C r
s \<equiv> SOME s. s \<in> S'

goal (1 subgoal):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<or> c\<^sub>1 = s \<and> c\<^sub>2 = s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<or> c\<^sub>1 = s \<and> c\<^sub>2 = s

goal (1 subgoal):
 1. \<And>c c\<^sub>2. \<lbrakk>c \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> 2 * r < dist c c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<or> c\<^sub>1 = s \<and> c\<^sub>2 = s
[PROOF STEP]
show "2 * r < dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<or> c\<^sub>1 = s \<and> c\<^sub>2 = s

goal (1 subgoal):
 1. 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 4. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume "c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C

goal (4 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 4. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C
[PROOF STEP]
show "2 * r < dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C

goal (1 subgoal):
 1. 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using IH inv_def local_assms
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C
local.inv S' C r
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2

goal (1 subgoal):
 1. 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * r < dist c\<^sub>1 c\<^sub>2

goal (3 subgoals):
 1. c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume case_assm: "c\<^sub>1 = s \<and> c\<^sub>2 \<in> C"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 = s \<and> c\<^sub>2 \<in> C

goal (3 subgoals):
 1. c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have "(\<forall>c \<in> C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s
[PROOF STEP]
using IH inv_def
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))

goal (1 subgoal):
 1. \<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s

goal (3 subgoals):
 1. c\<^sub>1 = s \<and> c\<^sub>2 \<in> C \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s

goal (1 subgoal):
 1. 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by (smt case_assm s_def assms(1) dist_self dist_triangle3 singletonD)
[PROOF STATE]
proof (state)
this:
2 * r < dist c\<^sub>1 c\<^sub>2

goal (2 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume case_assm: "c\<^sub>1 \<in> C \<and> c\<^sub>2 = s"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 = s

goal (2 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have "(\<forall>c \<in> C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s
[PROOF STEP]
using IH inv_def
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))

goal (1 subgoal):
 1. \<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s

goal (2 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>C. \<forall>s\<in>S'. S' \<noteq> {} \<longrightarrow> 2 * r < dist c s

goal (1 subgoal):
 1. 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by (smt case_assm s_def assms(1) dist_self dist_triangle3 singletonD)
[PROOF STATE]
proof (state)
this:
2 * r < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume "c\<^sub>1 = s \<and> c\<^sub>2 = s"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 = s \<and> c\<^sub>2 = s

goal (1 subgoal):
 1. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 = s \<and> c\<^sub>2 = s
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 = s \<and> c\<^sub>2 = s

goal (1 subgoal):
 1. False
[PROOF STEP]
using local_assms(3)
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 = s \<and> c\<^sub>2 = s
c\<^sub>1 \<noteq> c\<^sub>2

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

goal (1 subgoal):
 1. c\<^sub>1 = s \<and> c\<^sub>2 = s \<Longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. 2 * r < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * r < dist c\<^sub>1 c\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 * r < dist c\<^sub>1 c\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "(\<forall>c\<in>C \<union> {s}. \<forall>s'' \<in> S' - {s' \<in> S'. dist s s' \<le> 2 * r}.
           S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''
[PROOF STEP]
using IH inv_def
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))

goal (1 subgoal):
 1. \<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
have "(S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {}

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (C \<union> {s})
\<forall>s'\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) s' \<le> 2 * r
S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S
C \<union> {s} \<subseteq> S
\<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2
\<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''
S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (C \<union> {s})
\<forall>s'\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) s' \<le> 2 * r
S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S
C \<union> {s} \<subseteq> S
\<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2
\<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''
S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {}

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r
[PROOF STEP]
unfolding inv_def
[PROOF STATE]
proof (prove)
using this:
finite (C \<union> {s})
\<forall>s'\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) s' \<le> 2 * r
S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S
C \<union> {s} \<subseteq> S
\<forall>c\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c c\<^sub>2
\<forall>c\<in>C \<union> {s}. \<forall>s''\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c s''
S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {}

goal (1 subgoal):
 1. (\<forall>sa\<in>S - (S' - {s' \<in> S'. dist s s' \<le> 2 * r}). distance (C \<union> {s}) sa \<le> 2 * r) \<and> S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<subseteq> S \<and> C \<union> {s} \<subseteq> S \<and> (\<forall>c\<in>C \<union> {s}. \<forall>sa\<in>S' - {s' \<in> S'. dist s s' \<le> 2 * r}. S' - {s' \<in> S'. dist s s' \<le> 2 * r} \<noteq> {} \<longrightarrow> 2 * r < dist c sa) \<and> (S' - {s' \<in> S'. dist s s' \<le> 2 * r} = S \<or> C \<union> {s} \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.inv (S' - {s' \<in> S'. dist s s' \<le> 2 * r}) (C \<union> {s}) r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_last_1:
  assumes "\<forall>s \<in> (S - S'). distance C s \<le> 2*r"
    and "S' = {}"
  shows "radius C \<le> 2*r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radius C \<le> 2 * r
[PROOF STEP]
by (metis Diff_empty assms image_iff radius_contained)


[STATEMENT]
lemma inv_last_2:
  assumes "finite C"
  and "card C > n"
  and "C \<subseteq> S"
  and "\<forall>c\<^sub>1 \<in> C. \<forall>c\<^sub>2 \<in> C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> dist c\<^sub>1 c\<^sub>2 > 2*r"
  shows "\<forall>C'. card C' \<le> n \<and> card C' > 0 \<longrightarrow> radius C' > r" (is ?P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?P"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C')

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C')
[PROOF STEP]
obtain C' where card_C': "card C' \<le> n \<and> card C' > 0" and radius_C': "radius C' \<le> r"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C')

goal (1 subgoal):
 1. (\<And>C'. \<lbrakk>card C' \<le> n \<and> 0 < card C'; radius C' \<le> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card C' \<le> n \<and> 0 < card C'
radius C' \<le> r

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
have "\<forall>c \<in> C. (\<exists>c'. c' \<in> C' \<and> dist c c' \<le> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>C. \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
assume "c \<in> C"
[PROOF STATE]
proof (state)
this:
c \<in> C

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> C
[PROOF STEP]
have "c \<in> S"
[PROOF STATE]
proof (prove)
using this:
c \<in> C

goal (1 subgoal):
 1. c \<in> S
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
c \<in> C
C \<subseteq> S

goal (1 subgoal):
 1. c \<in> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<in> S

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> S
[PROOF STEP]
have "distance C' c \<le> radius C'"
[PROOF STATE]
proof (prove)
using this:
c \<in> S

goal (1 subgoal):
 1. distance C' c \<le> radius C'
[PROOF STEP]
using finite_distances
[PROOF STATE]
proof (prove)
using this:
c \<in> S
finite (distance ?C ` S)

goal (1 subgoal):
 1. distance C' c \<le> radius C'
[PROOF STEP]
by (simp add: radius_def)
[PROOF STATE]
proof (state)
this:
distance C' c \<le> radius C'

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distance C' c \<le> radius C'
[PROOF STEP]
have "distance C' c \<le> r"
[PROOF STATE]
proof (prove)
using this:
distance C' c \<le> radius C'

goal (1 subgoal):
 1. distance C' c \<le> r
[PROOF STEP]
using radius_C'
[PROOF STATE]
proof (prove)
using this:
distance C' c \<le> radius C'
radius C' \<le> r

goal (1 subgoal):
 1. distance C' c \<le> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distance C' c \<le> r

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distance C' c \<le> r
[PROOF STEP]
show "\<exists>c'. c' \<in> C' \<and> dist c c' \<le> r"
[PROOF STATE]
proof (prove)
using this:
distance C' c \<le> r

goal (1 subgoal):
 1. \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
using dist_lemmas
[PROOF STATE]
proof (prove)
using this:
distance C' c \<le> r
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> finite (dist ?s ` ?C)
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> distance ?C ?s \<in> dist ?s ` ?C
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>c\<in>?C. dist ?s c = distance ?C ?s
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> 0 \<le> distance ?C ?s

goal (1 subgoal):
 1. \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
by (metis card_C' card_gt_0_iff)
[PROOF STATE]
proof (state)
this:
\<exists>c'. c' \<in> C' \<and> dist c c' \<le> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C. \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>C. \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r
[PROOF STEP]
obtain f where f: "\<forall>c\<in>C. f c \<in> C' \<and> dist c (f c) \<le> r"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>C. \<exists>c'. c' \<in> C' \<and> dist c c' \<le> r

goal (1 subgoal):
 1. (\<And>f. \<forall>c\<in>C. f c \<in> C' \<and> dist c (f c) \<le> r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>C. f c \<in> C' \<and> dist c (f c) \<le> r

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
have "\<not>inj_on f C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> inj_on f C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on f C \<Longrightarrow> False
[PROOF STEP]
assume "inj_on f C"
[PROOF STATE]
proof (state)
this:
inj_on f C

goal (1 subgoal):
 1. inj_on f C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on f C
[PROOF STEP]
have "card C' \<ge> card C"
[PROOF STATE]
proof (prove)
using this:
inj_on f C

goal (1 subgoal):
 1. card C \<le> card C'
[PROOF STEP]
using \<open>inj_on f C\<close> card_inj_on_le card_ge_0_finite card_C' f
[PROOF STATE]
proof (prove)
using this:
inj_on f C
inj_on f C
\<lbrakk>inj_on ?f ?A; ?f ` ?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
0 < card ?A \<Longrightarrow> finite ?A
card C' \<le> n \<and> 0 < card C'
\<forall>c\<in>C. f c \<in> C' \<and> dist c (f c) \<le> r

goal (1 subgoal):
 1. card C \<le> card C'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card C \<le> card C'

goal (1 subgoal):
 1. inj_on f C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card C \<le> card C'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
card C \<le> card C'

goal (1 subgoal):
 1. False
[PROOF STEP]
using card_C' \<open>n < card C\<close>
[PROOF STATE]
proof (prove)
using this:
card C \<le> card C'
card C' \<le> n \<and> 0 < card C'
n < card C

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> inj_on f C

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on f C
[PROOF STEP]
obtain c1 c2 where defs: "c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on f C

goal (1 subgoal):
 1. (\<And>c1 c2. c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on f C
inj_on ?f ?A = (\<forall>x\<in>?A. \<forall>y\<in>?A. ?f x = ?f y \<longrightarrow> x = y)

goal (1 subgoal):
 1. (\<And>c1 c2. c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2
[PROOF STEP]
have *: "dist c1 (f c1) \<le> r \<and> dist c2 (f c1) \<le> r"
[PROOF STATE]
proof (prove)
using this:
c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2

goal (1 subgoal):
 1. dist c1 (f c1) \<le> r \<and> dist c2 (f c1) \<le> r
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2
\<forall>c\<in>C. f c \<in> C' \<and> dist c (f c) \<le> r

goal (1 subgoal):
 1. dist c1 (f c1) \<le> r \<and> dist c2 (f c1) \<le> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist c1 (f c1) \<le> r \<and> dist c2 (f c1) \<le> r

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
have "2 * r < dist c1 c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * r < dist c1 c2
[PROOF STEP]
using assms defs
[PROOF STATE]
proof (prove)
using this:
finite C
n < card C
C \<subseteq> S
\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2
c1 \<in> C \<and> c2 \<in> C \<and> c1 \<noteq> c2 \<and> f c1 = f c2

goal (1 subgoal):
 1. 2 * r < dist c1 c2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * r < dist c1 c2

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * r < dist c1 c2

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
have " ... \<le> dist c1 (f c1) + dist (f c1) c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c1 c2 \<le> dist c1 (f c1) + dist (f c1) c2
[PROOF STEP]
by(rule dist_triangle)
[PROOF STATE]
proof (state)
this:
dist c1 c2 \<le> dist c1 (f c1) + dist (f c1) c2

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist c1 c2 \<le> dist c1 (f c1) + dist (f c1) c2

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
have " ... = dist c1 (f c1) + dist c2 (f c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c1 (f c1) + dist (f c1) c2 = dist c1 (f c1) + dist c2 (f c1)
[PROOF STEP]
using dist_commute
[PROOF STATE]
proof (prove)
using this:
dist ?x ?y = dist ?y ?x

goal (1 subgoal):
 1. dist c1 (f c1) + dist (f c1) c2 = dist c1 (f c1) + dist c2 (f c1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist c1 (f c1) + dist (f c1) c2 = dist c1 (f c1) + dist c2 (f c1)

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist c1 (f c1) + dist (f c1) c2 = dist c1 (f c1) + dist c2 (f c1)

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
have " ... \<le> 2 * r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c1 (f c1) + dist c2 (f c1) \<le> 2 * r
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist c1 (f c1) \<le> r \<and> dist c2 (f c1) \<le> r

goal (1 subgoal):
 1. dist c1 (f c1) + dist c2 (f c1) \<le> 2 * r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist c1 (f c1) + dist c2 (f c1) \<le> 2 * r

goal (1 subgoal):
 1. \<not> (\<forall>C'. card C' \<le> n \<and> 0 < card C' \<longrightarrow> r < radius C') \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * r < 2 * r
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
2 * r < 2 * r

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_last:
  assumes "inv {} C r"
  shows "(card C \<le> k \<longrightarrow> radius C \<le> 2*r) \<and> (card C > k \<longrightarrow> (\<forall>C'. card C' > 0 \<and> card C' \<le> k \<longrightarrow> radius C' > r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
using assms inv_def inv_last_1 inv_last_2 finite_subset[OF _ finite_sites]
[PROOF STATE]
proof (prove)
using this:
local.inv {} C r
local.inv ?S' ?C ?r = ((\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r) \<and> ?S' \<subseteq> S \<and> ?C \<subseteq> S \<and> (\<forall>c\<in>?C. \<forall>s\<in>?S'. ?S' \<noteq> {} \<longrightarrow> 2 * ?r < dist c s) \<and> (?S' = S \<or> ?C \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2))
\<lbrakk>\<forall>s\<in>S - ?S'. distance ?C s \<le> 2 * ?r; ?S' = {}\<rbrakk> \<Longrightarrow> radius ?C \<le> 2 * ?r
\<lbrakk>finite ?C; ?n < card ?C; ?C \<subseteq> S; \<forall>c\<^sub>1\<in>?C. \<forall>c\<^sub>2\<in>?C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * ?r < dist c\<^sub>1 c\<^sub>2\<rbrakk> \<Longrightarrow> \<forall>C'. card C' \<le> ?n \<and> 0 < card C' \<longrightarrow> ?r < radius C'
?A \<subseteq> S \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
by auto


[STATEMENT]
theorem Center_Selection_r:
  "VARS (S' :: ('a :: metric_space) set) (C :: ('a :: metric_space) set) (r :: real) (s :: 'a)
  {True}
  S' := S;
  C := {};
  WHILE S' \<noteq> {} INV {inv S' C r} DO
    s := (SOME s. s \<in> S');
    C := C \<union> {s};
    S' := S' - {s' . s' \<in> S' \<and> dist s s' \<le> 2*r}
    OD
  {(card C \<le> k \<longrightarrow> radius C \<le> 2*r) \<and> (card C > k \<longrightarrow> (\<forall>C'. card C' > 0 \<and> card C' \<le> k \<longrightarrow> radius C' > r))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {True}
S' := S; C := {}; WHILE S' \<noteq> {} INV {local.inv S' C r}  VAR {0}
DO s := (SOME s. s \<in> S'); C := C \<union> {s}; S' := S' - {s' \<in> S'. dist s s' \<le> 2 * r} OD
{(card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))}
[PROOF STEP]
proof (vcg, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S' C r s. True \<Longrightarrow> local.inv S {} r
 2. \<And>S' C r s. local.inv S' C r \<and> S' \<noteq> {} \<Longrightarrow> local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
 3. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
case (1 S' C r)
[PROOF STATE]
proof (state)
this:
True

goal (3 subgoals):
 1. \<And>S' C r s. True \<Longrightarrow> local.inv S {} r
 2. \<And>S' C r s. local.inv S' C r \<and> S' \<noteq> {} \<Longrightarrow> local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
 3. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
True
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
True

goal (1 subgoal):
 1. local.inv S {} r
[PROOF STEP]
using inv_init
[PROOF STATE]
proof (prove)
using this:
True
local.inv S {} ?r

goal (1 subgoal):
 1. local.inv S {} r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.inv S {} r

goal (2 subgoals):
 1. \<And>S' C r s. local.inv S' C r \<and> S' \<noteq> {} \<Longrightarrow> local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
 2. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S' C r s. local.inv S' C r \<and> S' \<noteq> {} \<Longrightarrow> local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
 2. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
case (2 S' C r)
[PROOF STATE]
proof (state)
this:
local.inv S' C r \<and> S' \<noteq> {}

goal (2 subgoals):
 1. \<And>S' C r s. local.inv S' C r \<and> S' \<noteq> {} \<Longrightarrow> local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
 2. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.inv S' C r \<and> S' \<noteq> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r \<and> S' \<noteq> {}

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
[PROOF STEP]
using inv_step
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r \<and> S' \<noteq> {}
\<lbrakk>?S' \<noteq> {}; local.inv ?S' ?C ?r\<rbrakk> \<Longrightarrow> local.inv (?S' - {s' \<in> ?S'. dist (SOME s. s \<in> ?S') s' \<le> 2 * ?r}) (?C \<union> {SOME s. s \<in> ?S'}) ?r

goal (1 subgoal):
 1. local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.inv (S' - {s' \<in> S'. dist (SOME s. s \<in> S') s' \<le> 2 * r}) (C \<union> {SOME s. s \<in> S'}) r

goal (1 subgoal):
 1. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
case (3 S' C r)
[PROOF STATE]
proof (state)
this:
local.inv S' C r \<and> \<not> S' \<noteq> {}

goal (1 subgoal):
 1. \<And>S' C r s. local.inv S' C r \<and> \<not> S' \<noteq> {} \<Longrightarrow> (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.inv S' C r \<and> \<not> S' \<noteq> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r \<and> \<not> S' \<noteq> {}

goal (1 subgoal):
 1. (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
using inv_last
[PROOF STATE]
proof (prove)
using this:
local.inv S' C r \<and> \<not> S' \<noteq> {}
local.inv {} ?C ?r \<Longrightarrow> (card ?C \<le> k \<longrightarrow> radius ?C \<le> 2 * ?r) \<and> (k < card ?C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> ?r < radius C'))

goal (1 subgoal):
 1. (card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(card C \<le> k \<longrightarrow> radius C \<le> 2 * r) \<and> (k < card C \<longrightarrow> (\<forall>C'. 0 < card C' \<and> card C' \<le> k \<longrightarrow> r < radius C'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invar_init: "invar {some S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
let ?s = "some S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
have s_in_S: "?s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME s. s \<in> S) \<in> S
[PROOF STEP]
using some_in_eq non_empty_sites
[PROOF STATE]
proof (prove)
using this:
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})
S \<noteq> {}

goal (1 subgoal):
 1. (SOME s. s \<in> S) \<in> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(SOME s. s \<in> S) \<in> S

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
have "{?s} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {SOME s. s \<in> S} \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{SOME s. s \<in> S} \<noteq> {}

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{SOME s. s \<in> S} \<noteq> {}

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
have "{SOME s. s \<in> S} \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {SOME s. s \<in> S} \<subseteq> S
[PROOF STEP]
using s_in_S
[PROOF STATE]
proof (prove)
using this:
(SOME s. s \<in> S) \<in> S

goal (1 subgoal):
 1. {SOME s. s \<in> S} \<subseteq> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{SOME s. s \<in> S} \<subseteq> S

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{SOME s. s \<in> S} \<subseteq> S

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
have "card {SOME s. s \<in> S} \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {SOME s. s \<in> S} \<le> k
[PROOF STEP]
using non_zero_k
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. card {SOME s. s \<in> S} \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {SOME s. s \<in> S} \<le> k

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{SOME s. s \<in> S} \<noteq> {}
{SOME s. s \<in> S} \<subseteq> S
card {SOME s. s \<in> S} \<le> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{SOME s. s \<in> S} \<noteq> {}
{SOME s. s \<in> S} \<subseteq> S
card {SOME s. s \<in> S} \<le> k

goal (1 subgoal):
 1. invar {SOME s. s \<in> S}
[PROOF STEP]
by (auto simp: invar_def)
[PROOF STATE]
proof (state)
this:
invar {SOME s. s \<in> S}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invar_step:
assumes "invar C"
and "card C < k"
shows "invar (C \<union> {furthest_from C})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
have furthest_from_C_props: "furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C
[PROOF STEP]
using someI_ex[of "\<lambda>x. x \<in> S \<and> distance C x = radius C"] radius_def2 radius_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> S \<and> distance C x = radius C \<Longrightarrow> (SOME x. x \<in> S \<and> distance C x = radius C) \<in> S \<and> distance C (SOME x. x \<in> S \<and> distance C x = radius C) = radius C
\<exists>s\<in>S. distance ?C s = radius ?C
radius ?C = Max (distance ?C ` S)

goal (1 subgoal):
 1. furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
have C_props: "finite C \<and> C \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C \<and> C \<noteq> {}
[PROOF STEP]
using finite_subset[OF _ finite_sites] assms(1)
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> S \<Longrightarrow> finite ?A
invar C

goal (1 subgoal):
 1. finite C \<and> C \<noteq> {}
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> S \<Longrightarrow> finite ?A
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))

goal (1 subgoal):
 1. finite C \<and> C \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
have "card (C \<union> {furthest_from C}) \<le> card C + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (C \<union> {furthest_from C}) \<le> card C + 1
[PROOF STEP]
using assms(1) C_props
[PROOF STATE]
proof (prove)
using this:
invar C
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. card (C \<union> {furthest_from C}) \<le> card C + 1
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. card (C \<union> {furthest_from C}) \<le> card C + 1
[PROOF STEP]
by (simp add: card_insert_if)
[PROOF STATE]
proof (state)
this:
card (C \<union> {furthest_from C}) \<le> card C + 1

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (C \<union> {furthest_from C}) \<le> card C + 1
[PROOF STEP]
have "card (C \<union> {furthest_from C}) < k + 1"
[PROOF STATE]
proof (prove)
using this:
card (C \<union> {furthest_from C}) \<le> card C + 1

goal (1 subgoal):
 1. card (C \<union> {furthest_from C}) < k + 1
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
card (C \<union> {furthest_from C}) \<le> card C + 1
card C < k

goal (1 subgoal):
 1. card (C \<union> {furthest_from C}) < k + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (C \<union> {furthest_from C}) < k + 1

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (C \<union> {furthest_from C}) < k + 1
[PROOF STEP]
have "card (C \<union> {furthest_from C}) \<le> k"
[PROOF STATE]
proof (prove)
using this:
card (C \<union> {furthest_from C}) < k + 1

goal (1 subgoal):
 1. card (C \<union> {furthest_from C}) \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (C \<union> {furthest_from C}) \<le> k

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
card (C \<union> {furthest_from C}) \<le> k

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (C \<union> {furthest_from C}) \<le> k

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
have "C \<union> {furthest_from C} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<union> {furthest_from C} \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C \<union> {furthest_from C} \<noteq> {}

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<union> {furthest_from C} \<noteq> {}

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
have "(C \<union> {furthest_from C}) \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<union> {furthest_from C} \<subseteq> S
[PROOF STEP]
using assms(1) furthest_from_C_props
[PROOF STATE]
proof (prove)
using this:
invar C
furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C

goal (1 subgoal):
 1. C \<union> {furthest_from C} \<subseteq> S
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))
furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C

goal (1 subgoal):
 1. C \<union> {furthest_from C} \<subseteq> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C \<union> {furthest_from C} \<subseteq> S

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<union> {furthest_from C} \<subseteq> S

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
have "\<forall>C'. (\<forall>s \<in> S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C')
          \<or> (\<forall>c\<^sub>1 \<in> C \<union> {furthest_from C}. \<forall>c\<^sub>2 \<in> C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
fix C'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
have "distance C (furthest_from C) > 2 * radius C' \<or> distance C (furthest_from C) \<le> 2 * radius C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * radius C' < distance C (furthest_from C) \<or> distance C (furthest_from C) \<le> 2 * radius C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * radius C' < distance C (furthest_from C) \<or> distance C (furthest_from C) \<le> 2 * radius C'

goal (1 subgoal):
 1. \<And>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * radius C' < distance C (furthest_from C) \<or> distance C (furthest_from C) \<le> 2 * radius C'
[PROOF STEP]
show "(\<forall>s \<in> S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C')
               \<or> (\<forall>c\<^sub>1 \<in> C \<union> {furthest_from C}. \<forall>c\<^sub>2 \<in> C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
2 * radius C' < distance C (furthest_from C) \<or> distance C (furthest_from C) \<le> 2 * radius C'

goal (1 subgoal):
 1. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 * radius C' < distance C (furthest_from C) \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
 2. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
assume asm: "distance C (furthest_from C) > 2 * radius C'"
[PROOF STATE]
proof (state)
this:
2 * radius C' < distance C (furthest_from C)

goal (2 subgoals):
 1. 2 * radius C' < distance C (furthest_from C) \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
 2. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * radius C' < distance C (furthest_from C)
[PROOF STEP]
have "\<not>(\<forall>s \<in> S. distance C s \<le> 2 * radius C')"
[PROOF STATE]
proof (prove)
using this:
2 * radius C' < distance C (furthest_from C)

goal (1 subgoal):
 1. \<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
using furthest_from_C_props
[PROOF STATE]
proof (prove)
using this:
2 * radius C' < distance C (furthest_from C)
furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C

goal (1 subgoal):
 1. \<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')

goal (2 subgoals):
 1. 2 * radius C' < distance C (furthest_from C) \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
 2. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
[PROOF STEP]
have IH: "\<forall>c\<^sub>1 \<in> C. \<forall>c\<^sub>2 \<in> C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')

goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
invar C

goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s\<in>S. distance C s \<le> 2 * radius C')
C \<noteq> {} \<and> card C \<le> k \<and> C \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance C s \<le> 2 * radius C'))

goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (2 subgoals):
 1. 2 * radius C' < distance C (furthest_from C) \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
 2. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
have "(\<forall>c\<^sub>1 \<in> C \<union> {furthest_from C}. (\<forall>c\<^sub>2 \<in> C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using dist_ins[of "C" "2 * radius C'" "furthest_from C"] IH C_props asm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2; 2 * radius C' < distance C (furthest_from C); finite C; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
finite C \<and> C \<noteq> {}
2 * radius C' < distance C (furthest_from C)

goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (2 subgoals):
 1. 2 * radius C' < distance C (furthest_from C) \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
 2. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)

goal (1 subgoal):
 1. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
assume main_assm: "2 * radius C' \<ge> distance C (furthest_from C)"
[PROOF STATE]
proof (state)
this:
distance C (furthest_from C) \<le> 2 * radius C'

goal (1 subgoal):
 1. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
have "(\<forall>s \<in> S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
assume local_assm: "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
[PROOF STEP]
show "distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'"
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
have "distance (C \<union> {furthest_from C}) s \<le> distance C s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance (C \<union> {furthest_from C}) s \<le> distance C s
[PROOF STEP]
using distance_mono[of C "C \<union> {furthest_from C}"] C_props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>C \<subseteq> C \<union> {furthest_from C}; C \<noteq> {}; finite (C \<union> {furthest_from C})\<rbrakk> \<Longrightarrow> distance (C \<union> {furthest_from C}) ?s \<le> distance C ?s
finite C \<and> C \<noteq> {}

goal (1 subgoal):
 1. distance (C \<union> {furthest_from C}) s \<le> distance C s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distance (C \<union> {furthest_from C}) s \<le> distance C s

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distance (C \<union> {furthest_from C}) s \<le> distance C s

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
have " ... \<le> distance C (furthest_from C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C s \<le> distance C (furthest_from C)
[PROOF STEP]
using Max.coboundedI local_assm finite_distances radius_def furthest_from_C_props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?a \<in> ?A\<rbrakk> \<Longrightarrow> ?a \<le> Max ?A
s \<in> S
finite (distance ?C ` S)
radius ?C = Max (distance ?C ` S)
furthest_from C \<in> S \<and> distance C (furthest_from C) = radius C

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

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distance C s \<le> distance C (furthest_from C)

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
have " ... \<le> 2 * radius C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C (furthest_from C) \<le> 2 * radius C'
[PROOF STEP]
using main_assm
[PROOF STATE]
proof (prove)
using this:
distance C (furthest_from C) \<le> 2 * radius C'

goal (1 subgoal):
 1. distance C (furthest_from C) \<le> 2 * radius C'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distance C (furthest_from C) \<le> 2 * radius C'

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'

goal (1 subgoal):
 1. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'

goal (1 subgoal):
 1. distance C (furthest_from C) \<le> 2 * radius C' \<Longrightarrow> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'

goal (1 subgoal):
 1. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (C \<union> {furthest_from C}) \<le> k
C \<union> {furthest_from C} \<noteq> {}
C \<union> {furthest_from C} \<subseteq> S
\<forall>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (C \<union> {furthest_from C}) \<le> k
C \<union> {furthest_from C} \<noteq> {}
C \<union> {furthest_from C} \<subseteq> S
\<forall>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)

goal (1 subgoal):
 1. invar (C \<union> {furthest_from C})
[PROOF STEP]
unfolding invar_def
[PROOF STATE]
proof (prove)
using this:
card (C \<union> {furthest_from C}) \<le> k
C \<union> {furthest_from C} \<noteq> {}
C \<union> {furthest_from C} \<subseteq> S
\<forall>C'. (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C') \<or> (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2)

goal (1 subgoal):
 1. C \<union> {furthest_from C} \<noteq> {} \<and> card (C \<union> {furthest_from C}) \<le> k \<and> C \<union> {furthest_from C} \<subseteq> S \<and> (\<forall>C'. (\<forall>c\<^sub>1\<in>C \<union> {furthest_from C}. \<forall>c\<^sub>2\<in>C \<union> {furthest_from C}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * radius C' < dist c\<^sub>1 c\<^sub>2) \<or> (\<forall>s\<in>S. distance (C \<union> {furthest_from C}) s \<le> 2 * radius C'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar (C \<union> {furthest_from C})

goal:
No subgoals!
[PROOF STEP]
qed