[STATEMENT]
lemma akra_bazzi_upper:
  obtains c6 where "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> f x \<le> c6 * f_approx x" "c6 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain c3 where c3: "\<And>x i. x \<ge> x\<^sub>1 \<Longrightarrow> i < k \<Longrightarrow> c3 * g x \<le> g_approx i x" "c3 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> c3 * g x \<le> g_approx i x; 0 < c3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule g_bounds1) blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> c3 * g ?x \<le> g_approx ?i ?x
0 < c3

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "2 / c3 > 0"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> c3 * g ?x \<le> g_approx ?i ?x
0 < c3

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

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < 2 / c3
[PROOF STEP]
obtain c6 where c6: "\<And>x. x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> f x \<le> 1/2 * (c6 * f_approx x)"
                           "c6 \<ge> 2 / c3" "c6 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < 2 / c3

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> 1 / 2 * (c6 * f_approx x); 2 / c3 \<le> c6; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule f_bounded_above) blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume x: "x \<ge> x\<^sub>0"
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "f x \<le> c6 * (1 - ln x powr (-e/2)) * f_approx x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
proof (induction x rule: akra_bazzi_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
case (base x)
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
from base
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
[PROOF STEP]
have "f x \<le> 1/2 * (c6 * f_approx x)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. f x \<le> 1 / 2 * (c6 * f_approx x)
[PROOF STEP]
by (intro c6) simp_all
[PROOF STATE]
proof (state)
this:
f x \<le> 1 / 2 * (c6 * f_approx x)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x \<le> 1 / 2 * (c6 * f_approx x)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
have "1 - ln x powr (-e/2) \<ge> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 2 \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
using asymptotics4 base
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> ?x \<Longrightarrow> 1 \<le> (1 - ln ?x powr (- e / 2)) * 2
x\<^sub>0 \<le> x
x \<le> x\<^sub>1

goal (1 subgoal):
 1. 1 / 2 \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> 1 - ln x powr (- e / 2)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
hence "(1 - ln x powr (-e/2)) * (c6 * f_approx x) \<ge> 1/2 * (c6 * f_approx x)"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> 1 - ln x powr (- e / 2)

goal (1 subgoal):
 1. 1 / 2 * (c6 * f_approx x) \<le> (1 - ln x powr (- e / 2)) * (c6 * f_approx x)
[PROOF STEP]
using c6 f_approx_nonneg base x0_ge_1
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> 1 - ln x powr (- e / 2)
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> f_approx ?x
x\<^sub>0 \<le> x
x \<le> x\<^sub>1
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. 1 / 2 * (c6 * f_approx x) \<le> (1 - ln x powr (- e / 2)) * (c6 * f_approx x)
[PROOF STEP]
by (intro mult_right_mono mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
1 / 2 * (c6 * f_approx x) \<le> (1 - ln x powr (- e / 2)) * (c6 * f_approx x)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
 2. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f x \<le> (1 - ln x powr (- e / 2)) * (c6 * f_approx x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f x \<le> (1 - ln x powr (- e / 2)) * (c6 * f_approx x)

goal (1 subgoal):
 1. f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
case (rec x)
[PROOF STATE]
proof (state)
this:
x\<^sub>1 < x
?i < k \<Longrightarrow> f (bs ! ?i * x + (hs ! ?i) x) \<le> c6 * (1 - ln (bs ! ?i * x + (hs ! ?i) x) powr (- e / 2)) * f_approx (bs ! ?i * x + (hs ! ?i) x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
let ?a = "\<lambda>i. as!i" and ?b = "\<lambda>i. bs!i" and ?h = "\<lambda>i. hs!i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
let ?int = "integral (\<lambda>u. g u / u powr (p+1)) x\<^sub>0 x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
let ?int1 = "\<lambda>i. integral (\<lambda>u. g u / u powr (p+1)) x\<^sub>0 (?b i*x+?h i x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
let ?int2 = "\<lambda>i. integral (\<lambda>u. g u / u powr (p+1)) (?b i*x+?h i x) x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
let ?l = "ln x powr (-e/2)" and ?l' = "\<lambda>i. ln (?b i*x + ?h i x) powr (-e/2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
from rec and x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
?i < k \<Longrightarrow> f (bs ! ?i * x + (hs ! ?i) x) \<le> c6 * (1 - ln (bs ! ?i * x + (hs ! ?i) x) powr (- e / 2)) * f_approx (bs ! ?i * x + (hs ! ?i) x)
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have x: "x \<ge> x\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
?i < k \<Longrightarrow> f (bs ! ?i * x + (hs ! ?i) x) \<le> c6 * (1 - ln (bs ! ?i * x + (hs ! ?i) x) powr (- e / 2)) * f_approx (bs ! ?i * x + (hs ! ?i) x)
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
with x0_pos
[PROOF STATE]
proof (chain)
picking this:
0 < x\<^sub>0
x\<^sub>0 \<le> x
[PROOF STEP]
have x_pos: "x > 0" and x_nonneg: "x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < x\<^sub>0
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. 0 < x &&& 0 \<le> x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < x
0 \<le> x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
from c6 c3
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> c3 * g ?x \<le> g_approx ?i ?x
0 < c3
[PROOF STEP]
have "c6 * c3 \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> c3 * g ?x \<le> g_approx ?i ?x
0 < c3

goal (1 subgoal):
 1. 2 \<le> c6 * c3
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
2 \<le> c6 * c3

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
have "f x = (\<Sum>i<k. ?a i * f (?b i*x + ?h i x)) + g x" (is "_ = ?sum + _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x
[PROOF STEP]
using f_rec[of x] rec.hyps x0_le_x1
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x \<Longrightarrow> f x = g x + (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x))
x\<^sub>1 < x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. f x = (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x = (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x = (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
have "?sum \<le> (\<Sum>i<k. (?a i*?b i powr p) * (c6*x powr p*(1 - ?l)*(1 + ?int - c3*g x/x powr p)))" (is "_ \<le> ?sum'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) \<le> (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p)))
[PROOF STEP]
proof (rule sum_mono, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
assume i: "i < k"
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
from rec.hyps i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
i < k
[PROOF STEP]
have "x\<^sub>0 < bs ! i * x + (hs ! i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by (intro x0_hb_bound7) simp_all
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
hence "1 + ?int1 i \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. 1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (intro f_approx_aux x0_hb_bound7) simp_all
[PROOF STATE]
proof (state)
this:
1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
hence int_nonneg: "1 + ?int1 i \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. 0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> 1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
have l_le_1: "ln x powr -(e/2) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln x powr - (e / 2) \<le> 1
[PROOF STEP]
using asymptotics3[OF x]
[PROOF STATE]
proof (prove)
using this:
(1 + ln x powr (- e / 2)) / 2 \<le> 1

goal (1 subgoal):
 1. ln x powr - (e / 2) \<le> 1
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
ln x powr - (e / 2) \<le> 1

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < k
[PROOF STEP]
have "f (?b i*x + ?h i x) \<le> c6 * (1 - ?l' i) * f_approx (?b i*x + ?h i x)"
[PROOF STATE]
proof (prove)
using this:
i < k

goal (1 subgoal):
 1. f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)
[PROOF STEP]
by (rule rec.IH)
[PROOF STATE]
proof (state)
this:
f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
hence "?a i * f (?b i*x + ?h i x) \<le> ?a i * ..."
[PROOF STATE]
proof (prove)
using this:
f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)

goal (1 subgoal):
 1. as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))
[PROOF STEP]
using a_ge_0 i
[PROOF STATE]
proof (prove)
using this:
f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
i < k

goal (1 subgoal):
 1. as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))
[PROOF STEP]
by (intro mult_left_mono) simp_all
[PROOF STATE]
proof (state)
this:
as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
have "... = (c6*?a i*(1 + ?int1 i)) * ((?b i*x + ?h i x) powr p * (1 - ?l' i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)) = c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))
[PROOF STEP]
unfolding f_approx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * ((bs ! i * x + (hs ! i) x) powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)))) = c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)) = c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
as ! i * (c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)) = c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
from i rec.hyps c6 a_ge_0
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 < x
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
[PROOF STEP]
have "... \<le> (c6*?a i*(1 + ?int1 i)) * ((?b i*x) powr p * (1 - ?l))"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 < x
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
?a \<in> set as \<Longrightarrow> 0 \<le> ?a

goal (1 subgoal):
 1. c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2))) \<le> c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 - ln x powr (- e / 2)))
[PROOF STEP]
by (intro mult_left_mono asymptotics2' mult_nonneg_nonneg int_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2))) \<le> c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 - ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2))) \<le> c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 - ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
have "... = (1 + ?int1 i) * (c6*?a i*(?b i*x) powr p * (1 - ?l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 - ln x powr (- e / 2))) = (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 - ln x powr (- e / 2))) = (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c6 * as ! i * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * ((bs ! i * x) powr p * (1 - ln x powr (- e / 2))) = (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
from rec.hyps i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
i < k
[PROOF STEP]
have "x\<^sub>0 < bs ! i * x + (hs ! i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k

goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by (intro x0_hb_bound7) simp_all
[PROOF STATE]
proof (state)
this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
hence "?int1 i = ?int - ?int2 i"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x) = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
apply (subst eq_diff_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x \<Longrightarrow> integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x) + integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x
[PROOF STEP]
apply (intro integral_combine akra_bazzi_integrable)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. x\<^sub>0 < bs ! i * x + (hs ! i) x \<Longrightarrow> x\<^sub>0 \<le> bs ! i * x + (hs ! i) x
 2. x\<^sub>0 < bs ! i * x + (hs ! i) x \<Longrightarrow> bs ! i * x + (hs ! i) x \<le> x
 3. x\<^sub>0 < bs ! i * x + (hs ! i) x \<Longrightarrow> x\<^sub>0 \<le> x\<^sub>0
 4. x\<^sub>0 < bs ! i * x + (hs ! i) x \<Longrightarrow> x\<^sub>0 \<le> x
[PROOF STEP]
apply (insert rec.hyps step_le_x[OF i, of x], simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x) = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 (bs ! i * x + (hs ! i) x) = integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
from rec.hyps i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 < x
i < k
[PROOF STEP]
have "c3 * g x \<le> g_approx i x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 < x
i < k

goal (1 subgoal):
 1. c3 * g x \<le> g_approx i x
[PROOF STEP]
by (intro c3) simp_all
[PROOF STATE]
proof (state)
this:
c3 * g x \<le> g_approx i x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
hence "?int2 i \<ge> c3*g x/x powr p"
[PROOF STATE]
proof (prove)
using this:
c3 * g x \<le> g_approx i x

goal (1 subgoal):
 1. c3 * g x / x powr p \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
unfolding g_approx_def
[PROOF STATE]
proof (prove)
using this:
c3 * g x \<le> x powr p * integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. c3 * g x / x powr p \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
c3 * g x \<le> x powr p * integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
0 < x

goal (1 subgoal):
 1. c3 * g x / x powr p \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
c3 * g x / x powr p \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
hence "(1 + (?int - ?int2 i)) * (c6*?a i*(?b i*x) powr p * (1 - ?l)) \<le>
             (1 + ?int - c3*g x/x powr p) * (c6*?a i*(?b i*x) powr p * (1 - ?l))"
[PROOF STATE]
proof (prove)
using this:
c3 * g x / x powr p \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. (1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) \<le> (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))
[PROOF STEP]
using i c6 a_ge_0 l_le_1
[PROOF STATE]
proof (prove)
using this:
c3 * g x / x powr p \<le> integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x
i < k
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
ln x powr - (e / 2) \<le> 1

goal (1 subgoal):
 1. (1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) \<le> (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))
[PROOF STEP]
by (intro mult_right_mono mult_nonneg_nonneg) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
(1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) \<le> (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 + (integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x)) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) \<le> (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2)))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
have "... = (?a i*?b i powr p) * (c6*x powr p*(1 - ?l) * (1 + ?int - c3*g x/x powr p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) = as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
using b_pos[of "bs!i"] x x0_pos i
[PROOF STATE]
proof (prove)
using this:
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
x\<^sub>0 \<le> x
0 < x\<^sub>0
i < k

goal (1 subgoal):
 1. (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) = as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
by (subst powr_mult) (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) * (c6 * as ! i * (bs ! i * x) powr p * (1 - ln x powr (- e / 2))) = as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
show "?a i * f (?b i*x + ?h i x) \<le> ..."
[PROOF STATE]
proof (prove)
using this:
as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))

goal (1 subgoal):
 1. as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
as ! i * f (bs ! i * x + (hs ! i) x) \<le> as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) \<le> (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
hence "?sum + g x \<le> ?sum' + g x"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) \<le> (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p)))

goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x \<le> (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))) + g x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x \<le> (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * f (bs ! i * x + (hs ! i) x)) + g x \<le> (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
have "... = c6 * x powr p * (1 - ?l) * (1 + ?int - c3*g x/x powr p) + g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))) + g x = c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x
[PROOF STEP]
by (simp add: sum_distrib_right[symmetric] p_props)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))) + g x = c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * bs ! i powr p * (c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p))) + g x = c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
have "... = c6 * (1 - ?l) * f_approx x - (c6*c3*(1 - ?l) - 1) * g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x = c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x
[PROOF STEP]
unfolding f_approx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x = c6 * (1 - ln x powr (- e / 2)) * (x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x)) - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x = c6 * (1 - ln x powr (- e / 2)) * (x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x)) - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x = c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x = c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c6 * x powr p * (1 - ln x powr (- e / 2)) * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x - c3 * g x / x powr p) + g x = c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
from c6 c3
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> c3 * g ?x \<le> g_approx ?i ?x
0 < c3
[PROOF STEP]
have "c6*c3 \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k\<rbrakk> \<Longrightarrow> c3 * g ?x \<le> g_approx ?i ?x
0 < c3

goal (1 subgoal):
 1. 2 \<le> c6 * c3
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
2 \<le> c6 * c3

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
2 \<le> c6 * c3

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
have "(1 - ?l) \<ge> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 2 \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
using asymptotics4[OF x]
[PROOF STATE]
proof (prove)
using this:
1 \<le> (1 - ln x powr (- e / 2)) * 2

goal (1 subgoal):
 1. 1 / 2 \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> 1 - ln x powr (- e / 2)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
2 \<le> c6 * c3
1 / 2 \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
have "c6*c3*(1 - ?l) \<ge> 2 * (1/2)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> c6 * c3
1 / 2 \<le> 1 - ln x powr (- e / 2)

goal (1 subgoal):
 1. 2 * (1 / 2) \<le> c6 * c3 * (1 - ln x powr (- e / 2))
[PROOF STEP]
by (intro mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
2 * (1 / 2) \<le> c6 * c3 * (1 - ln x powr (- e / 2))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
with x x_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
0 < x
2 * (1 / 2) \<le> c6 * c3 * (1 - ln x powr (- e / 2))
[PROOF STEP]
have "(c6*c3*(1 - ?l) - 1) * g x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
0 < x
2 * (1 / 2) \<le> c6 * c3 * (1 - ln x powr (- e / 2))

goal (1 subgoal):
 1. 0 \<le> (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x
[PROOF STEP]
by (intro mult_nonneg_nonneg g_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
hence "c6 * (1 - ?l) * f_approx x - (c6*c3*(1 - ?l) - 1) * g x \<le>
                  c6 * (1 - ?l) * f_approx x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x

goal (1 subgoal):
 1. c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c6 * (1 - ln x powr (- e / 2)) * f_approx x - (c6 * c3 * (1 - ln x powr (- e / 2)) - 1) * g x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x\<^sub>1 < x; \<And>i. i < k \<Longrightarrow> f (bs ! i * x + (hs ! i) x) \<le> c6 * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) * f_approx (bs ! i * x + (hs ! i) x)\<rbrakk> \<Longrightarrow> f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x \<le> c6 * (1 - ln x powr (- e / 2)) * f_approx x

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x c6
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6
[PROOF STEP]
have "... \<le> c6 * 1 * f_approx x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
\<lbrakk>x\<^sub>0 \<le> ?x; ?x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> f ?x \<le> 1 / 2 * (c6 * f_approx ?x)
2 / c3 \<le> c6
0 < c6

goal (1 subgoal):
 1. c6 * (1 - ln x powr (- e / 2)) * f_approx x \<le> c6 * 1 * f_approx x
[PROOF STEP]
by (intro mult_left_mono mult_right_mono f_approx_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
c6 * (1 - ln x powr (- e / 2)) * f_approx x \<le> c6 * 1 * f_approx x

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f x \<le> c6 * 1 * f_approx x
[PROOF STEP]
have "f x \<le> c6 * f_approx x"
[PROOF STATE]
proof (prove)
using this:
f x \<le> c6 * 1 * f_approx x

goal (1 subgoal):
 1. f x \<le> c6 * f_approx x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x \<le> c6 * f_approx x

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> ?x2 \<Longrightarrow> f ?x2 \<le> c6 * f_approx ?x2

goal (1 subgoal):
 1. (\<And>c6. \<lbrakk>\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x; 0 < c6\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this and c6(3)
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> ?x2 \<Longrightarrow> f ?x2 \<le> c6 * f_approx ?x2
0 < c6
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> ?x2 \<Longrightarrow> f ?x2 \<le> c6 * f_approx ?x2
0 < c6

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma akra_bazzi_bigo:
  "f \<in> O(\<lambda>x. x powr p *(1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> O(\<lambda>x. x powr p * (1 + integral (\<lambda>u. g u / u powr (p + 1)) x\<^sub>0 x))
[PROOF STEP]
apply (fold f_approx_def, rule akra_bazzi_upper, erule landau_o.bigI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c6. (\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x) \<Longrightarrow> \<forall>\<^sub>F x in at_top. norm (f x) \<le> c6 * norm (f_approx x)
[PROOF STEP]
apply (subst eventually_at_top_linorder, rule exI[of _ x\<^sub>0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c6. (\<And>x. x\<^sub>0 \<le> x \<Longrightarrow> f x \<le> c6 * f_approx x) \<Longrightarrow> \<forall>n\<ge>x\<^sub>0. norm (f n) \<le> c6 * norm (f_approx n)
[PROOF STEP]
apply (simp add: f_nonneg f_approx_nonneg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma num_inner_nodes_gr_0:"#:c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < #:c
[PROOF STEP]
by(induct c) auto


[STATEMENT]
lemma [dest]:"#:c = 0 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #:c = 0 \<Longrightarrow> False
[PROOF STEP]
by(induct c) auto


[STATEMENT]
lemma lookup_Mapping_code [code]:
  "Mapping.lookup (Assoc_List_Mapping al) = DAList.lookup al"
  "Mapping.lookup (RBT_Mapping t) = RBT_Mapping2.lookup t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Assoc_List_Mapping al) = DAList.lookup al &&& Mapping.lookup (RBT_Mapping t) = RBT_Mapping2.lookup t
[PROOF STEP]
by(simp_all)(transfer, rule)+


[STATEMENT]
lemma is_empty_transfer [transfer_rule]:
  includes lifting_syntax
  shows "(pcr_mapping (=) (=) ===> (=)) (\<lambda>m. m = Map.empty) Mapping.is_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pcr_mapping (=) (=) ===> (=)) (\<lambda>m. m = Map.empty) Mapping.is_empty
[PROOF STEP]
unfolding mapping.pcr_cr_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_mapping ===> (=)) (\<lambda>m. m = Map.empty) Mapping.is_empty
[PROOF STEP]
apply(rule rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. cr_mapping x y \<Longrightarrow> (x = Map.empty) = Mapping.is_empty y
[PROOF STEP]
apply(case_tac y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y ya. \<lbrakk>cr_mapping x y; y = Mapping ya; ya \<in> UNIV\<rbrakk> \<Longrightarrow> (x = Map.empty) = Mapping.is_empty y
[PROOF STEP]
apply(simp add: Mapping.is_empty_def cr_mapping_def Mapping_inverse Mapping.keys.rep_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_empty_Mapping [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.is_empty (Assoc_List_Mapping al) \<longleftrightarrow> al = DAList.empty"
  "Mapping.is_empty (RBT_Mapping t) \<longleftrightarrow>
  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''is_empty RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.is_empty (RBT_Mapping t))
                     | Some _ \<Rightarrow> RBT_Mapping2.is_empty t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.is_empty (Assoc_List_Mapping al) = (al = DAList.empty) &&& Mapping.is_empty (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''is_empty RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.is_empty (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping2.is_empty t)
[PROOF STEP]
apply(simp_all split: option.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Mapping.is_empty (Mapping (DAList.lookup al)) = (al = DAList.empty)
 2. (\<exists>x2. ID ccompare = Some x2) \<longrightarrow> Mapping.is_empty (Mapping (RBT_Mapping2.lookup t)) = (t = RBT_Mapping2.empty)
[PROOF STEP]
apply(transfer, case_tac al, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x2. ID ccompare = Some x2) \<longrightarrow> Mapping.is_empty (Mapping (RBT_Mapping2.lookup t)) = (t = RBT_Mapping2.empty)
[PROOF STEP]
apply(transfer, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma update_Mapping [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.update k v (Mapping m) = Mapping (m(k \<mapsto> v))"
  "Mapping.update k v (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.update k v al)"
  "Mapping.update k v (RBT_Mapping t) =
  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''update RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.update k v (RBT_Mapping t))
                     | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.insert k v t))" (is ?RBT)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.update k v (Mapping m) = Mapping (m(k \<mapsto> v)) &&& Mapping.update k v (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.update k v al) &&& Mapping.update k v (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''update RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.update k v (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.insert k v t))
[PROOF STEP]
by(simp_all split: option.split)(transfer, simp)+


[STATEMENT]
lemma delete_Mapping [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.delete k (Mapping m) = Mapping (m(k := None))"
  "Mapping.delete k (Assoc_List_Mapping al) = Assoc_List_Mapping (AssocList.delete k al)"
  "Mapping.delete k (RBT_Mapping t) =
  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''delete RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.delete k (RBT_Mapping t))
                     | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.delete k t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.delete k (Mapping m) = Mapping (m(k := None)) &&& Mapping.delete k (Assoc_List_Mapping al) = Assoc_List_Mapping (AssocList.delete k al) &&& Mapping.delete k (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''delete RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.delete k (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.delete k t))
[PROOF STEP]
by(simp_all split: option.split)(transfer, simp)+


[STATEMENT]
theorem rbt_comp_lookup_map_const: "rbt_comp_lookup c (RBT_Impl.map (\<lambda>_. f) t) = map_option f \<circ> rbt_comp_lookup c t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbt_comp_lookup c (RBT_Impl.map (\<lambda>_. f) t) = map_option f \<circ> rbt_comp_lookup c t
[PROOF STEP]
by(induct t)(auto simp: fun_eq_iff split: order.split)


[STATEMENT]
lemma keys_Mapping [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.keys (Mapping m) = Collect (\<lambda>k. m k \<noteq> None)" (is "?Mapping")
  "Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al" (is "?Assoc_List")
  "Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)" (is "?RBT")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (Mapping m) = {k. m k \<noteq> None} &&& Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al &&& Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Mapping.keys (Mapping m) = {k. m k \<noteq> None}
 2. Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al
 3. Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)
[PROOF STEP]
show ?Mapping
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (Mapping m) = {k. m k \<noteq> None}
[PROOF STEP]
by transfer auto
[PROOF STATE]
proof (state)
this:
Mapping.keys (Mapping m) = {k. m k \<noteq> None}

goal (2 subgoals):
 1. Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al
 2. Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)
[PROOF STEP]
show ?Assoc_List
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al
[PROOF STEP]
by simp(transfer, auto intro: rev_image_eqI)
[PROOF STATE]
proof (state)
this:
Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al

goal (1 subgoal):
 1. Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)
[PROOF STEP]
show ?RBT
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)
[PROOF STEP]
by(simp add: RBT_set_def, transfer, auto simp add: rbt_comp_lookup_map_const o_def)
[PROOF STATE]
proof (state)
this:
Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_Mapping [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.size (Assoc_List_Mapping al) = size al"
  "Mapping.size (RBT_Mapping t) =
  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''size RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.size (RBT_Mapping t))
                     | Some _ \<Rightarrow> length (RBT_Mapping2.entries t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.size (Assoc_List_Mapping al) = size al &&& Mapping.size (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''size RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.size (RBT_Mapping t)) | Some x \<Rightarrow> length (RBT_Mapping2.entries t))
[PROOF STEP]
apply(simp_all split: option.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Mapping.size (Mapping (DAList.lookup al)) = size al
 2. (\<exists>x2. ID ccompare = Some x2) \<longrightarrow> Mapping.size (Mapping (RBT_Mapping2.lookup t)) = length (RBT_Mapping2.entries t)
[PROOF STEP]
apply(transfer, simp add: dom_map_of_conv_image_fst set_map[symmetric] distinct_card del: set_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x2. ID ccompare = Some x2) \<longrightarrow> Mapping.size (Mapping (RBT_Mapping2.lookup t)) = length (RBT_Mapping2.entries t)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. ord.is_rbt cless t \<or> ID ccompare = None \<Longrightarrow> (\<exists>x2. ID ccompare = Some x2) \<longrightarrow> (card \<circ> dom) (rbt_comp_lookup ccomp t) = length (RBT_Impl.entries t)
[PROOF STEP]
apply(clarsimp simp add: size_eq_card_dom_lookup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t x2. \<lbrakk>ord.is_rbt (lt_of_comp x2) t; ID ccompare = Some x2\<rbrakk> \<Longrightarrow> card (dom (ord.rbt_lookup (lt_of_comp x2) t)) = length (RBT_Impl.entries t)
[PROOF STEP]
apply(simp add: linorder.rbt_lookup_keys[OF ID_ccompare] ord.is_rbt_rbt_sorted RBT_Impl.keys_def distinct_card linorder.distinct_entries[OF ID_ccompare] del: set_map)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma filter_code [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.filter P (Mapping m) = Mapping (\<lambda>k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None)"
  "Mapping.filter P (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.filter (\<lambda>(k, v). P k v) al)"
  "Mapping.filter P (RBT_Mapping t) =
  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''filter RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.filter P (RBT_Mapping t))
                         | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.filter (\<lambda>(k, v). P k v) t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.filter P (Mapping m) = Mapping (\<lambda>k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None) &&& Mapping.filter P (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.filter (\<lambda>(k, v). P k v) al) &&& Mapping.filter P (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''filter RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.filter P (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.filter (\<lambda>(k, v). P k v) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.filter P (Mapping m) = Mapping (\<lambda>k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None)
[PROOF STEP]
by transfer simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Mapping.filter P (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.filter (\<lambda>(k, v). P k v) al)
 2. Mapping.filter P (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''filter RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.filter P (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.filter (\<lambda>(k, v). P k v) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.filter P (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.filter (\<lambda>(k, v). P k v) al)
[PROOF STEP]
by (simp, transfer)(simp add: map_of_filter_apply fun_eq_iff cong: if_cong option.case_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.filter P (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''filter RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.filter P (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.filter (\<lambda>(k, v). P k v) t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.filter P (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''filter RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.filter P (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.filter (\<lambda>(k, v). P k v) t))
[PROOF STEP]
by(clarsimp simp add: Mapping_inject Mapping.filter.abs_eq fun_eq_iff split: option.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_values_code [code]:
  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
  "Mapping.map_values f (Mapping m) = Mapping (\<lambda>k. map_option (f k) (m k))"
  "Mapping.map_values f (Assoc_List_Mapping al) = Assoc_List_Mapping (AssocList.map_values f al)"
  "Mapping.map_values f (RBT_Mapping t) =
  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''map_values RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.map_values f (RBT_Mapping t))
                         | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.map f t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.map_values f (Mapping m) = Mapping (\<lambda>k. map_option (f k) (m k)) &&& Mapping.map_values f (Assoc_List_Mapping al) = Assoc_List_Mapping (map_values f al) &&& Mapping.map_values f (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''map_values RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.map_values f (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.map f t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.map_values f (Mapping m) = Mapping (\<lambda>k. map_option (f k) (m k))
[PROOF STEP]
by transfer simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Mapping.map_values f (Assoc_List_Mapping al) = Assoc_List_Mapping (map_values f al)
 2. Mapping.map_values f (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''map_values RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.map_values f (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.map f t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.map_values f (Assoc_List_Mapping al) = Assoc_List_Mapping (map_values f al)
[PROOF STEP]
by(simp, transfer)(simp add: fun_eq_iff map_of_map')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.map_values f (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''map_values RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.map_values f (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.map f t))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.map_values f (RBT_Mapping t) = (case ID ccompare of None \<Rightarrow> Code.abort STR ''map_values RBT_Mapping: ccompare = None'' (\<lambda>_. Mapping.map_values f (RBT_Mapping t)) | Some x \<Rightarrow> RBT_Mapping (RBT_Mapping2.map f t))
[PROOF STEP]
by(clarsimp simp add: Mapping_inject Mapping.map_values.abs_eq fun_eq_iff split: option.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code]:
  fixes x :: mapping_impl
  shows "size x = 0"
  and "size_mapping_impl x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size x = 0 &&& size_mapping_impl x = 0
[PROOF STEP]
by(case_tac [!] x) simp_all


[STATEMENT]
lemma mapping_empty_choose_code [code]:
  "(mapping_empty_choose :: ('a :: ccompare, 'b) mapping) =
   (case ID CCOMPARE('a) of Some _  \<Rightarrow> RBT_Mapping RBT_Mapping2.empty
    | None \<Rightarrow> Assoc_List_Mapping DAList.empty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_empty_choose = (case ID ccompare of None \<Rightarrow> Assoc_List_Mapping DAList.empty | Some x \<Rightarrow> RBT_Mapping RBT_Mapping2.empty)
[PROOF STEP]
by(auto split: option.split simp add: DAList.lookup_empty[abs_def] Mapping.empty_def)


[STATEMENT]
lemma mapping_impl_choose2_code [code]:
  "mapping_impl_choose2 x y = mapping_Choose"
  "mapping_impl_choose2 mapping_Mapping mapping_Mapping = mapping_Mapping"
  "mapping_impl_choose2 mapping_Assoc_List mapping_Assoc_List = mapping_Assoc_List"
  "mapping_impl_choose2 mapping_RBT mapping_RBT = mapping_RBT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mapping_impl_choose2 x y = mapping_Choose &&& mapping_impl_choose2 mapping_Mapping mapping_Mapping = mapping_Mapping) &&& mapping_impl_choose2 mapping_Assoc_List mapping_Assoc_List = mapping_Assoc_List &&& mapping_impl_choose2 mapping_RBT mapping_RBT = mapping_RBT
[PROOF STEP]
by(simp_all)


[STATEMENT]
lemma mapping_empty_code [code]:
  "mapping_empty mapping_Choose = mapping_empty_choose"
  "mapping_empty mapping_Mapping = Mapping (\<lambda>_. None)"
  "mapping_empty mapping_Assoc_List = Assoc_List_Mapping DAList.empty"
  "mapping_empty mapping_RBT = RBT_Mapping RBT_Mapping2.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mapping_empty mapping_Choose = mapping_empty_choose &&& mapping_empty mapping_Mapping = Mapping Map.empty) &&& mapping_empty mapping_Assoc_List = Assoc_List_Mapping DAList.empty &&& mapping_empty mapping_RBT = RBT_Mapping RBT_Mapping2.empty
[PROOF STEP]
by(simp_all add: Mapping.empty_def DAList.lookup_empty[abs_def])


[STATEMENT]
lemma Mapping_empty_code [code, code_unfold]:
  "(Mapping.empty :: ('a :: mapping_impl, 'b) mapping) =
   mapping_empty (of_phantom MAPPING_IMPL('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.empty = mapping_empty (of_phantom mapping_impl)
[PROOF STEP]
by simp


[STATEMENT]
lemma bulkload_code [code]:
  "Mapping.bulkload vs = RBT_Mapping (RBT_Mapping2.bulkload (zip_with_index vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.bulkload vs = RBT_Mapping (RBT_Mapping2.bulkload (zip_with_index vs))
[PROOF STEP]
by(simp add: Mapping.bulkload.abs_eq Mapping_inject ccompare_nat_def ID_def fun_eq_iff)


[STATEMENT]
lemma hmsetmset_inject[simp]: "hmsetmset A = hmsetmset B \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hmsetmset A = hmsetmset B) = (A = B)
[PROOF STEP]
by (blast intro: hmultiset.expand)


[STATEMENT]
lemma HMSet_alt: "HMSet = Abs_hmultiset o MSet o image_mset Rep_hmultiset"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMSet = Hereditary_Multiset.Abs_hmultiset \<circ> MSet \<circ> image_mset Hereditary_Multiset.Rep_hmultiset
[PROOF STEP]
by (auto simp: type_definition.Rep_inverse[OF type_definition_hmultiset])


[STATEMENT]
lemma HMSet_transfer[transfer_rule]: "rel_fun (rel_mset pcr_hmultiset) pcr_hmultiset MSet HMSet"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_mset pcr_hmultiset) pcr_hmultiset MSet HMSet
[PROOF STEP]
unfolding HMSet_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_mset pcr_hmultiset) pcr_hmultiset MSet (Hereditary_Multiset.Abs_hmultiset \<circ> MSet \<circ> image_mset Hereditary_Multiset.Rep_hmultiset)
[PROOF STEP]
by (force simp: rel_fun_def multiset.in_rel nmultiset.rel_eq
    pcr_hmultiset_def cr_hmultiset_def
    type_definition.Rep_inverse[OF type_definition_hmultiset] intro!: multiset.map_cong)


[STATEMENT]
lemma less_HMSet_iff_less_multiset_ext\<^sub>D\<^sub>M: "HMSet M < HMSet N \<longleftrightarrow> less_multiset_ext\<^sub>D\<^sub>M (<) M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HMSet M < HMSet N) = less_multiset_ext\<^sub>D\<^sub>M (<) M N
[PROOF STEP]
unfolding less_multiset_ext\<^sub>D\<^sub>M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HMSet M < HMSet N) = (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))
[PROOF STEP]
proof (transfer, unfold less_nmultiset.simps less_multiset_ext\<^sub>D\<^sub>M_def, safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; X \<noteq> {#}; X \<subseteq># N; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa\<in>Collect (pred_mset no_elem). \<exists>Ya\<in>Collect (pred_mset no_elem). Xa \<noteq> {#} \<and> filter_mset no_elem Xa \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k\<in>Collect no_elem. k \<in># Ya \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># Xa \<and> k < a))
 2. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
fix M N :: "unit nmultiset multiset" and X Y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; X \<noteq> {#}; X \<subseteq># N; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa\<in>Collect (pred_mset no_elem). \<exists>Ya\<in>Collect (pred_mset no_elem). Xa \<noteq> {#} \<and> filter_mset no_elem Xa \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k\<in>Collect no_elem. k \<in># Ya \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># Xa \<and> k < a))
 2. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
assume *: "pred_mset no_elem (N - X + Y)" "pred_mset no_elem N" "X \<noteq> {#}"
    "X \<subseteq># N" "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
[PROOF STATE]
proof (state)
this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
X \<noteq> {#}
X \<subseteq># N
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)

goal (2 subgoals):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; X \<noteq> {#}; X \<subseteq># N; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa\<in>Collect (pred_mset no_elem). \<exists>Ya\<in>Collect (pred_mset no_elem). Xa \<noteq> {#} \<and> filter_mset no_elem Xa \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k\<in>Collect no_elem. k \<in># Ya \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># Xa \<and> k < a))
 2. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
X \<noteq> {#}
X \<subseteq># N
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)
[PROOF STEP]
have "X \<in> Collect (pred_mset no_elem)"
[PROOF STATE]
proof (prove)
using this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
X \<noteq> {#}
X \<subseteq># N
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)

goal (1 subgoal):
 1. X \<in> Collect (pred_mset no_elem)
[PROOF STEP]
unfolding multiset.pred_set mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
Multiset.Ball (N - X + Y) no_elem
Multiset.Ball N no_elem
X \<noteq> {#}
X \<subseteq># N
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)

goal (1 subgoal):
 1. Multiset.Ball X no_elem
[PROOF STEP]
by (metis rev_subsetD set_mset_mono)
[PROOF STATE]
proof (state)
this:
X \<in> Collect (pred_mset no_elem)

goal (2 subgoals):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; X \<noteq> {#}; X \<subseteq># N; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa\<in>Collect (pred_mset no_elem). \<exists>Ya\<in>Collect (pred_mset no_elem). Xa \<noteq> {#} \<and> filter_mset no_elem Xa \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k\<in>Collect no_elem. k \<in># Ya \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># Xa \<and> k < a))
 2. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
from *(1)
[PROOF STATE]
proof (chain)
picking this:
pred_mset no_elem (N - X + Y)
[PROOF STEP]
have "Y \<in> Collect (pred_mset no_elem)"
[PROOF STATE]
proof (prove)
using this:
pred_mset no_elem (N - X + Y)

goal (1 subgoal):
 1. Y \<in> Collect (pred_mset no_elem)
[PROOF STEP]
unfolding multiset.pred_set mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
Multiset.Ball (N - X + Y) no_elem

goal (1 subgoal):
 1. Multiset.Ball Y no_elem
[PROOF STEP]
by (metis add_diff_cancel_left' in_diffD)
[PROOF STATE]
proof (state)
this:
Y \<in> Collect (pred_mset no_elem)

goal (2 subgoals):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; X \<noteq> {#}; X \<subseteq># N; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa\<in>Collect (pred_mset no_elem). \<exists>Ya\<in>Collect (pred_mset no_elem). Xa \<noteq> {#} \<and> filter_mset no_elem Xa \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k\<in>Collect no_elem. k \<in># Ya \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># Xa \<and> k < a))
 2. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
show
    "\<exists>X'\<in>Collect (pred_mset no_elem). \<exists>Y'\<in>Collect (pred_mset no_elem).
      X' \<noteq> {#} \<and> filter_mset no_elem X' \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - X' + Y' \<and>
      (\<forall>k\<in>Collect no_elem. k \<in># Y' \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X' \<and> k < a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X'\<in>Collect (pred_mset no_elem). \<exists>Y'\<in>Collect (pred_mset no_elem). X' \<noteq> {#} \<and> filter_mset no_elem X' \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - X' + Y' \<and> (\<forall>k\<in>Collect no_elem. k \<in># Y' \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X' \<and> k < a))
[PROOF STEP]
by (rule bexI[OF _ \<open>X \<in> Collect (pred_mset no_elem)\<close>],
        rule bexI[OF _ \<open>Y \<in> Collect (pred_mset no_elem)\<close>])
      (insert *; force simp: set_mset_diff multiset.pred_set multiset_filter_mono)
[PROOF STATE]
proof (state)
this:
\<exists>X'\<in>Collect (pred_mset no_elem). \<exists>Y'\<in>Collect (pred_mset no_elem). X' \<noteq> {#} \<and> filter_mset no_elem X' \<subseteq># filter_mset no_elem N \<and> N - X + Y = N - X' + Y' \<and> (\<forall>k\<in>Collect no_elem. k \<in># Y' \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X' \<and> k < a))

goal (1 subgoal):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
fix M N :: "unit nmultiset multiset" and X Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
assume *:
    "pred_mset no_elem (N - X + Y)" "pred_mset no_elem N" "pred_mset no_elem X" "pred_mset no_elem Y"
    "X \<noteq> {#}" "filter_mset no_elem X \<subseteq># filter_mset no_elem N"
    "\<forall>k\<in>Collect no_elem.  k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)"
[PROOF STATE]
proof (state)
this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
pred_mset no_elem X
pred_mset no_elem Y
X \<noteq> {#}
filter_mset no_elem X \<subseteq># filter_mset no_elem N
\<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)

goal (1 subgoal):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
pred_mset no_elem X
pred_mset no_elem Y
X \<noteq> {#}
filter_mset no_elem X \<subseteq># filter_mset no_elem N
\<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)
[PROOF STEP]
have [simp]: "filter_mset no_elem X = X" "filter_mset no_elem N = N"
[PROOF STATE]
proof (prove)
using this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
pred_mset no_elem X
pred_mset no_elem Y
X \<noteq> {#}
filter_mset no_elem X \<subseteq># filter_mset no_elem N
\<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)

goal (1 subgoal):
 1. filter_mset no_elem X = X &&& filter_mset no_elem N = N
[PROOF STEP]
unfolding filter_mset_eq_conv
[PROOF STATE]
proof (prove)
using this:
pred_mset no_elem (N - X + Y)
pred_mset no_elem N
pred_mset no_elem X
pred_mset no_elem Y
X \<noteq> {#}
filter_mset no_elem X \<subseteq># filter_mset no_elem N
\<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)

goal (1 subgoal):
 1. X \<subseteq># X \<and> Multiset.Ball X no_elem \<and> (\<forall>a\<in>#X - X. \<not> no_elem a) &&& N \<subseteq># N \<and> Multiset.Ball N no_elem \<and> (\<forall>a\<in>#N - N. \<not> no_elem a)
[PROOF STEP]
by (auto simp: multiset.pred_set)
[PROOF STATE]
proof (state)
this:
filter_mset no_elem X = X
filter_mset no_elem N = N

goal (1 subgoal):
 1. \<And>M N X Y. \<lbrakk>pred_mset no_elem (N - X + Y); pred_mset no_elem N; pred_mset no_elem X; pred_mset no_elem Y; X \<noteq> {#}; filter_mset no_elem X \<subseteq># filter_mset no_elem N; \<forall>k\<in>Collect no_elem. k \<in># Y \<longrightarrow> (\<exists>a\<in>Collect no_elem. a \<in># X \<and> k < a)\<rbrakk> \<Longrightarrow> \<exists>Xa Ya. Xa \<noteq> {#} \<and> Xa \<subseteq># N \<and> N - X + Y = N - Xa + Ya \<and> (\<forall>k. k \<in># Ya \<longrightarrow> (\<exists>a. a \<in># Xa \<and> k < a))
[PROOF STEP]
show
    "\<exists>X' Y'. X' \<noteq> {#} \<and> X' \<subseteq># N \<and>  N - X + Y = N - X' + Y' \<and>
     (\<forall>k. k \<in># Y' \<longrightarrow> (\<exists>a. a \<in># X' \<and> k < a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X' Y'. X' \<noteq> {#} \<and> X' \<subseteq># N \<and> N - X + Y = N - X' + Y' \<and> (\<forall>k. k \<in># Y' \<longrightarrow> (\<exists>a. a \<in># X' \<and> k < a))
[PROOF STEP]
by (rule exI[of _ X], rule exI[of _ Y]) (insert *; auto simp: multiset.pred_set)
[PROOF STATE]
proof (state)
this:
\<exists>X' Y'. X' \<noteq> {#} \<and> X' \<subseteq># N \<and> N - X + Y = N - X' + Y' \<and> (\<forall>k. k \<in># Y' \<longrightarrow> (\<exists>a. a \<in># X' \<and> k < a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hmsetmset_less[simp]: "hmsetmset M < hmsetmset N \<longleftrightarrow> M < N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hmsetmset M < hmsetmset N) = (M < N)
[PROOF STEP]
by (cases M, cases N, simp add: less_multiset_ext\<^sub>D\<^sub>M_less less_HMSet_iff_less_multiset_ext\<^sub>D\<^sub>M)


[STATEMENT]
lemma hmsetmset_le[simp]: "hmsetmset M \<le> hmsetmset N \<longleftrightarrow> M \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hmsetmset M \<le> hmsetmset N) = (M \<le> N)
[PROOF STEP]
unfolding le_less hmsetmset_less
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M < N \<or> hmsetmset M = hmsetmset N) = (M < N \<or> M = N)
[PROOF STEP]
by (metis hmultiset.collapse)


[STATEMENT]
lemma wf_less_hmultiset: "wf {(X :: hmultiset, Y :: hmultiset). X < Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(X, Y). X < Y}
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> {(x, y). x < y} \<longrightarrow> y \<notin> Q)
[PROOF STEP]
by transfer (insert wf_less_nmultiset[unfolded wf_eq_minimal], fast)


[STATEMENT]
lemma HMSet_less[simp]: "HMSet M < HMSet N \<longleftrightarrow> M < N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HMSet M < HMSet N) = (M < N)
[PROOF STEP]
by (simp add: less_HMSet_iff_less_multiset_ext\<^sub>D\<^sub>M less_multiset_ext\<^sub>D\<^sub>M_less)


[STATEMENT]
lemma HMSet_le[simp]: "HMSet M \<le> HMSet N \<longleftrightarrow> M \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HMSet M \<le> HMSet N) = (M \<le> N)
[PROOF STEP]
by (simp add: hmsetmset_le[symmetric])


[STATEMENT]
lemma mem_imp_less_HMSet: "k \<in># L \<Longrightarrow> k < HMSet L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in># L \<Longrightarrow> k < HMSet L
[PROOF STEP]
by (induct k arbitrary: L) (auto intro: ex_gt_imp_less_multiset)


[STATEMENT]
lemma mem_hmsetmset_imp_less: "M \<in># hmsetmset N \<Longrightarrow> M < N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<in># hmsetmset N \<Longrightarrow> M < N
[PROOF STEP]
using mem_imp_less_HMSet
[PROOF STATE]
proof (prove)
using this:
?k \<in># ?L \<Longrightarrow> ?k < HMSet ?L

goal (1 subgoal):
 1. M \<in># hmsetmset N \<Longrightarrow> M < N
[PROOF STEP]
by force


[STATEMENT]
lemma hmsetmset_empty_iff[simp]: "hmsetmset n = {#} \<longleftrightarrow> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hmsetmset n = {#}) = (n = 0)
[PROOF STEP]
unfolding zero_hmultiset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hmsetmset n = {#}) = (n = HMSet {#})
[PROOF STEP]
by (cases n) simp


[STATEMENT]
lemma hmsetmset_0[simp]: "hmsetmset 0 = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmsetmset 0 = {#}
[PROOF STEP]
by simp


[STATEMENT]
lemma HMSet_plus: "HMSet (A + B) = HMSet A + HMSet B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMSet (A + B) = HMSet A + HMSet B
[PROOF STEP]
by (simp add: plus_hmultiset_def)


[STATEMENT]
lemma HMSet_diff: "HMSet (A - B) = HMSet A - HMSet B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMSet (A - B) = HMSet A - HMSet B
[PROOF STEP]
by (simp add: minus_hmultiset_def)


[STATEMENT]
lemma hmsetmset_plus: "hmsetmset (M + N) = hmsetmset M + hmsetmset N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmsetmset (M + N) = hmsetmset M + hmsetmset N
[PROOF STEP]
by (simp add: plus_hmultiset_def)


[STATEMENT]
lemma hmsetmset_diff: "hmsetmset (M - N) = hmsetmset M - hmsetmset N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmsetmset (M - N) = hmsetmset M - hmsetmset N
[PROOF STEP]
by (simp add: minus_hmultiset_def)


[STATEMENT]
lemma diff_diff_add_hmset[simp]: "a - b - c = a - (b + c)" for a b c :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - b - c = a - (b + c)
[PROOF STEP]
by (fact diff_diff_add)


[STATEMENT]
lemma le_minus_plus_same_hmset: "m \<le> m - n + n" for m n :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> m - n + n
[PROOF STEP]
proof (cases m n rule: hmultiset.exhaust[case_product hmultiset.exhaust])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
case (HMSet_HMSet m0 n0)
[PROOF STATE]
proof (state)
this:
m = HMSet m0
n = HMSet n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
note m = this(1) and n = this(2)
[PROOF STATE]
proof (state)
this:
m = HMSet m0
n = HMSet n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
m = HMSet m0
n = HMSet n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
assume "n0 \<subseteq># m0"
[PROOF STATE]
proof (state)
this:
n0 \<subseteq># m0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
hence "m0 = m0 - n0 + n0"
[PROOF STATE]
proof (prove)
using this:
n0 \<subseteq># m0

goal (1 subgoal):
 1. m0 = m0 - n0 + n0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m0 = m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n0 \<subseteq># m0 \<Longrightarrow> m0 = m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n0 \<subseteq># m0 \<Longrightarrow> m0 = m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n0 \<subseteq># m0 \<Longrightarrow> m0 = m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
assume "\<not> n0 \<subseteq># m0"
[PROOF STATE]
proof (state)
this:
\<not> n0 \<subseteq># m0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
hence "m0 \<subset># m0 - n0 + n0"
[PROOF STATE]
proof (prove)
using this:
\<not> n0 \<subseteq># m0

goal (1 subgoal):
 1. m0 \<subset># m0 - n0 + n0
[PROOF STEP]
by (metis mset_subset_eq_add_right subset_eq_diff_conv subset_mset.dual_order.refl
        subset_mset_def)
[PROOF STATE]
proof (state)
this:
m0 \<subset># m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
hence "m0 < m0 - n0 + n0"
[PROOF STATE]
proof (prove)
using this:
m0 \<subset># m0 - n0 + n0

goal (1 subgoal):
 1. m0 < m0 - n0 + n0
[PROOF STEP]
by (rule subset_imp_less_mset)
[PROOF STATE]
proof (state)
this:
m0 < m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> n0 \<subseteq># m0 \<Longrightarrow> m0 < m0 - n0 + n0

goal (1 subgoal):
 1. \<And>x__ xa__. \<lbrakk>m = HMSet x__; n = HMSet xa__\<rbrakk> \<Longrightarrow> m \<le> m - n + n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n0 \<subseteq># m0 \<Longrightarrow> m0 = m0 - n0 + n0
\<not> n0 \<subseteq># m0 \<Longrightarrow> m0 < m0 - n0 + n0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n0 \<subseteq># m0 \<Longrightarrow> m0 = m0 - n0 + n0
\<not> n0 \<subseteq># m0 \<Longrightarrow> m0 < m0 - n0 + n0

goal (1 subgoal):
 1. m \<le> m - n + n
[PROOF STEP]
by (simp (no_asm) add: m n order_le_less plus_hmultiset_def minus_hmultiset_def) blast
[PROOF STATE]
proof (state)
this:
m \<le> m - n + n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_le_hmset[simp]: "0 \<le> M" for M :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> M
[PROOF STEP]
by (simp add: order_le_less) (metis hmsetmset_less le_multiset_empty_left hmsetmset_empty_iff)


[STATEMENT]
lemma le_zero_eq_hmset[simp]: "M \<le> 0 \<longleftrightarrow> M = 0" for M :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M \<le> 0) = (M = 0)
[PROOF STEP]
by (simp add: dual_order.antisym)


[STATEMENT]
lemma not_less_zero_hmset[simp]: "\<not> M < 0" for M :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> M < 0
[PROOF STEP]
using not_le zero_le_hmset
[PROOF STATE]
proof (prove)
using this:
(\<not> ?x \<le> ?y) = (?y < ?x)
0 \<le> ?M

goal (1 subgoal):
 1. \<not> M < 0
[PROOF STEP]
by blast


[STATEMENT]
lemma not_gr_zero_hmset[simp]: "\<not> 0 < M \<longleftrightarrow> M = 0" for M :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> 0 < M) = (M = 0)
[PROOF STEP]
using neqE not_less_zero_hmset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> ?y; ?x < ?y \<Longrightarrow> ?R; ?y < ?x \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
\<not> ?M < 0

goal (1 subgoal):
 1. (\<not> 0 < M) = (M = 0)
[PROOF STEP]
by blast


[STATEMENT]
lemma zero_less_iff_neq_zero_hmset: "0 < M \<longleftrightarrow> M \<noteq> 0" for M :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < M) = (M \<noteq> 0)
[PROOF STEP]
using not_gr_zero_hmset
[PROOF STATE]
proof (prove)
using this:
(\<not> 0 < ?M) = (?M = 0)

goal (1 subgoal):
 1. (0 < M) = (M \<noteq> 0)
[PROOF STEP]
by blast