[STATEMENT]
lemma dvd_sym_div_mult_right [simp]:
  "(a symdiv b) * b = a" if "b > 0" "b dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a symdiv b * b = a
[PROOF STEP]
using sym_mod_sym_div[of b a] that
[PROOF STATE]
proof (prove)
using this:
0 < b \<Longrightarrow> a symmod b = a - a symdiv b * b
0 < b
b dvd a

goal (1 subgoal):
 1. a symdiv b * b = a
[PROOF STEP]
by simp


[STATEMENT]
lemma EM_remainder_converges_of_real_iff:
  fixes f :: "real \<Rightarrow> real"
  assumes "continuous_on {of_int a..} f"
  shows   "EM_remainder_converges n (\<lambda>x. of_real (f x) ::
            'a :: {banach, real_normed_algebra_1, real_inner}) a \<longleftrightarrow> EM_remainder_converges n f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a = EM_remainder_converges n f a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
assume "EM_remainder_converges n (\<lambda>x. of_real (f x) :: 'a) a"
[PROOF STATE]
proof (state)
this:
EM_remainder_converges n (\<lambda>x. of_real (f x)) a

goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
obtain L :: 'a
    where L: "((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (of_int a) (of_int b)) \<longlongrightarrow> L) at_top"
[PROOF STATE]
proof (prove)
using this:
EM_remainder_converges n (\<lambda>x. of_real (f x)) a

goal (1 subgoal):
 1. (\<And>L. ((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b)) \<longlongrightarrow> L) at_top \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: EM_remainder_converges_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b)) \<longlongrightarrow> L) at_top

goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
have "((\<lambda>b. EM_remainder' n f (of_int a) (of_int b)) \<longlongrightarrow> L \<bullet> 1) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top
[PROOF STEP]
proof (rule Lim_transform_eventually)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (?f \<longlongrightarrow> L \<bullet> (1::'a)) at_top
 2. \<forall>\<^sub>F x in at_top. ?f x = EM_remainder' n f (real_of_int a) (real_of_int x)
[PROOF STEP]
show "eventually (\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x) :: 'a) (of_int a) (of_int b) \<bullet> 1 =
            EM_remainder' n f (of_int a) (of_int b)) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F b in at_top. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a) = EM_remainder' n f (real_of_int a) (real_of_int b)
[PROOF STEP]
using eventually_ge_at_top[of a]
[PROOF STATE]
proof (prove)
using this:
eventually ((\<le>) a) at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F b in at_top. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a) = EM_remainder' n f (real_of_int a) (real_of_int b)
[PROOF STEP]
by eventually_elim
         (subst EM_remainder'_bounded_linear [OF bounded_linear_of_real],
          auto intro!: continuous_on_subset[OF assms])
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F b in at_top. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a) = EM_remainder' n f (real_of_int a) (real_of_int b)

goal (1 subgoal):
 1. ((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top
[PROOF STEP]
qed (intro tendsto_intros L)
[PROOF STATE]
proof (state)
this:
((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top

goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
thus "EM_remainder_converges n f a"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top

goal (1 subgoal):
 1. EM_remainder_converges n f a
[PROOF STEP]
unfolding EM_remainder_converges_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top

goal (1 subgoal):
 1. \<exists>L. ((\<lambda>x. EM_remainder' n f (real_of_int a) (real_of_int x)) \<longlongrightarrow> L) at_top
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
EM_remainder_converges n f a

goal (1 subgoal):
 1. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
qed (intro EM_remainder_converges_of_real assms)


[STATEMENT]
lemma at_within_interior:
  "NO_MATCH (UNIV::'a set) (S::'a::topological_space set) \<Longrightarrow> x \<in> interior S \<Longrightarrow> at x within S = at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>NO_MATCH UNIV S; x \<in> interior S\<rbrakk> \<Longrightarrow> at x within S = at x
[PROOF STEP]
by (rule at_within_interior)


[STATEMENT]
lemma sum_conjugate:
  fixes f :: "'b \<Rightarrow> 'a :: conjugatable_ring"
  assumes finX: "finite X"
  shows "conjugate (sum f X) = sum (\<lambda>x. conjugate (f x)) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (sum f X) = (\<Sum>x\<in>X. conjugate (f x))
[PROOF STEP]
using finX
[PROOF STATE]
proof (prove)
using this:
finite X

goal (1 subgoal):
 1. conjugate (sum f X) = (\<Sum>x\<in>X. conjugate (f x))
[PROOF STEP]
by (induct set:finite, auto simp: conjugate_dist_add)


[STATEMENT]
lemma is_pred_succ_no_node: "\<lbrakk>is_adj_map a; u\<notin>V\<rbrakk> \<Longrightarrow> a u = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_adj_map a; u \<notin> V\<rbrakk> \<Longrightarrow> a u = []
[PROOF STEP]
unfolding is_adj_map_def V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u. distinct (a u) \<and> set (a u) = E `` {u} \<union> E\<inverse> `` {u}; u \<notin> {u. \<exists>v. (u, v) \<in> E \<or> (v, u) \<in> E}\<rbrakk> \<Longrightarrow> a u = []
[PROOF STEP]
by auto


[STATEMENT]
lemma invariant_1_2_of_rat: assumes rc: "invariant_1_2 rai"
  shows "real_of_1 rai \<noteq> of_rat x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
obtain p l r where rai: "rai = (p, l, r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p l r. rai = (p, l, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases rai, auto)
[PROOF STATE]
proof (state)
this:
rai = (p, l, r)

goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
from rc[unfolded rai]
[PROOF STATE]
proof (chain)
picking this:
invariant_1_2 (p, l, r)
[PROOF STEP]
have "poly_cond2 p" "ipoly p (the_unique_root (p, l, r)) = 0"
[PROOF STATE]
proof (prove)
using this:
invariant_1_2 (p, l, r)

goal (1 subgoal):
 1. poly_cond2 p &&& poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0
[PROOF STEP]
by (auto elim!: invariant_1E)
[PROOF STATE]
proof (state)
this:
poly_cond2 p
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0

goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
from poly_cond2_no_rat_root[OF this(1), of x] this(2)
[PROOF STATE]
proof (chain)
picking this:
poly (real_of_int_poly p) (real_of_rat x) \<noteq> 0
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly (real_of_int_poly p) (real_of_rat x) \<noteq> 0
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0

goal (1 subgoal):
 1. real_of_1 rai \<noteq> real_of_rat x
[PROOF STEP]
unfolding rai
[PROOF STATE]
proof (prove)
using this:
poly (real_of_int_poly p) (real_of_rat x) \<noteq> 0
poly (real_of_int_poly p) (real_of_1 (p, l, r)) = 0

goal (1 subgoal):
 1. real_of_1 (p, l, r) \<noteq> real_of_rat x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_1 rai \<noteq> real_of_rat x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  shows "(P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
have "(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<sim> P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule Strong_Late_Bisim_SC.sumAssoc)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule strongBisimWeakEq)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uint8_shiftl_code [code]:
  "Rep_uint8 (uint8_shiftl w n) =
  (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined (push_bit :: nat \<Rightarrow> uint8 \<Rightarrow> _) w n)
   else push_bit (nat_of_integer n) (Rep_uint8 w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint8 (uint8_shiftl w n) = (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined push_bit w n) else push_bit (nat_of_integer n) (Rep_uint8 w))
[PROOF STEP]
including undefined_transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint8 (uint8_shiftl w n) = (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined push_bit w n) else push_bit (nat_of_integer n) (Rep_uint8 w))
[PROOF STEP]
unfolding uint8_shiftl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint8 (if n < 0 \<or> 8 \<le> n then undefined push_bit w n else push_bit (nat_of_integer n) w) = (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined push_bit w n) else push_bit (nat_of_integer n) (Rep_uint8 w))
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma add_col_to_multiple_carrier:
  "A \<in> carrier_mat n n \<Longrightarrow> add_col_to_multiple a ks l A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> carrier_mat n n \<Longrightarrow> add_col_to_multiple a ks l A \<in> carrier_mat n n
[PROOF STEP]
by (metis add_col_to_multiple_dim carrier_matD(1) carrier_matD(2) carrier_matI)


[STATEMENT]
lemma all_unrest: "x \<sharp> P \<Longrightarrow> (\<forall> x \<bullet> P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P \<Longrightarrow> (\<forall> x \<bullet> P) = P
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma weak_is_transitive:
 assumes "x \<in> carrier \<and> y \<in> carrier \<and> z \<in> carrier"
 shows "x \<succeq> y \<Longrightarrow> y \<succeq> z \<Longrightarrow> x \<succeq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<succeq> y; y \<succeq> z\<rbrakk> \<Longrightarrow> x \<succeq> z
[PROOF STEP]
by (meson transD transitivity)


[STATEMENT]
lemma "prime (8504276003 :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 8504276003
[PROOF STEP]
by (pratt (code))


[STATEMENT]
lemma Unassigned_not_to_Member: "\<not> allowed_subnet_flow Unassigned Member"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> allowed_subnet_flow Unassigned Member
[PROOF STEP]
by(simp)


[STATEMENT]
lemma escape_rate_pos: "0 < escape_rate x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < escape_rate x
[PROOF STEP]
using positive_weight
[PROOF STATE]
proof (prove)
using this:
0 < \<integral>\<^sup>+ x. ennreal (R ?x x) \<partial>count_space UNIV

goal (1 subgoal):
 1. 0 < escape_rate x
[PROOF STEP]
unfolding ennreal_escape_rate[symmetric]
[PROOF STATE]
proof (prove)
using this:
0 < ennreal (escape_rate ?x)

goal (1 subgoal):
 1. 0 < escape_rate x
[PROOF STEP]
by simp


[STATEMENT]
lemma list_split_two_elems:
  assumes "distinct xs"
    and "x \<in> set xs" and "y \<in> set xs"
    and "x \<noteq> y"
  shows "\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
obtain as bs where as_bs: "xs = as @ [x] @ bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as bs. xs = as @ [x] @ bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) split_list_first
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>as bs. xs = as @ [x] @ bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = as @ [x] @ bs

goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
proof(cases "y \<in> set as")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
 2. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> set as

goal (2 subgoals):
 1. y \<in> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
 2. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set as
[PROOF STEP]
obtain cs ds where "as = cs @ [y] @ ds"
[PROOF STATE]
proof (prove)
using this:
y \<in> set as

goal (1 subgoal):
 1. (\<And>cs ds. as = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3) split_list_first
[PROOF STATE]
proof (prove)
using this:
y \<in> set as
y \<in> set xs
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>cs ds. as = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
as = cs @ [y] @ ds

goal (2 subgoals):
 1. y \<in> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
 2. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as = cs @ [y] @ ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = cs @ [y] @ ds

goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
by (auto simp add: as_bs)
[PROOF STATE]
proof (state)
this:
\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> set as

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> set as
[PROOF STEP]
have "y \<in> set bs"
[PROOF STATE]
proof (prove)
using this:
y \<notin> set as

goal (1 subgoal):
 1. y \<in> set bs
[PROOF STEP]
using as_bs assms(3) assms(4)
[PROOF STATE]
proof (prove)
using this:
y \<notin> set as
xs = as @ [x] @ bs
y \<in> set xs
x \<noteq> y

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

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set bs
[PROOF STEP]
obtain cs ds where "bs = cs @ [y] @ ds"
[PROOF STATE]
proof (prove)
using this:
y \<in> set bs

goal (1 subgoal):
 1. (\<And>cs ds. bs = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3) split_list_first
[PROOF STATE]
proof (prove)
using this:
y \<in> set bs
y \<in> set xs
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. (\<And>cs ds. bs = cs @ [y] @ ds \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bs = cs @ [y] @ ds

goal (1 subgoal):
 1. y \<notin> set as \<Longrightarrow> \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bs = cs @ [y] @ ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bs = cs @ [y] @ ds

goal (1 subgoal):
 1. \<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf
[PROOF STEP]
by (auto simp add: as_bs)
[PROOF STATE]
proof (state)
this:
\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pre mid suf. xs = pre @ x # mid @ y # suf \<or> xs = pre @ y # mid @ x # suf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atom_map_compl_pres: "atom_map (-x) = Collect atom - atom_map x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
have "(y \<in> atom_map (-x)) = (atom y \<and> y \<le> -x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> atom_map (- x)) = (atom y \<and> y \<le> - x)
[PROOF STEP]
by (simp add: atom_map_def)
[PROOF STATE]
proof (state)
this:
(y \<in> atom_map (- x)) = (atom y \<and> y \<le> - x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y \<in> atom_map (- x)) = (atom y \<and> y \<le> - x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
have "... = (atom y \<and> \<not>(y \<le> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom y \<and> y \<le> - x) = (atom y \<and> \<not> y \<le> x)
[PROOF STEP]
by (metis atom_sup_iff inf.orderE inf_shunt sup_compl_top top.ordering_top_axioms ordering_top.extremum)
[PROOF STATE]
proof (state)
this:
(atom y \<and> y \<le> - x) = (atom y \<and> \<not> y \<le> x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(atom y \<and> y \<le> - x) = (atom y \<and> \<not> y \<le> x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
have "... = (y \<in> Collect atom - atom_map x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom y \<and> \<not> y \<le> x) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
using atom_map_def
[PROOF STATE]
proof (prove)
using this:
atom_map ?x = {y. atom y \<and> y \<le> ?x}

goal (1 subgoal):
 1. (atom y \<and> \<not> y \<le> x) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(atom y \<and> \<not> y \<le> x) = (y \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
have "(y \<in> atom_map (-x)) = (y \<in> Collect atom - atom_map x)"
[PROOF STATE]
proof (prove)
using this:
(y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. (y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(y \<in> atom_map (- x)) = (y \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?y2 \<in> atom_map (- x)) = (?y2 \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?y2 \<in> atom_map (- x)) = (?y2 \<in> Collect atom - atom_map x)

goal (1 subgoal):
 1. atom_map (- x) = Collect atom - atom_map x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
atom_map (- x) = Collect atom - atom_map x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma betaupright_upright_vut:
  assumes "beta_upright va vb"
    and     "upright vb"
    and     "vacant_upto (va + vb) t"
  shows   "vacant_upto va t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
assume s: "s \<le> t" "zcount va s > 0"
[PROOF STATE]
proof (state)
this:
s \<le> t
0 < zcount va s

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
[PROOF STEP]
obtain x where x: "x < s" "zcount va x < 0 \<or> zcount vb x < 0" "nonpos_upto va x"
[PROOF STATE]
proof (prove)
using this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using betaupright_obtain_support
[PROOF STATE]
proof (prove)
using this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
\<lbrakk>beta_upright ?va ?vb; 0 < zcount ?va ?t; \<And>s. \<lbrakk>s < ?t; zcount ?va s < 0 \<or> zcount ?vb s < 0; nonpos_upto ?va s\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x

goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "zcount va x < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
zcount va x < 0

goal (2 subgoals):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms(2,3) s x(1,3)
[PROOF STATE]
proof (chain)
picking this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
nonpos_upto va x
zcount va x < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
nonpos_upto va x
zcount va x < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
upright vb
\<forall>s\<le>t. zcount (va + vb) s = 0
s \<le> t
0 < zcount va s
x < s
nonpos_upto va x
zcount va x < 0

goal (1 subgoal):
 1. False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>upright vb; \<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule upright_obtain_support[of vb x])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0\<rbrakk> \<Longrightarrow> 0 < zcount vb x
 2. \<And>sa. \<lbrakk>\<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0; sa < x; zcount vb sa < 0; nonpos_upto vb sa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add_less_same_cancel2 order.trans order.strict_implies_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t; 0 < zcount va s; x < s; nonpos_upto va x; zcount va x < 0; sa < x; zcount vb sa < 0; nonpos_upto vb sa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add_less_same_cancel1 add_neg_neg order.order_iff_strict order.trans less_irrefl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> zcount va x < 0

goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms s x
[PROOF STATE]
proof (chain)
picking this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
\<not> zcount va x < 0
[PROOF STEP]
have "x \<le> t" "zcount va x > 0"
[PROOF STATE]
proof (prove)
using this:
beta_upright va vb
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
\<not> zcount va x < 0

goal (1 subgoal):
 1. x \<le> t &&& 0 < zcount va x
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>beta_upright va vb; upright vb; vacant_upto (va + vb) t; s \<le> t; 0 < zcount va s; x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> x \<le> t
 2. \<lbrakk>beta_upright va vb; upright vb; vacant_upto (va + vb) t; s \<le> t; 0 < zcount va s; x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> 0 < zcount va x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>beta_upright va vb; upright vb; vacant_upto (va + vb) t; s \<le> t; 0 < zcount va s; x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> 0 < zcount va x
[PROOF STEP]
apply (metis (no_types, opaque_lifting) add.left_neutral order.order_iff_strict order.trans vacant_upto_def zcount_union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
x \<le> t
0 < zcount va x

goal (1 subgoal):
 1. \<lbrakk>x < s; zcount va x < 0 \<or> zcount vb x < 0; nonpos_upto va x; \<not> zcount va x < 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms(2,3) s x
[PROOF STATE]
proof (chain)
picking this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
x \<le> t
0 < zcount va x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
upright vb
vacant_upto (va + vb) t
s \<le> t
0 < zcount va s
x < s
zcount va x < 0 \<or> zcount vb x < 0
nonpos_upto va x
x \<le> t
0 < zcount va x

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

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

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s2 \<le> t; 0 < zcount va ?s2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
note r = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s2 \<le> t; 0 < zcount va ?s2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
upright vb
vacant_upto (va + vb) t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
upright vb
vacant_upto (va + vb) t

goal (1 subgoal):
 1. vacant_upto va t
[PROOF STEP]
unfolding vacant_upto_def
[PROOF STATE]
proof (prove)
using this:
upright vb
\<forall>s\<le>t. zcount (va + vb) s = 0

goal (1 subgoal):
 1. \<forall>s\<le>t. zcount va s = 0
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>upright vb; \<forall>s\<le>t. zcount va s + zcount vb s = 0; s \<le> t\<rbrakk> \<Longrightarrow> zcount va s = 0
[PROOF STEP]
apply (metis (no_types, opaque_lifting) r add_cancel_right_left order.order_iff_strict order.trans le_less_linear less_add_same_cancel2 upright_obtain_support)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
vacant_upto va t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gbinomial_int_mult_fact: "fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - int i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - int i)
[PROOF STEP]
by (simp only: gbinomial_int_pochhammer' fact_dvd_pochhammer dvd_mult_div_cancel falling_fact_pochhammer')


[STATEMENT]
lemma step_size_ok_3: "\<lbrakk>
  invar (States dir big small);
  step (States dir big small) = States dir' big' small';
  remaining_steps (States dir big small) + 1 \<le> 4 * size small
\<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \<le> 4 * size small\<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'
[PROOF STEP]
using remaining_steps_decline step_size_small
[PROOF STATE]
proof (prove)
using this:
invar ?states \<Longrightarrow> remaining_steps (step ?states) \<le> remaining_steps ?states
\<lbrakk>invar (States ?dir ?big ?small); step (States ?dir ?big ?small) = States ?dir' ?big' ?small'\<rbrakk> \<Longrightarrow> size ?small' = size ?small

goal (1 subgoal):
 1. \<lbrakk>invar (States dir big small); step (States dir big small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \<le> 4 * size small\<rbrakk> \<Longrightarrow> remaining_steps (States dir' big' small') + 1 \<le> 4 * size small'
[PROOF STEP]
by (metis Suc_eq_plus1 Suc_le_mono le_trans)


[STATEMENT]
lemma stake_nil[simp]:
  "stake i \<sigma> = [] \<longleftrightarrow> i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stake i \<sigma> = []) = (i = 0)
[PROOF STEP]
by (cases i; clarsimp)