[STATEMENT]
lemma hausdorff_distance_closures [simp]:
  "hausdorff_distance (closure A) (closure B) = hausdorff_distance A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
proof (cases "A = {} \<or> B = {} \<or> (\<not>(bounded A)) \<or> (\<not>(bounded B))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B
[PROOF STEP]
have *: "hausdorff_distance A B = 0"
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B

goal (1 subgoal):
 1. hausdorff_distance A B = 0
[PROOF STEP]
unfolding hausdorff_distance_def
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B

goal (1 subgoal):
 1. (if A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B then 0 else max (SUP x\<in>A. infdist x B) (SUP x\<in>B. infdist x A)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B = 0

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "closure A = {} \<or> (\<not>(bounded (closure A))) \<or> closure B = {} \<or> (\<not>(bounded (closure B)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)
[PROOF STEP]
using True bounded_subset closure_subset
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B
\<lbrakk>bounded ?T; ?S \<subseteq> ?T\<rbrakk> \<Longrightarrow> bounded ?S
?S \<subseteq> closure ?S

goal (1 subgoal):
 1. closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)
[PROOF STEP]
have "hausdorff_distance (closure A) (closure B) = 0"
[PROOF STATE]
proof (prove)
using this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = 0
[PROOF STEP]
unfolding hausdorff_distance_def
[PROOF STATE]
proof (prove)
using this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)

goal (1 subgoal):
 1. (if closure A = {} \<or> closure B = {} \<or> \<not> bounded (closure A) \<or> \<not> bounded (closure B) then 0 else max (SUP x\<in>closure A. infdist x (closure B)) (SUP x\<in>closure B. infdist x (closure A))) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) = 0

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (closure A) (closure B) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) = 0
hausdorff_distance A B = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) = hausdorff_distance A B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B)
[PROOF STEP]
have H: "A \<noteq> {}" "B \<noteq> {}" "bounded A" "bounded B"
[PROOF STATE]
proof (prove)
using this:
\<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B)

goal (1 subgoal):
 1. (A \<noteq> {} &&& B \<noteq> {}) &&& bounded A &&& bounded B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
[PROOF STEP]
have H2: "closure A \<noteq> {}" "closure B \<noteq> {}" "bounded (closure A)" "bounded (closure B)"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B

goal (1 subgoal):
 1. (closure A \<noteq> {} &&& closure B \<noteq> {}) &&& bounded (closure A) &&& bounded (closure B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closure A \<noteq> {}
 2. bounded (closure A)
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. closure A \<noteq> {}
 2. bounded (closure A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance (closure A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) B \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closure B \<noteq> {}
 2. bounded (closure B)
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. closure B \<noteq> {}
 2. bounded (closure B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) B \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) B \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance (closure A) (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B = hausdorff_distance (closure A) (closure B)
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B = hausdorff_distance (closure A) (closure B)
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B = hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)
[PROOF STEP]
have *: "hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)"
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A \<noteq> {}
 2. bounded A
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. A \<noteq> {}
 2. bounded A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance A (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... \<le> hausdorff_distance A B + hausdorff_distance B (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A (closure B) \<le> hausdorff_distance A B + hausdorff_distance B (closure B)
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. B \<noteq> {}
 2. bounded B
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. B \<noteq> {}
 2. bounded B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure B) \<le> hausdorff_distance A B + hausdorff_distance B (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure B) \<le> hausdorff_distance A B + hausdorff_distance B (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A B + hausdorff_distance B (closure B) = hausdorff_distance A B
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance A B + hausdorff_distance B (closure B) = hausdorff_distance A B
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B + hausdorff_distance B (closure B) = hausdorff_distance A B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
[PROOF STEP]
have "hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B"
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) = hausdorff_distance A B

goal:
No subgoals!
[PROOF STEP]
qed