[STATEMENT]
theorem Bondy :
  assumes "\<forall>A \<in> F. A \<subseteq> X" and "card X \<ge> 1" and "card F = card X"
  shows "\<exists>D. D \<subseteq> X & card D < card X & card (inter D ` F) = card F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
1 \<le> card X
card F = card X
[PROOF STEP]
have "finite F" and "finite X"
[PROOF STATE]
proof (prove)
using this:
1 \<le> card X
card F = card X

goal (1 subgoal):
 1. finite F &&& finite X
[PROOF STEP]
by (metis card.infinite not_one_le_zero)+
[PROOF STATE]
proof (state)
this:
finite F
finite X

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite F
finite X

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
have "m < card F \<Longrightarrow> \<exists>D. D \<subseteq> X & card D \<le> m & card (inter D ` F) \<ge> m + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
proof (induction m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) D ` F)
 2. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < card F

goal (2 subgoals):
 1. 0 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) D ` F)
 2. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
hence "{} \<subseteq> X & card {} \<le> 0 & card (inter {} ` F) \<ge> 0 + 1"
[PROOF STATE]
proof (prove)
using this:
0 < card F

goal (1 subgoal):
 1. {} \<subseteq> X \<and> card {} \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) {} ` F)
[PROOF STEP]
by auto (metis Suc_leI card_eq_0_iff empty_is_image finite_imageI gr0I)
[PROOF STATE]
proof (state)
this:
{} \<subseteq> X \<and> card {} \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) {} ` F)

goal (2 subgoals):
 1. 0 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) D ` F)
 2. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
thus "\<exists>D. (D \<subseteq> X & card D \<le> 0 & card (inter D ` F) \<ge> 0 + 1)"
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> X \<and> card {} \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) {} ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>D\<subseteq>X. card D \<le> 0 \<and> 0 + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
Suc m < card F

goal (1 subgoal):
 1. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
hence "m < card F"
[PROOF STATE]
proof (prove)
using this:
m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
Suc m < card F

goal (1 subgoal):
 1. m < card F
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
m < card F

goal (1 subgoal):
 1. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
with Suc.IH
[PROOF STATE]
proof (chain)
picking this:
m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
m < card F
[PROOF STEP]
obtain D
        where D: "D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card (inter D ` F)"
[PROOF STATE]
proof (prove)
using this:
m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
m < card F

goal (1 subgoal):
 1. (\<And>D. D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
with \<open>finite X\<close>
[PROOF STATE]
proof (chain)
picking this:
finite X
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
have "finite D"
[PROOF STATE]
proof (prove)
using this:
finite X
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)

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

goal (1 subgoal):
 1. \<And>m. \<lbrakk>m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F); Suc m < card F\<rbrakk> \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
proof (cases "card (inter D ` F) = card F")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card ((\<inter>) D ` F) = card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
 2. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
card ((\<inter>) D ` F) = card F

goal (2 subgoals):
 1. card ((\<inter>) D ` F) = card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
 2. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
hence "D \<subseteq> X \<and> card D \<le> Suc m \<and> Suc m + 1 \<le> card(inter D ` F)"
[PROOF STATE]
proof (prove)
using this:
card ((\<inter>) D ` F) = card F

goal (1 subgoal):
 1. D \<subseteq> X \<and> card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
using D Suc.prems
[PROOF STATE]
proof (prove)
using this:
card ((\<inter>) D ` F) = card F
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
Suc m < card F

goal (1 subgoal):
 1. D \<subseteq> X \<and> card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<subseteq> X \<and> card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)

goal (2 subgoals):
 1. card ((\<inter>) D ` F) = card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
 2. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
card ((\<inter>) D ` F) \<noteq> card F

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
hence "~ inj_on (inter D) F"
[PROOF STATE]
proof (prove)
using this:
card ((\<inter>) D ` F) \<noteq> card F

goal (1 subgoal):
 1. \<not> inj_on ((\<inter>) D) F
[PROOF STEP]
by (auto simp: card_image)
[PROOF STATE]
proof (state)
this:
\<not> inj_on ((\<inter>) D) F

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inj_on ((\<inter>) D) F
[PROOF STEP]
obtain A1 A2 where "A1 \<in> F" and "A2 \<in> F" and
          "D \<inter> A1 = D \<inter> A2" and "A1 \<noteq> A2"
[PROOF STATE]
proof (prove)
using this:
\<not> inj_on ((\<inter>) D) F

goal (1 subgoal):
 1. (\<And>A1 A2. \<lbrakk>A1 \<in> F; A2 \<in> F; D \<inter> A1 = D \<inter> A2; A1 \<noteq> A2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
A1 \<in> F
A2 \<in> F
D \<inter> A1 = D \<inter> A2
A1 \<noteq> A2

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A1 \<in> F
A2 \<in> F
D \<inter> A1 = D \<inter> A2
A1 \<noteq> A2
[PROOF STEP]
obtain x where x: "x : (A1 - A2) \<union> (A2 - A1)"
[PROOF STATE]
proof (prove)
using this:
A1 \<in> F
A2 \<in> F
D \<inter> A1 = D \<inter> A2
A1 \<noteq> A2

goal (1 subgoal):
 1. (\<And>x. x \<in> A1 - A2 \<union> (A2 - A1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> A1 - A2 \<union> (A2 - A1)

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
from \<open>\<forall>A \<in> F. A \<subseteq> X\<close> \<open>A1 \<in> F\<close> \<open>A2 \<in> F\<close> x
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>F. A \<subseteq> X
A1 \<in> F
A2 \<in> F
x \<in> A1 - A2 \<union> (A2 - A1)
[PROOF STEP]
have "x : X"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. A \<subseteq> X
A1 \<in> F
A2 \<in> F
x \<in> A1 - A2 \<union> (A2 - A1)

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

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
let ?E = "insert x D"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
from D \<open>finite D\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
finite D
[PROOF STEP]
have "card ?E \<le> Suc m"
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
finite D

goal (1 subgoal):
 1. card (insert x D) \<le> Suc m
[PROOF STEP]
by (metis (full_types) Suc_le_mono card_insert_if le_Suc_eq)
[PROOF STATE]
proof (state)
this:
card (insert x D) \<le> Suc m

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (insert x D) \<le> Suc m

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
with D \<open>x:X\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
x \<in> X
card (insert x D) \<le> Suc m
[PROOF STEP]
have "?E \<subseteq> X"
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
x \<in> X
card (insert x D) \<le> Suc m

goal (1 subgoal):
 1. insert x D \<subseteq> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x D \<subseteq> X

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert x D \<subseteq> X

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
have "Suc m < card (inter ?E ` F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
from \<open>D \<inter> A1 = D \<inter> A2\<close>
[PROOF STATE]
proof (chain)
picking this:
D \<inter> A1 = D \<inter> A2
[PROOF STEP]
have 1: "(D \<inter> (?E \<inter> A1)) = (D \<inter> (?E \<inter> A2))"
[PROOF STATE]
proof (prove)
using this:
D \<inter> A1 = D \<inter> A2

goal (1 subgoal):
 1. D \<inter> (insert x D \<inter> A1) = D \<inter> (insert x D \<inter> A2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<inter> (insert x D \<inter> A1) = D \<inter> (insert x D \<inter> A2)

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> A1 - A2 \<union> (A2 - A1)
[PROOF STEP]
have 2: "?E Int A1 \<noteq> ?E Int A2"
[PROOF STATE]
proof (prove)
using this:
x \<in> A1 - A2 \<union> (A2 - A1)

goal (1 subgoal):
 1. insert x D \<inter> A1 \<noteq> insert x D \<inter> A2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x D \<inter> A1 \<noteq> insert x D \<inter> A2

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
have 3: "inter D \<circ> inter ?E = inter D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<inter>) D \<circ> (\<inter>) (insert x D) = (\<inter>) D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<inter>) D \<circ> (\<inter>) (insert x D) = (\<inter>) D

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
have 4: "~ inj_on (inter D) (inter ?E ` F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> inj_on ((\<inter>) D) ((\<inter>) (insert x D) ` F)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>xa\<in>(\<inter>) (insert x D) ` F. \<forall>y\<in>(\<inter>) (insert x D) ` F. D \<inter> xa = D \<inter> y \<longrightarrow> xa = y)
[PROOF STEP]
using 1 2 \<open>A1 \<in> F\<close> \<open>A2 \<in> F\<close>
[PROOF STATE]
proof (prove)
using this:
D \<inter> (insert x D \<inter> A1) = D \<inter> (insert x D \<inter> A2)
insert x D \<inter> A1 \<noteq> insert x D \<inter> A2
A1 \<in> F
A2 \<in> F

goal (1 subgoal):
 1. \<not> (\<forall>xa\<in>(\<inter>) (insert x D) ` F. \<forall>y\<in>(\<inter>) (insert x D) ` F. D \<inter> xa = D \<inter> y \<longrightarrow> xa = y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> inj_on ((\<inter>) D) ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
from D
[PROOF STATE]
proof (chain)
picking this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
have "Suc m \<le> card (inter D ` F)"
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. Suc m \<le> card ((\<inter>) D ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc m \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc m \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
have "... < card (inter ?E ` F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<inter>) D ` F) < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
by (rule card_less_if_surj_not_inj[of _ "inter D"])
              (auto simp add: image_image 3 4 \<open>finite F\<close>)
[PROOF STATE]
proof (state)
this:
card ((\<inter>) D ` F) < card ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc m < card ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Suc m < card ((\<inter>) (insert x D) ` F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc m < card ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (insert x D) \<le> Suc m
insert x D \<subseteq> X
Suc m < card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
have "?E\<subseteq>X \<and> card ?E \<le> Suc m \<and> Suc m + 1 \<le> card (inter ?E ` F)"
[PROOF STATE]
proof (prove)
using this:
card (insert x D) \<le> Suc m
insert x D \<subseteq> X
Suc m < card ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. insert x D \<subseteq> X \<and> card (insert x D) \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) (insert x D) ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x D \<subseteq> X \<and> card (insert x D) \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<noteq> card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
thus "\<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card (inter D ` F)"
[PROOF STATE]
proof (prove)
using this:
insert x D \<subseteq> X \<and> card (insert x D) \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) (insert x D) ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>D\<subseteq>X. card D \<le> Suc m \<and> Suc m + 1 \<le> card ((\<inter>) D ` F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> m \<and> m + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?m2 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> ?m2 \<and> ?m2 + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?m2 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> ?m2 \<and> ?m2 + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
1 \<le> card X
card F = card X
[PROOF STEP]
have "card X - 1 < card F"
[PROOF STATE]
proof (prove)
using this:
1 \<le> card X
card F = card X

goal (1 subgoal):
 1. card X - 1 < card F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card X - 1 < card F

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?m2 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> ?m2 \<and> ?m2 + 1 \<le> card ((\<inter>) D ` F)
card X - 1 < card F
[PROOF STEP]
obtain D where
    "D \<subseteq> X & card D \<le> card X - 1 & card (inter D ` F) \<ge> (card X - 1) + 1"
[PROOF STATE]
proof (prove)
using this:
?m2 < card F \<Longrightarrow> \<exists>D\<subseteq>X. card D \<le> ?m2 \<and> ?m2 + 1 \<le> card ((\<inter>) D ` F)
card X - 1 < card F

goal (1 subgoal):
 1. (\<And>D. D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
with \<open>finite F\<close>
[PROOF STATE]
proof (chain)
picking this:
finite F
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)
[PROOF STEP]
have "card (inter D ` F) \<le> card F"
[PROOF STATE]
proof (prove)
using this:
finite F
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)

goal (1 subgoal):
 1. card ((\<inter>) D ` F) \<le> card F
[PROOF STEP]
by (elim card_image_le)
[PROOF STATE]
proof (state)
this:
card ((\<inter>) D ` F) \<le> card F

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)
card ((\<inter>) D ` F) \<le> card F
[PROOF STEP]
have "D \<subseteq> X & card D < card X & card (inter D ` F) = card F"
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)
card ((\<inter>) D ` F) \<le> card F

goal (1 subgoal):
 1. D \<subseteq> X \<and> card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
using \<open>card F = card X\<close>
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D \<le> card X - 1 \<and> card X - 1 + 1 \<le> card ((\<inter>) D ` F)
card ((\<inter>) D ` F) \<le> card F
card F = card X

goal (1 subgoal):
 1. D \<subseteq> X \<and> card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<subseteq> X \<and> card D < card X \<and> card ((\<inter>) D ` F) = card F

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> X \<and> card D < card X \<and> card ((\<inter>) D ` F) = card F

goal (1 subgoal):
 1. \<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>D\<subseteq>X. card D < card X \<and> card ((\<inter>) D ` F) = card F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neq_Leaf_if_l_gt0: "0 < l t \<Longrightarrow> t \<noteq> Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < l t \<Longrightarrow> t \<noteq> Leaf
[PROOF STEP]
by auto


[STATEMENT]
lemma combine_non_Leaves: "\<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> combine t u = Node (l t) (r u) (val t + val u) (discharge t) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> combine t u = Node (l t) (r u) (val t + val u) (discharge t) u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> combine t u = Node (l t) (r u) (val t + val u) (discharge t) u
[PROOF STEP]
assume assms: "t \<noteq> Leaf" "u \<noteq> Leaf"
[PROOF STATE]
proof (state)
this:
t \<noteq> Leaf
u \<noteq> Leaf

goal (1 subgoal):
 1. \<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> combine t u = Node (l t) (r u) (val t + val u) (discharge t) u
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> Leaf
u \<noteq> Leaf
[PROOF STEP]
have "combine t u = Node (l (Node (l t) (r t) (val t) (lchild t) (rchild t))) (r (Node (l u) (r u) (val u) (lchild u) (rchild u))) (val (Node (l t) (r t) (val t) (lchild t) (rchild t)) + val (Node (l u) (r u) (val u) (lchild u) (rchild u))) (discharge (Node (l t) (r t) (val t) (lchild t) (rchild t))) (Node (l u) (r u) (val u) (lchild u) (rchild u))"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> Leaf
u \<noteq> Leaf

goal (1 subgoal):
 1. combine t u = Node (l (Node (l t) (r t) (val t) (lchild t) (rchild t))) (r (Node (l u) (r u) (val u) (lchild u) (rchild u))) (val (Node (l t) (r t) (val t) (lchild t) (rchild t)) + val (Node (l u) (r u) (val u) (lchild u) (rchild u))) (discharge (Node (l t) (r t) (val t) (lchild t) (rchild t))) (Node (l u) (r u) (val u) (lchild u) (rchild u))
[PROOF STEP]
by (metis (no_types) combine.simps(3) tree.exhaust_sel)
[PROOF STATE]
proof (state)
this:
combine t u = Node (l (Node (l t) (r t) (val t) (lchild t) (rchild t))) (r (Node (l u) (r u) (val u) (lchild u) (rchild u))) (val (Node (l t) (r t) (val t) (lchild t) (rchild t)) + val (Node (l u) (r u) (val u) (lchild u) (rchild u))) (discharge (Node (l t) (r t) (val t) (lchild t) (rchild t))) (Node (l u) (r u) (val u) (lchild u) (rchild u))

goal (1 subgoal):
 1. \<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> combine t u = Node (l t) (r u) (val t + val u) (discharge t) u
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> Leaf
u \<noteq> Leaf
combine t u = Node (l (Node (l t) (r t) (val t) (lchild t) (rchild t))) (r (Node (l u) (r u) (val u) (lchild u) (rchild u))) (val (Node (l t) (r t) (val t) (lchild t) (rchild t)) + val (Node (l u) (r u) (val u) (lchild u) (rchild u))) (discharge (Node (l t) (r t) (val t) (lchild t) (rchild t))) (Node (l u) (r u) (val u) (lchild u) (rchild u))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<noteq> Leaf
u \<noteq> Leaf
combine t u = Node (l (Node (l t) (r t) (val t) (lchild t) (rchild t))) (r (Node (l u) (r u) (val u) (lchild u) (rchild u))) (val (Node (l t) (r t) (val t) (lchild t) (rchild t)) + val (Node (l u) (r u) (val u) (lchild u) (rchild u))) (discharge (Node (l t) (r t) (val t) (lchild t) (rchild t))) (Node (l u) (r u) (val u) (lchild u) (rchild u))

goal (1 subgoal):
 1. combine t u = Node (l t) (r u) (val t + val u) (discharge t) u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
combine t u = Node (l t) (r u) (val t + val u) (discharge t) u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_combine_non_Leaves: "\<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> r (combine t u) = r u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<noteq> Leaf; u \<noteq> Leaf\<rbrakk> \<Longrightarrow> r (combine t u) = r u
[PROOF STEP]
by (simp add: combine_non_Leaves)


[STATEMENT]
lemma reusables_Leaf[simp]: "0 < fst w \<Longrightarrow> reusables Leaf w = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < fst w \<Longrightarrow> reusables Leaf w = []
[PROOF STEP]
by (simp add: reusables.simps)


[STATEMENT]
lemma l_lchild_eq_l_if_well_shaped[simp]:
  "\<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> l (lchild t) = l t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> l (lchild t) = l t
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma r_rchild_eq_r_if_well_shaped[simp]:
  "\<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> r (rchild t) = r t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> r (rchild t) = r t
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma r_lchild_eq_l_rchild_if_well_shaped:
  "\<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> r (lchild t) = l (rchild t) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> r (lchild t) = l (rchild t) - 1
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma r_lchild_le_r: "well_shaped t \<Longrightarrow> r (lchild t) \<le> r t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped t \<Longrightarrow> r (lchild t) \<le> r t
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. well_shaped Leaf \<Longrightarrow> r (lchild Leaf) \<le> r Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>well_shaped t1 \<Longrightarrow> r (lchild t1) \<le> r t1; well_shaped t2 \<Longrightarrow> r (lchild t2) \<le> r t2; well_shaped (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> r (lchild (Node x1 x2 x3 t1 t2)) \<le> r (Node x1 x2 x3 t1 t2)
[PROOF STEP]
case (Node i j a t1 t2)
[PROOF STATE]
proof (state)
this:
well_shaped t1 \<Longrightarrow> r (lchild t1) \<le> r t1
well_shaped t2 \<Longrightarrow> r (lchild t2) \<le> r t2
well_shaped (Node i j a t1 t2)

goal (2 subgoals):
 1. well_shaped Leaf \<Longrightarrow> r (lchild Leaf) \<le> r Leaf
 2. \<And>x1 x2 x3 t1 t2. \<lbrakk>well_shaped t1 \<Longrightarrow> r (lchild t1) \<le> r t1; well_shaped t2 \<Longrightarrow> r (lchild t2) \<le> r t2; well_shaped (Node x1 x2 x3 t1 t2)\<rbrakk> \<Longrightarrow> r (lchild (Node x1 x2 x3 t1 t2)) \<le> r (Node x1 x2 x3 t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_shaped t1 \<Longrightarrow> r (lchild t1) \<le> r t1
well_shaped t2 \<Longrightarrow> r (lchild t2) \<le> r t2
well_shaped (Node i j a t1 t2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_shaped t1 \<Longrightarrow> r (lchild t1) \<le> r t1
well_shaped t2 \<Longrightarrow> r (lchild t2) \<le> r t2
well_shaped (Node i j a t1 t2)

goal (1 subgoal):
 1. r (lchild (Node i j a t1 t2)) \<le> r (Node i j a t1 t2)
[PROOF STEP]
by auto
      (metis Suc_eq_plus1_left order.trans le_add2 tree.exhaust_sel well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
r (lchild (Node i j a t1 t2)) \<le> r (Node i j a t1 t2)

goal (1 subgoal):
 1. well_shaped Leaf \<Longrightarrow> r (lchild Leaf) \<le> r Leaf
[PROOF STEP]
qed simp


[STATEMENT]
lemma well_shaped_lchild[simp]: "well_shaped t \<Longrightarrow> well_shaped (lchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped t \<Longrightarrow> well_shaped (lchild t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma well_shaped_rchild[simp]: "well_shaped t \<Longrightarrow> well_shaped (rchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped t \<Longrightarrow> well_shaped (rchild t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma adjacent_Nil[simp]: "adjacent w []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent w []
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Leaf \<notin> set [] \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast []) (tl []) \<and> ([] = [] \<or> l (last []) = fst w \<and> r (hd []) = snd w)
[PROOF STEP]
by simp


[STATEMENT]
lemma adjacent_Cons: "adjacent w (t # ts) =
  (t \<noteq> Leaf \<and> r t = snd w \<and> (case ts of [] \<Rightarrow> l t = fst w
     | u # us \<Rightarrow> adjacent (fst w, r u) ts \<and> l t = Suc (r u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent w (t # ts) = (t \<noteq> Leaf \<and> r t = snd w \<and> (case ts of [] \<Rightarrow> l t = fst w | u # us \<Rightarrow> adjacent (fst w, r u) ts \<and> l t = Suc (r u)))
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Leaf \<notin> set (t # ts) \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast (t # ts)) (tl (t # ts)) \<and> (t # ts = [] \<or> l (last (t # ts)) = fst w \<and> r (hd (t # ts)) = snd w)) = (t \<noteq> Leaf \<and> r t = snd w \<and> (case ts of [] \<Rightarrow> l t = fst w | u # us \<Rightarrow> (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst (fst w, r u) \<and> r (hd ts) = snd (fst w, r u))) \<and> l t = Suc (r u)))
[PROOF STEP]
by (auto split: list.splits)


[STATEMENT]
lemma adjacent_ConsI: "\<lbrakk>t \<noteq> Leaf; r t = snd w;
  (case ts of [] \<Rightarrow> l t = fst w
     | u # us \<Rightarrow> adjacent (fst w, r u) ts \<and> l t = Suc (r u))\<rbrakk> \<Longrightarrow>
  adjacent w (t # ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<noteq> Leaf; r t = snd w; case ts of [] \<Rightarrow> l t = fst w | u # us \<Rightarrow> adjacent (fst w, r u) ts \<and> l t = Suc (r u)\<rbrakk> \<Longrightarrow> adjacent w (t # ts)
[PROOF STEP]
by (simp add: adjacent_Cons)


[STATEMENT]
lemma append_Cons_eq_append_append: "xs @ y # ys = xs @ [y] @ ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @ y # ys = xs @ [y] @ ys
[PROOF STEP]
by simp


[STATEMENT]
lemma list_all2_append_singletonI: "\<lbrakk>list_all2 P xs ys; P x y\<rbrakk> \<Longrightarrow> list_all2 P (xs @ [x]) (ys @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 P xs ys; P x y\<rbrakk> \<Longrightarrow> list_all2 P (xs @ [x]) (ys @ [y])
[PROOF STEP]
by (simp add: list_all2_appendI)


[STATEMENT]
lemma list_all2_Cons_append_singletonI: "\<lbrakk>xs \<noteq> []; list_all2 P (x # butlast xs) ys; P (last xs) y\<rbrakk> \<Longrightarrow> list_all2 P (x # xs) (ys @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; list_all2 P (x # butlast xs) ys; P (last xs) y\<rbrakk> \<Longrightarrow> list_all2 P (x # xs) (ys @ [y])
[PROOF STEP]
using list_all2_append_singletonI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>list_all2 ?P ?xs ?ys; ?P ?x ?y\<rbrakk> \<Longrightarrow> list_all2 ?P (?xs @ [?x]) (?ys @ [?y])

goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; list_all2 P (x # butlast xs) ys; P (last xs) y\<rbrakk> \<Longrightarrow> list_all2 P (x # xs) (ys @ [y])
[PROOF STEP]
by fastforce


[STATEMENT]
lemma adjacent_appendI: "\<lbrakk>0 < fst w; fst w \<le> snd w;
  (case us of [] \<Rightarrow> adjacent w ts
    | u # us' \<Rightarrow> adjacent (Suc (r u), snd w) ts \<and> adjacent (fst w, (case ts of [] \<Rightarrow> snd w | ts \<Rightarrow> r u)) (u # us'))\<rbrakk> \<Longrightarrow>
  adjacent w (ts @ us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; fst w \<le> snd w; case us of [] \<Rightarrow> adjacent w ts | u # us' \<Rightarrow> adjacent (Suc (r u), snd w) ts \<and> adjacent (fst w, case ts of [] \<Rightarrow> snd w | a # list \<Rightarrow> r u) (u # us')\<rbrakk> \<Longrightarrow> adjacent w (ts @ us)
[PROOF STEP]
unfolding adjacent_def butlast_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; fst w \<le> snd w; case us of [] \<Rightarrow> Leaf \<notin> set ts \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst w \<and> r (hd ts) = snd w) | u # us' \<Rightarrow> (Leaf \<notin> set ts \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast ts) (tl ts) \<and> (ts = [] \<or> l (last ts) = fst (Suc (r u), snd w) \<and> r (hd ts) = snd (Suc (r u), snd w))) \<and> Leaf \<notin> set (u # us') \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast (u # us')) (tl (u # us')) \<and> (u # us' = [] \<or> l (last (u # us')) = fst (fst w, case ts of [] \<Rightarrow> snd w | a # list \<Rightarrow> r u) \<and> r (hd (u # us')) = snd (fst w, case ts of [] \<Rightarrow> snd w | a # list \<Rightarrow> r u))\<rbrakk> \<Longrightarrow> Leaf \<notin> set (ts @ us) \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (if us = [] then butlast ts else ts @ butlast us) (tl (ts @ us)) \<and> (ts @ us = [] \<or> l (last (ts @ us)) = fst w \<and> r (hd (ts @ us)) = snd w)
[PROOF STEP]
by (auto simp: intro: list_all2_Cons_append_singletonI
    list_all2_appendI[OF list_all2_Cons_append_singletonI, simplified] split: list.splits if_splits)


[STATEMENT]
lemma adjacent_Cons_implies_adjacent: "adjacent (a, b) (t # ts) \<Longrightarrow> adjacent (a, l t - Suc 0) ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent (a, b) (t # ts) \<Longrightarrow> adjacent (a, l t - Suc 0) ts
[PROOF STEP]
by (cases ts) (simp_all add: adjacent_def)


[STATEMENT]
lemma (in semigroup_add) fold_add_add: "fold (+) xs (x + y) = fold (+) xs x + y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (+) xs (x + y) = fold (+) xs x + y
[PROOF STEP]
by (induct xs arbitrary: x) (auto simp: add_assoc[symmetric])


[STATEMENT]
lemma valid_Leaf: "valid Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.valid Leaf
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped Leaf \<and> local.well_valued0 Leaf \<and> (Leaf \<noteq> Leaf \<longrightarrow> val Leaf \<noteq> None)
[PROOF STEP]
by auto


[STATEMENT]
lemma add_sum:
  assumes "i > 0" "j \<ge> i" "k > j"
  shows "sum i j + sum (Suc j) k = sum i k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sum i j + local.sum (Suc j) k = local.sum i k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.sum i j + local.sum (Suc j) k = local.sum i k
[PROOF STEP]
have *: "[i - 1 ..< k - 1] = [i - 1..< j] @ [j..< k - 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i - 1..<k - 1] = [i - 1..<j] @ [j..<k - 1]
[PROOF STEP]
using assms upt_add_eq_append[of "i - 1" "j - 1" "k - j"]
[PROOF STATE]
proof (prove)
using this:
0 < i
i \<le> j
j < k
i - 1 \<le> j - 1 \<Longrightarrow> [i - 1..<j - 1 + (k - j)] = [i - 1..<j - 1] @ [j - 1..<j - 1 + (k - j)]

goal (1 subgoal):
 1. [i - 1..<k - 1] = [i - 1..<j] @ [j..<k - 1]
[PROOF STEP]
by (cases j) (auto simp: upt_conv_Cons)
[PROOF STATE]
proof (state)
this:
[i - 1..<k - 1] = [i - 1..<j] @ [j..<k - 1]

goal (1 subgoal):
 1. local.sum i j + local.sum (Suc j) k = local.sum i k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[i - 1..<k - 1] = [i - 1..<j] @ [j..<k - 1]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[i - 1..<k - 1] = [i - 1..<j] @ [j..<k - 1]

goal (1 subgoal):
 1. local.sum i j + local.sum (Suc j) k = local.sum i k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[i - 1..<k - 1] = [i - 1..<j] @ [j..<k - 1]
0 < i
i \<le> j
j < k

goal (1 subgoal):
 1. local.sum i j + local.sum (Suc j) k = local.sum i k
[PROOF STEP]
by (cases j) (auto simp: fold_add_add)
[PROOF STATE]
proof (state)
this:
local.sum i j + local.sum (Suc j) k = local.sum i k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma well_valued0_rchild_if_well_valued0[simp]: "well_valued0 t \<Longrightarrow> well_valued0 (rchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.well_valued0 t \<Longrightarrow> local.well_valued0 (rchild t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma well_valued0_lchild_if_well_valued0[simp]: "well_valued0 t \<Longrightarrow> well_valued0 (lchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.well_valued0 t \<Longrightarrow> local.well_valued0 (lchild t)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma valid_rchild_if_valid: "valid t \<Longrightarrow> valid (rchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.valid t \<Longrightarrow> local.valid (rchild t)
[PROOF STEP]
by (metis tree.exhaust_sel tree.sel(9) valid_def well_shaped_rchild well_valued0.simps(2))


[STATEMENT]
lemma val_eq_Some_sum_if_valid_neq_Leaf: "\<lbrakk>valid t; t \<noteq> Leaf\<rbrakk> \<Longrightarrow> val t = Some (sum (l t) (r t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.valid t; t \<noteq> Leaf\<rbrakk> \<Longrightarrow> val t = Some (local.sum (l t) (r t))
[PROOF STEP]
by (auto simp: valid_def foldr_conv_fold)
    (metis One_nat_def option.distinct(1) option.inject tree.exhaust_sel well_valued0.simps(2))


[STATEMENT]
lemma adjacent_atomics: "adjacent (i, j) (atomics i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent (i, j) (local.atomics i j)
[PROOF STEP]
unfolding adjacent_def atomics_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Leaf \<notin> set (map local.atomic (rev [i..<Suc j])) \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast (map local.atomic (rev [i..<Suc j]))) (tl (map local.atomic (rev [i..<Suc j]))) \<and> (map local.atomic (rev [i..<Suc j]) = [] \<or> l (last (map local.atomic (rev [i..<Suc j]))) = fst (i, j) \<and> r (hd (map local.atomic (rev [i..<Suc j]))) = snd (i, j))
[PROOF STEP]
by (auto 0 1 simp: last_map last_rev nth_tl
    map_butlast[symmetric] list_all2_conv_all_nth nth_Cons' rev_nth nth_append)


[STATEMENT]
lemma valid_atomics: "\<lbrakk>t \<in> set (atomics i j); 0 < i; j \<le> length as\<rbrakk> \<Longrightarrow> valid t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (local.atomics i j); 0 < i; j \<le> length as\<rbrakk> \<Longrightarrow> local.valid t
[PROOF STEP]
unfolding atomics_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set (map local.atomic (rev [i..<Suc j])); 0 < i; j \<le> length as\<rbrakk> \<Longrightarrow> local.valid t
[PROOF STEP]
by (auto simp: valid_def)


[STATEMENT]
lemma reusables_neq_Nil_if_well_shaped_and_overlapping:
  "\<lbrakk>well_shaped t; l t \<le> fst w; r t \<le> snd w; fst w \<le> r t\<rbrakk> \<Longrightarrow> reusables t w \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; l t \<le> fst w; r t \<le> snd w; fst w \<le> r t\<rbrakk> \<Longrightarrow> reusables t w \<noteq> []
[PROOF STEP]
by (induction t w rule: reusables.induct) (simp add: reusables.simps Let_def)


[STATEMENT]
lemma reusables_lchild_neq_Nil_under_some_conditions:
  "\<lbrakk>well_shaped t; l t \<le> fst w; r t \<le> snd w; fst w \<noteq> l t; r t \<ge> fst w; l (rchild t) > fst w\<rbrakk> \<Longrightarrow>
    reusables (lchild t) w \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; l t \<le> fst w; r t \<le> snd w; fst w \<noteq> l t; fst w \<le> r t; fst w < l (rchild t)\<rbrakk> \<Longrightarrow> reusables (lchild t) w \<noteq> []
[PROOF STEP]
using r_lchild_eq_l_rchild_if_well_shaped[of "t"] r_lchild_le_r[of t]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_shaped t; l t < r t\<rbrakk> \<Longrightarrow> r (lchild t) = l (rchild t) - 1
well_shaped t \<Longrightarrow> r (lchild t) \<le> r t

goal (1 subgoal):
 1. \<lbrakk>well_shaped t; l t \<le> fst w; r t \<le> snd w; fst w \<noteq> l t; fst w \<le> r t; fst w < l (rchild t)\<rbrakk> \<Longrightarrow> reusables (lchild t) w \<noteq> []
[PROOF STEP]
by (intro reusables_neq_Nil_if_well_shaped_and_overlapping) auto


[STATEMENT]
lemma adjacent_reusables: "\<lbrakk>0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow>
  adjacent (fst w, r t) (reusables t w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
proof (induction t w rule: reusables.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t w. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
case (1 t w)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w

goal (1 subgoal):
 1. \<And>t w. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
proof (cases "fst w > r t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r t < fst w \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
 2. \<not> r t < fst w \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> r t < fst w

goal (2 subgoals):
 1. r t < fst w \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
 2. \<not> r t < fst w \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
\<not> r t < fst w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
\<not> r t < fst w

goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
proof (cases "fst w = l t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
 2. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w; \<not> r t < fst w; fst w \<noteq> l t\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst w \<noteq> l t

goal (2 subgoals):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
 2. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w; \<not> r t < fst w; fst w \<noteq> l t\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst w \<noteq> l t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst w \<noteq> l t

goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
proof (cases "fst w \<ge> l (rchild t)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>fst w \<noteq> l t; l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
 2. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l (rchild t) \<le> fst w

goal (2 subgoals):
 1. \<lbrakk>fst w \<noteq> l t; l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
 2. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
l (rchild t) \<le> fst w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
l (rchild t) \<le> fst w

goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
by (subst reusables.simps) auto
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r t) (reusables t w)

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> l (rchild t) \<le> fst w

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
[PROOF STEP]
obtain x xs where *: "reusables (lchild t) w = x # xs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w

goal (1 subgoal):
 1. (\<And>x xs. reusables (lchild t) w = x # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "reusables (lchild t) w") (auto simp: reusables_lchild_neq_Nil_under_some_conditions)
[PROOF STATE]
proof (state)
this:
reusables (lchild t) w = x # xs

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
with 1(2-6) \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close> \<open>\<not> l (rchild t) \<le> fst w\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
reusables (lchild t) w = x # xs
[PROOF STEP]
have "adjacent (fst w, r (lchild t)) (x # xs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
reusables (lchild t) w = x # xs

goal (1 subgoal):
 1. adjacent (fst w, r (lchild t)) (x # xs)
[PROOF STEP]
by (simp add: adjacent_Cons r_lchild_le_r dual_order.trans)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r (lchild t)) (x # xs)

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close> *
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
reusables (lchild t) w = x # xs
adjacent (fst w, r (lchild t)) (x # xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; well_shaped ?xa; l ?xa \<le> fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?xa) (reusables ?xa w)
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; well_shaped ?x; l ?x \<le> fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r ?x) (reusables ?x w)
0 < fst w
well_shaped t
l t \<le> fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
reusables (lchild t) w = x # xs
adjacent (fst w, r (lchild t)) (x # xs)

goal (1 subgoal):
 1. adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
by (subst reusables.simps)
            (auto simp add: Let_def adjacent_Cons r_lchild_eq_l_rchild_if_well_shaped)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r t) (reusables t w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r t) (reusables t w)

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; well_shaped xa; l xa \<le> fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r xa) (reusables xa w); \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; well_shaped x; l x \<le> fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> adjacent (fst w, r x) (reusables x w); 0 < fst w; well_shaped t; l t \<le> fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
qed (auto simp: reusables.simps intro!: adjacent_singleton)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r t) (reusables t w)

goal (1 subgoal):
 1. r t < fst w \<Longrightarrow> adjacent (fst w, r t) (reusables t w)
[PROOF STEP]
qed (auto simp: reusables.simps)
[PROOF STATE]
proof (state)
this:
adjacent (fst w, r t) (reusables t w)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_rchild_if_well_valued0: "\<lbrakk>well_shaped t; well_valued0 t\<rbrakk> \<Longrightarrow> valid (rchild t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_shaped t; local.well_valued0 t\<rbrakk> \<Longrightarrow> local.valid (rchild t)
[PROOF STEP]
by (metis tree.exhaust_sel tree.sel(9) valid_def well_shaped_rchild well_valued0.simps(2))


[STATEMENT]
lemma valid_reusables_under_some_conditions:
  "\<lbrakk>0 < fst w; well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow>
    \<forall>t' \<in> set (reusables t w). valid t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
proof (induction t w rule: reusables.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t w. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case (1 t w)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w

goal (1 subgoal):
 1. \<And>t w. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
proof (cases "fst w > r t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<not> r t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> r t < fst w

goal (2 subgoals):
 1. r t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<not> r t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
\<not> r t < fst w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
\<not> r t < fst w

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
proof (cases "fst w = l t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w \<noteq> l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w \<noteq> l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst w \<noteq> l t

goal (2 subgoals):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w \<noteq> l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst w \<noteq> l t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst w \<noteq> l t

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
proof (cases "fst w \<ge> l (rchild t)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>fst w \<noteq> l t; l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l (rchild t) \<le> fst w

goal (2 subgoals):
 1. \<lbrakk>fst w \<noteq> l t; l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
l (rchild t) \<le> fst w
[PROOF STEP]
have *: "Ball (set (reusables (rchild t) w)) valid"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
l (rchild t) \<le> fst w

goal (1 subgoal):
 1. Ball (set (reusables (rchild t) w)) local.valid
[PROOF STEP]
by (metis (no_types, lifting) ball_empty dual_order.strict_trans2 leI le_neq_implies_less list.set(1) r_rchild_eq_r_if_well_shaped reusables.simps set_ConsD valid_rchild_if_well_valued0 well_shaped_rchild well_valued0_rchild_if_well_valued0)
[PROOF STATE]
proof (state)
this:
Ball (set (reusables (rchild t) w)) local.valid

goal (2 subgoals):
 1. \<lbrakk>fst w \<noteq> l t; l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
from 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close> True
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
l (rchild t) \<le> fst w
[PROOF STEP]
have "reusables t w = reusables (rchild t) w"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
l (rchild t) \<le> fst w

goal (1 subgoal):
 1. reusables t w = reusables (rchild t) w
[PROOF STEP]
by (subst reusables.simps)
            simp
[PROOF STATE]
proof (state)
this:
reusables t w = reusables (rchild t) w

goal (2 subgoals):
 1. \<lbrakk>fst w \<noteq> l t; l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1 *
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
Ball (set (reusables (rchild t) w)) local.valid
reusables t w = reusables (rchild t) w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
Ball (set (reusables (rchild t) w)) local.valid
reusables t w = reusables (rchild t) w

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> l (rchild t) \<le> fst w

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
[PROOF STEP]
have *: "Ball (set (reusables (lchild t) w)) valid"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w

goal (1 subgoal):
 1. Ball (set (reusables (lchild t) w)) local.valid
[PROOF STEP]
by (metis dual_order.strict_trans2 l_lchild_eq_l_if_well_shaped leI order_trans r_lchild_le_r well_shaped_lchild well_valued0_lchild_if_well_valued0)
[PROOF STATE]
proof (state)
this:
Ball (set (reusables (lchild t) w)) local.valid

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
Ball (set (reusables (lchild t) w)) local.valid
[PROOF STEP]
have valid_rchild: "valid (rchild t)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
Ball (set (reusables (lchild t) w)) local.valid

goal (1 subgoal):
 1. local.valid (rchild t)
[PROOF STEP]
by (simp add: valid_rchild_if_well_valued0)
[PROOF STATE]
proof (state)
this:
local.valid (rchild t)

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close> False
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
local.valid (rchild t)
[PROOF STEP]
have "reusables t w = rchild t # reusables (lchild t) w"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
local.valid (rchild t)

goal (1 subgoal):
 1. reusables t w = rchild t # reusables (lchild t) w
[PROOF STEP]
by (subst reusables.simps) presburger
[PROOF STATE]
proof (state)
this:
reusables t w = rchild t # reusables (lchild t) w

goal (1 subgoal):
 1. \<lbrakk>fst w \<noteq> l t; \<not> l (rchild t) \<le> fst w\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with 1 \<open>fst w \<noteq> l t\<close> \<open>\<not> fst w > r t\<close> False * valid_rchild
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
Ball (set (reusables (lchild t) w)) local.valid
local.valid (rchild t)
reusables t w = rchild t # reusables (lchild t) w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?xa; well_shaped ?xa; l ?xa < fst w; r ?xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?xa w)) local.valid
\<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; ?x = lchild t; ?xa = rchild t; \<not> l ?xa \<le> fst w; 0 < fst w; local.well_valued0 ?x; well_shaped ?x; l ?x < fst w; r ?x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?x w)) local.valid
0 < fst w
local.well_valued0 t
well_shaped t
l t < fst w
r t \<le> snd w
fst w \<noteq> l t
\<not> r t < fst w
\<not> l (rchild t) \<le> fst w
Ball (set (reusables (lchild t) w)) local.valid
local.valid (rchild t)
reusables t w = rchild t # reusables (lchild t) w

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
by (metis set_ConsD)
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; l xa \<le> fst w; 0 < fst w; local.well_valued0 xa; well_shaped xa; l xa < fst w; r xa \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables xa w)) local.valid; \<And>x xa. \<lbrakk>\<not> r t < fst w; fst w \<noteq> l t; x = lchild t; xa = rchild t; \<not> l xa \<le> fst w; 0 < fst w; local.well_valued0 x; well_shaped x; l x < fst w; r x \<le> snd w\<rbrakk> \<Longrightarrow> Ball (set (reusables x w)) local.valid; 0 < fst w; local.well_valued0 t; well_shaped t; l t < fst w; r t \<le> snd w; \<not> r t < fst w; fst w = l t\<rbrakk> \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
qed (auto simp: reusables.simps)
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal (1 subgoal):
 1. r t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
qed (auto simp: reusables.simps)
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_reusables:
  assumes "0 < fst w" "valid t" "l t \<le> fst w" "r t \<le> snd w"
  shows "\<forall>t' \<in> set (reusables t w). valid t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
proof (cases "l t < fst w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<not> l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l t < fst w

goal (2 subgoals):
 1. l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
 2. \<not> l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
local.valid t
l t \<le> fst w
r t \<le> snd w
l t < fst w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < fst w
local.valid t
l t \<le> fst w
r t \<le> snd w
l t < fst w

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
using valid_def valid_reusables_under_some_conditions
[PROOF STATE]
proof (prove)
using this:
0 < fst w
local.valid t
l t \<le> fst w
r t \<le> snd w
l t < fst w
local.valid ?t = (well_shaped ?t \<and> local.well_valued0 ?t \<and> (?t \<noteq> Leaf \<longrightarrow> val ?t \<noteq> None))
\<lbrakk>0 < fst ?w; local.well_valued0 ?t; well_shaped ?t; l ?t < fst ?w; r ?t \<le> snd ?w\<rbrakk> \<Longrightarrow> Ball (set (reusables ?t ?w)) local.valid

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal (1 subgoal):
 1. \<not> l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> l t < fst w

goal (1 subgoal):
 1. \<not> l t < fst w \<Longrightarrow> Ball (set (reusables t w)) local.valid
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < fst w
local.valid t
l t \<le> fst w
r t \<le> snd w
\<not> l t < fst w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < fst w
local.valid t
l t \<le> fst w
r t \<le> snd w
\<not> l t < fst w

goal (1 subgoal):
 1. Ball (set (reusables t w)) local.valid
[PROOF STEP]
by (simp add: reusables.simps)
[PROOF STATE]
proof (state)
this:
Ball (set (reusables t w)) local.valid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma combine_valid_Nodes_aux:
  assumes prems: "0 < l a" "a \<noteq> Leaf" "z \<noteq> Leaf" "l z = Suc (r a)" "well_shaped a" "well_shaped z"
    "well_valued0 a" "val a = Some va" "well_valued0 z" "val z = Some vz"
  shows "va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz
[PROOF STEP]
have "l a > 0"
[PROOF STATE]
proof (prove)
using this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz

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

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < l a

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz
[PROOF STEP]
have "r a \<ge> l a"
[PROOF STATE]
proof (prove)
using this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz

goal (1 subgoal):
 1. l a \<le> r a
[PROOF STEP]
by (metis tree.collapse well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
l a \<le> r a

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l a \<le> r a

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
have "r z > r a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r a < r z
[PROOF STEP]
by (metis Suc_le_lessD prems(3) prems(4) prems(6) tree.collapse well_shaped.simps(2))
[PROOF STATE]
proof (state)
this:
r a < r z

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < l a
l a \<le> r a
r a < r z
[PROOF STEP]
have *: "sum (l a) (r a) + sum (Suc (r a)) (r z) = sum (l a) (r z)"
[PROOF STATE]
proof (prove)
using this:
0 < l a
l a \<le> r a
r a < r z

goal (1 subgoal):
 1. local.sum (l a) (r a) + local.sum (Suc (r a)) (r z) = local.sum (l a) (r z)
[PROOF STEP]
by (frule add_sum)
[PROOF STATE]
proof (state)
this:
local.sum (l a) (r a) + local.sum (Suc (r a)) (r z) = local.sum (l a) (r z)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz
[PROOF STEP]
have "va = sum (l a) (r a)"
[PROOF STATE]
proof (prove)
using this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz

goal (1 subgoal):
 1. va = local.sum (l a) (r a)
[PROOF STEP]
by (metis option.discI option.inject tree.collapse well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
va = local.sum (l a) (r a)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
va = local.sum (l a) (r a)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz
[PROOF STEP]
have "vz = sum (Suc (r a)) (r z)"
[PROOF STATE]
proof (prove)
using this:
0 < l a
a \<noteq> Leaf
z \<noteq> Leaf
l z = Suc (r a)
well_shaped a
well_shaped z
local.well_valued0 a
val a = Some va
local.well_valued0 z
val z = Some vz

goal (1 subgoal):
 1. vz = local.sum (Suc (r a)) (r z)
[PROOF STEP]
by (metis option.discI option.inject prems(2) prems(3) prems(8) prems(9) tree.collapse well_valued0.simps(2))
[PROOF STATE]
proof (state)
this:
vz = local.sum (Suc (r a)) (r z)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vz = local.sum (Suc (r a)) (r z)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
have "fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = sum (l a) (r z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = local.sum (l a) (r z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = local.sum (l a) (r z)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
va = local.sum (l a) (r a)
vz = local.sum (Suc (r a)) (r z)
fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = local.sum (l a) (r z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
va = local.sum (l a) (r a)
vz = local.sum (Suc (r a)) (r z)
fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = local.sum (l a) (r z)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
va = local.sum (l a) (r a)
vz = local.sum (Suc (r a)) (r z)
fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0)) = local.sum (l a) (r z)
local.sum (l a) (r a) + local.sum (Suc (r a)) (r z) = local.sum (l a) (r z)

goal (1 subgoal):
 1. va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))
[PROOF STEP]
by (auto simp: add_sum)
[PROOF STATE]
proof (state)
this:
va + vz = fold (+) (rev (map ((!) as) [l a - Suc 0..<r z - Suc 0])) (as ! (r z - Suc 0))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma discharge_is_Leaf[simp]: "discharge a = Leaf \<longleftrightarrow> a = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (discharge a = Leaf) = (a = Leaf)
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma well_shaped_discharge[simp]: "well_shaped a \<Longrightarrow> well_shaped (discharge a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped a \<Longrightarrow> well_shaped (discharge a)
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma well_valued0_discharge[simp]: "well_valued0 a \<Longrightarrow> well_valued0 (discharge a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.well_valued0 a \<Longrightarrow> local.well_valued0 (discharge a)
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma r_discharge[simp]: "r (discharge a) = r a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r (discharge a) = r a
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma well_shaped_lr: "well_shaped a \<Longrightarrow> l a \<le> r a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_shaped a \<Longrightarrow> l a \<le> r a
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma well_valued0_r: "well_valued0 a \<Longrightarrow> a \<noteq> Leaf \<Longrightarrow> r a \<le> length as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.well_valued0 a; a \<noteq> Leaf\<rbrakk> \<Longrightarrow> r a \<le> length as
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma valid_combine_if_valid: "\<lbrakk>0 < l a; valid a; valid z; a \<noteq> Leaf; z \<noteq> Leaf; l z = Suc (r a)\<rbrakk> \<Longrightarrow>
  valid (combine a z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l a; local.valid a; local.valid z; a \<noteq> Leaf; z \<noteq> Leaf; l z = Suc (r a)\<rbrakk> \<Longrightarrow> local.valid (combine a z)
[PROOF STEP]
by (force simp add: valid_def combine_non_Leaves combine_valid_Nodes_aux
    dest: well_shaped_lr well_valued0_r)


[STATEMENT]
lemma combine_neq_Leaf_if_both_non_Leaf: "\<lbrakk>a \<noteq> Leaf; z \<noteq> Leaf\<rbrakk> \<Longrightarrow>
  combine a z \<noteq> Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> Leaf; z \<noteq> Leaf\<rbrakk> \<Longrightarrow> combine a z \<noteq> Leaf
[PROOF STEP]
by (simp add: combine_non_Leaves)