[STATEMENT]
lemma is_interval_uminusI:
  assumes "is_interval X"
  shows "is_interval (uminus ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interval (uminus ` X)
[PROOF STEP]
unfolding is_interval_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>uminus ` X. \<forall>b\<in>uminus ` X. \<forall>x. (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i) \<longrightarrow> x \<in> uminus ` X
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x b xa xb. \<lbrakk>x \<in> X; xa \<in> X; \<forall>i\<in>Basis. - x \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - xa \<bullet> i \<or> - xa \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - x \<bullet> i\<rbrakk> \<Longrightarrow> xb \<in> uminus ` X
[PROOF STEP]
fix b d e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x b xa xb. \<lbrakk>x \<in> X; xa \<in> X; \<forall>i\<in>Basis. - x \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - xa \<bullet> i \<or> - xa \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - x \<bullet> i\<rbrakk> \<Longrightarrow> xb \<in> uminus ` X
[PROOF STEP]
assume "b \<in> X" "d \<in> X"
    "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
       (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
[PROOF STATE]
proof (state)
this:
b \<in> X
d \<in> X
\<forall>i\<in>Basis. - b \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> - d \<bullet> i \<or> - d \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> - b \<bullet> i

goal (1 subgoal):
 1. \<And>a x b xa xb. \<lbrakk>x \<in> X; xa \<in> X; \<forall>i\<in>Basis. - x \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - xa \<bullet> i \<or> - xa \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - x \<bullet> i\<rbrakk> \<Longrightarrow> xb \<in> uminus ` X
[PROOF STEP]
hence "- e \<in> X"
[PROOF STATE]
proof (prove)
using this:
b \<in> X
d \<in> X
\<forall>i\<in>Basis. - b \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> - d \<bullet> i \<or> - d \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> - b \<bullet> i

goal (1 subgoal):
 1. - e \<in> X
[PROOF STEP]
by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
      (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
- e \<in> X

goal (1 subgoal):
 1. \<And>a x b xa xb. \<lbrakk>x \<in> X; xa \<in> X; \<forall>i\<in>Basis. - x \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - xa \<bullet> i \<or> - xa \<bullet> i \<le> xb \<bullet> i \<and> xb \<bullet> i \<le> - x \<bullet> i\<rbrakk> \<Longrightarrow> xb \<in> uminus ` X
[PROOF STEP]
thus "e \<in> uminus ` X"
[PROOF STATE]
proof (prove)
using this:
- e \<in> X

goal (1 subgoal):
 1. e \<in> uminus ` X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
e \<in> uminus ` X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>(P, t, Q). {P} t\<succ> {Q})
[PROOF STEP]
apply (rule inj_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; (case x of (P, t, Q) \<Rightarrow> {P} t\<succ> {Q}) = (case y of (P, t, Q) \<Rightarrow> {P} t\<succ> {Q})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in information_space) entropy_le_space:
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
  assumes X: "distributed M MX X Px" and Px_nn[simp]: "\<And>x. x \<in> space MX \<Longrightarrow> 0 \<le> Px x"
  and fin: "finite_measure MX"
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
  shows "entropy b MX X \<le> log b (measure MX (space MX))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
note Px = distributed_borel_measurable[OF X]
[PROOF STATE]
proof (state)
this:
(\<lambda>x. ennreal (Px x)) \<in> borel_measurable MX

goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
interpret finite_measure MX
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_measure MX
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
have "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. entropy b MX X \<le> log b \<P>(x in MX. Px x \<noteq> 0)
[PROOF STEP]
using int X
[PROOF STATE]
proof (prove)
using this:
integrable MX (\<lambda>x. - Px x * log b (Px x))
distributed M MX X (\<lambda>x. ennreal (Px x))

goal (1 subgoal):
 1. entropy b MX X \<le> log b \<P>(x in MX. Px x \<noteq> 0)
[PROOF STEP]
by (intro entropy_le) auto
[PROOF STATE]
proof (state)
this:
entropy b MX X \<le> log b \<P>(x in MX. Px x \<noteq> 0)

goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
entropy b MX X \<le> log b \<P>(x in MX. Px x \<noteq> 0)

goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
have "\<dots> \<le> log b (measure MX (space MX))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log b \<P>(x in MX. Px x \<noteq> 0) \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
using Px distributed_imp_emeasure_nonzero[OF X]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. ennreal (Px x)) \<in> borel_measurable MX
emeasure MX {x \<in> space MX. ennreal (Px x) \<noteq> 0} \<noteq> 0

goal (1 subgoal):
 1. log b \<P>(x in MX. Px x \<noteq> 0) \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
by (intro log_le)
       (auto intro!: finite_measure_mono b_gt_1 less_le[THEN iffD2]
             simp: emeasure_eq_measure cong: conj_cong)
[PROOF STATE]
proof (state)
this:
log b \<P>(x in MX. Px x \<noteq> 0) \<le> log b (Sigma_Algebra.measure MX (space MX))

goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))

goal (1 subgoal):
 1. entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
entropy b MX X \<le> log b (Sigma_Algebra.measure MX (space MX))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "fst (x, y) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (x, y) = x
[PROOF STEP]
nitpick [expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (x, y) = x
[PROOF STEP]
by (simp add: fst_def)


[STATEMENT]
lemma finite_imp_bounded_convex_hull:
  fixes s :: "'a::real_normed_vector set"
  shows "finite s \<Longrightarrow> bounded (convex hull s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s \<Longrightarrow> bounded (convex hull s)
[PROOF STEP]
using bounded_convex_hull finite_imp_bounded
[PROOF STATE]
proof (prove)
using this:
bounded ?s \<Longrightarrow> bounded (convex hull ?s)
finite ?S \<Longrightarrow> bounded ?S

goal (1 subgoal):
 1. finite s \<Longrightarrow> bounded (convex hull s)
[PROOF STEP]
by auto


[STATEMENT]
lemma Int_stableD:
  "Int_stable M \<Longrightarrow> a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Int_stable M; a \<in> M; b \<in> M\<rbrakk> \<Longrightarrow> a \<inter> b \<in> M
[PROOF STEP]
unfolding Int_stable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>M. \<forall>b\<in>M. a \<inter> b \<in> M; a \<in> M; b \<in> M\<rbrakk> \<Longrightarrow> a \<inter> b \<in> M
[PROOF STEP]
by auto


[STATEMENT]
lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \<Omega> M \<mu>) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (measure_of \<Omega> M \<mu>) = M
[PROOF STEP]
using space_closed
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> Pow \<Omega>

goal (1 subgoal):
 1. sets (measure_of \<Omega> M \<mu>) = M
[PROOF STEP]
by (auto intro!: sigma_sets_eq)


[STATEMENT]
lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
  for a :: "'a::real_normed_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at a = filtermap (\<lambda>x. x + a) (at (0::'a))
[PROOF STEP]
using filtermap_at_shift[of "-a" 0]
[PROOF STATE]
proof (prove)
using this:
filtermap (\<lambda>x. x - - a) (at (0::'a)) = at ((0::'a) - - a)

goal (1 subgoal):
 1. at a = filtermap (\<lambda>x. x + a) (at (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma filterlim_divide_at_infinity:
  fixes f g :: "'a \<Rightarrow> 'a :: real_normed_field"
  assumes "filterlim f (nhds c) F" "filterlim g (at 0) F" "c \<noteq> 0"
  shows   "filterlim (\<lambda>x. f x / g x) at_infinity F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x F. f x / g x :> at_infinity
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LIM x F. f x / g x :> at_infinity
[PROOF STEP]
have "filterlim (\<lambda>x. f x * inverse (g x)) at_infinity F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x F. f x * inverse (g x) :> at_infinity
[PROOF STEP]
by (intro tendsto_mult_filterlim_at_infinity[OF assms(1,3)]
          filterlim_compose [OF filterlim_inverse_at_infinity assms(2)])
[PROOF STATE]
proof (state)
this:
LIM x F. f x * inverse (g x) :> at_infinity

goal (1 subgoal):
 1. LIM x F. f x / g x :> at_infinity
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
LIM x F. f x * inverse (g x) :> at_infinity

goal (1 subgoal):
 1. LIM x F. f x / g x :> at_infinity
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
LIM x F. f x / g x :> at_infinity

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eventually_floor_less:
  fixes f :: "'a \<Rightarrow> 'b::{order_topology,floor_ceiling}"
  assumes f: "(f \<longlongrightarrow> l) F"
    and l: "l \<notin> \<int>"
  shows "\<forall>\<^sub>F x in F. of_int (floor l) < f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. of_int \<lfloor>l\<rfloor> < f x
[PROOF STEP]
by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l)


[STATEMENT]
lemma bij_module_hom_imp_inv_module_hom: "module_hom scale1 scale2 f \<Longrightarrow> bij f \<Longrightarrow>
  module_hom scale2 scale1 (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>module_hom scale1 scale2 f; bij f\<rbrakk> \<Longrightarrow> module_hom scale2 scale1 (inv f)
[PROOF STEP]
by (auto simp: module_hom_iff bij_is_surj bij_is_inj surj_f_inv_f
      intro!: Hilbert_Choice.inv_f_eq)


[STATEMENT]
lemma limit_vimage: "(a \<in> limit x) = infinite (x -` {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<in> limit x) = infinite (x -` {a})
[PROOF STEP]
by (simp add: limit_def Inf_many_def vimage_def)


[STATEMENT]
lemma contour_integrable_joinD2:
  assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2"
    shows "f contour_integrable_on g2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
obtain s2
    where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on g1 +++ g2
valid_path g2

goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
[PROOF STATE]
proof (state)
this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
have "(\<lambda>x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}
[PROOF STEP]
using assms integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"]
                integrable_on_subcbox [where a="1/2" and b=1]
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on g1 +++ g2
valid_path g2
\<lbrakk>?f integrable_on cbox (1 / 2) 1; 1 / 2 \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. ?f ((1 / 2) *\<^sub>R x + 1 / 2)) integrable_on (\<lambda>x. (1 / (1 / 2)) *\<^sub>R x + - ((1 / (1 / 2)) *\<^sub>R (1 / 2))) ` cbox (1 / 2) 1
\<lbrakk>?f integrable_on ?S; cbox ((1::?'a1) / (2::?'a1)) (1::?'a1) \<subseteq> ?S\<rbrakk> \<Longrightarrow> ?f integrable_on cbox ((1::?'a1) / (2::?'a1)) (1::?'a1)

goal (1 subgoal):
 1. (\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}
[PROOF STEP]
by (fastforce simp: contour_integrable_on image_affinity_atLeastAtMost_diff)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}

goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}
[PROOF STEP]
have *: "(\<lambda>x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2)))
                integrable_on {0..1}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}

goal (1 subgoal):
 1. (\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) / 2 * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}
[PROOF STEP]
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f ((g1 +++ g2) (x / 2 + 1 / 2)) / 2 * vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2))) integrable_on {0..1}

goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
have g2: "vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
            2 *\<^sub>R vector_derivative g2 (at z)"
        if "0 < z" "z < 1" "z \<notin> s2" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at (z / 2 + 1 / 2)) = 2 *\<^sub>R vector_derivative g2 (at z)
[PROOF STEP]
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (?f1 has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))
 2. 0 < ?d1
 3. z / 2 + 1 / 2 \<in> UNIV
 4. \<And>x'. \<lbrakk>x' \<in> UNIV; dist x' (z / 2 + 1 / 2) < ?d1\<rbrakk> \<Longrightarrow> ?f1 x' = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
[PROOF STEP]
show "0 < \<bar>z/2\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<bar>z / 2\<bar>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < z
z < 1
z \<notin> s2

goal (1 subgoal):
 1. 0 < \<bar>z / 2\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < \<bar>z / 2\<bar>

goal (3 subgoals):
 1. (?f1 has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))
 2. z / 2 + 1 / 2 \<in> UNIV
 3. \<And>x'. \<lbrakk>x' \<in> UNIV; dist x' (z / 2 + 1 / 2) < \<bar>z / 2\<bar>\<rbrakk> \<Longrightarrow> ?f1 x' = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
[PROOF STEP]
have \<section>: "((\<lambda>x. x * 2 - 1) has_vector_derivative 2) (at ((1 + z)/2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. x * 2 - 1) has_vector_derivative 2) (at ((1 + z) / 2))
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. ((\<lambda>x. x * 2 - 1) has_vector_derivative 2) (at ((1 + z) / 2))
[PROOF STEP]
by (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. x * 2 - 1) has_vector_derivative 2) (at ((1 + z) / 2))

goal (3 subgoals):
 1. (?f1 has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))
 2. z / 2 + 1 / 2 \<in> UNIV
 3. \<And>x'. \<lbrakk>x' \<in> UNIV; dist x' (z / 2 + 1 / 2) < \<bar>z / 2\<bar>\<rbrakk> \<Longrightarrow> ?f1 x' = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
[PROOF STEP]
have "(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g2 has_vector_derivative vector_derivative g2 (at z)) (at z)
[PROOF STEP]
using s2 that
[PROOF STATE]
proof (prove)
using this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x
0 < z
z < 1
z \<notin> s2

goal (1 subgoal):
 1. (g2 has_vector_derivative vector_derivative g2 (at z)) (at z)
[PROOF STEP]
by (auto simp: vector_derivative_works)
[PROOF STATE]
proof (state)
this:
(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)

goal (3 subgoals):
 1. (?f1 has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))
 2. z / 2 + 1 / 2 \<in> UNIV
 3. \<And>x'. \<lbrakk>x' \<in> UNIV; dist x' (z / 2 + 1 / 2) < \<bar>z / 2\<bar>\<rbrakk> \<Longrightarrow> ?f1 x' = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)
[PROOF STEP]
show "((\<lambda>x. g2 (2*x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z/2 + 1/2))"
[PROOF STATE]
proof (prove)
using this:
(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)

goal (1 subgoal):
 1. ((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))
[PROOF STEP]
using vector_diff_chain_at [OF \<section>]
[PROOF STATE]
proof (prove)
using this:
(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)
(?g has_vector_derivative ?g') (at ((1 + z) / 2 * 2 - 1)) \<Longrightarrow> (?g \<circ> (\<lambda>x. x * 2 - 1) has_vector_derivative 2 *\<^sub>R ?g') (at ((1 + z) / 2))

goal (1 subgoal):
 1. ((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))
[PROOF STEP]
by (auto simp: field_simps o_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at z)) (at (z / 2 + 1 / 2))

goal (2 subgoals):
 1. z / 2 + 1 / 2 \<in> UNIV
 2. \<And>x'. \<lbrakk>x' \<in> UNIV; dist x' (z / 2 + 1 / 2) < \<bar>z / 2\<bar>\<rbrakk> \<Longrightarrow> g2 (2 * x' - 1) = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
[PROOF STEP]
qed (use that in \<open>simp_all add: field_simps dist_real_def abs_if split: if_split_asm\<close>)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?z; ?z < 1; ?z \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at (?z / 2 + 1 / 2)) = 2 *\<^sub>R vector_derivative g2 (at ?z)

goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
have fin01: "finite ({0, 1} \<union> s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({0, 1} \<union> s2)
[PROOF STEP]
by (simp add: s2)
[PROOF STATE]
proof (state)
this:
finite ({0, 1} \<union> s2)

goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f contour_integrable_on g2
[PROOF STEP]
unfolding contour_integrable_on
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. f (g2 t) * vector_derivative g2 (at t)) integrable_on {0..1}
[PROOF STEP]
by (intro integrable_spike_finite [OF fin01 _ *]) (auto simp: joinpaths_def scaleR_conv_of_real g2)
[PROOF STATE]
proof (state)
this:
f contour_integrable_on g2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in weak_lower_semilattice) finite_inf_greatest:
  "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
[PROOF STEP]
proof (induct set: finite)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> carrier L; {} \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>{}) {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier L; F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>F) F; insert x F \<subseteq> carrier L; insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>insert x F) (insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> carrier L
{} \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>{} \<subseteq> carrier L; {} \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>{}) {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier L; F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>F) F; insert x F \<subseteq> carrier L; insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>insert x F) (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<subseteq> carrier L
{} \<noteq> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> carrier L
{} \<noteq> {}

goal (1 subgoal):
 1. is_glb L (\<Sqinter>{}) {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_glb L (\<Sqinter>{}) {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier L; F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>F) F; insert x F \<subseteq> carrier L; insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>insert x F) (insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier L; F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>F) F; insert x F \<subseteq> carrier L; insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>insert x F) (insert x F)
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier L; F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>F) F; insert x F \<subseteq> carrier L; insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>insert x F) (insert x F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
proof (cases "A = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
 2. A \<noteq> {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = {}

goal (2 subgoals):
 1. A = {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
 2. A \<noteq> {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
with insert
[PROOF STATE]
proof (chain)
picking this:
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}
A = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}
A = {}

goal (1 subgoal):
 1. is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
        inf_of_singleton_closed inf_of_singletonI)
[PROOF STATE]
proof (state)
this:
is_glb L (\<Sqinter>insert x A) (insert x A)

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}

goal (1 subgoal):
 1. is_glb L (\<Sqinter>insert x A) (insert x A)
[PROOF STEP]
proof (rule_tac inf_insertI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}; is_glb L i (insert x A)\<rbrakk> \<Longrightarrow> is_glb L i (insert x A)
 2. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L ?a5 A
 3. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> carrier L
 4. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}\<rbrakk> \<Longrightarrow> A \<subseteq> carrier L
[PROOF STEP]
from False insert
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}
[PROOF STEP]
show "greatest L (\<Sqinter>A) (Lower L A)"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
finite A
x \<notin> A
\<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A
insert x A \<subseteq> carrier L
insert x A \<noteq> {}

goal (1 subgoal):
 1. is_glb L (\<Sqinter>A) A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_glb L (\<Sqinter>A) A

goal (3 subgoals):
 1. \<And>i. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}; is_glb L i (insert x A)\<rbrakk> \<Longrightarrow> is_glb L i (insert x A)
 2. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> carrier L
 3. \<lbrakk>finite A; x \<notin> A; \<lbrakk>A \<subseteq> carrier L; A \<noteq> {}\<rbrakk> \<Longrightarrow> is_glb L (\<Sqinter>A) A; insert x A \<subseteq> carrier L; insert x A \<noteq> {}\<rbrakk> \<Longrightarrow> A \<subseteq> carrier L
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
is_glb L (\<Sqinter>insert x A) (insert x A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_glb L (\<Sqinter>insert x A) (insert x A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_interior_convex_scaleR:
  fixes S :: "'n::euclidean_space set"
  assumes "convex S"
  shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*\<^sub>R) c ` rel_interior S = rel_interior ((*\<^sub>R) c ` S)
[PROOF STEP]
by (metis assms linear_scaleR rel_interior_convex_linear_image)


[STATEMENT]
lemma coplanar_linear_image_eq:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes "linear f" "inj f" shows "coplanar(f ` S) = coplanar S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coplanar (f ` S) = coplanar S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. coplanar (f ` S) \<Longrightarrow> coplanar S
 2. coplanar S \<Longrightarrow> coplanar (f ` S)
[PROOF STEP]
assume "coplanar S"
[PROOF STATE]
proof (state)
this:
coplanar S

goal (2 subgoals):
 1. coplanar (f ` S) \<Longrightarrow> coplanar S
 2. coplanar S \<Longrightarrow> coplanar (f ` S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
coplanar S
[PROOF STEP]
show "coplanar (f ` S)"
[PROOF STATE]
proof (prove)
using this:
coplanar S

goal (1 subgoal):
 1. coplanar (f ` S)
[PROOF STEP]
using assms(1) coplanar_linear_image
[PROOF STATE]
proof (prove)
using this:
coplanar S
linear f
\<lbrakk>coplanar ?S; linear ?f\<rbrakk> \<Longrightarrow> coplanar (?f ` ?S)

goal (1 subgoal):
 1. coplanar (f ` S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
coplanar (f ` S)

goal (1 subgoal):
 1. coplanar (f ` S) \<Longrightarrow> coplanar S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coplanar (f ` S) \<Longrightarrow> coplanar S
[PROOF STEP]
obtain g where g: "linear g" "g \<circ> f = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>linear g; g \<circ> f = id\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using linear_injective_left_inverse [OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>g. linear g \<and> g \<circ> f = id

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>linear g; g \<circ> f = id\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
linear g
g \<circ> f = id

goal (1 subgoal):
 1. coplanar (f ` S) \<Longrightarrow> coplanar S
[PROOF STEP]
assume "coplanar (f ` S)"
[PROOF STATE]
proof (state)
this:
coplanar (f ` S)

goal (1 subgoal):
 1. coplanar (f ` S) \<Longrightarrow> coplanar S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
coplanar (f ` S)
[PROOF STEP]
show "coplanar S"
[PROOF STATE]
proof (prove)
using this:
coplanar (f ` S)

goal (1 subgoal):
 1. coplanar S
[PROOF STEP]
by (metis coplanar_linear_image g(1) g(2) id_apply image_comp image_id)
[PROOF STATE]
proof (state)
this:
coplanar S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qfree p; qfree q\<rbrakk> \<Longrightarrow> qfree (MIR.iff p q)
[PROOF STEP]
by (unfold iff_def,cases "p=q", auto)


[STATEMENT]
lemma a_\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d_\<beta> p l" and lp: "l>0"
  shows "(\<exists> x. l dvd x \<and> Ifm (real_of_int x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm (real_of_int x#bs) p)"
  (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l))
[PROOF STEP]
using unity_coeff_ex[where l="l" and P="?P", simplified]
[PROOF STATE]
proof (prove)
using this:
\<exists>x. Ifm (real_of_int l * real_of_int x # bs) (a_\<beta> p l) \<equiv> \<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)

goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l))

goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l))

goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
have "\<dots> = (\<exists> (x::int). ?P' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
using a_\<beta>[OF linp d lp]
[PROOF STATE]
proof (prove)
using this:
iszlfm (a_\<beta> p l) (a # bs) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> Ifm (real_of_int (l * ?x) # bs) (a_\<beta> p l) = Ifm (real_of_int ?x # bs) p

goal (1 subgoal):
 1. (\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>x. Ifm (real_of_int (l * x) # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)

goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)

goal (1 subgoal):
 1. (\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<exists>x. l dvd x \<and> Ifm (real_of_int x # bs) (a_\<beta> p l)) = (\<exists>x. Ifm (real_of_int x # bs) p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rplusinf_ex:
  assumes lp: "isrlfm p"
  and ex: "Ifm (a#bs) (plusinf p)"
  shows "\<exists> x. Ifm (x#bs) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
from bound0_I [OF rplusinf_bound0[OF lp], where b="a" and bs ="bs"] ex
[PROOF STATE]
proof (chain)
picking this:
Ifm (a # bs) (plusinf p) = Ifm (?b' # bs) (plusinf p)
Ifm (a # bs) (plusinf p)
[PROOF STEP]
have th: "\<forall> x. Ifm (x#bs) (plusinf p)"
[PROOF STATE]
proof (prove)
using this:
Ifm (a # bs) (plusinf p) = Ifm (?b' # bs) (plusinf p)
Ifm (a # bs) (plusinf p)

goal (1 subgoal):
 1. \<forall>x. Ifm (x # bs) (plusinf p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. Ifm (x # bs) (plusinf p)

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
from rplusinf_inf[OF lp, where bs="bs"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. \<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p
[PROOF STEP]
obtain z where z_def: "\<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p"
[PROOF STATE]
proof (prove)
using this:
\<exists>z. \<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p

goal (1 subgoal):
 1. (\<And>z. \<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
from th
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. Ifm (x # bs) (plusinf p)
[PROOF STEP]
have "Ifm ((z + 1)#bs) (plusinf p)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. Ifm (x # bs) (plusinf p)

goal (1 subgoal):
 1. Ifm ((z + 1) # bs) (plusinf p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ifm ((z + 1) # bs) (plusinf p)

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ifm ((z + 1) # bs) (plusinf p)

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
have "z + 1 > z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z < z + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z < z + 1

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Ifm ((z + 1) # bs) (plusinf p)
z < z + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ifm ((z + 1) # bs) (plusinf p)
z < z + 1

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
using z_def
[PROOF STATE]
proof (prove)
using this:
Ifm ((z + 1) # bs) (plusinf p)
z < z + 1
\<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p

goal (1 subgoal):
 1. \<exists>x. Ifm (x # bs) p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. Ifm (x # bs) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in factorial_monoid) divides_as_fmsubset:
  assumes "wfactors G as a"
    and "wfactors G bs b"
    and "a \<in> carrier G"
    and "b \<in> carrier G"
    and "set as \<subseteq> carrier G"
    and "set bs \<subseteq> carrier G"
  shows "a divides b = (fmset G as \<subseteq># fmset G bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a divides b = (fmset G as \<subseteq># fmset G bs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wfactors G as a
wfactors G bs b
a \<in> carrier G
b \<in> carrier G
set as \<subseteq> carrier G
set bs \<subseteq> carrier G

goal (1 subgoal):
 1. a divides b = (fmset G as \<subseteq># fmset G bs)
[PROOF STEP]
by (blast intro: divides_fmsubset fmsubset_divides)


[STATEMENT]
lemma (in upper_semilattice) join_assoc:
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> y \<squnion> z = x \<squnion> (y \<squnion> z)
[PROOF STEP]
using weak_join_assoc L
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier L; ?y \<in> carrier L; ?z \<in> carrier L\<rbrakk> \<Longrightarrow> ?x \<squnion> ?y \<squnion> ?z .= ?x \<squnion> (?y \<squnion> ?z)
x \<in> carrier L
y \<in> carrier L
z \<in> carrier L

goal (1 subgoal):
 1. x \<squnion> y \<squnion> z = x \<squnion> (y \<squnion> z)
[PROOF STEP]
unfolding eq_is_equal
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier L; ?y \<in> carrier L; ?z \<in> carrier L\<rbrakk> \<Longrightarrow> ?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)
x \<in> carrier L
y \<in> carrier L
z \<in> carrier L

goal (1 subgoal):
 1. x \<squnion> y \<squnion> z = x \<squnion> (y \<squnion> z)
[PROOF STEP]
.


[STATEMENT]
theorem powerset_is_complete_lattice:
  "complete_lattice \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>"
  (is "complete_lattice ?L")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete_lattice \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>
[PROOF STEP]
proof (rule partial_order.complete_latticeI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. partial_order \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>
 2. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s Aa
 3. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
show "partial_order ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_order \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>
[PROOF STEP]
by standard auto
[PROOF STATE]
proof (state)
this:
partial_order \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>

goal (2 subgoals):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s Aa
 2. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s Aa
 2. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s Aa
 2. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
assume "B \<subseteq> carrier ?L"
[PROOF STATE]
proof (state)
this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>

goal (2 subgoals):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s Aa
 2. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>
[PROOF STEP]
have "least ?L (\<Union> B) (Upper ?L B)"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>

goal (1 subgoal):
 1. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Union> B) B
[PROOF STEP]
by (fastforce intro!: least_UpperI simp: Upper_def)
[PROOF STATE]
proof (state)
this:
is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Union> B) B

goal (2 subgoals):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s Aa
 2. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Union> B) B
[PROOF STEP]
show "\<exists>s. least ?L s (Upper ?L B)"
[PROOF STATE]
proof (prove)
using this:
is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Union> B) B

goal (1 subgoal):
 1. \<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s B
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>s. is_lub \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> s B

goal (1 subgoal):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
assume "B \<subseteq> carrier ?L"
[PROOF STATE]
proof (state)
this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>

goal (1 subgoal):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>
[PROOF STEP]
have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>

goal (1 subgoal):
 1. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Inter> B \<inter> A) B
[PROOF STEP]
txt \<open>\<^term>\<open>\<Inter> B\<close> is not the infimum of \<^term>\<open>B\<close>:
      \<^term>\<open>\<Inter> {} = UNIV\<close> which is in general bigger than \<^term>\<open>A\<close>! \<close>
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>

goal (1 subgoal):
 1. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Inter> B \<inter> A) B
[PROOF STEP]
by (fastforce intro!: greatest_LowerI simp: Lower_def)
[PROOF STATE]
proof (state)
this:
is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Inter> B \<inter> A) B

goal (1 subgoal):
 1. \<And>Aa. Aa \<subseteq> carrier \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> \<Longrightarrow> \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i Aa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Inter> B \<inter> A) B
[PROOF STEP]
show "\<exists>i. greatest ?L i (Lower ?L B)"
[PROOF STATE]
proof (prove)
using this:
is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> (\<Inter> B \<inter> A) B

goal (1 subgoal):
 1. \<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i B
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>i. is_glb \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr> i B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma image_lepoll: "f ` A \<lesssim> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A \<lesssim> A
[PROOF STEP]
by (auto simp: lepoll_iff)


[STATEMENT]
lemma STL4:
  assumes "\<turnstile> F \<longrightarrow> G"
  shows "\<turnstile> \<box>F \<longrightarrow> \<box>G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>F \<longrightarrow> \<box>G
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sigma. sigma \<Turnstile> \<box>F \<Longrightarrow> sigma \<Turnstile> \<box>G
[PROOF STEP]
apply (rule normalT [temp_use])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>sigma. sigma \<Turnstile> \<box>F \<Longrightarrow> sigma \<Turnstile> \<box>(?F2 sigma \<longrightarrow> G)
 2. \<And>sigma. sigma \<Turnstile> \<box>F \<Longrightarrow> sigma \<Turnstile> \<box>?F2 sigma
[PROOF STEP]
apply (rule assms [THEN necT, temp_use])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sigma. sigma \<Turnstile> \<box>F \<Longrightarrow> sigma \<Turnstile> \<box>F
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_of_code [code]:
  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.list_of as = map ((!!) as) [0..<IArray.length as]
[PROOF STEP]
by (cases as) (simp add: map_nth)


[STATEMENT]
lemma decrnum:
  assumes nb: "numbound0 t"
  shows "Inum (x # bs) t = Inum bs (decrnum t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inum (x # bs) t = Inum bs (decrnum t)
[PROOF STEP]
using nb
[PROOF STATE]
proof (prove)
using this:
numbound0 t

goal (1 subgoal):
 1. Inum (x # bs) t = Inum bs (decrnum t)
[PROOF STEP]
by (induct t rule: decrnum.induct) simp_all


[STATEMENT]
lemma certificate_merSK_valid:
     "[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs);
         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
 ==> \<exists>X Y Z. Says (CA i) M
                  \<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs); CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr\<rbrakk> \<Longrightarrow> \<exists>X Y Z. Says (CA i) M \<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs
[PROOF STEP]
by auto


[STATEMENT]
lemma fls_regpart_sub_prpart: "fls_regpart (f - fls_prpart_as_fls f) = fls_regpart f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fls_regpart (f - fls_prpart_as_fls f) = fls_regpart f
[PROOF STEP]
using fls_decompose_reg_pr_parts(2)[of f]
        add_diff_cancel[of "fls_regpart_as_fls f" "fls_prpart_as_fls f"]
[PROOF STATE]
proof (prove)
using this:
f = fls_regpart_as_fls f + fls_prpart_as_fls f
fls_regpart_as_fls f + fls_prpart_as_fls f - fls_prpart_as_fls f = fls_regpart_as_fls f

goal (1 subgoal):
 1. fls_regpart (f - fls_prpart_as_fls f) = fls_regpart f
[PROOF STEP]
by    simp


[STATEMENT]
lemma fls_deriv_mult_const_right:
  "fls_deriv (f * fls_const c) = fls_deriv f * fls_const c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fls_deriv (f * fls_const c) = fls_deriv f * fls_const c
[PROOF STEP]
by simp


[STATEMENT]
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> 0 < fib n
[PROOF STEP]
by (induct n rule: fib.induct) auto


[STATEMENT]
lemma present_set [simp]:
  "present (set r v h) = present h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. present (Ref.set r v h) = present h
[PROOF STEP]
by (simp add: present_def fun_eq_iff)


[STATEMENT]
lemma execute_ref [execute_simps]:
  "execute (ref v) h = Some (alloc v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (ref v) h = Some (alloc v h)
[PROOF STEP]
by (simp add: ref_def execute_simps)


[STATEMENT]
lemma ndepth_Push_Node_aux:
     "case_nat (Inr (Suc i)) f k = Inr 0 \<longrightarrow> Suc(LEAST x. f x = Inr 0) \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case k of 0 \<Rightarrow> Inr (Suc i) | Suc x \<Rightarrow> f x) = Inr 0 \<longrightarrow> Suc (LEAST x. f x = Inr 0) \<le> k
[PROOF STEP]
apply (induct_tac "k", auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>f n = Inr 0; (case n of 0 \<Rightarrow> Inr (Suc i) | Suc a \<Rightarrow> f a) \<noteq> Inr 0\<rbrakk> \<Longrightarrow> (LEAST x. f x = Inr 0) \<le> n
[PROOF STEP]
apply (erule Least_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dsum_In0I [intro]: "(M,M') \<in> r \<Longrightarrow> (In0(M), In0(M')) \<in> dsum r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, M') \<in> r \<Longrightarrow> (In0 M, In0 M') \<in> dsum r s
[PROOF STEP]
by (auto simp add: dsum_def)


[STATEMENT]
lemma cmod_le: "cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>
[PROOF STEP]
using norm_complex_def sqrt_sum_squares_le_sum_abs
[PROOF STATE]
proof (prove)
using this:
cmod ?z = sqrt ((Re ?z)\<^sup>2 + (Im ?z)\<^sup>2)
sqrt (?x\<^sup>2 + ?y\<^sup>2) \<le> \<bar>?x\<bar> + \<bar>?y\<bar>

goal (1 subgoal):
 1. cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>
[PROOF STEP]
by presburger


[STATEMENT]
lemma PRes_imp_LID_used:
     "[| Crypt (priSK M) (Hash \<lbrace>N, X\<rbrace>) \<in> parts (knows Spy evs);
         M \<notin> bad;  evs \<in> set_pur|] ==> N \<in> used evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Crypt (priSK M) (Hash \<lbrace>N, X\<rbrace>) \<in> parts (knows Spy evs); M \<notin> bad; evs \<in> set_pur\<rbrakk> \<Longrightarrow> N \<in> used evs
[PROOF STEP]
by (drule signed_imp_used, auto)


[STATEMENT]
lemma fmember_transfer [transfer_rule]:
  assumes "bi_unique A"
  shows "(A ===> rel_fset A ===> (=)) (|\<in>|) (|\<in>|)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> rel_fset A ===> (=)) (|\<in>|) (|\<in>|)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bi_unique A

goal (1 subgoal):
 1. (A ===> rel_fset A ===> (=)) (|\<in>|) (|\<in>|)
[PROOF STEP]
unfolding rel_fun_def rel_fset_alt_def bi_unique_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x y z. A x y \<longrightarrow> A x z \<longrightarrow> y = z) \<and> (\<forall>x y z. A x z \<longrightarrow> A y z \<longrightarrow> x = y)

goal (1 subgoal):
 1. \<forall>x y. A x y \<longrightarrow> (\<forall>xa ya. (\<forall>x. \<exists>y. x |\<in>| xa \<longrightarrow> y |\<in>| ya \<and> A x y) \<and> (\<forall>y. \<exists>x. y |\<in>| ya \<longrightarrow> x |\<in>| xa \<and> A x y) \<longrightarrow> (x |\<in>| xa) = (y |\<in>| ya))
[PROOF STEP]
by metis


[STATEMENT]
theorem sup_loc_Cons2:
  "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<turnstile> YT <=l X # XT = (\<exists>Y YT'. YT = Y # YT' \<and> G \<turnstile> Y <=o X \<and> G \<turnstile> YT' <=l XT)
[PROOF STEP]
by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2)


[STATEMENT]
lemma star_of_approx_numeral_iff [simp]: "star_of k \<approx> numeral w \<longleftrightarrow> k = numeral w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (star_of k \<approx> numeral w) = (k = numeral w)
[PROOF STEP]
by (subst star_of_approx_iff [symmetric]) auto


[STATEMENT]
lemma QR_lemma_03: "f = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f = m
[PROOF STEP]
have "F = QR.E q p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = QR.E q p
[PROOF STEP]
unfolding F_def pq_commute
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> {0<..(int q * int p - 1) div 2}. x mod int p \<in> {(int p - 1) div 2<..int p - 1} \<and> x mod int q \<in> {0}} = QR.E q p
[PROOF STEP]
using QRqp QR.E_def[of q p]
[PROOF STATE]
proof (prove)
using this:
QR q p
QR q p \<Longrightarrow> QR.E q p = {x \<in> {0<..(int q * int p - 1) div 2}. x mod int q \<in> {0} \<and> x mod int p \<in> {(int p - 1) div 2<..int p - 1}}

goal (1 subgoal):
 1. {x \<in> {0<..(int q * int p - 1) div 2}. x mod int p \<in> {(int p - 1) div 2<..int p - 1} \<and> x mod int q \<in> {0}} = QR.E q p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
F = QR.E q p

goal (1 subgoal):
 1. f = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F = QR.E q p
[PROOF STEP]
have "f = QR.e q p"
[PROOF STATE]
proof (prove)
using this:
F = QR.E q p

goal (1 subgoal):
 1. f = QR.e q p
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
F = QR.E q p

goal (1 subgoal):
 1. card F = QR.e q p
[PROOF STEP]
using QRqp QR.e_def[of q p]
[PROOF STATE]
proof (prove)
using this:
F = QR.E q p
QR q p
QR q p \<Longrightarrow> QR.e q p = card (QR.E q p)

goal (1 subgoal):
 1. card F = QR.e q p
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
f = QR.e q p

goal (1 subgoal):
 1. f = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = QR.e q p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f = QR.e q p

goal (1 subgoal):
 1. f = m
[PROOF STEP]
using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def
[PROOF STATE]
proof (prove)
using this:
f = QR.e q p
QR q p
QR ?p ?q \<Longrightarrow> QR.e ?p ?q = QR.n ?p ?q
m = card (GAUSS.E p (int q))
QR q p
QR ?p ?q \<Longrightarrow> QR.n ?p ?q = card (GAUSS.E ?q (int ?p))

goal (1 subgoal):
 1. f = m
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
f = m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
proof (cases "n \<le> k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
 2. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n \<le> k

goal (2 subgoals):
 1. n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
 2. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> k

goal (1 subgoal):
 1. (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(n - k) * (n choose k) = n * (n - 1 choose k)

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n \<le> k

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> n \<le> k
[PROOF STEP]
have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))"
[PROOF STATE]
proof (prove)
using this:
\<not> n \<le> k

goal (1 subgoal):
 1. n * (n - 1 choose k) = Suc (n - 1 - k) * (n choose Suc (n - 1 - k))
[PROOF STEP]
using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n]
[PROOF STATE]
proof (prove)
using this:
\<not> n \<le> k
k \<le> n - 1 \<Longrightarrow> n - 1 choose k = n - 1 choose (n - 1 - k)
Suc (n - 1 - k) * (n choose Suc (n - 1 - k)) = n * (n - 1 choose (n - 1 - k))

goal (1 subgoal):
 1. n * (n - 1 choose k) = Suc (n - 1 - k) * (n choose Suc (n - 1 - k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n * (n - 1 choose k) = Suc (n - 1 - k) * (n choose Suc (n - 1 - k))

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n * (n - 1 choose k) = Suc (n - 1 - k) * (n choose Suc (n - 1 - k))

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
have "Suc ((n - 1) - k) = n - k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (n - 1 - k) = n - k
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> n \<le> k

goal (1 subgoal):
 1. Suc (n - 1 - k) = n - k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (n - 1 - k) = n - k

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (n - 1 - k) = n - k

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
have "n choose \<dots> = n choose k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose (n - k) = n choose k
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> n \<le> k

goal (1 subgoal):
 1. n choose (n - k) = n choose k
[PROOF STEP]
by (intro binomial_symmetric [symmetric]) simp_all
[PROOF STATE]
proof (state)
this:
n choose (n - k) = n choose k

goal (1 subgoal):
 1. \<not> n \<le> k \<Longrightarrow> (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n * (n - 1 choose k) = (n - k) * (n choose k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n * (n - 1 choose k) = (n - k) * (n choose k)

goal (1 subgoal):
 1. (n - k) * (n choose k) = n * (n - 1 choose k)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(n - k) * (n choose k) = n * (n - 1 choose k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> \<infinity> \<Longrightarrow> x + y - x = y
[PROOF STEP]
by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)


[STATEMENT]
lemma in_graphD: "(k, v) \<in> graph m \<Longrightarrow> m k = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k, v) \<in> graph m \<Longrightarrow> m k = Some v
[PROOF STEP]
unfolding graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k, v) \<in> {(a, b) |a b. m a = Some b} \<Longrightarrow> m k = Some v
[PROOF STEP]
by blast


[STATEMENT]
lemma Opair_in_games_lfp:
  assumes l: "explode l \<subseteq> games_lfp"
  and r: "explode r \<subseteq> games_lfp"
  shows "Opair l r \<in> games_lfp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Opair l r \<in> games_lfp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Opair l r \<in> games_lfp
[PROOF STEP]
note f = unique_games[of games_lfp, simplified]
[PROOF STATE]
proof (state)
this:
games_lfp = fixgames games_lfp

goal (1 subgoal):
 1. Opair l r \<in> games_lfp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Opair l r \<in> games_lfp
[PROOF STEP]
apply (subst f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Opair l r \<in> fixgames games_lfp
[PROOF STEP]
apply (simp add: fixgames_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>la ra. Opair l r = Opair la ra \<and> explode la \<subseteq> games_lfp \<and> explode ra \<subseteq> games_lfp
[PROOF STEP]
apply (rule exI[where x=l])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ra. Opair l r = Opair l ra \<and> explode l \<subseteq> games_lfp \<and> explode ra \<subseteq> games_lfp
[PROOF STEP]
apply (rule exI[where x=r])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Opair l r = Opair l r \<and> explode l \<subseteq> games_lfp \<and> explode r \<subseteq> games_lfp
[PROOF STEP]
apply (auto simp add: l r)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Opair l r \<in> games_lfp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sums_finite:
  assumes [simp]: "finite N"
    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
  shows "f sums (\<Sum>n\<in>N. f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f sums sum f N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f sums sum f N
[PROOF STEP]
have eq: "sum f {..<n + Suc (Max N)} = sum f N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<n + Suc (Max N)} = sum f N
[PROOF STEP]
by (rule sum.mono_neutral_right) (auto simp: add_increasing less_Suc_eq_le f)
[PROOF STATE]
proof (state)
this:
sum f {..<?n + Suc (Max N)} = sum f N

goal (1 subgoal):
 1. f sums sum f N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f sums sum f N
[PROOF STEP]
unfolding sums_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> sum f N
[PROOF STEP]
by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
      (simp add: eq atLeast0LessThan del: add_Suc_right)
[PROOF STATE]
proof (state)
this:
f sums sum f N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sums_If_finite_set':
  fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_ab_group_add}"
  assumes "g sums S" and "finite A" and "S' = S + (\<Sum>n\<in>A. f n - g n)"
  shows   "(\<lambda>n. if n \<in> A then f n else g n) sums S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
have "(\<lambda>n. g n + (if n \<in> A then f n - g n else 0)) sums (S + (\<Sum>n\<in>A. f n - g n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. g n + (if n \<in> A then f n - g n else (0::'a))) sums (S + (\<Sum>n\<in>A. f n - g n))
[PROOF STEP]
by (intro sums_add assms sums_If_finite_set)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. g n + (if n \<in> A then f n - g n else (0::'a))) sums (S + (\<Sum>n\<in>A. f n - g n))

goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. g n + (if n \<in> A then f n - g n else (0::'a))) sums (S + (\<Sum>n\<in>A. f n - g n))

goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
have "(\<lambda>n. g n + (if n \<in> A then f n - g n else 0)) = (\<lambda>n. if n \<in> A then f n else g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. g n + (if n \<in> A then f n - g n else (0::'a))) = (\<lambda>n. if n \<in> A then f n else g n)
[PROOF STEP]
by (simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. g n + (if n \<in> A then f n - g n else (0::'a))) = (\<lambda>n. if n \<in> A then f n else g n)

goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. if n \<in> A then f n else g n) sums (S + (\<Sum>n\<in>A. f n - g n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. if n \<in> A then f n else g n) sums (S + (\<Sum>n\<in>A. f n - g n))

goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. if n \<in> A then f n else g n) sums (S + (\<Sum>n\<in>A. f n - g n))
g sums S
finite A
S' = S + (\<Sum>n\<in>A. f n - g n)

goal (1 subgoal):
 1. (\<lambda>n. if n \<in> A then f n else g n) sums S'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. if n \<in> A then f n else g n) sums S'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_exists:
  obtains B where "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> V; independent B; V \<subseteq> span B; card B = dim V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson basis_card_eq_dim empty_subsetI independent_empty maximal_independent_subset_extend)


[STATEMENT]
lemma solvable_seq_condition:
  assumes "group_hom G H f" "group_hom H K g" and "f ` I \<subseteq> J" and "kernel H K g \<subseteq> f ` I"
    and "subgroup J H" and "solvable_seq G I" "solvable_seq K (g ` J)"
  shows "solvable_seq H J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
interpret G: group G + H: group H + K: group K + J: subgroup J H + I: subgroup I G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Group.group G &&& Group.group H) &&& Group.group K &&& subgroup J H &&& subgroup I G
[PROOF STEP]
using assms(1-2,5) group.solvable_imp_subgroup[OF _ assms(6)]
[PROOF STATE]
proof (prove)
using this:
group_hom G H f
group_hom H K g
subgroup J H
Group.group G \<Longrightarrow> subgroup I G

goal (1 subgoal):
 1. (Group.group G &&& Group.group H) &&& Group.group K &&& subgroup J H &&& subgroup I G
[PROOF STEP]
unfolding group_hom_def
[PROOF STATE]
proof (prove)
using this:
Group.group G \<and> Group.group H \<and> group_hom_axioms G H f
Group.group H \<and> Group.group K \<and> group_hom_axioms H K g
subgroup J H
Group.group G \<Longrightarrow> subgroup I G

goal (1 subgoal):
 1. (Group.group G &&& Group.group H) &&& Group.group K &&& subgroup J H &&& subgroup I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
obtain n m
    where n: "(derived G ^^ n) I = { \<one>\<^bsub>G\<^esub> }" and m: "(derived K ^^ m) (g ` J) = { \<one>\<^bsub>K\<^esub> }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n m. \<lbrakk>(derived G ^^ n) I = {\<one>\<^bsub>G\<^esub>}; (derived K ^^ m) (g ` J) = {\<one>\<^bsub>K\<^esub>}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G.solvable_imp_trivial_derived_seq[OF assms(6)]
          K.solvable_imp_trivial_derived_seq[OF assms(7)]
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (derived G ^^ n) I = {\<one>\<^bsub>G\<^esub>}
\<exists>n. (derived K ^^ n) (g ` J) = {\<one>\<^bsub>K\<^esub>}

goal (1 subgoal):
 1. (\<And>n m. \<lbrakk>(derived G ^^ n) I = {\<one>\<^bsub>G\<^esub>}; (derived K ^^ m) (g ` J) = {\<one>\<^bsub>K\<^esub>}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(derived G ^^ n) I = {\<one>\<^bsub>G\<^esub>}
(derived K ^^ m) (g ` J) = {\<one>\<^bsub>K\<^esub>}

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
have "(derived H ^^ m) J \<subseteq> f ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (derived H ^^ m) J \<subseteq> f ` I
[PROOF STEP]
using m H.exp_of_derived_in_carrier[OF J.subset, of m] assms(4)
[PROOF STATE]
proof (prove)
using this:
(derived K ^^ m) (g ` J) = {\<one>\<^bsub>K\<^esub>}
(derived H ^^ m) J \<subseteq> carrier H
kernel H K g \<subseteq> f ` I

goal (1 subgoal):
 1. (derived H ^^ m) J \<subseteq> f ` I
[PROOF STEP]
by (auto simp add: group_hom.exp_of_derived_img[OF assms(2) J.subset] kernel_def)
[PROOF STATE]
proof (state)
this:
(derived H ^^ m) J \<subseteq> f ` I

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
hence "(derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` ((derived G ^^ n) I)"
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ m) J \<subseteq> f ` I

goal (1 subgoal):
 1. (derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` (derived G ^^ n) I
[PROOF STEP]
using n H.mono_exp_of_derived
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ m) J \<subseteq> f ` I
(derived G ^^ n) I = {\<one>\<^bsub>G\<^esub>}
?K \<subseteq> ?H \<Longrightarrow> (derived H ^^ ?n) ?K \<subseteq> (derived H ^^ ?n) ?H

goal (1 subgoal):
 1. (derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` (derived G ^^ n) I
[PROOF STEP]
unfolding sym[OF group_hom.exp_of_derived_img[OF assms(1) I.subset, of n]]
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ m) J \<subseteq> f ` I
(derived G ^^ n) I = {\<one>\<^bsub>G\<^esub>}
?K \<subseteq> ?H \<Longrightarrow> (derived H ^^ ?n) ?K \<subseteq> (derived H ^^ ?n) ?H

goal (1 subgoal):
 1. (derived H ^^ n) ((derived H ^^ m) J) \<subseteq> (derived H ^^ n) (f ` I)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` (derived G ^^ n) I

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
hence "(derived H ^^ (n + m)) J \<subseteq> { \<one>\<^bsub>H\<^esub> }"
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` (derived G ^^ n) I

goal (1 subgoal):
 1. (derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}
[PROOF STEP]
using group_hom.hom_one[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` (derived G ^^ n) I
f \<one>\<^bsub>G\<^esub> = \<one>\<^bsub>H\<^esub>

goal (1 subgoal):
 1. (derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}
[PROOF STEP]
unfolding n
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ n) ((derived H ^^ m) J) \<subseteq> f ` {\<one>\<^bsub>G\<^esub>}
f \<one>\<^bsub>G\<^esub> = \<one>\<^bsub>H\<^esub>

goal (1 subgoal):
 1. (derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}
[PROOF STEP]
by (simp add: funpow_add)
[PROOF STATE]
proof (state)
this:
(derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
have "{ \<one>\<^bsub>H\<^esub> } \<subseteq> (derived H ^^ (n + m)) J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<one>\<^bsub>H\<^esub>} \<subseteq> (derived H ^^ (n + m)) J
[PROOF STEP]
using subgroup.one_closed[OF H.exp_of_derived_is_subgroup[OF assms(5), of "n + m"]]
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>H\<^esub> \<in> (derived H ^^ (n + m)) J

goal (1 subgoal):
 1. {\<one>\<^bsub>H\<^esub>} \<subseteq> (derived H ^^ (n + m)) J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{\<one>\<^bsub>H\<^esub>} \<subseteq> (derived H ^^ (n + m)) J

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}
{\<one>\<^bsub>H\<^esub>} \<subseteq> (derived H ^^ (n + m)) J
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}
{\<one>\<^bsub>H\<^esub>} \<subseteq> (derived H ^^ (n + m)) J

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
using H.trivial_derived_seq_imp_solvable[OF assms(5)]
[PROOF STATE]
proof (prove)
using this:
(derived H ^^ (n + m)) J \<subseteq> {\<one>\<^bsub>H\<^esub>}
{\<one>\<^bsub>H\<^esub>} \<subseteq> (derived H ^^ (n + m)) J
(derived H ^^ ?n) J = {\<one>\<^bsub>H\<^esub>} \<Longrightarrow> solvable_seq H J

goal (1 subgoal):
 1. solvable_seq H J
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
solvable_seq H J

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<not> (\<exists>y. \<forall>x. p x y = (\<not> (\<exists>z. p x z \<and> p z x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>y. \<forall>x. p x y = (\<nexists>z. p x z \<and> p z x)
[PROOF STEP]
by blast


[STATEMENT]
lemma one_subgroup_generated [simp]: "\<one>\<^bsub>subgroup_generated G S\<^esub> = \<one>\<^bsub>G\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>subgroup_generated G S\<^esub> = \<one>\<^bsub>G\<^esub>
[PROOF STEP]
by (auto simp: subgroup_generated_def)


[STATEMENT]
lemma singleton_undefinedI:
  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton default A = default ()" for default
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>!x. eval A x \<Longrightarrow> singleton default A = default ()
[PROOF STEP]
by (simp add: singleton_def)


[STATEMENT]
lemma project_extend_transient_D:
     "project h C (extend h F) \<in> transient (project_set h C \<inter> D)
      ==> F \<in> transient (project_set h C \<inter> D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. project h C (extend h F) \<in> transient (project_set h C \<inter> D) \<Longrightarrow> F \<in> transient (project_set h C \<inter> D)
[PROOF STEP]
apply (simp add: transient_def Domain_project_act, safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. project_set h C \<inter> D \<subseteq> - project_set h C \<union> - D \<Longrightarrow> \<exists>act\<in>Acts F. act `` (project_set h C \<inter> D) \<subseteq> - project_set h C \<union> - D
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_bit_eq_xor [simp, code]:
  \<open>(+) = (Bit_Operations.xor :: bit \<Rightarrow> _)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (+) = xor
[PROOF STEP]
by (auto simp add: fun_eq_iff)


[STATEMENT]
lemma quotient_map_compose_eq:
   "quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) = quotient_map X' X'' g
[PROOF STEP]
by (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_compose quotient_map_from_composition)


[STATEMENT]
lemma open_greaterThan [continuous_intros, simp]: "open {a <..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open {a<..}
[PROOF STEP]
unfolding open_generated_order
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. generate_topology (range lessThan \<union> range greaterThan) {a<..}
[PROOF STEP]
by (auto intro: generate_topology.Basis)


[STATEMENT]
lemma (in topological_space) at_within_eq:
  "at x within s = (INF S\<in>{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at x within s = (INF S\<in>{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))
[PROOF STEP]
unfolding nhds_def at_within_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf (Inf (principal ` {S. open S \<and> x \<in> S})) (principal (s - {x})) = (INF S\<in>{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))
[PROOF STEP]
by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)


[STATEMENT]
lemma sequentially_imp_eventually_at_left:
  fixes a :: "'a::{linorder_topology,first_countable_topology}"
  assumes b[simp]: "b < a"
    and *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f \<longlonglongrightarrow> a \<Longrightarrow>
      eventually (\<lambda>n. P (f n)) sequentially"
  shows "eventually P (at_left a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (at_left a)
[PROOF STEP]
proof (safe intro!: sequentially_imp_eventually_within)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. f n \<in> {..<a} \<and> f n \<noteq> a; f \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. P (f n)
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. f n \<in> {..<a} \<and> f n \<noteq> a; f \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. P (f n)
[PROOF STEP]
assume X: "\<forall>n. X n \<in> {..< a} \<and> X n \<noteq> a" "X \<longlonglongrightarrow> a"
[PROOF STATE]
proof (state)
this:
\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a
X \<longlonglongrightarrow> a

goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. f n \<in> {..<a} \<and> f n \<noteq> a; f \<longlonglongrightarrow> a\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. P (f n)
[PROOF STEP]
show "eventually (\<lambda>n. P (X n)) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. P (X n)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. P (X n)) \<Longrightarrow> False
[PROOF STEP]
assume neg: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>\<^sub>F n in sequentially. P (X n))

goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. P (X n)) \<Longrightarrow> False
[PROOF STEP]
have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> (X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n))"
      (is "\<exists>s. ?P s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)
[PROOF STEP]
proof (rule dependent_nat_choice)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. \<not> P (X x) \<and> b < X x
 2. \<And>x n. \<not> P (X x) \<and> b < X x \<Longrightarrow> \<exists>y. (\<not> P (X y) \<and> b < X y) \<and> X x \<le> X y \<and> Suc x \<le> y
[PROOF STEP]
have "\<not> eventually (\<lambda>n. b < X n \<longrightarrow> P (X n)) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. b < X n \<longrightarrow> P (X n))
[PROOF STEP]
by (intro not_eventually_impI neg order_tendstoD(1) [OF X(2) b])
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>\<^sub>F n in sequentially. b < X n \<longrightarrow> P (X n))

goal (2 subgoals):
 1. \<exists>x. \<not> P (X x) \<and> b < X x
 2. \<And>x n. \<not> P (X x) \<and> b < X x \<Longrightarrow> \<exists>y. (\<not> P (X y) \<and> b < X y) \<and> X x \<le> X y \<and> Suc x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>\<^sub>F n in sequentially. b < X n \<longrightarrow> P (X n))
[PROOF STEP]
show "\<exists>x. \<not> P (X x) \<and> b < X x"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>\<^sub>F n in sequentially. b < X n \<longrightarrow> P (X n))

goal (1 subgoal):
 1. \<exists>x. \<not> P (X x) \<and> b < X x
[PROOF STEP]
by (auto dest!: not_eventuallyD)
[PROOF STATE]
proof (state)
this:
\<exists>x. \<not> P (X x) \<and> b < X x

goal (1 subgoal):
 1. \<And>x n. \<not> P (X x) \<and> b < X x \<Longrightarrow> \<exists>y. (\<not> P (X y) \<and> b < X y) \<and> X x \<le> X y \<and> Suc x \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x n. \<not> P (X x) \<and> b < X x \<Longrightarrow> \<exists>y. (\<not> P (X y) \<and> b < X y) \<and> X x \<le> X y \<and> Suc x \<le> y
[PROOF STEP]
fix x n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x n. \<not> P (X x) \<and> b < X x \<Longrightarrow> \<exists>y. (\<not> P (X y) \<and> b < X y) \<and> X x \<le> X y \<and> Suc x \<le> y
[PROOF STEP]
have "\<not> eventually (\<lambda>n. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n)) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n))
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a
X \<longlonglongrightarrow> a

goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n))
[PROOF STEP]
by (intro not_eventually_impI order_tendstoD(1)[OF X(2)] eventually_ge_at_top neg) auto
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>\<^sub>F n in sequentially. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n))

goal (1 subgoal):
 1. \<And>x n. \<not> P (X x) \<and> b < X x \<Longrightarrow> \<exists>y. (\<not> P (X y) \<and> b < X y) \<and> X x \<le> X y \<and> Suc x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>\<^sub>F n in sequentially. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n))
[PROOF STEP]
show "\<exists>n. (\<not> P (X n) \<and> b < X n) \<and> (X x \<le> X n \<and> Suc x \<le> n)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>\<^sub>F n in sequentially. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n))

goal (1 subgoal):
 1. \<exists>n. (\<not> P (X n) \<and> b < X n) \<and> X x \<le> X n \<and> Suc x \<le> n
[PROOF STEP]
by (auto dest!: not_eventuallyD)
[PROOF STATE]
proof (state)
this:
\<exists>n. (\<not> P (X n) \<and> b < X n) \<and> X x \<le> X n \<and> Suc x \<le> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)

goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. P (X n)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)
[PROOF STEP]
obtain s where "?P s"
[PROOF STATE]
proof (prove)
using this:
\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)

goal (1 subgoal):
 1. (\<And>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)

goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. P (X n)) \<Longrightarrow> False
[PROOF STEP]
with X
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a
X \<longlonglongrightarrow> a
\<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)
[PROOF STEP]
have "b < X (s n)"
      and "X (s n) < a"
      and "incseq (\<lambda>n. X (s n))"
      and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
      and "\<not> P (X (s n))"
      for n
[PROOF STATE]
proof (prove)
using this:
\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a
X \<longlonglongrightarrow> a
\<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n)

goal (1 subgoal):
 1. (b < X (s n) &&& X (s n) < a) &&& incseq (\<lambda>n. X (s n)) &&& (\<lambda>n. X (s n)) \<longlonglongrightarrow> a &&& \<not> P (X (s n))
[PROOF STEP]
by (auto simp: strict_mono_Suc_iff Suc_le_eq incseq_Suc_iff
          intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
[PROOF STATE]
proof (state)
this:
b < X (s ?n)
X (s ?n) < a
incseq (\<lambda>n. X (s n))
(\<lambda>n. X (s n)) \<longlonglongrightarrow> a
\<not> P (X (s ?n))

goal (1 subgoal):
 1. \<not> (\<forall>\<^sub>F n in sequentially. P (X n)) \<Longrightarrow> False
[PROOF STEP]
from *[OF this(1,2,3,4)] this(5)
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. P (X (s n))
\<not> P (X (s ?n))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. P (X (s n))
\<not> P (X (s ?n))

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:
\<forall>\<^sub>F n in sequentially. P (X n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_summable_on_Times_swap:
  "f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f abs_summable_on A \<times> B) = ((\<lambda>(x, y). f (y, x)) abs_summable_on B \<times> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f abs_summable_on A \<times> B) = ((\<lambda>(x, y). f (y, x)) abs_summable_on B \<times> A)
[PROOF STEP]
have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)
[PROOF STEP]
by (auto simp: bij_betw_def inj_on_def)
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)

goal (1 subgoal):
 1. (f abs_summable_on A \<times> B) = ((\<lambda>(x, y). f (y, x)) abs_summable_on B \<times> A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f abs_summable_on A \<times> B) = ((\<lambda>(x, y). f (y, x)) abs_summable_on B \<times> A)
[PROOF STEP]
by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
       (simp_all add: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
(f abs_summable_on A \<times> B) = ((\<lambda>(x, y). f (y, x)) abs_summable_on B \<times> A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_summable_on_Sigma_project1':
  assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
  shows   "(\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) abs_summable_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. infsetsum (f x) (B x)) abs_summable_on A
[PROOF STEP]
by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
        norm_infsetsum_bound)


[STATEMENT]
lemma inv_split_min: "\<lbrakk> split_min t = (x,t'); t \<noteq> Leaf; invh t; invc t \<rbrakk> \<Longrightarrow>
   invh t' \<and>
   (color t = Red \<longrightarrow> bheight t' = bheight t \<and> invc t') \<and>
   (color t = Black \<longrightarrow> bheight t' = bheight t - 1 \<and> invc2 t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>split_min t = (x, t'); t \<noteq> \<langle>\<rangle>; invh t; invc t\<rbrakk> \<Longrightarrow> invh t' \<and> (color t = Red \<longrightarrow> bheight t' = bheight t \<and> invc t') \<and> (color t = Black \<longrightarrow> bheight t' = bheight t - 1 \<and> invc2 t')
[PROOF STEP]
apply(induction t arbitrary: x t' rule: split_min.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l a uu_ r x t'. \<lbrakk>\<And>x t'. \<lbrakk>l \<noteq> \<langle>\<rangle>; split_min l = (x, t'); l \<noteq> \<langle>\<rangle>; invh l; invc l\<rbrakk> \<Longrightarrow> invh t' \<and> (color l = Red \<longrightarrow> bheight t' = bheight l \<and> invc t') \<and> (color l = Black \<longrightarrow> bheight t' = bheight l - 1 \<and> invc2 t'); split_min \<langle>l, (a, uu_), r\<rangle> = (x, t'); \<langle>l, (a, uu_), r\<rangle> \<noteq> \<langle>\<rangle>; invh \<langle>l, (a, uu_), r\<rangle>; invc \<langle>l, (a, uu_), r\<rangle>\<rbrakk> \<Longrightarrow> invh t' \<and> (color \<langle>l, (a, uu_), r\<rangle> = Red \<longrightarrow> bheight t' = bheight \<langle>l, (a, uu_), r\<rangle> \<and> invc t') \<and> (color \<langle>l, (a, uu_), r\<rangle> = Black \<longrightarrow> bheight t' = bheight \<langle>l, (a, uu_), r\<rangle> - 1 \<and> invc2 t')
 2. \<And>x t'. \<lbrakk>split_min \<langle>\<rangle> = (x, t'); \<langle>\<rangle> \<noteq> \<langle>\<rangle>; invh \<langle>\<rangle>; invc \<langle>\<rangle>\<rbrakk> \<Longrightarrow> invh t' \<and> (color \<langle>\<rangle> = Red \<longrightarrow> bheight t' = bheight \<langle>\<rangle> \<and> invc t') \<and> (color \<langle>\<rangle> = Black \<longrightarrow> bheight t' = bheight \<langle>\<rangle> - 1 \<and> invc2 t')
[PROOF STEP]
apply(auto simp: inv_baldR inv_baldL invc2I dest!: neq_LeafD
           split: if_splits prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done