[STATEMENT]
lemma max_all_edges_between:
  assumes "finite X" "finite Y"
  shows "card (all_edges_between X Y) \<le> card X * card Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges_between X Y) \<le> card X * card Y
[PROOF STEP]
by (metis assms card_mono finite_SigmaI all_edges_between_subset card_cartesian_product)


[STATEMENT]
lemma all_edges_between_Un1:
  "all_edges_between (X \<union> Y) Z = all_edges_between X Z \<union> all_edges_between Y Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between (X \<union> Y) Z = all_edges_between X Z \<union> all_edges_between Y Z
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_Un2:
  "all_edges_between X (Y \<union> Z) = all_edges_between X Y \<union> all_edges_between X Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X (Y \<union> Z) = all_edges_between X Y \<union> all_edges_between X Z
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma finite_all_edges_between:
  assumes "finite X" "finite Y"
  shows "finite (all_edges_between X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (all_edges_between X Y)
[PROOF STEP]
by (meson all_edges_between_subset assms finite_cartesian_product finite_subset)


[STATEMENT]
lemma all_edges_between_Union1:
  "all_edges_between (Union \<X>) Y = (\<Union>X\<in>\<X>. all_edges_between X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between (\<Union> \<X>) Y = (\<Union>X\<in>\<X>. all_edges_between X Y)
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_Union2:
  "all_edges_between X (Union \<Y>) = (\<Union>Y\<in>\<Y>. all_edges_between X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X (\<Union> \<Y>) = \<Union> (all_edges_between X ` \<Y>)
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_disjoint1:
  assumes "disjoint R"
  shows "disjoint ((\<lambda>X. all_edges_between X Y) ` R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint ((\<lambda>X. all_edges_between X Y) ` R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
disjoint R

goal (1 subgoal):
 1. disjoint ((\<lambda>X. all_edges_between X Y) ` R)
[PROOF STEP]
by (auto simp: all_edges_between_def disjoint_def)


[STATEMENT]
lemma all_edges_between_disjoint2:
  assumes "disjoint R"
  shows "disjoint ((\<lambda>Y. all_edges_between X Y) ` R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint (all_edges_between X ` R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
disjoint R

goal (1 subgoal):
 1. disjoint (all_edges_between X ` R)
[PROOF STEP]
by (auto simp: all_edges_between_def disjoint_def)


[STATEMENT]
lemma all_edges_between_disjoint_family_on2:
  assumes "disjoint R"
  shows "disjoint_family_on (\<lambda>Y. all_edges_between X Y) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_family_on (all_edges_between X) R
[PROOF STEP]
by (metis (no_types, lifting) all_edges_between_disjnt2 assms disjnt_def disjoint_family_on_def pairwiseD)


[STATEMENT]
lemma all_edges_between_mono1:
  "Y \<subseteq> Z \<Longrightarrow> all_edges_between Y X \<subseteq> all_edges_between Z X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<subseteq> Z \<Longrightarrow> all_edges_between Y X \<subseteq> all_edges_between Z X
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_mono2:
  "Y \<subseteq> Z \<Longrightarrow> all_edges_between X Y \<subseteq> all_edges_between X Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<subseteq> Z \<Longrightarrow> all_edges_between X Y \<subseteq> all_edges_between X Z
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma inj_on_mk_edge: "X \<inter> Y = {} \<Longrightarrow> inj_on mk_edge (all_edges_between X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<inter> Y = {} \<Longrightarrow> inj_on mk_edge (all_edges_between X Y)
[PROOF STEP]
by (auto simp: inj_on_def doubleton_eq_iff all_edges_between_def)


[STATEMENT]
lemma all_edges_between_subset_times: "all_edges_between X Y \<subseteq> (X \<inter> \<Union>E) \<times> (Y \<inter> \<Union>E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y \<subseteq> (X \<inter> \<Union> E) \<times> (Y \<inter> \<Union> E)
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_betw_prod_def_neighbors: "all_edges_between X Y = {(x, y) \<in> X \<times> Y . vert_adj x y }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y = {(x, y). (x, y) \<in> X \<times> Y \<and> vert_adj x y}
[PROOF STEP]
by (auto simp: vert_adj_def all_edges_between_def)


[STATEMENT]
lemma all_edges_betw_sigma_neighbor:
"all_edges_between X Y = (SIGMA x:X. neighbors_ss x Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y = (SIGMA x:X. neighbors_ss x Y)
[PROOF STEP]
by (auto simp add: all_edges_between_def neighbors_ss_def vert_adj_def)


[STATEMENT]
lemma card_all_edges_betw_neighbor:
  assumes "finite X" "finite Y"
  shows "card (all_edges_between X Y) = (\<Sum>x\<in>X. card (neighbors_ss x Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>x\<in>X. card (neighbors_ss x Y))
[PROOF STEP]
using all_edges_betw_sigma_neighbor assms
[PROOF STATE]
proof (prove)
using this:
all_edges_between ?X ?Y = (SIGMA x:?X. neighbors_ss x ?Y)
finite X
finite Y

goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>x\<in>X. card (neighbors_ss x Y))
[PROOF STEP]
by (simp add: neighbors_ss_def)


[STATEMENT]
lemma all_edges_between_swap:
  "all_edges_between X Y = (\<lambda>(x,y). (y,x)) ` (all_edges_between Y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y = (\<lambda>(x, y). (y, x)) ` all_edges_between Y X
[PROOF STEP]
unfolding all_edges_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} = (\<lambda>(x, y). (y, x)) ` {(x, y). x \<in> Y \<and> y \<in> X \<and> {x, y} \<in> E}
[PROOF STEP]
by (auto simp add: insert_commute image_iff split: prod.split)


[STATEMENT]
lemma card_all_edges_between_commute:
  "card (all_edges_between X Y) = card (all_edges_between Y X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges_between X Y) = card (all_edges_between Y X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (all_edges_between X Y) = card (all_edges_between Y X)
[PROOF STEP]
have "inj_on (\<lambda>(x, y). (y, x)) A" for A :: "(nat*nat)set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>(x, y). (y, x)) A
[PROOF STEP]
by (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(x, y). (y, x)) ?A

goal (1 subgoal):
 1. card (all_edges_between X Y) = card (all_edges_between Y X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on (\<lambda>(x, y). (y, x)) ?A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>(x, y). (y, x)) ?A

goal (1 subgoal):
 1. card (all_edges_between X Y) = card (all_edges_between Y X)
[PROOF STEP]
using all_edges_between_swap [of X Y] card_image
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>(x, y). (y, x)) ?A
all_edges_between X Y = (\<lambda>(x, y). (y, x)) ` all_edges_between Y X
inj_on ?f ?A \<Longrightarrow> card (?f ` ?A) = card ?A

goal (1 subgoal):
 1. card (all_edges_between X Y) = card (all_edges_between Y X)
[PROOF STEP]
by (metis swap_inj_on)
[PROOF STATE]
proof (state)
this:
card (all_edges_between X Y) = card (all_edges_between Y X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_edges_between_set: "mk_edge ` all_edges_between X Y = {{x, y}| x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_edge ` all_edges_between X Y = {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
unfolding all_edges_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} = {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
proof (intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
assume "e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}"
[PROOF STATE]
proof (state)
this:
e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}

goal (2 subgoals):
 1. \<And>x. x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
obtain x y where "e = mk_edge (x, y)" and "x \<in> X" and "y \<in> Y" and "{x, y} \<in> E"
[PROOF STATE]
proof (prove)
using this:
e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>e = mk_edge (x, y); x \<in> X; y \<in> Y; {x, y} \<in> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e = mk_edge (x, y)
x \<in> X
y \<in> Y
{x, y} \<in> E

goal (2 subgoals):
 1. \<And>x. x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = mk_edge (x, y)
x \<in> X
y \<in> Y
{x, y} \<in> E
[PROOF STEP]
show "e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}"
[PROOF STATE]
proof (prove)
using this:
e = mk_edge (x, y)
x \<in> X
y \<in> Y
{x, y} \<in> E

goal (1 subgoal):
 1. e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}

goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
assume "e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}"
[PROOF STATE]
proof (state)
this:
e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}

goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
obtain x y where "e ={x, y}" and "x \<in> X" and "y \<in> Y" and "{x, y} \<in> E"
[PROOF STATE]
proof (prove)
using this:
e \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>e = {x, y}; x \<in> X; y \<in> Y; {x, y} \<in> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e = {x, y}
x \<in> X
y \<in> Y
{x, y} \<in> E

goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = {x, y}
x \<in> X
y \<in> Y
{x, y} \<in> E
[PROOF STEP]
have "e = mk_edge (x, y)"
[PROOF STATE]
proof (prove)
using this:
e = {x, y}
x \<in> X
y \<in> Y
{x, y} \<in> E

goal (1 subgoal):
 1. e = mk_edge (x, y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e = mk_edge (x, y)

goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E} \<Longrightarrow> x \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = mk_edge (x, y)
[PROOF STEP]
show "e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}"
[PROOF STATE]
proof (prove)
using this:
e = mk_edge (x, y)

goal (1 subgoal):
 1. e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
using \<open>x \<in> X\<close> \<open>y \<in> Y\<close> \<open>{x, y} \<in> E\<close>
[PROOF STATE]
proof (prove)
using this:
e = mk_edge (x, y)
x \<in> X
y \<in> Y
{x, y} \<in> E

goal (1 subgoal):
 1. e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e \<in> mk_edge ` {(x, y). x \<in> X \<and> y \<in> Y \<and> {x, y} \<in> E}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma edge_density_ge0: "edge_density X Y \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> edge_density X Y
[PROOF STEP]
by (auto simp: edge_density_def)


[STATEMENT]
lemma edge_density_le1: "edge_density X Y \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_density X Y \<le> 1
[PROOF STEP]
proof (cases "finite X \<and> finite Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite X \<and> finite Y \<Longrightarrow> edge_density X Y \<le> 1
 2. \<not> (finite X \<and> finite Y) \<Longrightarrow> edge_density X Y \<le> 1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite X \<and> finite Y

goal (2 subgoals):
 1. finite X \<and> finite Y \<Longrightarrow> edge_density X Y \<le> 1
 2. \<not> (finite X \<and> finite Y) \<Longrightarrow> edge_density X Y \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X \<and> finite Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite X \<and> finite Y

goal (1 subgoal):
 1. edge_density X Y \<le> 1
[PROOF STEP]
using of_nat_mono [OF max_all_edges_between, of X Y]
[PROOF STATE]
proof (prove)
using this:
finite X \<and> finite Y
\<lbrakk>finite X; finite Y\<rbrakk> \<Longrightarrow> of_nat (card (all_edges_between X Y)) \<le> of_nat (card X * card Y)

goal (1 subgoal):
 1. edge_density X Y \<le> 1
[PROOF STEP]
by (fastforce simp add: edge_density_def divide_simps)
[PROOF STATE]
proof (state)
this:
edge_density X Y \<le> 1

goal (1 subgoal):
 1. \<not> (finite X \<and> finite Y) \<Longrightarrow> edge_density X Y \<le> 1
[PROOF STEP]
qed (auto simp: edge_density_def)


[STATEMENT]
lemma edge_density_zero:  "Y = {} \<Longrightarrow> edge_density X Y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y = {} \<Longrightarrow> edge_density X Y = 0
[PROOF STEP]
by (simp add: edge_density_def)


[STATEMENT]
lemma edge_density_commute: "edge_density X Y = edge_density Y X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_density X Y = edge_density Y X
[PROOF STEP]
by (simp add: edge_density_def card_all_edges_between_commute mult.commute)


[STATEMENT]
lemma edge_density_Un:
  assumes "disjnt X1 X2" "finite X1" "finite X2" "finite Y"
  shows "edge_density (X1 \<union> X2) Y = (edge_density X1 Y * card X1 + edge_density X2 Y * card X2) / (card X1 + card X2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_density (X1 \<union> X2) Y = (edge_density X1 Y * real (card X1) + edge_density X2 Y * real (card X2)) / real (card X1 + card X2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
disjnt X1 X2
finite X1
finite X2
finite Y

goal (1 subgoal):
 1. edge_density (X1 \<union> X2) Y = (edge_density X1 Y * real (card X1) + edge_density X2 Y * real (card X2)) / real (card X1 + card X2)
[PROOF STEP]
unfolding edge_density_def
[PROOF STATE]
proof (prove)
using this:
disjnt X1 X2
finite X1
finite X2
finite Y

goal (1 subgoal):
 1. real (card (all_edges_between (X1 \<union> X2) Y)) / real (card (X1 \<union> X2) * card Y) = (real (card (all_edges_between X1 Y)) / real (card X1 * card Y) * real (card X1) + real (card (all_edges_between X2 Y)) / real (card X2 * card Y) * real (card X2)) / real (card X1 + card X2)
[PROOF STEP]
by (simp add: all_edges_between_disjnt1 all_edges_between_Un1 finite_all_edges_between card_Un_disjnt divide_simps)


[STATEMENT]
lemma edge_density_eq0:
  assumes "all_edges_between A B = {}" and "X \<subseteq> A" "Y \<subseteq> B"
  shows "edge_density X Y  = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_density X Y = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edge_density X Y = 0
[PROOF STEP]
have "all_edges_between X Y = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y = {}
[PROOF STEP]
by (metis all_edges_between_mono1 all_edges_between_mono2 assms subset_empty)
[PROOF STATE]
proof (state)
this:
all_edges_between X Y = {}

goal (1 subgoal):
 1. edge_density X Y = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
all_edges_between X Y = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
all_edges_between X Y = {}

goal (1 subgoal):
 1. edge_density X Y = 0
[PROOF STEP]
by (auto simp: edge_density_def)
[PROOF STATE]
proof (state)
this:
edge_density X Y = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_is_has_loop_eq: "card {e \<in> E . is_loop e} = card {v \<in> V . has_loop v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
have "\<And> e . e \<in> E \<Longrightarrow> is_loop e \<longleftrightarrow> (\<exists> v. e = {v})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. e \<in> E \<Longrightarrow> is_loop e = (\<exists>v. e = {v})
[PROOF STEP]
using is_loop_def
[PROOF STATE]
proof (prove)
using this:
is_loop ?e \<equiv> card ?e = 1

goal (1 subgoal):
 1. \<And>e. e \<in> E \<Longrightarrow> is_loop e = (\<exists>v. e = {v})
[PROOF STEP]
using is_singleton_altdef is_singleton_def
[PROOF STATE]
proof (prove)
using this:
is_loop ?e \<equiv> card ?e = 1
is_singleton ?A = (card ?A = 1)
is_singleton ?A = (\<exists>x. ?A = {x})

goal (1 subgoal):
 1. \<And>e. e \<in> E \<Longrightarrow> is_loop e = (\<exists>v. e = {v})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?e \<in> E \<Longrightarrow> is_loop ?e = (\<exists>v. ?e = {v})

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
define f :: "'a \<Rightarrow> 'a set"  where "f = (\<lambda> v . {v})"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>v. {v})

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
have feq: "f ` {v \<in> V . has_loop v} = {{v} | v . has_loop v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {v \<in> V. has_loop v} = {{v} |v. has_loop v}
[PROOF STEP]
using has_loop_in_verts f_def
[PROOF STATE]
proof (prove)
using this:
has_loop ?v \<Longrightarrow> ?v \<in> V
f = (\<lambda>v. {v})

goal (1 subgoal):
 1. f ` {v \<in> V. has_loop v} = {{v} |v. has_loop v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` {v \<in> V. has_loop v} = {{v} |v. has_loop v}

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
have "inj_on f {v \<in> V . has_loop v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f {v \<in> V. has_loop v}
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
inj_on f {v \<in> V. has_loop v}

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on f {v \<in> V. has_loop v}
[PROOF STEP]
have "card {v \<in> V . has_loop v} = card (f ` {v \<in> V . has_loop v})"
[PROOF STATE]
proof (prove)
using this:
inj_on f {v \<in> V. has_loop v}

goal (1 subgoal):
 1. card {v \<in> V. has_loop v} = card (f ` {v \<in> V. has_loop v})
[PROOF STEP]
using card_image
[PROOF STATE]
proof (prove)
using this:
inj_on f {v \<in> V. has_loop v}
inj_on ?f ?A \<Longrightarrow> card (?f ` ?A) = card ?A

goal (1 subgoal):
 1. card {v \<in> V. has_loop v} = card (f ` {v \<in> V. has_loop v})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card {v \<in> V. has_loop v} = card (f ` {v \<in> V. has_loop v})

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {v \<in> V. has_loop v} = card (f ` {v \<in> V. has_loop v})

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
have "... = card {{v} | v . has_loop v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (f ` {v \<in> V. has_loop v}) = card {{v} |v. has_loop v}
[PROOF STEP]
using feq
[PROOF STATE]
proof (prove)
using this:
f ` {v \<in> V. has_loop v} = {{v} |v. has_loop v}

goal (1 subgoal):
 1. card (f ` {v \<in> V. has_loop v}) = card {{v} |v. has_loop v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (f ` {v \<in> V. has_loop v}) = card {{v} |v. has_loop v}

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {v \<in> V. has_loop v} = card {{v} |v. has_loop v}
[PROOF STEP]
have "card {v \<in> V . has_loop v} = card {e \<in> E . is_loop e}"
[PROOF STATE]
proof (prove)
using this:
card {v \<in> V. has_loop v} = card {{v} |v. has_loop v}

goal (1 subgoal):
 1. card {v \<in> V. has_loop v} = card {e \<in> E. is_loop e}
[PROOF STEP]
using is_loop_set_alt
[PROOF STATE]
proof (prove)
using this:
card {v \<in> V. has_loop v} = card {{v} |v. has_loop v}
{{v} |v. has_loop v} = {e \<in> E. is_loop e}

goal (1 subgoal):
 1. card {v \<in> V. has_loop v} = card {e \<in> E. is_loop e}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {v \<in> V. has_loop v} = card {e \<in> E. is_loop e}

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
thus "card {e \<in> E . is_loop e} = card {v \<in> V . has_loop v}"
[PROOF STATE]
proof (prove)
using this:
card {v \<in> V. has_loop v} = card {e \<in> E. is_loop e}

goal (1 subgoal):
 1. card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {e \<in> E. is_loop e} = card {v \<in> V. has_loop v}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_all_edges_between': "finite (all_edges_between X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (all_edges_between X Y)
[PROOF STEP]
using finV wellformed
[PROOF STATE]
proof (prove)
using this:
finite V
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. finite (all_edges_between X Y)
[PROOF STEP]
by (metis all_edges_between_rem_wf finite_Int finite_all_edges_between)


[STATEMENT]
lemma card_all_edges_between:
  assumes "finite Y"
  shows "card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))
[PROOF STEP]
have "all_edges_between X Y = (\<Union>y\<in>Y. all_edges_between X {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y = (\<Union>y\<in>Y. all_edges_between X {y})
[PROOF STEP]
by (auto simp: all_edges_between_def)
[PROOF STATE]
proof (state)
this:
all_edges_between X Y = (\<Union>y\<in>Y. all_edges_between X {y})

goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
all_edges_between X Y = (\<Union>y\<in>Y. all_edges_between X {y})

goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))
[PROOF STEP]
have "disjoint_family_on (\<lambda>y. all_edges_between X {y}) Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_family_on (\<lambda>y. all_edges_between X {y}) Y
[PROOF STEP]
unfolding disjoint_family_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<in>Y. \<forall>n\<in>Y. m \<noteq> n \<longrightarrow> all_edges_between X {m} \<inter> all_edges_between X {n} = {}
[PROOF STEP]
by (auto simp: disjoint_family_on_def all_edges_between_def)
[PROOF STATE]
proof (state)
this:
disjoint_family_on (\<lambda>y. all_edges_between X {y}) Y

goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
all_edges_between X Y = (\<Union>y\<in>Y. all_edges_between X {y})
disjoint_family_on (\<lambda>y. all_edges_between X {y}) Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
all_edges_between X Y = (\<Union>y\<in>Y. all_edges_between X {y})
disjoint_family_on (\<lambda>y. all_edges_between X {y}) Y

goal (1 subgoal):
 1. card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))
[PROOF STEP]
by (simp add: card_UN_disjoint' assms finite_all_edges_between')
[PROOF STATE]
proof (state)
this:
card (all_edges_between X Y) = (\<Sum>y\<in>Y. card (all_edges_between X {y}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wellformed_all_edges: "E \<subseteq> all_edges V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<subseteq> all_edges V
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<subseteq> {e. e \<subseteq> V \<and> card e = 2}
[PROOF STEP]
using wellformed two_edges
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V
?e \<in> E \<Longrightarrow> card ?e = 2

goal (1 subgoal):
 1. E \<subseteq> {e. e \<subseteq> V \<and> card e = 2}
[PROOF STEP]
by auto


[STATEMENT]
lemma e_in_all_edges: "e \<in> E \<Longrightarrow> e \<in> all_edges V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> e \<in> all_edges V
[PROOF STEP]
using wellformed_all_edges
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> all_edges V

goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> e \<in> all_edges V
[PROOF STEP]
by auto


[STATEMENT]
lemma e_in_all_edges_ss: "e \<in> E \<Longrightarrow> e \<subseteq> V' \<Longrightarrow> V' \<subseteq> V \<Longrightarrow> e \<in> all_edges V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<in> E; e \<subseteq> V'; V' \<subseteq> V\<rbrakk> \<Longrightarrow> e \<in> all_edges V'
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<in> E; e \<subseteq> V'; V' \<subseteq> V\<rbrakk> \<Longrightarrow> e \<in> {e. e \<subseteq> V' \<and> card e = 2}
[PROOF STEP]
using wellformed two_edges
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V
?e \<in> E \<Longrightarrow> card ?e = 2

goal (1 subgoal):
 1. \<lbrakk>e \<in> E; e \<subseteq> V'; V' \<subseteq> V\<rbrakk> \<Longrightarrow> e \<in> {e. e \<subseteq> V' \<and> card e = 2}
[PROOF STEP]
by auto


[STATEMENT]
lemma singleton_not_edge: "{x} \<notin> E" \<comment> \<open> Suggested by Mantas Baksys \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} \<notin> E
[PROOF STEP]
using two_edges
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> card ?e = 2

goal (1 subgoal):
 1. {x} \<notin> E
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fin_neighbourhood: "finite (neighborhood x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (neighborhood x)
[PROOF STEP]
unfolding neighborhood_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {v \<in> V. vert_adj x v}
[PROOF STEP]
using finV
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite {v \<in> V. vert_adj x v}
[PROOF STEP]
by simp


[STATEMENT]
lemma fin_all_edges: "finite (all_edges V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (all_edges V)
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {e. e \<subseteq> V \<and> card e = 2}
[PROOF STEP]
by (simp add: finV)


[STATEMENT]
lemma max_edges_graph:  "card E \<le> (card V)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_size \<le> order\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph_size \<le> order\<^sup>2
[PROOF STEP]
have "card E \<le> card V choose 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_size \<le> order choose 2
[PROOF STEP]
by (metis fin_all_edges finV card_all_edges card_mono wellformed_all_edges)
[PROOF STATE]
proof (state)
this:
graph_size \<le> order choose 2

goal (1 subgoal):
 1. graph_size \<le> order\<^sup>2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
graph_size \<le> order choose 2

goal (1 subgoal):
 1. graph_size \<le> order\<^sup>2
[PROOF STEP]
by (metis binomial_le_pow le0 neq0_conv order.trans zero_less_binomial_iff)
[PROOF STATE]
proof (state)
this:
graph_size \<le> order\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_loops: "v \<in> V \<Longrightarrow> \<not> has_loop v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> V \<Longrightarrow> \<not> has_loop v
[PROOF STEP]
using has_loop_def two_edges
[PROOF STATE]
proof (prove)
using this:
has_loop ?v \<equiv> {?v} \<in> E
?e \<in> E \<Longrightarrow> card ?e = 2

goal (1 subgoal):
 1. v \<in> V \<Longrightarrow> \<not> has_loop v
[PROOF STEP]
by fastforce


[STATEMENT]
lemma alt_degree_def[simp]: "degree v = card (incident_edges v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v = card (incident_edges v)
[PROOF STEP]
using no_loops degree_no_loops  degree_none incident_edges_empty
[PROOF STATE]
proof (prove)
using this:
?v \<in> V \<Longrightarrow> \<not> has_loop ?v
\<not> has_loop ?v \<Longrightarrow> degree ?v = card (incident_edges ?v)
?v \<notin> V \<Longrightarrow> degree ?v = 0
?v \<notin> V \<Longrightarrow> incident_edges ?v = {}

goal (1 subgoal):
 1. degree v = card (incident_edges v)
[PROOF STEP]
by (cases "v \<in> V") simp_all


[STATEMENT]
lemma alt_deg_neighborhood: "degree v = card (neighborhood v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v = card (neighborhood v)
[PROOF STEP]
using card_incident_sedges_neighborhood
[PROOF STATE]
proof (prove)
using this:
card (incident_edges ?v) = card (neighborhood ?v)

goal (1 subgoal):
 1. degree v = card (neighborhood v)
[PROOF STEP]
by simp


[STATEMENT]
lemma is_complement_edges: "is_complement (V', E')  \<longleftrightarrow> V = V' \<and> complement_edges = E'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_complement (V', E') = (V = V' \<and> complement_edges = E')
[PROOF STEP]
unfolding is_complement_def complement_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V = gverts (V', E') \<and> gedges (V', E') = all_edges V - E) = (V = V' \<and> all_edges V - E = E')
[PROOF STEP]
by auto


[STATEMENT]
lemma is_complement_edge_iff: "e \<subseteq> V \<Longrightarrow> e \<in> complement_edges \<longleftrightarrow> e \<notin> E \<and> card e = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<subseteq> V \<Longrightarrow> (e \<in> complement_edges) = (e \<notin> E \<and> card e = 2)
[PROOF STEP]
unfolding complement_edges_def all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<subseteq> V \<Longrightarrow> (e \<in> {e. e \<subseteq> V \<and> card e = 2} - E) = (e \<notin> E \<and> card e = 2)
[PROOF STEP]
by auto


[STATEMENT]
lemma complete_sgraph: "sgraph S (all_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgraph S (all_edges S)
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgraph S {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
by (unfold_locales) (simp_all)


[STATEMENT]
lemma complete_fin_sgraph: "finite S \<Longrightarrow> fin_sgraph S (all_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> fin_sgraph S (all_edges S)
[PROOF STEP]
using complete_sgraph
[PROOF STATE]
proof (prove)
using this:
sgraph ?S (all_edges ?S)

goal (1 subgoal):
 1. finite S \<Longrightarrow> fin_sgraph S (all_edges S)
[PROOF STEP]
by (intro_locales) (auto simp add: sgraph.axioms(1) sgraph_def fin_graph_system_axioms_def)


[STATEMENT]
lemma is_subgraphI[intro]: "V' \<subseteq> V \<Longrightarrow> E' \<subseteq> E \<Longrightarrow> graph_system V' E' \<Longrightarrow> graph_system V E \<Longrightarrow> subgraph V' E' V E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>V' \<subseteq> V; E' \<subseteq> E; graph_system V' E'; graph_system V E\<rbrakk> \<Longrightarrow> subgraph V' E' V E
[PROOF STEP]
using graph_system_def
[PROOF STATE]
proof (prove)
using this:
graph_system ?vertices ?edges \<equiv> \<forall>e. e \<in> ?edges \<longrightarrow> e \<subseteq> ?vertices

goal (1 subgoal):
 1. \<lbrakk>V' \<subseteq> V; E' \<subseteq> E; graph_system V' E'; graph_system V E\<rbrakk> \<Longrightarrow> subgraph V' E' V E
[PROOF STEP]
by (unfold_locales)
    (auto simp add: graph_system.incident_def graph_system.incident_edge_in_wf)


[STATEMENT]
lemma is_subgraph_ulgraph:
  assumes "ulgraph V\<^sub>G E\<^sub>G"
  shows "ulgraph V\<^sub>H E\<^sub>H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ulgraph V\<^sub>H E\<^sub>H
[PROOF STEP]
using assms ulgraph.edge_size[ of V\<^sub>G E\<^sub>G] edges_ss
[PROOF STATE]
proof (prove)
using this:
ulgraph V\<^sub>G E\<^sub>G
\<lbrakk>ulgraph V\<^sub>G E\<^sub>G; ?e \<in> E\<^sub>G\<rbrakk> \<Longrightarrow> 0 < card ?e \<and> card ?e \<le> 2
E\<^sub>H \<subseteq> E\<^sub>G

goal (1 subgoal):
 1. ulgraph V\<^sub>H E\<^sub>H
[PROOF STEP]
by (unfold_locales) auto


[STATEMENT]
lemma is_simp_subgraph:
  assumes "sgraph V\<^sub>G E\<^sub>G"
  shows "sgraph V\<^sub>H E\<^sub>H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgraph V\<^sub>H E\<^sub>H
[PROOF STEP]
using assms sgraph.two_edges edges_ss
[PROOF STATE]
proof (prove)
using this:
sgraph V\<^sub>G E\<^sub>G
\<lbrakk>sgraph ?vertices ?edges; ?e \<in> ?edges\<rbrakk> \<Longrightarrow> card ?e = 2
E\<^sub>H \<subseteq> E\<^sub>G

goal (1 subgoal):
 1. sgraph V\<^sub>H E\<^sub>H
[PROOF STEP]
by (unfold_locales) auto


[STATEMENT]
lemma is_finite_subgraph:
  assumes "fin_graph_system V\<^sub>G E\<^sub>G"
  shows "fin_graph_system V\<^sub>H E\<^sub>H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_graph_system V\<^sub>H E\<^sub>H
[PROOF STEP]
using assms verts_ss
[PROOF STATE]
proof (prove)
using this:
fin_graph_system V\<^sub>G E\<^sub>G
V\<^sub>H \<subseteq> V\<^sub>G

goal (1 subgoal):
 1. fin_graph_system V\<^sub>H E\<^sub>H
[PROOF STEP]
by (unfold_locales) (simp add: fin_graph_system.finV finite_subset)


[STATEMENT]
lemma (in graph_system) subgraph_refl: "subgraph V E V E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph V E V E
[PROOF STEP]
by (simp add: graph_system_axioms is_subgraphI)


[STATEMENT]
lemma subgraph_antisym: "subgraph V' E' V E \<Longrightarrow> subgraph V E V' E' \<Longrightarrow> V = V' \<and> E = E'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>subgraph V' E' V E; subgraph V E V' E'\<rbrakk> \<Longrightarrow> V = V' \<and> E = E'
[PROOF STEP]
by (simp add: dual_order.eq_iff subgraph.edges_ss subgraph.verts_ss)


[STATEMENT]
lemma (in sgraph) subgraph_complete: "subgraph V E V (all_edges V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph V E V (all_edges V)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgraph V E V (all_edges V)
[PROOF STEP]
interpret comp: sgraph V "(all_edges V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgraph V (all_edges V)
[PROOF STEP]
using complete_sgraph
[PROOF STATE]
proof (prove)
using this:
sgraph ?S (all_edges ?S)

goal (1 subgoal):
 1. sgraph V (all_edges V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgraph V E V (all_edges V)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph V E V (all_edges V)
[PROOF STEP]
by (unfold_locales) (simp_all add: wellformed_all_edges)
[PROOF STATE]
proof (state)
this:
subgraph V E V (all_edges V)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in sgraph) induced_edges_alt: "induced_edges V' = E \<inter> all_edges V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. induced_edges V' = E \<inter> all_edges V'
[PROOF STEP]
unfolding induced_edges_def all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e \<in> E. e \<subseteq> V'} = E \<inter> {e. e \<subseteq> V' \<and> card e = 2}
[PROOF STEP]
using two_edges
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> card ?e = 2

goal (1 subgoal):
 1. {e \<in> E. e \<subseteq> V'} = E \<inter> {e. e \<subseteq> V' \<and> card e = 2}
[PROOF STEP]
by blast


[STATEMENT]
lemma (in sgraph) induced_edges_self: "induced_edges V = E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. induced_edges V = E
[PROOF STEP]
unfolding induced_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e \<in> E. e \<subseteq> V} = E
[PROOF STEP]
by (simp add: subsetI subset_antisym wellformed)


[STATEMENT]
lemma induced_edges_ss: "V' \<subseteq> V \<Longrightarrow> induced_edges V' \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V' \<subseteq> V \<Longrightarrow> induced_edges V' \<subseteq> E
[PROOF STEP]
unfolding induced_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V' \<subseteq> V \<Longrightarrow> {e \<in> E. e \<subseteq> V'} \<subseteq> E
[PROOF STEP]
by auto


[STATEMENT]
lemma induced_is_graph_sys: "graph_system V' (induced_edges V')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_system V' (induced_edges V')
[PROOF STEP]
by (unfold_locales) (simp add: induced_edges_def)


[STATEMENT]
lemma induced_is_subgraph: "V' \<subseteq> V \<Longrightarrow> subgraph V' (induced_edges V') V E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V' \<subseteq> V \<Longrightarrow> subgraph V' (induced_edges V') V E
[PROOF STEP]
using induced_edges_ss
[PROOF STATE]
proof (prove)
using this:
?V' \<subseteq> V \<Longrightarrow> induced_edges ?V' \<subseteq> E

goal (1 subgoal):
 1. V' \<subseteq> V \<Longrightarrow> subgraph V' (induced_edges V') V E
[PROOF STEP]
by (unfold_locales) auto


[STATEMENT]
lemma induced_edges_union:
  assumes "VH1 \<subseteq> S" "VH2 \<subseteq> T"
  assumes "graph_system VH1 EH1" "graph_system VH2 EH2"
  assumes "EH1 \<union> EH2 \<subseteq> (induced_edges (S \<union> T))"
  shows "EH1 \<subseteq> (induced_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EH1 \<subseteq> induced_edges S
[PROOF STEP]
proof (intro subsetI, simp add: induced_edges_def, intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> EH1 \<Longrightarrow> x \<in> E
 2. \<And>x. x \<in> EH1 \<Longrightarrow> x \<subseteq> S
[PROOF STEP]
show "\<And>x. x \<in> EH1 \<Longrightarrow> x \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> EH1 \<Longrightarrow> x \<in> E
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
EH1 \<union> EH2 \<subseteq> induced_edges (S \<union> T)

goal (1 subgoal):
 1. \<And>x. x \<in> EH1 \<Longrightarrow> x \<in> E
[PROOF STEP]
by (simp add: induced_edges_def subset_iff)
[PROOF STATE]
proof (state)
this:
?x \<in> EH1 \<Longrightarrow> ?x \<in> E

goal (1 subgoal):
 1. \<And>x. x \<in> EH1 \<Longrightarrow> x \<subseteq> S
[PROOF STEP]
show "\<And>x. x \<in> EH1 \<Longrightarrow> x \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> EH1 \<Longrightarrow> x \<subseteq> S
[PROOF STEP]
using assms(1) assms(3) graph_system.wellformed
[PROOF STATE]
proof (prove)
using this:
VH1 \<subseteq> S
graph_system VH1 EH1
\<lbrakk>graph_system ?vertices ?edges; ?e \<in> ?edges\<rbrakk> \<Longrightarrow> ?e \<subseteq> ?vertices

goal (1 subgoal):
 1. \<And>x. x \<in> EH1 \<Longrightarrow> x \<subseteq> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> EH1 \<Longrightarrow> ?x \<subseteq> S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma induced_edges_union_subgraph_single:
  assumes "VH1 \<subseteq> S" "VH2 \<subseteq> T"
  assumes "graph_system VH1 EH1" "graph_system VH2 EH2"
  assumes "subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))"
  shows "subgraph VH1 EH1 S (induced_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
interpret ug: subgraph "(VH1 \<union> VH2)" "(EH1 \<union> EH2)" "(S \<union> T)" "(induced_edges (S \<union> T))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))

goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
show "subgraph VH1 EH1 S (induced_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
using assms(3) graph_system_def
[PROOF STATE]
proof (prove)
using this:
graph_system VH1 EH1
graph_system ?vertices ?edges \<equiv> \<forall>e. e \<in> ?edges \<longrightarrow> e \<subseteq> ?vertices

goal (1 subgoal):
 1. subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
by (unfold_locales) (blast, simp add: assms(1), meson assms induced_edges_union ug.edges_ss)
[PROOF STATE]
proof (state)
this:
subgraph VH1 EH1 S (induced_edges S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma induced_union_subgraph:
  assumes "VH1 \<subseteq> S" and "VH2 \<subseteq> T"
  assumes "graph_system VH1 EH1" "graph_system VH2 EH2"
  shows "subgraph VH1 EH1 S (induced_edges S) \<and> subgraph VH2 EH2 T (induced_edges T) \<longleftrightarrow>
    subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subgraph VH1 EH1 S (induced_edges S) \<and> subgraph VH2 EH2 T (induced_edges T)) = subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
proof (intro iffI conjI, elim conjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>subgraph VH1 EH1 S (induced_edges S); subgraph VH2 EH2 T (induced_edges T)\<rbrakk> \<Longrightarrow> subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
 2. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH1 EH1 S (induced_edges S)
 3. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
show "subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
      \<Longrightarrow> subgraph VH1 EH1 S (induced_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
using induced_edges_union_subgraph_single assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?VH1.0 \<subseteq> ?S; ?VH2.0 \<subseteq> ?T; graph_system ?VH1.0 ?EH1.0; graph_system ?VH2.0 ?EH2.0; subgraph (?VH1.0 \<union> ?VH2.0) (?EH1.0 \<union> ?EH2.0) (?S \<union> ?T) (induced_edges (?S \<union> ?T))\<rbrakk> \<Longrightarrow> subgraph ?VH1.0 ?EH1.0 ?S (induced_edges ?S)
VH1 \<subseteq> S
VH2 \<subseteq> T
graph_system VH1 EH1
graph_system VH2 EH2

goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH1 EH1 S (induced_edges S)

goal (2 subgoals):
 1. \<lbrakk>subgraph VH1 EH1 S (induced_edges S); subgraph VH2 EH2 T (induced_edges T)\<rbrakk> \<Longrightarrow> subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
 2. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
show "subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
      \<Longrightarrow> subgraph VH2 EH2 T (induced_edges T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
using induced_edges_union_subgraph_single assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?VH1.0 \<subseteq> ?S; ?VH2.0 \<subseteq> ?T; graph_system ?VH1.0 ?EH1.0; graph_system ?VH2.0 ?EH2.0; subgraph (?VH1.0 \<union> ?VH2.0) (?EH1.0 \<union> ?EH2.0) (?S \<union> ?T) (induced_edges (?S \<union> ?T))\<rbrakk> \<Longrightarrow> subgraph ?VH1.0 ?EH1.0 ?S (induced_edges ?S)
VH1 \<subseteq> S
VH2 \<subseteq> T
graph_system VH1 EH1
graph_system VH2 EH2

goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
by (simp add: Un_commute)
[PROOF STATE]
proof (state)
this:
subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T)) \<Longrightarrow> subgraph VH2 EH2 T (induced_edges T)

goal (1 subgoal):
 1. \<lbrakk>subgraph VH1 EH1 S (induced_edges S); subgraph VH2 EH2 T (induced_edges T)\<rbrakk> \<Longrightarrow> subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
assume a1: "subgraph VH1 EH1 S (induced_edges S)" and a2: "subgraph VH2 EH2 T (induced_edges T)"
[PROOF STATE]
proof (state)
this:
subgraph VH1 EH1 S (induced_edges S)
subgraph VH2 EH2 T (induced_edges T)

goal (1 subgoal):
 1. \<lbrakk>subgraph VH1 EH1 S (induced_edges S); subgraph VH2 EH2 T (induced_edges T)\<rbrakk> \<Longrightarrow> subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subgraph VH1 EH1 S (induced_edges S)
subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
interpret h1: subgraph VH1 EH1 S "(induced_edges S)"
[PROOF STATE]
proof (prove)
using this:
subgraph VH1 EH1 S (induced_edges S)
subgraph VH2 EH2 T (induced_edges T)

goal (1 subgoal):
 1. subgraph VH1 EH1 S (induced_edges S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>subgraph VH1 EH1 S (induced_edges S); subgraph VH2 EH2 T (induced_edges T)\<rbrakk> \<Longrightarrow> subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
interpret h2: subgraph VH2 EH2 T "(induced_edges T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
subgraph VH2 EH2 T (induced_edges T)

goal (1 subgoal):
 1. subgraph VH2 EH2 T (induced_edges T)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>subgraph VH1 EH1 S (induced_edges S); subgraph VH2 EH2 T (induced_edges T)\<rbrakk> \<Longrightarrow> subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
show "subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
using h1.H.wellformed h2.H.wellformed h1.verts_ss h2.verts_ss h1.edges_ss h2.edges_ss
[PROOF STATE]
proof (prove)
using this:
?e \<in> EH1 \<Longrightarrow> ?e \<subseteq> VH1
?e \<in> EH2 \<Longrightarrow> ?e \<subseteq> VH2
VH1 \<subseteq> S
VH2 \<subseteq> T
EH1 \<subseteq> induced_edges S
EH2 \<subseteq> induced_edges T

goal (1 subgoal):
 1. subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))
[PROOF STEP]
by (unfold_locales) (auto simp add: induced_edges_def)
[PROOF STATE]
proof (state)
this:
subgraph (VH1 \<union> VH2) (EH1 \<union> EH2) (S \<union> T) (induced_edges (S \<union> T))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [code]:
  "ExcessTable g =
   List.map_filter (\<lambda>v. let e = ExcessAt g v in if 0 < e then Some (v, e) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ExcessTable g = List.map_filter (\<lambda>v. let e = ExcessAt g v in if 0 < e then Some (v, e) else None)
[PROOF STEP]
by (rule ext) (simp add: ExcessTable_def map_filter_def)


[STATEMENT]
lemma [code]: "deleteAround g v ps =
      (let vs = (\<lambda>f. let n = f\<bullet>v
                     in if |vertices f| = 4 then [n, f\<bullet>n] else [n])
       in removeKeyList (concat(map vs (facesAt g v))) ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deleteAround g v ps = (let vs = \<lambda>f. let n = f \<bullet> v in if |vertices f| = 4 then [n, f \<bullet> n] else [n] in removeKeyList (concat (map vs (facesAt g v))) ps)
[PROOF STEP]
by (simp only: concat_map_singleton Let_def deleteAround_def nextV2)


[STATEMENT]
lemma length_deleteAround: "length (deleteAround g v ps) \<le> length ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |deleteAround g v ps| \<le> |ps|
[PROOF STEP]
by (auto simp only: deleteAround_def length_removeKeyList Let_def)


[STATEMENT]
lemma merge_Empty[simp]: "merge heap.Empty h = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge heap.Empty h = h
[PROOF STEP]
by(cases h) auto


[STATEMENT]
lemma merge2: "merge (Hp x lx) h = (case h of heap.Empty \<Rightarrow> Hp x lx | (Hp y ly) \<Rightarrow>
    (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge (Hp x lx) h = (case h of heap.Empty \<Rightarrow> Hp x lx | Hp y ly \<Rightarrow> if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))
[PROOF STEP]
by(auto split: heap.split)


[STATEMENT]
lemma pass1_Nil_iff: "pass\<^sub>1 hs = [] \<longleftrightarrow> hs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pass\<^sub>1 hs = []) = (hs = [])
[PROOF STEP]
by(cases hs rule: pass\<^sub>1.cases) auto


[STATEMENT]
lemma is_root_if_no_Empty: "no_Empty h \<Longrightarrow> is_root h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Empty h \<Longrightarrow> is_root h
[PROOF STEP]
by(cases h) auto


[STATEMENT]
lemma no_Emptys_hps: "no_Empty h \<Longrightarrow> no_Emptys(hps h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Empty h \<Longrightarrow> no_Emptys (hps h)
[PROOF STEP]
by(induction h) auto


[STATEMENT]
lemma no_Empty_merge: "\<lbrakk> no_Empty h1; no_Empty h2\<rbrakk> \<Longrightarrow> no_Empty (merge h1 h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_Empty h1; no_Empty h2\<rbrakk> \<Longrightarrow> no_Empty (merge h1 h2)
[PROOF STEP]
by (cases "(h1,h2)" rule: merge.cases) auto


[STATEMENT]
lemma is_root_merge: "\<lbrakk> is_root h1; is_root h2\<rbrakk> \<Longrightarrow> is_root (merge h1 h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_root h1; is_root h2\<rbrakk> \<Longrightarrow> is_root (merge h1 h2)
[PROOF STEP]
by (cases "(h1,h2)" rule: merge.cases) auto


[STATEMENT]
lemma no_Emptys_pass1:
  "no_Emptys hs \<Longrightarrow> no_Emptys (pass\<^sub>1 hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> no_Emptys (pass\<^sub>1 hs)
[PROOF STEP]
by(induction hs rule: pass\<^sub>1.induct)(auto simp: no_Empty_merge)


[STATEMENT]
lemma is_root_pass2: "no_Emptys hs \<Longrightarrow> is_root(pass\<^sub>2 hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> is_root (pass\<^sub>2 hs)
[PROOF STEP]
proof(induction hs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. no_Emptys [] \<Longrightarrow> is_root (pass\<^sub>2 [])
 2. \<And>a hs. \<lbrakk>no_Emptys hs \<Longrightarrow> is_root (pass\<^sub>2 hs); no_Emptys (a # hs)\<rbrakk> \<Longrightarrow> is_root (pass\<^sub>2 (a # hs))
[PROOF STEP]
case (Cons _ hs)
[PROOF STATE]
proof (state)
this:
no_Emptys hs \<Longrightarrow> is_root (pass\<^sub>2 hs)
no_Emptys (a_ # hs)

goal (2 subgoals):
 1. no_Emptys [] \<Longrightarrow> is_root (pass\<^sub>2 [])
 2. \<And>a hs. \<lbrakk>no_Emptys hs \<Longrightarrow> is_root (pass\<^sub>2 hs); no_Emptys (a # hs)\<rbrakk> \<Longrightarrow> is_root (pass\<^sub>2 (a # hs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
 2. \<not> ?P \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
assume "hs = []"
[PROOF STATE]
proof (state)
this:
hs = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
 2. \<not> ?P \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hs = []

goal (1 subgoal):
 1. is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
hs = []
no_Emptys hs \<Longrightarrow> is_root (pass\<^sub>2 hs)
no_Emptys (a_ # hs)

goal (1 subgoal):
 1. is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
by (auto simp: is_root_if_no_Empty)
[PROOF STATE]
proof (state)
this:
is_root (pass\<^sub>2 (a_ # hs))

goal (1 subgoal):
 1. hs \<noteq> [] \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hs \<noteq> [] \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
assume "hs \<noteq> []"
[PROOF STATE]
proof (state)
this:
hs \<noteq> []

goal (1 subgoal):
 1. hs \<noteq> [] \<Longrightarrow> is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hs \<noteq> []

goal (1 subgoal):
 1. is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
hs \<noteq> []
no_Emptys hs \<Longrightarrow> is_root (pass\<^sub>2 hs)
no_Emptys (a_ # hs)

goal (1 subgoal):
 1. is_root (pass\<^sub>2 (a_ # hs))
[PROOF STEP]
by(auto simp: is_root_merge is_root_if_no_Empty)
[PROOF STATE]
proof (state)
this:
is_root (pass\<^sub>2 (a_ # hs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_root (pass\<^sub>2 (a_ # hs))

goal (1 subgoal):
 1. no_Emptys [] \<Longrightarrow> is_root (pass\<^sub>2 [])
[PROOF STEP]
qed simp


[STATEMENT]
lemma \<Phi>_hps_ge0: "\<Phi>_hps hs \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<Phi>_hps hs
[PROOF STEP]
by (induction hs rule: \<Phi>_hps.induct) auto


[STATEMENT]
lemma no_Empty_ge0: "no_Empty h \<Longrightarrow> size_hp h > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Empty h \<Longrightarrow> 0 < size_hp h
[PROOF STEP]
by(cases h) auto


[STATEMENT]
lemma \<Phi>_hps1: "\<Phi>_hps [h] = \<Phi> h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi>_hps [h] = \<Phi> h
[PROOF STEP]
by(cases h) auto


[STATEMENT]
lemma size_hp_merge: "size_hp(merge h1 h2) = size_hp h1 + size_hp h2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size_hp (merge h1 h2) = size_hp h1 + size_hp h2
[PROOF STEP]
by (induction h1 h2 rule: merge.induct) simp_all


[STATEMENT]
lemma pass\<^sub>1_size[simp]: "size_hps (pass\<^sub>1 hs) = size_hps hs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size_hps (pass\<^sub>1 hs) = size_hps hs
[PROOF STEP]
by (induct hs rule: pass\<^sub>1.induct) (simp_all add: size_hp_merge)


[STATEMENT]
lemma \<Delta>\<Phi>_insert:
  "\<Phi> (Pairing_Heap_List1.insert x h) - \<Phi> h \<le> log 2 (size_hp h + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (Pairing_Heap_List1.insert x h) - \<Phi> h \<le> log 2 (real (size_hp h + 1))
[PROOF STEP]
by(cases h)(auto simp: size_hp_merge)


[STATEMENT]
lemma \<Delta>\<Phi>_merge:
  "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2
  \<le> log 2 (size_hp h1 + size_hp h2 + 1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size_hp h1 + size_hp h2 + 1)) + 1
[PROOF STEP]
proof(induction h1 h2 rule: merge.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>h. \<Phi> (merge h heap.Empty) - \<Phi> h - \<Phi> heap.Empty \<le> log 2 (real (size_hp h + size_hp heap.Empty + 1)) + 1
 2. \<And>v va. \<Phi> (merge heap.Empty (Hp v va)) - \<Phi> heap.Empty - \<Phi> (Hp v va) \<le> log 2 (real (size_hp heap.Empty + size_hp (Hp v va) + 1)) + 1
 3. \<And>x hsx y hsy. \<Phi> (merge (Hp x hsx) (Hp y hsy)) - \<Phi> (Hp x hsx) - \<Phi> (Hp y hsy) \<le> log 2 (real (size_hp (Hp x hsx) + size_hp (Hp y hsy) + 1)) + 1
[PROOF STEP]
case (3 x lx y ly)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>h. \<Phi> (merge h heap.Empty) - \<Phi> h - \<Phi> heap.Empty \<le> log 2 (real (size_hp h + size_hp heap.Empty + 1)) + 1
 2. \<And>v va. \<Phi> (merge heap.Empty (Hp v va)) - \<Phi> heap.Empty - \<Phi> (Hp v va) \<le> log 2 (real (size_hp heap.Empty + size_hp (Hp v va) + 1)) + 1
 3. \<And>x hsx y hsy. \<Phi> (merge (Hp x hsx) (Hp y hsy)) - \<Phi> (Hp x hsx) - \<Phi> (Hp y hsy) \<le> log 2 (real (size_hp (Hp x hsx) + size_hp (Hp y hsy) + 1)) + 1
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (merge (Hp x lx) (Hp y ly)) - \<Phi> (Hp x lx) - \<Phi> (Hp y ly) \<le> log 2 (real (size_hp (Hp x lx) + size_hp (Hp y ly) + 1)) + 1
[PROOF STEP]
using ld_le_2ld[of "size_hps lx" "size_hps ly"]
      log_le_cancel_iff[of 2 "size_hps lx + size_hps ly + 2" "size_hps lx + size_hps ly + 3"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> real (size_hps lx); 0 \<le> real (size_hps ly)\<rbrakk> \<Longrightarrow> log 2 (1 + real (size_hps lx) + real (size_hps ly)) \<le> 1 + log 2 (1 + real (size_hps lx)) + log 2 (1 + real (size_hps ly))
\<lbrakk>1 < 2; 0 < real (size_hps lx + size_hps ly + 2); 0 < real (size_hps lx + size_hps ly + 3)\<rbrakk> \<Longrightarrow> (log 2 (real (size_hps lx + size_hps ly + 2)) \<le> log 2 (real (size_hps lx + size_hps ly + 3))) = (real (size_hps lx + size_hps ly + 2) \<le> real (size_hps lx + size_hps ly + 3))

goal (1 subgoal):
 1. \<Phi> (merge (Hp x lx) (Hp y ly)) - \<Phi> (Hp x lx) - \<Phi> (Hp y ly) \<le> log 2 (real (size_hp (Hp x lx) + size_hp (Hp y ly) + 1)) + 1
[PROOF STEP]
by (auto simp del: log_le_cancel_iff)
[PROOF STATE]
proof (state)
this:
\<Phi> (merge (Hp x lx) (Hp y ly)) - \<Phi> (Hp x lx) - \<Phi> (Hp y ly) \<le> log 2 (real (size_hp (Hp x lx) + size_hp (Hp y ly) + 1)) + 1

goal (2 subgoals):
 1. \<And>h. \<Phi> (merge h heap.Empty) - \<Phi> h - \<Phi> heap.Empty \<le> log 2 (real (size_hp h + size_hp heap.Empty + 1)) + 1
 2. \<And>v va. \<Phi> (merge heap.Empty (Hp v va)) - \<Phi> heap.Empty - \<Phi> (Hp v va) \<le> log 2 (real (size_hp heap.Empty + size_hp (Hp v va) + 1)) + 1
[PROOF STEP]
qed auto


[STATEMENT]
lemma \<Delta>\<Phi>_pass1_sum_ub: "no_Emptys hs \<Longrightarrow>
  \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs  \<le> sum_ub hs" (is "_ \<Longrightarrow> ?P hs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> sum_ub hs
[PROOF STEP]
proof (induction hs rule: sum_ub.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2. no_Emptys [h1, h2] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]
 4. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
case (3 h1 h2)
[PROOF STATE]
proof (state)
this:
no_Emptys [h1, h2]

goal (4 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2. no_Emptys [h1, h2] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]
 4. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
no_Emptys [h1, h2]
[PROOF STEP]
obtain x hsx y hsy where [simp]: "h1 = Hp x hsx" "h2 = Hp y hsy"
[PROOF STATE]
proof (prove)
using this:
no_Emptys [h1, h2]

goal (1 subgoal):
 1. (\<And>x hsx y hsy. \<lbrakk>h1 = Hp x hsx; h2 = Hp y hsy\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp (meson no_Empty.elims(2))
[PROOF STATE]
proof (state)
this:
h1 = Hp x hsx
h2 = Hp y hsy

goal (4 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2. no_Emptys [h1, h2] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]
 4. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
have 0: "\<And>x y::real. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x \<le> 2*y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> x \<le> 2 * y
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x \<le> 2 * ?y

goal (4 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2. no_Emptys [h1, h2] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]
 4. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
no_Emptys [h1, h2]

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]
[PROOF STEP]
by (auto simp add: add_increasing 0)
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 [h1, h2]) - \<Phi>_hps [h1, h2] \<le> sum_ub [h1, h2]

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
case (4 h1 h2 h3 hs)
[PROOF STATE]
proof (state)
this:
no_Emptys (h3 # hs) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h3 # hs)) - \<Phi>_hps (h3 # hs) \<le> sum_ub (h3 # hs)
no_Emptys (h1 # h2 # h3 # hs)

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
hence IH: "?P(h3#hs)"
[PROOF STATE]
proof (prove)
using this:
no_Emptys (h3 # hs) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h3 # hs)) - \<Phi>_hps (h3 # hs) \<le> sum_ub (h3 # hs)
no_Emptys (h1 # h2 # h3 # hs)

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 (h3 # hs)) - \<Phi>_hps (h3 # hs) \<le> sum_ub (h3 # hs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 (h3 # hs)) - \<Phi>_hps (h3 # hs) \<le> sum_ub (h3 # hs)

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
from "4.prems"
[PROOF STATE]
proof (chain)
picking this:
no_Emptys (h1 # h2 # h3 # hs)
[PROOF STEP]
obtain x hsx y hsy where [simp]: "h1 = Hp x hsx" "h2 = Hp y hsy"
[PROOF STATE]
proof (prove)
using this:
no_Emptys (h1 # h2 # h3 # hs)

goal (1 subgoal):
 1. (\<And>x hsx y hsy. \<lbrakk>h1 = Hp x hsx; h2 = Hp y hsy\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp (meson no_Empty.elims(2))
[PROOF STATE]
proof (state)
this:
h1 = Hp x hsx
h2 = Hp y hsy

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
from "4.prems"
[PROOF STATE]
proof (chain)
picking this:
no_Emptys (h1 # h2 # h3 # hs)
[PROOF STEP]
have s3: "size_hp h3 > 0"
[PROOF STATE]
proof (prove)
using this:
no_Emptys (h1 # h2 # h3 # hs)

goal (1 subgoal):
 1. 0 < size_hp h3
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_Emptys hsx; no_Emptys hsy; no_Empty h3; no_Emptys hs\<rbrakk> \<Longrightarrow> 0 < size_hp h3
[PROOF STEP]
using size_hp.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>size_hp ?x = ?y; \<lbrakk>?x = heap.Empty; ?y = 0\<rbrakk> \<Longrightarrow> ?P; \<And>x hs. \<lbrakk>?x = Hp x hs; ?y = size_hps hs + 1\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk>no_Emptys hsx; no_Emptys hsy; no_Empty h3; no_Emptys hs\<rbrakk> \<Longrightarrow> 0 < size_hp h3
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 < size_hp h3

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
let ?ry = "h3 # hs"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
let ?rx = "Hp y hsy # ?ry"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
let ?h = "Hp x hsx # ?rx"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
have "\<Phi>_hps(pass\<^sub>1 ?h) - \<Phi>_hps ?h
    \<le> log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry) + sum_ub ?ry"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 (Hp x hsx # Hp y hsy # h3 # hs)) - \<Phi>_hps (Hp x hsx # Hp y hsy # h3 # hs) \<le> log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) + sum_ub (h3 # hs)
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
\<Phi>_hps (pass\<^sub>1 (h3 # hs)) - \<Phi>_hps (h3 # hs) \<le> sum_ub (h3 # hs)

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 (Hp x hsx # Hp y hsy # h3 # hs)) - \<Phi>_hps (Hp x hsx # Hp y hsy # h3 # hs) \<le> log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) + sum_ub (h3 # hs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 (Hp x hsx # Hp y hsy # h3 # hs)) - \<Phi>_hps (Hp x hsx # Hp y hsy # h3 # hs) \<le> log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) + sum_ub (h3 # hs)

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 (Hp x hsx # Hp y hsy # h3 # hs)) - \<Phi>_hps (Hp x hsx # Hp y hsy # h3 # hs) \<le> log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) + sum_ub (h3 # hs)

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
have "log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry)
    \<le> 2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) - 2*log 2 (size_hps ?h)
      = log 2 ((1 + size_hps hsx + size_hps hsy)/(size_hps ?h) ) + log 2 (size_hps ?ry / size_hps ?h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) - 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) = log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
[PROOF STEP]
using s3
[PROOF STATE]
proof (prove)
using this:
0 < size_hp h3

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) - 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) = log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
[PROOF STEP]
by (simp add: log_divide)
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) - 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) = log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) - 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) = log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
have "\<dots> \<le> -2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
have "2 + \<dots>
        \<le> 2*log 2 ((1 + size_hps hsx + size_hps hsy) / size_hps ?h +  size_hps ?ry / size_hps ?h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
[PROOF STEP]
using ld_sum_inequality [of "(1 + size_hps hsx + size_hps hsy) / size_hps ?h" "(size_hps ?ry / size_hps ?h)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)); 0 < real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))\<rbrakk> \<Longrightarrow> log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + 2 \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. 2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
[PROOF STEP]
using s3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)); 0 < real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))\<rbrakk> \<Longrightarrow> log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + 2 \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
0 < size_hp h3

goal (1 subgoal):
 1. 2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
have "\<dots> \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> 0
[PROOF STEP]
by (simp add: field_simps log_divide add_pos_nonneg)
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)) + real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> 0

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 + (log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))) \<le> 0

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) + log 2 (real (size_hps (h3 # hs)) / real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) - 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2
[PROOF STEP]
have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) + 2
      \<le>  2*log 2 (size_hps ?h)"
[PROOF STATE]
proof (prove)
using this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) - 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) \<le> - 2

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) + 2 \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) + 2 \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) + 2 \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
have "log 2 (size_hps ?ry) \<le> log 2 (size_hps ?rx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (size_hps (h3 # hs))) \<le> log 2 (real (size_hps (Hp y hsy # h3 # hs)))
[PROOF STEP]
using s3
[PROOF STATE]
proof (prove)
using this:
0 < size_hp h3

goal (1 subgoal):
 1. log 2 (real (size_hps (h3 # hs))) \<le> log 2 (real (size_hps (Hp y hsy # h3 # hs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
log 2 (real (size_hps (h3 # hs))) \<le> log 2 (real (size_hps (Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) + 2 \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
log 2 (real (size_hps (h3 # hs))) \<le> log 2 (real (size_hps (Hp y hsy # h3 # hs)))
[PROOF STEP]
have "log 2 (1 + size_hps hsx + size_hps hsy) - \<dots>
      \<le>  2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2"
[PROOF STATE]
proof (prove)
using this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) + log 2 (real (size_hps (h3 # hs))) + 2 \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs)))
log 2 (real (size_hps (h3 # hs))) \<le> log 2 (real (size_hps (Hp y hsy # h3 # hs)))

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (size_hps (Hp y hsy # h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (size_hps (Hp y hsy # h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (size_hps (Hp y hsy # h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2

goal (1 subgoal):
 1. log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
log 2 (real (1 + size_hps hsx + size_hps hsy)) - log 2 (real (1 + size_hps hsy + size_hps (h3 # hs))) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2

goal (3 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
 3. \<And>h1 h2 v va. \<lbrakk>no_Emptys (v # va) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (v # va)) - \<Phi>_hps (v # va) \<le> sum_ub (v # va); no_Emptys (h1 # h2 # v # va)\<rbrakk> \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (h1 # h2 # v # va)) - \<Phi>_hps (h1 # h2 # v # va) \<le> sum_ub (h1 # h2 # v # va)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + sum_ub (h3 # hs) \<le> y + sum_ub (h3 # hs)) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (Hp x hsx # Hp y hsy # h3 # hs)) - \<Phi>_hps (Hp x hsx # Hp y hsy # h3 # hs) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2 + sum_ub (h3 # hs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + sum_ub (h3 # hs) \<le> y + sum_ub (h3 # hs)) \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 (Hp x hsx # Hp y hsy # h3 # hs)) - \<Phi>_hps (Hp x hsx # Hp y hsy # h3 # hs) \<le> 2 * log 2 (real (size_hps (Hp x hsx # Hp y hsy # h3 # hs))) - 2 * log 2 (real (size_hps (h3 # hs))) - 2 + sum_ub (h3 # hs)

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 (h1 # h2 # h3 # hs)) - \<Phi>_hps (h1 # h2 # h3 # hs) \<le> sum_ub (h1 # h2 # h3 # hs)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 (h1 # h2 # h3 # hs)) - \<Phi>_hps (h1 # h2 # h3 # hs) \<le> sum_ub (h1 # h2 # h3 # hs)

goal (2 subgoals):
 1. no_Emptys [] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 []) - \<Phi>_hps [] \<le> sum_ub []
 2. \<And>uu_. no_Emptys [uu_] \<Longrightarrow> \<Phi>_hps (pass\<^sub>1 [uu_]) - \<Phi>_hps [uu_] \<le> sum_ub [uu_]
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma \<Delta>\<Phi>_pass1: assumes "hs \<noteq> []" "no_Emptys hs"
  shows "\<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (size_hps hs) - length hs + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
have "sum_ub hs \<le> 2 * log 2 (size_hps hs) - length hs + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_ub hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hs \<noteq> []
no_Emptys hs

goal (1 subgoal):
 1. sum_ub hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
by (induct hs rule: sum_ub.induct) (auto dest: no_Empty_ge0)
[PROOF STATE]
proof (state)
this:
sum_ub hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_ub hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
using \<Delta>\<Phi>_pass1_sum_ub[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
sum_ub hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
\<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> sum_ub hs

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 hs) - \<Phi>_hps hs \<le> 2 * log 2 (real (size_hps hs)) - real (length hs) + 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_hps_pass2: "hs \<noteq> [] \<Longrightarrow> no_Emptys hs \<Longrightarrow>
  no_Empty(pass\<^sub>2 hs) & size_hps hs = size_hps(hps(pass\<^sub>2 hs))+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 hs) \<and> size_hps hs = size_hps (hps (pass\<^sub>2 hs)) + 1
[PROOF STEP]
apply(induction hs rule: \<Phi>_hps.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>[] \<noteq> []; no_Emptys []\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 []) \<and> size_hps [] = size_hps (hps (pass\<^sub>2 [])) + 1
 2. \<And>hs. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 hs) \<and> size_hps hs = size_hps (hps (pass\<^sub>2 hs)) + 1; heap.Empty # hs \<noteq> []; no_Emptys (heap.Empty # hs)\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 (heap.Empty # hs)) \<and> size_hps (heap.Empty # hs) = size_hps (hps (pass\<^sub>2 (heap.Empty # hs))) + 1
 3. \<And>x hsl hsr. \<lbrakk>\<lbrakk>hsl \<noteq> []; no_Emptys hsl\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 hsl) \<and> size_hps hsl = size_hps (hps (pass\<^sub>2 hsl)) + 1; \<lbrakk>hsr \<noteq> []; no_Emptys hsr\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 hsr) \<and> size_hps hsr = size_hps (hps (pass\<^sub>2 hsr)) + 1; Hp x hsl # hsr \<noteq> []; no_Emptys (Hp x hsl # hsr)\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 (Hp x hsl # hsr)) \<and> size_hps (Hp x hsl # hsr) = size_hps (hps (pass\<^sub>2 (Hp x hsl # hsr))) + 1
[PROOF STEP]
apply (fastforce simp: merge2 split: heap.split)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done