[STATEMENT]
lemma root_sign_change: assumes
    p0: "poly (p::real poly) x = 0" and
    pd_ne0: "poly (pderiv p) x \<noteq> 0"
  obtains d where
    "0 < d"
    "sgn (poly p (x - d)) \<noteq> sgn (poly p (x + d))"
    "sgn (poly p (x - d)) \<noteq> 0"
    "0 \<noteq> sgn (poly p (x + d))"
    "\<forall> d' > 0. d' \<le> d \<longrightarrow> sgn (poly p (x + d')) = sgn (poly p (x + d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; sgn (poly p (x - d)) \<noteq> sgn (poly p (x + d)); sgn (poly p (x - d)) \<noteq> 0; 0 \<noteq> sgn (poly p (x + d)); \<forall>d'>0. d' \<le> d \<longrightarrow> sgn (poly p (x + d')) = sgn (poly p (x + d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - d))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; sgn (poly p (x - d)) \<noteq> sgn (poly p (x + d)); sgn (poly p (x - d)) \<noteq> 0; 0 \<noteq> sgn (poly p (x + d)); \<forall>d'>0. d' \<le> d \<longrightarrow> sgn (poly p (x + d')) = sgn (poly p (x + d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - d))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume a:"(\<And>d. 0 < d \<Longrightarrow>
          sgn (poly p (x - d)) \<noteq> sgn (poly p (x + d)) \<Longrightarrow>
          sgn (poly p (x - d)) \<noteq> 0 \<Longrightarrow>
          0 \<noteq> sgn (poly p (x + d)) \<Longrightarrow>
          \<forall>d'>0. d' \<le> d \<longrightarrow>
                 sgn (poly p (x + d')) = sgn (poly p (x + d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - d)) \<Longrightarrow>
          thesis)"
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?d; sgn (poly p (x - ?d)) \<noteq> sgn (poly p (x + ?d)); sgn (poly p (x - ?d)) \<noteq> 0; 0 \<noteq> sgn (poly p (x + ?d)); \<forall>d'>0. d' \<le> ?d \<longrightarrow> sgn (poly p (x + d')) = sgn (poly p (x + ?d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - ?d))\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; sgn (poly p (x - d)) \<noteq> sgn (poly p (x + d)); sgn (poly p (x - d)) \<noteq> 0; 0 \<noteq> sgn (poly p (x + d)); \<forall>d'>0. d' \<le> d \<longrightarrow> sgn (poly p (x + d')) = sgn (poly p (x + d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - d))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from pd_ne0
[PROOF STATE]
proof (chain)
picking this:
poly (pderiv p) x \<noteq> 0
[PROOF STEP]
consider "poly (pderiv p) x > 0" | "poly (pderiv p) x < 0"
[PROOF STATE]
proof (prove)
using this:
poly (pderiv p) x \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < poly (pderiv p) x \<Longrightarrow> thesis; poly (pderiv p) x < 0 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < poly (pderiv p) x \<Longrightarrow> ?thesis; poly (pderiv p) x < 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; sgn (poly p (x - d)) \<noteq> sgn (poly p (x + d)); sgn (poly p (x - d)) \<noteq> 0; 0 \<noteq> sgn (poly p (x + d)); \<forall>d'>0. d' \<le> d \<longrightarrow> sgn (poly p (x + d')) = sgn (poly p (x + d)) \<and> sgn (poly p (x - d')) = sgn (poly p (x - d))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < poly (pderiv p) x \<Longrightarrow> ?thesis; poly (pderiv p) x < 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
0 < poly (pderiv p) x

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
obtain d1 where d1:"\<And>h. 0<h \<Longrightarrow> h < d1 \<Longrightarrow> poly p (x - h) < 0" "d1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d1. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d1\<rbrakk> \<Longrightarrow> poly p (x - h) < 0; 0 < d1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using DERIV_pos_inc_left[OF poly_DERIV 1] p0
[PROOF STATE]
proof (prove)
using this:
\<exists>d>0. \<forall>h>0. h < d \<longrightarrow> poly p (x - h) < poly p x
poly p x = 0

goal (1 subgoal):
 1. (\<And>d1. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d1\<rbrakk> \<Longrightarrow> poly p (x - h) < 0; 0 < d1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?h; ?h < d1\<rbrakk> \<Longrightarrow> poly p (x - ?h) < 0
0 < d1

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
obtain d2 where d2:"\<And>h. 0<h \<Longrightarrow> h < d2 \<Longrightarrow> poly p (x + h) > 0" "d2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d2. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d2\<rbrakk> \<Longrightarrow> 0 < poly p (x + h); 0 < d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using DERIV_pos_inc_right[OF poly_DERIV 1] p0
[PROOF STATE]
proof (prove)
using this:
\<exists>d>0. \<forall>h>0. h < d \<longrightarrow> poly p x < poly p (x + h)
poly p x = 0

goal (1 subgoal):
 1. (\<And>d2. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d2\<rbrakk> \<Longrightarrow> 0 < poly p (x + h); 0 < d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?h; ?h < d2\<rbrakk> \<Longrightarrow> 0 < poly p (x + ?h)
0 < d2

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
have g0:"0 < (min d1 d2) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < min d1 d2 / 2
[PROOF STEP]
using d1 d2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?h; ?h < d1\<rbrakk> \<Longrightarrow> poly p (x - ?h) < 0
0 < d1
\<lbrakk>0 < ?h; ?h < d2\<rbrakk> \<Longrightarrow> 0 < poly p (x + ?h)
0 < d2

goal (1 subgoal):
 1. 0 < min d1 d2 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < min d1 d2 / 2

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
hence m1:"min d1 d2 / 2 < d1" and m2:"min d1 d2 / 2 < d2"
[PROOF STATE]
proof (prove)
using this:
0 < min d1 d2 / 2

goal (1 subgoal):
 1. min d1 d2 / 2 < d1 &&& min d1 d2 / 2 < d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min d1 d2 / 2 < d1
min d1 d2 / 2 < d2

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
min d1 d2 / 2 < d1
min d1 d2 / 2 < d2

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
assume a1:"0 < d" and a2:"d < min d1 d2"
[PROOF STATE]
proof (state)
this:
0 < d
d < min d1 d2

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
have "sgn (poly p (x - d)) = -1" "sgn (poly p (x + d)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly p (x - d)) = - 1 &&& sgn (poly p (x + d)) = 1
[PROOF STEP]
using d1(1)[OF a1] d2(1)[OF a1] a2
[PROOF STATE]
proof (prove)
using this:
d < d1 \<Longrightarrow> poly p (x - d) < 0
d < d2 \<Longrightarrow> 0 < poly p (x + d)
d < min d1 d2

goal (1 subgoal):
 1. sgn (poly p (x - d)) = - 1 &&& sgn (poly p (x + d)) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn (poly p (x - d)) = - 1
sgn (poly p (x + d)) = 1

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x - ?d2)) = - 1
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x + ?d2)) = 1

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
note d=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x - ?d2)) = - 1
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x + ?d2)) = 1

goal (2 subgoals):
 1. 0 < poly (pderiv p) x \<Longrightarrow> thesis
 2. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule a[OF g0];insert d g0 m1 m2, simp)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
poly (pderiv p) x < 0

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
obtain d1 where d1:"\<And>h. 0<h \<Longrightarrow> h < d1 \<Longrightarrow> poly p (x - h) > 0" "d1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d1. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d1\<rbrakk> \<Longrightarrow> 0 < poly p (x - h); 0 < d1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using DERIV_neg_dec_left[OF poly_DERIV 2] p0
[PROOF STATE]
proof (prove)
using this:
\<exists>d>0. \<forall>h>0. h < d \<longrightarrow> poly p x < poly p (x - h)
poly p x = 0

goal (1 subgoal):
 1. (\<And>d1. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d1\<rbrakk> \<Longrightarrow> 0 < poly p (x - h); 0 < d1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?h; ?h < d1\<rbrakk> \<Longrightarrow> 0 < poly p (x - ?h)
0 < d1

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
obtain d2 where d2:"\<And>h. 0<h \<Longrightarrow> h < d2 \<Longrightarrow> poly p (x + h) < 0" "d2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d2. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d2\<rbrakk> \<Longrightarrow> poly p (x + h) < 0; 0 < d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using DERIV_neg_dec_right[OF poly_DERIV 2] p0
[PROOF STATE]
proof (prove)
using this:
\<exists>d>0. \<forall>h>0. h < d \<longrightarrow> poly p (x + h) < poly p x
poly p x = 0

goal (1 subgoal):
 1. (\<And>d2. \<lbrakk>\<And>h. \<lbrakk>0 < h; h < d2\<rbrakk> \<Longrightarrow> poly p (x + h) < 0; 0 < d2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?h; ?h < d2\<rbrakk> \<Longrightarrow> poly p (x + ?h) < 0
0 < d2

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
have g0:"0 < (min d1 d2) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < min d1 d2 / 2
[PROOF STEP]
using d1 d2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?h; ?h < d1\<rbrakk> \<Longrightarrow> 0 < poly p (x - ?h)
0 < d1
\<lbrakk>0 < ?h; ?h < d2\<rbrakk> \<Longrightarrow> poly p (x + ?h) < 0
0 < d2

goal (1 subgoal):
 1. 0 < min d1 d2 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < min d1 d2 / 2

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
hence m1:"min d1 d2 / 2 < d1" and m2:"min d1 d2 / 2 < d2"
[PROOF STATE]
proof (prove)
using this:
0 < min d1 d2 / 2

goal (1 subgoal):
 1. min d1 d2 / 2 < d1 &&& min d1 d2 / 2 < d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min d1 d2 / 2 < d1
min d1 d2 / 2 < d2

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
min d1 d2 / 2 < d1
min d1 d2 / 2 < d2

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
assume a1:"0 < d" and a2:"d < min d1 d2"
[PROOF STATE]
proof (state)
this:
0 < d
d < min d1 d2

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
have "sgn (poly p (x - d)) = 1" "sgn (poly p (x + d)) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly p (x - d)) = 1 &&& sgn (poly p (x + d)) = - 1
[PROOF STEP]
using d1(1)[OF a1] d2(1)[OF a1] a2
[PROOF STATE]
proof (prove)
using this:
d < d1 \<Longrightarrow> 0 < poly p (x - d)
d < d2 \<Longrightarrow> poly p (x + d) < 0
d < min d1 d2

goal (1 subgoal):
 1. sgn (poly p (x - d)) = 1 &&& sgn (poly p (x + d)) = - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn (poly p (x - d)) = 1
sgn (poly p (x + d)) = - 1

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x - ?d2)) = 1
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x + ?d2)) = - 1

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
note d=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x - ?d2)) = 1
\<lbrakk>0 < ?d2; ?d2 < min d1 d2\<rbrakk> \<Longrightarrow> sgn (poly p (x + ?d2)) = - 1

goal (1 subgoal):
 1. poly (pderiv p) x < 0 \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule a[OF g0];insert d g0 m1 m2, simp)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gt_rat_sign_change_square_free:
  assumes ur: "\<exists>! x. root_cond plr x"
    and plr[simp]: "plr = (p,l,r)"
    and sf: "square_free p" and in_interval: "l \<le> y" "y \<le> r"
    and py0: "ipoly p y \<noteq> 0" and pr0: "ipoly p r \<noteq> 0"
  shows "(sgn (ipoly p y) = sgn (ipoly p r)) = (of_rat y > (THE x. root_cond plr x))" (is "?gt = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) = ((THE x. root_cond plr x) < real_of_rat y)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
define ur where "ur = (THE x. root_cond plr x)"
[PROOF STATE]
proof (state)
this:
ur = (THE x. root_cond plr x)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
hence "?gt \<noteq> (real_of_rat y > ur)"
[PROOF STATE]
proof (prove)
using this:
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (ur < real_of_rat y)
[PROOF STEP]
unfolding ur_def
[PROOF STATE]
proof (prove)
using this:
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (The (root_cond plr) < real_of_rat y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (ur < real_of_rat y)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
note a = this[unfolded plr]
[PROOF STATE]
proof (state)
this:
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (ur < real_of_rat y)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from py0
[PROOF STATE]
proof (chain)
picking this:
ipoly p y \<noteq> 0
[PROOF STEP]
have "p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
ipoly p y \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
unfolding irreducible_def
[PROOF STATE]
proof (prove)
using this:
ipoly p y \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
hence p0_real: "real_of_int_poly p \<noteq> (0::real poly)"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. real_of_int_poly p \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int_poly p \<noteq> 0

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
let ?p = "real_of_int_poly p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
let ?r = real_of_rat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from in_interval
[PROOF STATE]
proof (chain)
picking this:
l \<le> y
y \<le> r
[PROOF STEP]
have in':"?r l \<le> ?r y" "?r y \<le> ?r r"
[PROOF STATE]
proof (prove)
using this:
l \<le> y
y \<le> r

goal (1 subgoal):
 1. real_of_rat l \<le> real_of_rat y &&& real_of_rat y \<le> real_of_rat r
[PROOF STEP]
unfolding of_rat_less_eq
[PROOF STATE]
proof (prove)
using this:
l \<le> y
y \<le> r

goal (1 subgoal):
 1. l \<le> y &&& y \<le> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> real_of_rat y
real_of_rat y \<le> real_of_rat r

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from sf square_free_of_int_poly[of p] square_free_rsquarefree
[PROOF STATE]
proof (chain)
picking this:
square_free p
square_free p \<Longrightarrow> square_free (of_int_poly p)
square_free ?f \<Longrightarrow> rsquarefree ?f
[PROOF STEP]
have rsf:"rsquarefree ?p"
[PROOF STATE]
proof (prove)
using this:
square_free p
square_free p \<Longrightarrow> square_free (of_int_poly p)
square_free ?f \<Longrightarrow> rsquarefree ?f

goal (1 subgoal):
 1. rsquarefree (real_of_int_poly p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rsquarefree (real_of_int_poly p)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from ur
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. root_cond plr x
[PROOF STEP]
have "root_cond plr ur"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x

goal (1 subgoal):
 1. root_cond plr ur
[PROOF STEP]
by (metis ur_def theI')
[PROOF STATE]
proof (state)
this:
root_cond plr ur

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
note urD = this[unfolded root_cond_def plr split] this[unfolded plr]
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
have ur3:"poly ?p ur = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (real_of_int_poly p) ur = 0
[PROOF STEP]
using urD
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. poly (real_of_int_poly p) ur = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (real_of_int_poly p) ur = 0

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from urD
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
[PROOF STEP]
have "ur \<le> of_rat r"
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. ur \<le> real_of_rat r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ur \<le> real_of_rat r

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ur \<le> real_of_rat r

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from pr0
[PROOF STATE]
proof (chain)
picking this:
ipoly p r \<noteq> 0
[PROOF STEP]
have "ipoly p (real_of_rat r) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
ipoly p r \<noteq> 0

goal (1 subgoal):
 1. poly (real_of_int_poly p) (real_of_rat r) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (real_of_int_poly p) (real_of_rat r) \<noteq> 0

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
with ur3
[PROOF STATE]
proof (chain)
picking this:
poly (real_of_int_poly p) ur = 0
poly (real_of_int_poly p) (real_of_rat r) \<noteq> 0
[PROOF STEP]
have "real_of_rat r \<noteq> ur"
[PROOF STATE]
proof (prove)
using this:
poly (real_of_int_poly p) ur = 0
poly (real_of_int_poly p) (real_of_rat r) \<noteq> 0

goal (1 subgoal):
 1. real_of_rat r \<noteq> ur
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
real_of_rat r \<noteq> ur

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ur \<le> real_of_rat r
real_of_rat r \<noteq> ur
[PROOF STEP]
have "ur < ?r r"
[PROOF STATE]
proof (prove)
using this:
ur \<le> real_of_rat r
real_of_rat r \<noteq> ur

goal (1 subgoal):
 1. ur < real_of_rat r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ur < real_of_rat r

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
hence ur2: "0 < ?r r - ur"
[PROOF STATE]
proof (prove)
using this:
ur < real_of_rat r

goal (1 subgoal):
 1. 0 < real_of_rat r - ur
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < real_of_rat r - ur

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
from rsquarefree_roots rsf ur3
[PROOF STATE]
proof (chain)
picking this:
rsquarefree ?p = (\<forall>a. \<not> (poly ?p a = (0::?'a) \<and> poly (pderiv ?p) a = (0::?'a)))
rsquarefree (real_of_int_poly p)
poly (real_of_int_poly p) ur = 0
[PROOF STEP]
have pd_nonz:"poly (pderiv ?p) ur \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
rsquarefree ?p = (\<forall>a. \<not> (poly ?p a = (0::?'a) \<and> poly (pderiv ?p) a = (0::?'a)))
rsquarefree (real_of_int_poly p)
poly (real_of_int_poly p) ur = 0

goal (1 subgoal):
 1. poly (pderiv (real_of_int_poly p)) ur \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (pderiv (real_of_int_poly p)) ur \<noteq> 0

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
obtain d where d':"\<And>d'. d'>0 \<Longrightarrow> d' \<le> d \<Longrightarrow>
             sgn (poly ?p (ur + d')) = sgn (poly ?p (ur + d)) \<and>
             sgn (poly ?p (ur - d')) = sgn (poly ?p (ur - d))"
    "sgn (poly ?p (ur - d)) \<noteq> sgn (poly ?p (ur + d))"
    "sgn (poly ?p (ur + d)) \<noteq> 0"
    and d_ge_0:"d > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. \<lbrakk>\<And>d'. \<lbrakk>0 < d'; d' \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d')) = sgn (poly (real_of_int_poly p) (ur + d)) \<and> sgn (poly (real_of_int_poly p) (ur - d')) = sgn (poly (real_of_int_poly p) (ur - d)); sgn (poly (real_of_int_poly p) (ur - d)) \<noteq> sgn (poly (real_of_int_poly p) (ur + d)); sgn (poly (real_of_int_poly p) (ur + d)) \<noteq> 0; 0 < d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis root_sign_change[OF ur3 pd_nonz])
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?d'; ?d' \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + ?d')) = sgn (poly (real_of_int_poly p) (ur + d)) \<and> sgn (poly (real_of_int_poly p) (ur - ?d')) = sgn (poly (real_of_int_poly p) (ur - d))
sgn (poly (real_of_int_poly p) (ur - d)) \<noteq> sgn (poly (real_of_int_poly p) (ur + d))
sgn (poly (real_of_int_poly p) (ur + d)) \<noteq> 0
0 < d

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
have sr:"sgn (poly ?p (ur + d)) = sgn (poly ?p (?r r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
proof (cases "?r r - ur \<le> d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
 2. \<not> real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
real_of_rat r - ur \<le> d

goal (2 subgoals):
 1. real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
 2. \<not> real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
using d'(1)[OF ur2 True]
[PROOF STATE]
proof (prove)
using this:
sgn (poly (real_of_int_poly p) (ur + (real_of_rat r - ur))) = sgn (poly (real_of_int_poly p) (ur + d)) \<and> sgn (poly (real_of_int_poly p) (ur - (real_of_rat r - ur))) = sgn (poly (real_of_int_poly p) (ur - d))

goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))

goal (1 subgoal):
 1. \<not> real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> real_of_rat r - ur \<le> d

goal (1 subgoal):
 1. \<not> real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
hence less:"ur + d < ?r r"
[PROOF STATE]
proof (prove)
using this:
\<not> real_of_rat r - ur \<le> d

goal (1 subgoal):
 1. ur + d < real_of_rat r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ur + d < real_of_rat r

goal (1 subgoal):
 1. \<not> real_of_rat r - ur \<le> d \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
proof(rule no_roots_inbetween_imp_same_sign[OF less,rule_format],goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ur + d \<le> x \<and> x \<le> real_of_rat r \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
ur + d \<le> x \<and> x \<le> real_of_rat r

goal (1 subgoal):
 1. \<And>x. ur + d \<le> x \<and> x \<le> real_of_rat r \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
from ur 1 d_ge_0
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. root_cond plr x
ur + d \<le> x \<and> x \<le> real_of_rat r
0 < d
[PROOF STEP]
have ran: "real_of_rat l \<le> x" "x \<le> real_of_rat r"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x
ur + d \<le> x \<and> x \<le> real_of_rat r
0 < d

goal (1 subgoal):
 1. real_of_rat l \<le> x &&& x \<le> real_of_rat r
[PROOF STEP]
using urD
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x
ur + d \<le> x \<and> x \<le> real_of_rat r
0 < d
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. real_of_rat l \<le> x &&& x \<le> real_of_rat r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> x
x \<le> real_of_rat r

goal (1 subgoal):
 1. \<And>x. ur + d \<le> x \<and> x \<le> real_of_rat r \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
from 1 d_ge_0
[PROOF STATE]
proof (chain)
picking this:
ur + d \<le> x \<and> x \<le> real_of_rat r
0 < d
[PROOF STEP]
have "ur \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
ur + d \<le> x \<and> x \<le> real_of_rat r
0 < d

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

goal (1 subgoal):
 1. \<And>x. ur + d \<le> x \<and> x \<le> real_of_rat r \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
with ur urD
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
ur \<noteq> x
[PROOF STEP]
have "\<not> root_cond (p,l,r) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
ur \<noteq> x

goal (1 subgoal):
 1. \<not> root_cond (p, l, r) x
[PROOF STEP]
by (auto simp: root_cond_def)
[PROOF STATE]
proof (state)
this:
\<not> root_cond (p, l, r) x

goal (1 subgoal):
 1. \<And>x. ur + d \<le> x \<and> x \<le> real_of_rat r \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
with ran
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> x
x \<le> real_of_rat r
\<not> root_cond (p, l, r) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> x
x \<le> real_of_rat r
\<not> root_cond (p, l, r) x

goal (1 subgoal):
 1. poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
by (auto simp: root_cond_def)
[PROOF STATE]
proof (state)
this:
poly (real_of_int_poly p) x \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
consider "?r l < ur - d" "?r l < ur" | "0 < ur - ?r l" "ur - ?r l \<le> d" | "ur = ?r l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> thesis; ur = real_of_rat l \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using urD
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> thesis; ur = real_of_rat l \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> ?thesis; ur = real_of_rat l \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
hence sl:"sgn (poly ?p (ur - d)) = sgn (poly ?p (?r l)) \<or> 0 = sgn (poly ?p (?r l))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> ?thesis; ur = real_of_rat l \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 2. \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 3. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
real_of_rat l < ur - d
real_of_rat l < ur

goal (3 subgoals):
 1. \<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 2. \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 3. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
have "sgn (poly ?p (?r l)) = sgn (poly ?p (ur - d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (real_of_rat l)) = sgn (poly (real_of_int_poly p) (ur - d))
[PROOF STEP]
proof(rule no_roots_inbetween_imp_same_sign[OF 1(1),rule_format],goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. real_of_rat l \<le> x \<and> x \<le> ur - d \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> x \<and> x \<le> ur - d

goal (1 subgoal):
 1. \<And>x. real_of_rat l \<le> x \<and> x \<le> ur - d \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
from ur 1 d_ge_0 urD
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> x \<and> x \<le> ur - d
0 < d
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
[PROOF STEP]
have ran: "real_of_rat l \<le> x" "x \<le> real_of_rat r"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> x \<and> x \<le> ur - d
0 < d
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. real_of_rat l \<le> x &&& x \<le> real_of_rat r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> x
x \<le> real_of_rat r

goal (1 subgoal):
 1. \<And>x. real_of_rat l \<le> x \<and> x \<le> ur - d \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
from 1 d_ge_0
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> x \<and> x \<le> ur - d
0 < d
[PROOF STEP]
have "ur \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> x \<and> x \<le> ur - d
0 < d

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

goal (1 subgoal):
 1. \<And>x. real_of_rat l \<le> x \<and> x \<le> ur - d \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
with ur urD
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
ur \<noteq> x
[PROOF STEP]
have "\<not> root_cond (p,l,r) x"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
ur \<noteq> x

goal (1 subgoal):
 1. \<not> root_cond (p, l, r) x
[PROOF STEP]
by (auto simp: root_cond_def)
[PROOF STATE]
proof (state)
this:
\<not> root_cond (p, l, r) x

goal (1 subgoal):
 1. \<And>x. real_of_rat l \<le> x \<and> x \<le> ur - d \<Longrightarrow> poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
with ran
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> x
x \<le> real_of_rat r
\<not> root_cond (p, l, r) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> x
x \<le> real_of_rat r
\<not> root_cond (p, l, r) x

goal (1 subgoal):
 1. poly (real_of_int_poly p) x \<noteq> 0
[PROOF STEP]
by (auto simp: root_cond_def)
[PROOF STATE]
proof (state)
this:
poly (real_of_int_poly p) x \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (real_of_rat l)) = sgn (poly (real_of_int_poly p) (ur - d))

goal (3 subgoals):
 1. \<lbrakk>real_of_rat l < ur - d; real_of_rat l < ur\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 2. \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 3. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sgn (poly (real_of_int_poly p) (real_of_rat l)) = sgn (poly (real_of_int_poly p) (ur - d))

goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))

goal (2 subgoals):
 1. \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 2. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 2. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < ur - real_of_rat l
ur - real_of_rat l \<le> d

goal (2 subgoals):
 1. \<lbrakk>0 < ur - real_of_rat l; ur - real_of_rat l \<le> d\<rbrakk> \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
 2. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
using d'(1)[OF 2]
[PROOF STATE]
proof (prove)
using this:
sgn (poly (real_of_int_poly p) (ur + (ur - real_of_rat l))) = sgn (poly (real_of_int_poly p) (ur + d)) \<and> sgn (poly (real_of_int_poly p) (ur - (ur - real_of_rat l))) = sgn (poly (real_of_int_poly p) (ur - d))

goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))

goal (1 subgoal):
 1. ur = real_of_rat l \<Longrightarrow> sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
[PROOF STEP]
qed (insert ur3,simp)
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
have diff_sign: "sgn (ipoly p l) \<noteq> sgn (ipoly p r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (ipoly p l) \<noteq> sgn (ipoly p r)
[PROOF STEP]
using d'(2-) sr sl real_of_rat_sgn
[PROOF STATE]
proof (prove)
using this:
sgn (poly (real_of_int_poly p) (ur - d)) \<noteq> sgn (poly (real_of_int_poly p) (ur + d))
sgn (poly (real_of_int_poly p) (ur + d)) \<noteq> 0
sgn (poly (real_of_int_poly p) (ur + d)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
sgn (poly (real_of_int_poly p) (ur - d)) = sgn (poly (real_of_int_poly p) (real_of_rat l)) \<or> 0 = sgn (poly (real_of_int_poly p) (real_of_rat l))
sgn (real_of_rat ?x) = real_of_rat (sgn ?x)

goal (1 subgoal):
 1. sgn (ipoly p l) \<noteq> sgn (ipoly p r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn (ipoly p l) \<noteq> sgn (ipoly p r)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
have ur':"\<And>x. real_of_rat l \<le> x \<and> x \<le> real_of_rat y \<Longrightarrow> ipoly p x = 0 \<Longrightarrow> \<not> (?r y \<le> ur)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0\<rbrakk> \<Longrightarrow> \<not> real_of_rat y \<le> ur
[PROOF STEP]
proof(standard+,goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> x \<and> x \<le> real_of_rat y
poly (real_of_int_poly p) x = 0
real_of_rat y \<le> ur

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
real_of_rat l \<le> x \<and> x \<le> real_of_rat y
poly (real_of_int_poly p) x = 0
real_of_rat y \<le> ur

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume id: "ur = ?r y"
[PROOF STATE]
proof (state)
this:
ur = real_of_rat y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with urD ur py0
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
\<exists>!x. root_cond plr x
ipoly p y \<noteq> 0
ur = real_of_rat y
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
\<exists>!x. root_cond plr x
ipoly p y \<noteq> 0
ur = real_of_rat y

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ur = real_of_rat y \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note neq = this
[PROOF STATE]
proof (state)
this:
ur = real_of_rat y \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have x: "root_cond (p, l, r) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_cond (p, l, r) x
[PROOF STEP]
unfolding root_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (p, l, r) of (p, l, r) \<Rightarrow> real_of_rat l \<le> x \<and> x \<le> real_of_rat r \<and> poly (real_of_int_poly p) x = 0
[PROOF STEP]
using 1 a ur urD
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> x \<and> x \<le> real_of_rat y
poly (real_of_int_poly p) x = 0
real_of_rat y \<le> ur
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (ur < real_of_rat y)
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. case (p, l, r) of (p, l, r) \<Rightarrow> real_of_rat l \<le> x \<and> x \<le> real_of_rat r \<and> poly (real_of_int_poly p) x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
root_cond (p, l, r) x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from ur urD x
[PROOF STATE]
proof (chain)
picking this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
root_cond (p, l, r) x
[PROOF STEP]
have ur_eqI: "ur = x"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. root_cond plr x
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
root_cond (p, l, r) x

goal (1 subgoal):
 1. ur = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ur = x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> x \<and> x \<le> real_of_rat y
poly (real_of_int_poly p) x = 0
real_of_rat y \<le> ur
ur = x
[PROOF STEP]
have "ur = of_rat y"
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> x \<and> x \<le> real_of_rat y
poly (real_of_int_poly p) x = 0
real_of_rat y \<le> ur
ur = x

goal (1 subgoal):
 1. ur = real_of_rat y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ur = real_of_rat y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>real_of_rat l \<le> x \<and> x \<le> real_of_rat y; poly (real_of_int_poly p) x = 0; real_of_rat y \<le> ur\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with urD(1) py0
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
ipoly p y \<noteq> 0
ur = real_of_rat y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
ipoly p y \<noteq> 0
ur = real_of_rat y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>real_of_rat l \<le> ?x \<and> ?x \<le> real_of_rat y; poly (real_of_int_poly p) ?x = 0\<rbrakk> \<Longrightarrow> \<not> real_of_rat y \<le> ur

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
hence ur'':"\<forall>x. real_of_rat y \<le> x \<and> x \<le> real_of_rat r \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> \<not> (?r y \<le> ur)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>real_of_rat l \<le> ?x \<and> ?x \<le> real_of_rat y; poly (real_of_int_poly p) ?x = 0\<rbrakk> \<Longrightarrow> \<not> real_of_rat y \<le> ur

goal (1 subgoal):
 1. \<forall>x. real_of_rat y \<le> x \<and> x \<le> real_of_rat r \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> \<not> real_of_rat y \<le> ur
[PROOF STEP]
using urD
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>real_of_rat l \<le> ?x \<and> ?x \<le> real_of_rat y; poly (real_of_int_poly p) ?x = 0\<rbrakk> \<Longrightarrow> \<not> real_of_rat y \<le> ur
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

goal (1 subgoal):
 1. \<forall>x. real_of_rat y \<le> x \<and> x \<le> real_of_rat r \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> \<not> real_of_rat y \<le> ur
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. real_of_rat y \<le> x \<and> x \<le> real_of_rat r \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> \<not> real_of_rat y \<le> ur

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
have "(sgn (ipoly p y) = sgn (ipoly p r)) = (?r y > ur)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
proof(cases "sgn (ipoly p r) = sgn (ipoly p y)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sgn (ipoly p r) = sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
 2. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
sgn (ipoly p r) = sgn (ipoly p y)

goal (2 subgoals):
 1. sgn (ipoly p r) = sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
 2. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
have sgn:"sgn (poly ?p (real_of_rat l)) \<noteq> sgn (poly ?p (real_of_rat y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (real_of_rat l)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat y))
[PROOF STEP]
using True diff_sign
[PROOF STATE]
proof (prove)
using this:
sgn (ipoly p r) = sgn (ipoly p y)
sgn (ipoly p l) \<noteq> sgn (ipoly p r)

goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (real_of_rat l)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat y))
[PROOF STEP]
by (simp add: real_of_rat_sgn)
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (real_of_rat l)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat y))

goal (2 subgoals):
 1. sgn (ipoly p r) = sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
 2. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
have ly:"of_rat l < (of_rat y::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat l < real_of_rat y
[PROOF STEP]
using in_interval True diff_sign less_eq_rat_def of_rat_less
[PROOF STATE]
proof (prove)
using this:
l \<le> y
y \<le> r
sgn (ipoly p r) = sgn (ipoly p y)
sgn (ipoly p l) \<noteq> sgn (ipoly p r)
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
(of_rat ?r < of_rat ?s) = (?r < ?s)

goal (1 subgoal):
 1. real_of_rat l < real_of_rat y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat l < real_of_rat y

goal (2 subgoals):
 1. sgn (ipoly p r) = sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
 2. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
with no_roots_inbetween_imp_same_sign[OF ly,of ?p] sgn ur' True
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. real_of_rat l \<le> x \<and> x \<le> real_of_rat y \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> sgn (poly (real_of_int_poly p) (real_of_rat l)) = sgn (poly (real_of_int_poly p) (real_of_rat y))
sgn (poly (real_of_int_poly p) (real_of_rat l)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat y))
\<lbrakk>real_of_rat l \<le> ?x \<and> ?x \<le> real_of_rat y; poly (real_of_int_poly p) ?x = 0\<rbrakk> \<Longrightarrow> \<not> real_of_rat y \<le> ur
sgn (ipoly p r) = sgn (ipoly p y)
real_of_rat l < real_of_rat y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. real_of_rat l \<le> x \<and> x \<le> real_of_rat y \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> sgn (poly (real_of_int_poly p) (real_of_rat l)) = sgn (poly (real_of_int_poly p) (real_of_rat y))
sgn (poly (real_of_int_poly p) (real_of_rat l)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat y))
\<lbrakk>real_of_rat l \<le> ?x \<and> ?x \<le> real_of_rat y; poly (real_of_int_poly p) ?x = 0\<rbrakk> \<Longrightarrow> \<not> real_of_rat y \<le> ur
sgn (ipoly p r) = sgn (ipoly p y)
real_of_rat l < real_of_rat y

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
sgn (ipoly p r) \<noteq> sgn (ipoly p y)

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
hence ne:"sgn (ipoly p (real_of_rat y)) \<noteq> sgn (ipoly p (real_of_rat r))"
[PROOF STATE]
proof (prove)
using this:
sgn (ipoly p r) \<noteq> sgn (ipoly p y)

goal (1 subgoal):
 1. sgn (poly (real_of_int_poly p) (real_of_rat y)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat r))
[PROOF STEP]
by (simp add: real_of_rat_sgn)
[PROOF STATE]
proof (state)
this:
sgn (poly (real_of_int_poly p) (real_of_rat y)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat r))

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
have ry:"of_rat y < (of_rat r::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat y < real_of_rat r
[PROOF STEP]
using in_interval False diff_sign less_eq_rat_def of_rat_less
[PROOF STATE]
proof (prove)
using this:
l \<le> y
y \<le> r
sgn (ipoly p r) \<noteq> sgn (ipoly p y)
sgn (ipoly p l) \<noteq> sgn (ipoly p r)
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
(of_rat ?r < of_rat ?s) = (?r < ?s)

goal (1 subgoal):
 1. real_of_rat y < real_of_rat r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat y < real_of_rat r

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
obtain x where x:"real_of_rat y \<le> x" "x \<le> real_of_rat r" "ipoly p x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>real_of_rat y \<le> x; x \<le> real_of_rat r; poly (real_of_int_poly p) x = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using no_roots_inbetween_imp_same_sign[OF ry,of ?p] ne
[PROOF STATE]
proof (prove)
using this:
\<forall>x. real_of_rat y \<le> x \<and> x \<le> real_of_rat r \<longrightarrow> poly (real_of_int_poly p) x \<noteq> 0 \<Longrightarrow> sgn (poly (real_of_int_poly p) (real_of_rat y)) = sgn (poly (real_of_int_poly p) (real_of_rat r))
sgn (poly (real_of_int_poly p) (real_of_rat y)) \<noteq> sgn (poly (real_of_int_poly p) (real_of_rat r))

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>real_of_rat y \<le> x; x \<le> real_of_rat r; poly (real_of_int_poly p) x = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
hence lx:"real_of_rat l \<le> x"
[PROOF STATE]
proof (prove)
using this:
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0

goal (1 subgoal):
 1. real_of_rat l \<le> x
[PROOF STEP]
using in_interval
[PROOF STATE]
proof (prove)
using this:
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0
l \<le> y
y \<le> r

goal (1 subgoal):
 1. real_of_rat l \<le> x
[PROOF STEP]
using False a urD
[PROOF STATE]
proof (prove)
using this:
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0
l \<le> y
y \<le> r
sgn (ipoly p r) \<noteq> sgn (ipoly p y)
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (ur < real_of_rat y)
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur

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

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0
real_of_rat l \<le> x
[PROOF STEP]
have "root_cond (p,l,r) x"
[PROOF STATE]
proof (prove)
using this:
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0
real_of_rat l \<le> x

goal (1 subgoal):
 1. root_cond (p, l, r) x
[PROOF STEP]
by (auto simp: root_cond_def)
[PROOF STATE]
proof (state)
this:
root_cond (p, l, r) x

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
with urD ur
[PROOF STATE]
proof (chain)
picking this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
\<exists>!x. root_cond plr x
root_cond (p, l, r) x
[PROOF STEP]
have "ur = x"
[PROOF STATE]
proof (prove)
using this:
real_of_rat l \<le> ur \<and> ur \<le> real_of_rat r \<and> poly (real_of_int_poly p) ur = 0
root_cond (p, l, r) ur
\<exists>!x. root_cond plr x
root_cond (p, l, r) x

goal (1 subgoal):
 1. ur = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ur = x

goal (1 subgoal):
 1. sgn (ipoly p r) \<noteq> sgn (ipoly p y) \<Longrightarrow> (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ur = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ur = x

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
using False x
[PROOF STATE]
proof (prove)
using this:
ur = x
sgn (ipoly p r) \<noteq> sgn (ipoly p y)
real_of_rat y \<le> x
x \<le> real_of_rat r
poly (real_of_int_poly p) x = 0

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)

goal (1 subgoal):
 1. (sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> ((THE x. root_cond plr x) < real_of_rat y) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
(sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)

goal (1 subgoal):
 1. False
[PROOF STEP]
using diff_sign(1) a py0
[PROOF STATE]
proof (prove)
using this:
(sgn (ipoly p y) = sgn (ipoly p r)) = (ur < real_of_rat y)
sgn (ipoly p l) \<noteq> sgn (ipoly p r)
(sgn (ipoly p y) = sgn (ipoly p r)) \<noteq> (ur < real_of_rat y)
ipoly p y \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by(cases "ipoly p r = 0";auto simp:sgn_0_0)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma algebraic_real_iff[code_unfold]: "algebraic = algebraic_real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. algebraic = algebraic_real
[PROOF STEP]
by simp


[STATEMENT]
lemma run_effectE:
  assumes "run c \<sigma> \<sigma>' r"
  assumes "\<not>is_exn \<sigma>'"
  obtains h h' where
    "\<sigma>=Some h" "\<sigma>' = Some h'"
    "effect c h h' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h h'. \<lbrakk>\<sigma> = Some h; \<sigma>' = Some h'; effect c h h' r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run c \<sigma> \<sigma>' r
\<not> is_exn \<sigma>'

goal (1 subgoal):
 1. (\<And>h h'. \<lbrakk>\<sigma> = Some h; \<sigma>' = Some h'; effect c h h' r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding effect_def
[PROOF STATE]
proof (prove)
using this:
run c \<sigma> \<sigma>' r
\<not> is_exn \<sigma>'

goal (1 subgoal):
 1. (\<And>h h'. \<lbrakk>\<sigma> = Some h; \<sigma>' = Some h'; execute c h = Some (r, h')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>\<sigma> = Some h; \<sigma>' = Some h'; execute c h = Some (r, h')\<rbrakk> \<Longrightarrow> thesis; run c \<sigma> \<sigma>' r; \<not> is_exn \<sigma>'; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>h h'. \<lbrakk>\<sigma> = Some h; \<sigma>' = Some h'; execute c h = Some (r, h')\<rbrakk> \<Longrightarrow> thesis; run c \<sigma> \<sigma>' r; \<not> is_exn \<sigma>'; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: run.simps)


[STATEMENT]
lemma run_effectI:
  assumes  "run c (Some h) (Some h') r"
  shows  "effect c h h' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect c h h' r
[PROOF STEP]
using run_effectE[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> is_exn (Some h'); \<And>ha h'a. \<lbrakk>Some h = Some ha; Some h' = Some h'a; effect c ha h'a r\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. effect c h h' r
[PROOF STEP]
by auto


[STATEMENT]
lemma effect_run:
  assumes "effect c h h' r"
  shows "run c (Some h) (Some h') r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run c (Some h) (Some h') r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect c h h' r

goal (1 subgoal):
 1. run c (Some h) (Some h') r
[PROOF STEP]
unfolding effect_def
[PROOF STATE]
proof (prove)
using this:
execute c h = Some (r, h')

goal (1 subgoal):
 1. run c (Some h) (Some h') r
[PROOF STEP]
by (auto intro: run.intros)


[STATEMENT]
lemma success_run:
  assumes "success f h"
  obtains h' r where "run f (Some h) (Some h') r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h' r. run f (Some h) (Some h') r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>h' r. run f (Some h) (Some h') r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
success f h
[PROOF STEP]
obtain r h'
    where "Heap_Monad.execute f h = Some (r, h')"
[PROOF STATE]
proof (prove)
using this:
success f h

goal (1 subgoal):
 1. (\<And>r h'. execute f h = Some (r, h') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding success_def
[PROOF STATE]
proof (prove)
using this:
execute f h \<noteq> None

goal (1 subgoal):
 1. (\<And>r h'. execute f h = Some (r, h') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
execute f h = Some (r, h')

goal (1 subgoal):
 1. (\<And>h' r. run f (Some h) (Some h') r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
execute f h = Some (r, h')
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
execute f h = Some (r, h')

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that[OF regular[of "Some h", simplified]])
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma run_complete:
  obtains \<sigma>' r where "run c \<sigma> \<sigma>' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>' r. run c \<sigma> \<sigma>' r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "is_exn \<sigma>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>\<sigma>' r. run c \<sigma> \<sigma>' r \<Longrightarrow> thesis; is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<sigma>' r. run c \<sigma> \<sigma>' r \<Longrightarrow> thesis; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto intro: run.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<sigma>' r. run c \<sigma> \<sigma>' r \<Longrightarrow> thesis; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "execute c (the_state \<sigma>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>\<sigma>' r. run c \<sigma> \<sigma>' r \<Longrightarrow> thesis; \<not> is_exn \<sigma>; execute c (the_state \<sigma>) = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>\<sigma>' r. run c \<sigma> \<sigma>' r \<Longrightarrow> thesis; \<not> is_exn \<sigma>; execute c (the_state \<sigma>) = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: run.intros)


[STATEMENT]
lemma run_detE:
  assumes "run c \<sigma> \<sigma>' r" "run c \<sigma> \<tau> s"
          "\<not>is_exn \<sigma>"
  obtains "is_exn \<sigma>'" "\<sigma>' = \<tau>" | "\<not> is_exn \<sigma>'" "\<sigma>' = \<tau>" "r = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>is_exn \<sigma>'; \<sigma>' = \<tau>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> is_exn \<sigma>'; \<sigma>' = \<tau>; r = s\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run c \<sigma> \<sigma>' r
run c \<sigma> \<tau> s
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>is_exn \<sigma>'; \<sigma>' = \<tau>\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> is_exn \<sigma>'; \<sigma>' = \<tau>; r = s\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: run.simps)


[STATEMENT]
lemma run_detI:
  assumes "run c (Some h) (Some h') r" "run c (Some h) \<sigma> s"
  shows "\<sigma> = Some h' \<and> r = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> = Some h' \<and> r = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run c (Some h) (Some h') r
run c (Some h) \<sigma> s

goal (1 subgoal):
 1. \<sigma> = Some h' \<and> r = s
[PROOF STEP]
by (auto simp add: run.simps)


[STATEMENT]
lemma run_exn:
  assumes "run f \<sigma> \<sigma>' r"
          "is_exn \<sigma>"
  obtains "\<sigma>'=\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>' = \<sigma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run f \<sigma> \<sigma>' r
is_exn \<sigma>

goal (1 subgoal):
 1. (\<sigma>' = \<sigma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<sigma>' = \<sigma> \<Longrightarrow> thesis; run f \<sigma> \<sigma>' r; is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<sigma>' = \<sigma> \<Longrightarrow> thesis; run f \<sigma> \<sigma>' r; is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto elim!: run.cases intro: that)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma runE[run_elims]:
  assumes "run (f \<bind> g) \<sigma> \<sigma>'' r"
  obtains \<sigma>' r' where
    "run f \<sigma> \<sigma>' r'"
    "run (g r') \<sigma>' \<sigma>'' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (f \<bind> g) \<sigma> \<sigma>'' r

goal (1 subgoal):
 1. (\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "is_exn \<sigma>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis; run (f \<bind> g) \<sigma> \<sigma>'' r; is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis; run (f \<bind> g) \<sigma> \<sigma>'' r; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis; run (f \<bind> g) \<sigma> \<sigma>'' r; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "execute f (the_state \<sigma>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis; run (f \<bind> g) \<sigma> \<sigma>'' r; \<not> is_exn \<sigma>; execute f (the_state \<sigma>) = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis; run (f \<bind> g) \<sigma> \<sigma>'' r; \<not> is_exn \<sigma>; execute f (the_state \<sigma>) = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: run.simps bind_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>\<sigma>' r'. \<lbrakk>run f \<sigma> \<sigma>' r'; run (g r') \<sigma>' \<sigma>'' r\<rbrakk> \<Longrightarrow> thesis; run (f \<bind> g) \<sigma> \<sigma>'' r; \<not> is_exn \<sigma>; execute f (the_state \<sigma>) = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: bind_def run.simps)


[STATEMENT]
lemma runE'[run_elims]:
  assumes "run (f \<then> g) \<sigma> \<sigma>'' res"
  obtains \<sigma>t rt where
    "run f \<sigma> \<sigma>t rt"
    "run g \<sigma>t \<sigma>'' res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>t rt. \<lbrakk>run f \<sigma> \<sigma>t rt; run g \<sigma>t \<sigma>'' res\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (f \<bind> (\<lambda>_. g)) \<sigma> \<sigma>'' res

goal (1 subgoal):
 1. (\<And>\<sigma>t rt. \<lbrakk>run f \<sigma> \<sigma>t rt; run g \<sigma>t \<sigma>'' res\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule_tac runE)


[STATEMENT]
lemma run_return[run_elims]:
  assumes "run (return x) \<sigma> \<sigma>' r"
  obtains "r = x" "\<sigma>' = \<sigma>" "\<not> is_exn \<sigma>" | "\<sigma> = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = x; \<sigma>' = \<sigma>; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<sigma> = None \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (return x) \<sigma> \<sigma>' r

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = x; \<sigma>' = \<sigma>; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<sigma> = None \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>r = x; \<sigma>' = \<sigma>; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<sigma> = None \<Longrightarrow> thesis; run (return x) \<sigma> \<sigma>' r; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>r = x; \<sigma>' = \<sigma>; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<sigma> = None \<Longrightarrow> thesis; run (return x) \<sigma> \<sigma>' r; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>r = x; \<sigma>' = \<sigma>; \<not> is_exn \<sigma>\<rbrakk> \<Longrightarrow> thesis; \<sigma> = None \<Longrightarrow> thesis; run (return x) \<sigma> \<sigma>' r; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: run.simps execute_simps)


[STATEMENT]
lemma run_raise_iff: "run (raise s) \<sigma> \<sigma>' r \<longleftrightarrow> (\<sigma>'=None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (raise s) \<sigma> \<sigma>' r = (\<sigma>' = None)
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<sigma> = None \<Longrightarrow> run (raise s) \<sigma> \<sigma>' r = (\<sigma>' = None)
 2. \<And>a. \<sigma> = Some a \<Longrightarrow> run (raise s) \<sigma> \<sigma>' r = (\<sigma>' = None)
[PROOF STEP]
by (auto simp add: run.simps execute_simps)


[STATEMENT]
lemma run_raise[run_elims]:
  assumes "run (raise s) \<sigma> \<sigma>' r"
  obtains "\<sigma>' = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>' = None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (raise s) \<sigma> \<sigma>' r

goal (1 subgoal):
 1. (\<sigma>' = None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: run_raise_iff)


[STATEMENT]
lemma run_raiseI:
  "run (raise s) \<sigma> None r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (raise s) \<sigma> None r
[PROOF STEP]
by (simp add: run_raise_iff)


[STATEMENT]
lemma run_if[run_elims]:
  assumes "run (if c then t else e) h h' r"
  obtains "c" "run t h h' r"
        | "\<not>c" "run e h h' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>c; run t h h' r\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> c; run e h h' r\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (if c then t else e) h h' r

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>c; run t h h' r\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> c; run e h h' r\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto split: if_split_asm)


[STATEMENT]
lemma run_case_option[run_elims]:
  assumes "run (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "x = None" "run n \<sigma> \<sigma>' r"
        | y where "x = Some y" "run (s y) \<sigma> \<sigma>' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>x = None; run n \<sigma> \<sigma>' r\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>x = Some y; run (s y) \<sigma> \<sigma>' r\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>x = None; run n \<sigma> \<sigma>' r\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>x = Some y; run (s y) \<sigma> \<sigma>' r\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma run_heap[run_elims]:
  assumes "run (Heap_Monad.heap f) \<sigma> \<sigma>' res"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (f (the_state \<sigma>)))"
  and "res = (fst (f (the_state \<sigma>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (f (the_state \<sigma>))); res = fst (f (the_state \<sigma>))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Heap_Monad.heap f) \<sigma> \<sigma>' res
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (f (the_state \<sigma>))); res = fst (f (the_state \<sigma>))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (f (the_state \<sigma>))); res = fst (f (the_state \<sigma>))\<rbrakk> \<Longrightarrow> thesis; run (Heap_Monad.heap f) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (f (the_state \<sigma>))); res = fst (f (the_state \<sigma>))\<rbrakk> \<Longrightarrow> thesis; run (Heap_Monad.heap f) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (f (the_state \<sigma>))); res = fst (f (the_state \<sigma>))\<rbrakk> \<Longrightarrow> thesis; run (Heap_Monad.heap f) \<sigma> \<sigma>' res; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<sigma> = Some a; execute (Heap_Monad.heap f) a = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (f a); res = fst (f a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Heap_Monad.heap f) a = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: execute_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (f a); res = fst (f a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Heap_Monad.heap f) a = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp only: execute_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (f a); res = fst (f a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; (Some \<circ> f) a = Some (res, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (f a); res = fst (f a)\<rbrakk> \<Longrightarrow> thesis; (Some \<circ> f) a = Some (res, h')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal premises prems for a h'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
(Some \<circ> f) a = Some (res, h')
[PROOF STEP]
have "h' = snd (f a)" "res = fst (f a)"
[PROOF STATE]
proof (prove)
using this:
(Some \<circ> f) a = Some (res, h')

goal (1 subgoal):
 1. h' = snd (f a) &&& res = fst (f a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
h' = snd (f a)
res = fst (f a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma run_length[run_elims]:
  assumes "run (Array.len a) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<not>is_exn \<sigma>" "\<sigma>' = \<sigma>" "r = Array.length (the_state \<sigma>) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.len a) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis; run (Array.len a) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa. \<lbrakk>\<lbrakk>\<not> is_exn \<sigma>; \<sigma>' = \<sigma>; r = Array.length (the_state \<sigma>) a\<rbrakk> \<Longrightarrow> thesis; run (Array.len a) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some aa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: run.simps execute_simps)


[STATEMENT]
lemma run_new_array[run_elims]:
  assumes "run (Array.new n x) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>)))"
  and "r = fst (Array.alloc (replicate n x) (the_state \<sigma>))"
  and "Array.get (the_state \<sigma>') r = replicate n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>))); r = fst (Array.alloc (replicate n x) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = replicate n x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.new n x) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>))); r = fst (Array.alloc (replicate n x) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = replicate n x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>))); r = fst (Array.alloc (replicate n x) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = replicate n x\<rbrakk> \<Longrightarrow> thesis; run (Array.new n x) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>))); r = fst (Array.alloc (replicate n x) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = replicate n x\<rbrakk> \<Longrightarrow> thesis; run (Array.new n x) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (replicate n x) (the_state \<sigma>))); r = fst (Array.alloc (replicate n x) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = replicate n x\<rbrakk> \<Longrightarrow> thesis; run (Array.new n x) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: run.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<sigma> = Some a; execute (Array.new n x) a = None; \<sigma>' = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc (replicate n x) a); r = fst (Array.alloc (replicate n x) a); Array.get (snd (Array.alloc (replicate n x) a)) (fst (Array.alloc (replicate n x) a)) = replicate n x\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Array.new n x) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: execute_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc (replicate n x) a); r = fst (Array.alloc (replicate n x) a); Array.get (snd (Array.alloc (replicate n x) a)) (fst (Array.alloc (replicate n x) a)) = replicate n x\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Array.new n x) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: Array.get_alloc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc (replicate n x) a); r = fst (Array.alloc (replicate n x) a)\<rbrakk> \<Longrightarrow> thesis; \<sigma> = Some a; execute (Array.new n x) a = Some (r, h'); \<sigma>' = Some h'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a h'. \<lbrakk>\<lbrakk>h' = snd (Array.alloc (replicate n x) a); r = fst (Array.alloc (replicate n x) a)\<rbrakk> \<Longrightarrow> thesis; execute (Array.new n x) a = Some (r, h')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal premises prems for a h'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
execute (Array.new n x) a = Some (r, h')
[PROOF STEP]
have "h' = snd (Array.alloc (replicate n x) a)"
      "r = fst (Array.alloc (replicate n x) a)"
[PROOF STATE]
proof (prove)
using this:
execute (Array.new n x) a = Some (r, h')

goal (1 subgoal):
 1. h' = snd (Array.alloc (replicate n x) a) &&& r = fst (Array.alloc (replicate n x) a)
[PROOF STEP]
by (auto simp add: execute_simps)
[PROOF STATE]
proof (state)
this:
h' = snd (Array.alloc (replicate n x) a)
r = fst (Array.alloc (replicate n x) a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h' = snd (Array.alloc (replicate n x) a)
r = fst (Array.alloc (replicate n x) a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h' = snd (Array.alloc (replicate n x) a)
r = fst (Array.alloc (replicate n x) a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma run_make[run_elims]:
  assumes "run (Array.make n f) \<sigma> \<sigma>' r"
          "\<not>is_exn \<sigma>"
  obtains "\<sigma>' = Some (snd (Array.alloc (map f [0 ..< n]) (the_state \<sigma>)))"
          "r = fst (Array.alloc (map f [0 ..< n]) (the_state \<sigma>))"
          "Array.get (the_state \<sigma>') r = (map f [0 ..< n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run (Array.make n f) \<sigma> \<sigma>' r
\<not> is_exn \<sigma>

goal (1 subgoal):
 1. (\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis; run (Array.make n f) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis; run (Array.make n f) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis; run (Array.make n f) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis; run (Array.make n f) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<sigma>' = Some (snd (Array.alloc (map f [0..<n]) (the_state \<sigma>))); r = fst (Array.alloc (map f [0..<n]) (the_state \<sigma>)); Array.get (the_state \<sigma>') r = map f [0..<n]\<rbrakk> \<Longrightarrow> thesis; run (Array.make n f) \<sigma> \<sigma>' r; \<not> is_exn \<sigma>; \<sigma> = Some a_\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: run.simps execute_simps Array.get_alloc; fastforce)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done