[STATEMENT]
lemma residue_lmul:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. c * (f z)) z= c * residue f z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
proof (cases "c=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
 2. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
 2. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
using residue_const
[PROOF STATE]
proof (prove)
using this:
c = 0
residue (\<lambda>_. ?c) ?z = 0

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
residue (\<lambda>z. c * f z) z = c * residue f z

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
define c' where "c' \<equiv> 2 * pi * \<i>"
[PROOF STATE]
proof (state)
this:
c' \<equiv> complex_of_real (2 * pi) * \<i>

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
define f' where "f' \<equiv> (\<lambda>z. c * (f z))"
[PROOF STATE]
proof (state)
this:
f' \<equiv> \<lambda>z. c * f z

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
obtain e where "e>0" and e_cball:"cball z e \<subseteq> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; cball z e \<subseteq> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>open s\<close> \<open>z\<in>s\<close>
[PROOF STATE]
proof (prove)
using this:
open s
z \<in> s

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; cball z e \<subseteq> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using open_contains_cball_eq
[PROOF STATE]
proof (prove)
using this:
open s
z \<in> s
open ?S \<Longrightarrow> \<forall>x. (x \<in> ?S) = (\<exists>e>0. cball x e \<subseteq> ?S)

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; cball z e \<subseteq> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < e
cball z e \<subseteq> s

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f' has_contour_integral c' * residue f' z) (circlepath z e)
[PROOF STEP]
unfolding f'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c' * residue (\<lambda>z. c * f z) z) (circlepath z e)
[PROOF STEP]
using f_holo
[PROOF STATE]
proof (prove)
using this:
f holomorphic_on s - {z}

goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c' * residue (\<lambda>z. c * f z) z) (circlepath z e)
[PROOF STEP]
apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f holomorphic_on s - {z} \<Longrightarrow> (\<lambda>z. c * f z) holomorphic_on s - {z}
[PROOF STEP]
by (auto intro:holomorphic_intros)
[PROOF STATE]
proof (state)
this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
have "(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f' has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
unfolding f'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
using f_holo
[PROOF STATE]
proof (prove)
using this:
f holomorphic_on s - {z}

goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
by (auto intro: has_contour_integral_lmul
      base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
[PROOF STATE]
proof (state)
this:
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
have "c' * residue f' z  = c * (c' * residue f z)"
[PROOF STATE]
proof (prove)
using this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)

goal (1 subgoal):
 1. c' * residue f' z = c * (c' * residue f z)
[PROOF STEP]
using has_contour_integral_unique
[PROOF STATE]
proof (prove)
using this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)
\<lbrakk>(?f has_contour_integral ?i) ?g; (?f has_contour_integral ?j) ?g\<rbrakk> \<Longrightarrow> ?i = ?j

goal (1 subgoal):
 1. c' * residue f' z = c * (c' * residue f z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c' * residue f' z = c * (c' * residue f z)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c' * residue f' z = c * (c' * residue f z)

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
unfolding f'_def c'_def
[PROOF STATE]
proof (prove)
using this:
complex_of_real (2 * pi) * \<i> * residue (\<lambda>z. c * f z) z = c * (complex_of_real (2 * pi) * \<i> * residue f z)

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
complex_of_real (2 * pi) * \<i> * residue (\<lambda>z. c * f z) z = c * (complex_of_real (2 * pi) * \<i> * residue f z)
c \<noteq> 0

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
residue (\<lambda>z. c * f z) z = c * residue f z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gamma_residue:
  "residue Gamma (-of_nat n) = (-1) ^ n / fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue Gamma (- of_nat n) = (- 1) ^ n / fact n
[PROOF STEP]
proof (rule residue_simple')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. open ?s
 2. - of_nat n \<in> ?s
 3. Gamma holomorphic_on ?s - {- of_nat n}
 4. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- 1) ^ n / fact n
[PROOF STEP]
show "open (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) :: complex set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (- (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}))
[PROOF STEP]
by (intro open_Compl closed_subset_Ints) auto
[PROOF STATE]
proof (state)
this:
open (- (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}))

goal (3 subgoals):
 1. - of_nat n \<in> - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n})
 2. Gamma holomorphic_on - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}) - {- of_nat n}
 3. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- 1) ^ n / fact n
[PROOF STEP]
show "Gamma holomorphic_on (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) - {- of_nat n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gamma holomorphic_on - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}) - {- of_nat n}
[PROOF STEP]
by (rule holomorphic_Gamma) auto
[PROOF STATE]
proof (state)
this:
Gamma holomorphic_on - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}) - {- of_nat n}

goal (2 subgoals):
 1. - of_nat n \<in> - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n})
 2. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- 1) ^ n / fact n
[PROOF STEP]
show "(\<lambda>w. Gamma w * (w - (-of_nat n))) \<midarrow>(-of_nat n)\<rightarrow> (- 1) ^ n / fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::'a)) ^ n / fact n
[PROOF STEP]
using Gamma_residues[of n]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>z. Gamma z * (z + of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::?'a)) ^ n / fact n

goal (1 subgoal):
 1. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::'a)) ^ n / fact n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::?'a1)) ^ n / fact n

goal (1 subgoal):
 1. - of_nat n \<in> - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n})
[PROOF STEP]
qed auto


[STATEMENT]
lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>open {x. P x}; closed {x. Q x}\<rbrakk> \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}
[PROOF STEP]
unfolding imp_conv_disj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>open {x. P x}; closed {x. Q x}\<rbrakk> \<Longrightarrow> closed {x. \<not> P x \<or> Q x}
[PROOF STEP]
by (intro closed_Collect_disj closed_Collect_neg)


[STATEMENT]
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n \<Longrightarrow> monoseq X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. X (Suc n) \<le> X n \<Longrightarrow> monoseq X
[PROOF STEP]
by (simp add: monoseq_Suc)


[STATEMENT]
lemma ennreal_mult_le_mult_iff: "c \<noteq> 0 \<Longrightarrow> c \<noteq> top \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> (b :: ennreal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<noteq> 0; c \<noteq> top\<rbrakk> \<Longrightarrow> (c * a \<le> c * b) = (a \<le> b)
[PROOF STEP]
including ennreal.lifting
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<noteq> 0; c \<noteq> top\<rbrakk> \<Longrightarrow> (c * a \<le> c * b) = (a \<le> b)
[PROOF STEP]
by (transfer, subst ereal_mult_le_mult_iff) (auto simp: top_ereal_def)


[STATEMENT]
lemma transfer_sup_continuous[transfer_rule]:
  "(rel_fun (rel_fun (=) pcr_ennreal) (=)) sup_continuous sup_continuous"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_fun (=) pcr_ennreal) (=) sup_continuous sup_continuous
[PROOF STEP]
proof (safe intro!: rel_funI dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. sup_continuous (enn2ereal \<circ> y) \<Longrightarrow> sup_continuous y
 2. \<And>x y. sup_continuous y \<Longrightarrow> sup_continuous (enn2ereal \<circ> y)
[PROOF STEP]
show "sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f" for f :: "'a \<Rightarrow> _"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f
[PROOF STEP]
using sup_continuous_e2ennreal[of "enn2ereal \<circ> f"]
[PROOF STATE]
proof (prove)
using this:
sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous (\<lambda>x. e2ennreal ((enn2ereal \<circ> f) x))

goal (1 subgoal):
 1. sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_continuous (enn2ereal \<circ> ?f) \<Longrightarrow> sup_continuous ?f

goal (1 subgoal):
 1. \<And>x y. sup_continuous y \<Longrightarrow> sup_continuous (enn2ereal \<circ> y)
[PROOF STEP]
show "sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)" for f :: "'a \<Rightarrow> _"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)
[PROOF STEP]
using sup_continuous_enn2ereal[of f]
[PROOF STATE]
proof (prove)
using this:
sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. enn2ereal (f x))

goal (1 subgoal):
 1. sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
sup_continuous ?f \<Longrightarrow> sup_continuous (enn2ereal \<circ> ?f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_rat_less: "(of_rat r :: 'a::linordered_field) < of_rat s \<longleftrightarrow> r < s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_rat r < of_rat s) = (r < s)
[PROOF STEP]
proof (induct r, induct s)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
fix a b c d :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
assume not_zero: "b > 0" "d > 0"
[PROOF STATE]
proof (state)
this:
0 < b
0 < d

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < b
0 < d
[PROOF STEP]
have "b * d > 0"
[PROOF STATE]
proof (prove)
using this:
0 < b
0 < d

goal (1 subgoal):
 1. 0 < b * d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < b * d

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
have of_int_divide_less_eq:
    "(of_int a :: 'a) / of_int b < of_int c / of_int d \<longleftrightarrow>
      (of_int a :: 'a) * of_int d < of_int c * of_int b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int a / of_int b < of_int c / of_int d) = (of_int a * of_int d < of_int c * of_int b)
[PROOF STEP]
using not_zero
[PROOF STATE]
proof (prove)
using this:
0 < b
0 < d

goal (1 subgoal):
 1. (of_int a / of_int b < of_int c / of_int d) = (of_int a * of_int d < of_int c * of_int b)
[PROOF STEP]
by (simp add: pos_less_divide_eq pos_divide_less_eq)
[PROOF STATE]
proof (state)
this:
(of_int a / of_int b < of_int c / of_int d) = (of_int a * of_int d < of_int c * of_int b)

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) \<longleftrightarrow>
      Fract a b < Fract c d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_rat (Fract a b) < of_rat (Fract c d)) = (Fract a b < Fract c d)
[PROOF STEP]
using not_zero \<open>b * d > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < b
0 < d
0 < b * d

goal (1 subgoal):
 1. (of_rat (Fract a b) < of_rat (Fract c d)) = (Fract a b < Fract c d)
[PROOF STEP]
by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
[PROOF STATE]
proof (state)
this:
(of_rat (Fract a b) < of_rat (Fract c d)) = (Fract a b < Fract c d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_cdecl_fdecl:
"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_cdecl G (C, c); f \<in> set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f
[PROOF STEP]
apply (unfold wf_cdecl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case (C, c) of (C, c) \<Rightarrow> \<not> is_iface G C \<and> (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> (\<forall>s. \<forall>im\<in>DeclConcepts.imethds G I s. ? cm:methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not> is_static cm \<and> accmodi im \<le> accmodi cm)) \<and> Ball (set (cfields c)) (wf_fdecl G (pid C)) \<and> unique (cfields c) \<and> Ball (set (methods c)) (wf_mdecl G C) \<and> unique (methods c) \<and> jumpNestingOkS {} (init c) \<and> Ex (da \<lparr>prg = G, cls = C, lcl = Map.empty\<rparr> {} \<langle>init c\<rangle>) \<and> \<lparr>prg = G, cls = C, lcl = Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> (C \<noteq> Object \<longrightarrow> is_acc_class G (pid C) (super c) \<and> (table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) entails \<lambda>new. \<forall>old sig. (G \<turnstile> qmdecl sig new overrides\<^sub>S qmdecl sig old \<longrightarrow> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old) \<and> (G,sig\<turnstile> new hides old \<longrightarrow> accmodi old \<le> accmodi new \<and> is_static old))); f \<in> set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma of_int_sint [simp]:
  \<open>of_int (sint a) = signed a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sint a) = signed a
[PROOF STEP]
by transfer (simp_all add: take_bit_signed_take_bit)


[STATEMENT]
lemma [code_abbrev, simp]:
  \<open>Word.the_int = uint\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Word.the_int = uint
[PROOF STEP]
by transfer rule


[STATEMENT]
lemma signed_xor_eq:
  \<open>signed (v XOR w) = signed v XOR signed w\<close>
  for v w :: \<open>'b::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed (v XOR w) = signed v XOR signed w
[PROOF STEP]
by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff)


[STATEMENT]
lemma bit_signed_drop_bit_iff [bit_simps]:
  \<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (signed_drop_bit m w) n = bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w n. (n < LENGTH('a) \<and> bit ((drop_bit m \<circ> signed_take_bit (LENGTH('a) - Suc 0)) w) n) = ((if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n) < LENGTH('a) \<and> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n))
[PROOF STEP]
apply (auto simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m w n. \<lbrakk>LENGTH('a) - Suc 0 \<le> m + n; n < LENGTH('a) - m; n < LENGTH('a); bit w (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> bit w (m + n)
 2. \<And>m w n. \<lbrakk>LENGTH('a) - Suc 0 \<le> m + n; n < LENGTH('a) - m; m + n < LENGTH('a); bit w (m + n)\<rbrakk> \<Longrightarrow> bit w (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (metis add.commute le_antisym less_diff_conv less_eq_decr_length_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w n. \<lbrakk>LENGTH('a) - Suc 0 \<le> m + n; n < LENGTH('a) - m; m + n < LENGTH('a); bit w (m + n)\<rbrakk> \<Longrightarrow> bit w (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (metis le_antisym less_eq_decr_length_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_less_minus_mono_left: "y < z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x < z - x"
  for x y z :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < z; x \<le> y\<rbrakk> \<Longrightarrow> y - x < z - x
[PROOF STEP]
by uint_arith


[STATEMENT]
lemma word_rec_max:
  assumes "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id"
  shows "word_rec z f (- 1) = word_rec z f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
have \<section>: "\<And>m. \<lbrakk>m < - 1 - n\<rbrakk> \<Longrightarrow> (f \<circ> (+) n) m = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. m < - 1 - n \<Longrightarrow> (f \<circ> (+) n) m = id
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id

goal (1 subgoal):
 1. \<And>m. m < - 1 - n \<Longrightarrow> (f \<circ> (+) n) m = id
[PROOF STEP]
by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge)
[PROOF STATE]
proof (state)
this:
?m < - 1 - n \<Longrightarrow> (f \<circ> (+) n) ?m = id

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
have "word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)
[PROOF STEP]
by (meson word_n1_ge word_rec_twice)
[PROOF STATE]
proof (state)
this:
word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
have "... = word_rec z f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n) = word_rec z f n
[PROOF STEP]
by (metis (no_types, lifting) \<section> diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq)
[PROOF STATE]
proof (state)
this:
word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n) = word_rec z f n

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
word_rec z f (- 1) = word_rec z f n

goal (1 subgoal):
 1. word_rec z f (- 1) = word_rec z f n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
word_rec z f (- 1) = word_rec z f n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma factor_double_map: "double (map f xs) ys \<Longrightarrow> \<exists>zs. Dlist.dlist_eq xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. double (map f xs) ys \<Longrightarrow> \<exists>zs. Dlist.dlist_eq xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs
[PROOF STEP]
by(auto simp add: double.simps Dlist.dlist_eq_def vimage2p_def map_eq_append_conv)
    (metis (no_types, opaque_lifting) list.simps(9) map_append remdups.simps(2) remdups_append2 set_append set_eq_subset set_remdups)


[STATEMENT]
lemma lipschitz_extend_closure:
  fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
  assumes "C-lipschitz_on U f"
  shows "\<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
obtain g where g: "\<And>x. x \<in> U \<Longrightarrow> g x = f x" "uniformly_continuous_on (closure U) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>x. x \<in> U \<Longrightarrow> g x = f x; uniformly_continuous_on (closure U) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using uniformly_continuous_on_extension_on_closure[OF lipschitz_on_uniformly_continuous[OF assms]]
[PROOF STATE]
proof (prove)
using this:
(\<And>g. \<lbrakk>uniformly_continuous_on (closure U) g; \<And>x. x \<in> U \<Longrightarrow> f x = g x; \<And>Y h x. \<lbrakk>U \<subseteq> Y; Y \<subseteq> closure U; continuous_on Y h; \<And>x. x \<in> U \<Longrightarrow> f x = h x; x \<in> Y\<rbrakk> \<Longrightarrow> h x = g x\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>x. x \<in> U \<Longrightarrow> g x = f x; uniformly_continuous_on (closure U) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> U \<Longrightarrow> g ?x = f ?x
uniformly_continuous_on (closure U) g

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
have "C-lipschitz_on (closure U) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C-lipschitz_on (closure U) g
[PROOF STEP]
apply (rule lipschitz_on_closure, rule lipschitz_on_transform[OF assms])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> U \<Longrightarrow> g x = f x
 2. continuous_on (closure U) g
[PROOF STEP]
using g uniformly_continuous_imp_continuous[OF g(2)]
[PROOF STATE]
proof (prove)
using this:
?x \<in> U \<Longrightarrow> g ?x = f ?x
uniformly_continuous_on (closure U) g
continuous_on (closure U) g

goal (2 subgoals):
 1. \<And>x. x \<in> U \<Longrightarrow> g x = f x
 2. continuous_on (closure U) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C-lipschitz_on (closure U) g

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C-lipschitz_on (closure U) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C-lipschitz_on (closure U) g

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
using g(1)
[PROOF STATE]
proof (prove)
using this:
C-lipschitz_on (closure U) g
?x \<in> U \<Longrightarrow> g ?x = f ?x

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measurable_Pair_compose_split[measurable_dest]:
  assumes f: "case_prod f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f (g x) (h x)) \<in> M \<rightarrow>\<^sub>M N
[PROOF STEP]
using measurable_compose[OF measurable_Pair f, OF g h]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. case (g x, h x) of (x, xa) \<Rightarrow> f x xa) \<in> M \<rightarrow>\<^sub>M N

goal (1 subgoal):
 1. (\<lambda>x. f (g x) (h x)) \<in> M \<rightarrow>\<^sub>M N
[PROOF STEP]
by simp


[STATEMENT]
lemma uniformly_summable_deriv_ln_Gamma:
  assumes z: "(z :: 'a :: {real_normed_field,banach}) \<noteq> 0" and d: "d > 0" "d \<le> norm z/2"
  shows "uniformly_convergent_on (ball z d)
            (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))"
           (is "uniformly_convergent_on _ (\<lambda>k z. \<Sum>i<k. ?f i z)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))
[PROOF STEP]
proof (rule Weierstrass_m_test'_ev)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
assume t: "t \<in> ball z d"
[PROOF STATE]
proof (state)
this:
t \<in> ball z d

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "norm z = norm (t + (z - t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm z = norm (t + (z - t))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm z = norm (t + (z - t))

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "norm (t + (z - t)) \<le> norm t + norm (z - t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (t + (z - t)) \<le> norm t + norm (z - t)
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (t + (z - t)) \<le> norm t + norm (z - t)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (t + (z - t)) \<le> norm t + norm (z - t)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
from t d
[PROOF STATE]
proof (chain)
picking this:
t \<in> ball z d
0 < d
d \<le> norm z / 2
[PROOF STEP]
have "norm (z - t) < norm z / 2"
[PROOF STATE]
proof (prove)
using this:
t \<in> ball z d
0 < d
d \<le> norm z / 2

goal (1 subgoal):
 1. norm (z - t) < norm z / 2
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
norm (z - t) < norm z / 2

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x < y \<Longrightarrow> norm t + x < norm t + y) \<Longrightarrow> norm (t + (z - t)) < norm t + norm z / 2
[PROOF STEP]
have A: "norm t > norm z / 2"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> norm t + x < norm t + y) \<Longrightarrow> norm (t + (z - t)) < norm t + norm z / 2

goal (1 subgoal):
 1. norm z / 2 < norm t
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> norm t + x < norm t + y) \<Longrightarrow> norm (t + (z - t)) < norm t + norm z / 2
z \<noteq> (0::'a)

goal (1 subgoal):
 1. norm z / 2 < norm t
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
norm z / 2 < norm t

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "norm t = norm (z + (t - z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm t = norm (z + (t - z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm t = norm (z + (t - z))

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm t = norm (z + (t - z))

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "\<dots> \<le> norm z + norm (t - z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (z + (t - z)) \<le> norm z + norm (t - z)
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (z + (t - z)) \<le> norm z + norm (t - z)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (z + (t - z)) \<le> norm z + norm (t - z)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
from t d
[PROOF STATE]
proof (chain)
picking this:
t \<in> ball z d
0 < d
d \<le> norm z / 2
[PROOF STEP]
have "norm (t - z) \<le> norm z / 2"
[PROOF STATE]
proof (prove)
using this:
t \<in> ball z d
0 < d
d \<le> norm z / 2

goal (1 subgoal):
 1. norm (t - z) \<le> norm z / 2
[PROOF STEP]
by (simp add: dist_norm norm_minus_commute)
[PROOF STATE]
proof (state)
this:
norm (t - z) \<le> norm z / 2

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (t - z) \<le> norm z / 2

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
from z
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
[PROOF STEP]
have "\<dots> < norm z"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)

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

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> norm z + x \<le> norm z + y; \<And>x y. x < y \<Longrightarrow> norm z + x < norm z + y\<rbrakk> \<Longrightarrow> norm t < norm z + norm z
[PROOF STEP]
have B: "norm t < 2 * norm z"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> norm z + x \<le> norm z + y; \<And>x y. x < y \<Longrightarrow> norm z + x < norm z + y\<rbrakk> \<Longrightarrow> norm t < norm z + norm z

goal (1 subgoal):
 1. norm t < 2 * norm z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm t < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
note A B
[PROOF STATE]
proof (state)
this:
norm z / 2 < norm t
norm t < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?t2 \<in> ball z d \<Longrightarrow> norm z / 2 < norm ?t2
?t2 \<in> ball z d \<Longrightarrow> norm ?t2 < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
note ball = this
[PROOF STATE]
proof (state)
this:
?t2 \<in> ball z d \<Longrightarrow> norm z / 2 < norm ?t2
?t2 \<in> ball z d \<Longrightarrow> norm ?t2 < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
show "eventually (\<lambda>n. \<forall>t\<in>ball z d. norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
using eventually_gt_at_top
[PROOF STATE]
proof (prove)
using this:
eventually ((<) ?c) at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. ?c1 < n \<Longrightarrow> \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
fix t :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
assume t: "t \<in> ball z d"
[PROOF STATE]
proof (state)
this:
t \<in> ball z d

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from z ball[OF t]
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z
[PROOF STEP]
have t_nz: "t \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z

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

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
assume n: "n > nat \<lceil>4 * norm z\<rceil>"
[PROOF STATE]
proof (state)
this:
nat \<lceil>4 * norm z\<rceil> < n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from ball[OF t] t_nz
[PROOF STATE]
proof (chain)
picking this:
norm z / 2 < norm t
norm t < 2 * norm z
t \<noteq> (0::'a)
[PROOF STEP]
have "4 * norm z > 2 * norm t"
[PROOF STATE]
proof (prove)
using this:
norm z / 2 < norm t
norm t < 2 * norm z
t \<noteq> (0::'a)

goal (1 subgoal):
 1. 2 * norm t < 4 * norm z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * norm t < 4 * norm z

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * norm t < 4 * norm z

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
nat \<lceil>4 * norm z\<rceil> < n
[PROOF STEP]
have "\<dots>  < of_nat n"
[PROOF STATE]
proof (prove)
using this:
nat \<lceil>4 * norm z\<rceil> < n

goal (1 subgoal):
 1. 4 * norm z < real n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
4 * norm z < real n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * norm t < real n
[PROOF STEP]
have n: "of_nat n > 2 * norm t"
[PROOF STATE]
proof (prove)
using this:
2 * norm t < real n

goal (1 subgoal):
 1. 2 * norm t < real n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
2 * norm t < real n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
hence "of_nat n > norm t"
[PROOF STATE]
proof (prove)
using this:
2 * norm t < real n

goal (1 subgoal):
 1. norm t < real n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm t < real n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
hence t': "t \<noteq> -of_nat (Suc n)"
[PROOF STATE]
proof (prove)
using this:
norm t < real n

goal (1 subgoal):
 1. t \<noteq> - of_nat (Suc n)
[PROOF STEP]
by (intro notI) (simp del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
t \<noteq> - of_nat (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
with t_nz
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> (0::'a)
t \<noteq> - of_nat (Suc n)
[PROOF STEP]
have "?f n t = 1 / (of_nat (Suc n) * (1 + of_nat (Suc n)/t))"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> (0::'a)
t \<noteq> - of_nat (Suc n)

goal (1 subgoal):
 1. inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n)) = (1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))
[PROOF STEP]
by (simp add: field_split_simps eq_neg_iff_add_eq_0 del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n)) = (1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n)) = (1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "norm \<dots> = inverse (of_nat (Suc n)) * inverse (norm (of_nat (Suc n)/t + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))
[PROOF STEP]
by (simp add: norm_divide norm_mult field_split_simps del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from z t_nz ball[OF t]
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
t \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z
[PROOF STEP]
have "of_nat (Suc n) / (4 * norm z) \<le> of_nat (Suc n) / (2 * norm t)"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)
t \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z

goal (1 subgoal):
 1. real (Suc n) / (4 * norm z) \<le> real (Suc n) / (2 * norm t)
[PROOF STEP]
by (intro divide_left_mono mult_pos_pos) simp_all
[PROOF STATE]
proof (state)
this:
real (Suc n) / (4 * norm z) \<le> real (Suc n) / (2 * norm t)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (Suc n) / (4 * norm z) \<le> real (Suc n) / (2 * norm t)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "\<dots> < norm (of_nat (Suc n) / t) - norm (1 :: 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)
[PROOF STEP]
using t_nz n
[PROOF STATE]
proof (prove)
using this:
t \<noteq> (0::'a)
2 * norm t < real n

goal (1 subgoal):
 1. real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)
[PROOF STEP]
by (simp add: field_simps norm_divide del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "\<dots> \<le> norm (of_nat (Suc n)/t + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_nat (Suc n) / t) - norm (1::'a) \<le> norm (of_nat (Suc n) / t + (1::'a))
[PROOF STEP]
by (rule norm_diff_ineq)
[PROOF STATE]
proof (state)
this:
norm (of_nat (Suc n) / t) - norm (1::'a) \<le> norm (of_nat (Suc n) / t + (1::'a))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (Suc n) / (4 * norm z) < norm (of_nat (Suc n) / t + (1::'a))
[PROOF STEP]
have "inverse (norm (of_nat (Suc n)/t + 1)) \<le> 4 * norm z / of_nat (Suc n)"
[PROOF STATE]
proof (prove)
using this:
real (Suc n) / (4 * norm z) < norm (of_nat (Suc n) / t + (1::'a))

goal (1 subgoal):
 1. inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
real (Suc n) / (4 * norm z) < norm (of_nat (Suc n) / t + (1::'a))
z \<noteq> (0::'a)

goal (1 subgoal):
 1. inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)
[PROOF STEP]
by (simp add: field_split_simps norm_divide mult_ac del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "inverse (real_of_nat (Suc n)) * (4 * norm z / real_of_nat (Suc n)) =
                 4 * norm z * inverse (of_nat (Suc n)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real (Suc n)) * (4 * norm z / real (Suc n)) = 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
by (simp add: field_split_simps power2_eq_square del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
inverse (real (Suc n)) * (4 * norm z / real (Suc n)) = 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> inverse (real (Suc n)) * x \<le> inverse (real (Suc n)) * y) \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
show "norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> inverse (real (Suc n)) * x \<le> inverse (real (Suc n)) * y) \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal (1 subgoal):
 1. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
by (simp del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal (1 subgoal):
 1. summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))
[PROOF STEP]
show "summable (\<lambda>n. 4 * norm z * inverse ((of_nat (Suc n))^2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))
[PROOF STEP]
by (subst summable_Suc_iff) (simp add: summable_mult inverse_power_summable)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rGamma_series_LIMSEQ [tendsto_intros]:
  "rGamma_series z \<longlonglongrightarrow> rGamma z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
 2. z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<notin> \<int>\<^sub>\<le>\<^sub>0

goal (2 subgoals):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
 2. z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
hence "z \<noteq> - of_nat n" for n
[PROOF STATE]
proof (prove)
using this:
z \<notin> \<int>\<^sub>\<le>\<^sub>0

goal (1 subgoal):
 1. z \<noteq> - of_nat n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<noteq> - of_nat ?n

goal (2 subgoals):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
 2. z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
from rGamma_series_aux[OF this]
[PROOF STATE]
proof (chain)
picking this:
let fact' = \<lambda>n. prod of_nat {1..n}; exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e; pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real n) *\<^sub>R (1::'a)))) \<longlonglongrightarrow> rGamma z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
let fact' = \<lambda>n. prod of_nat {1..n}; exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e; pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real n) *\<^sub>R (1::'a)))) \<longlonglongrightarrow> rGamma z

goal (1 subgoal):
 1. rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
by (simp add: rGamma_series_def[abs_def] fact_prod pochhammer_Suc_prod
                  exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
[PROOF STATE]
proof (state)
this:
rGamma_series z \<longlonglongrightarrow> rGamma z

goal (1 subgoal):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)


[STATEMENT]
lemma (in ccpo) mcont_if_bot:
  fixes bot and lub ("\<Or>") and ord (infix "\<sqsubseteq>" 60)
  assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
  and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
  and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x"
  shows "mcont Sup (\<le>) lub (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont Sup (\<le>) \<Or> (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
[PROOF STEP]
proof(intro mcontI contI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
 2. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
interpret c: ccpo lub "(\<sqsubseteq>)" lt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.ccpo \<Or> (\<sqsubseteq>) lt
[PROOF STEP]
by(fact ccpo)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
 2. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show "monotone (\<le>) (\<sqsubseteq>) ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
[PROOF STEP]
by(rule monotone_if_bot)(simp_all add: mono bot)
[PROOF STATE]
proof (state)
this:
monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
assume chain: "Complete_Partial_Order.chain (\<le>) Y" and Y: "Y \<noteq> {}"
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<le>) Y
Y \<noteq> {}

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show "?g (\<Squnion>Y) = \<Or>(?g ` Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
proof(cases "Y \<subseteq> {x. x \<le> bound}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Y \<subseteq> {x. x \<le> bound}

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<Squnion>Y \<le> bound"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. \<Squnion> Y \<le> bound
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> {x. x \<le> bound}
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. \<Squnion> Y \<le> bound
[PROOF STEP]
by(auto intro: ccpo_Sup_least)
[PROOF STATE]
proof (state)
this:
\<Squnion> Y \<le> bound

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Squnion> Y \<le> bound

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "Y \<inter> {x. \<not> x \<le> bound} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<inter> {x. \<not> x \<le> bound} = {}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. Y \<inter> {x. \<not> x \<le> bound} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<inter> {x. \<not> x \<le> bound} = {}

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Squnion> Y \<le> bound
Y \<inter> {x. \<not> x \<le> bound} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y \<le> bound
Y \<inter> {x. \<not> x \<le> bound} = {}

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
using True Y
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y \<le> bound
Y \<inter> {x. \<not> x \<le> bound} = {}
Y \<subseteq> {x. x \<le> bound}
Y \<noteq> {}

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have chain': "Complete_Partial_Order.chain (\<le>) ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
by(rule chain_subset) simp
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> Y \<subseteq> {x. x \<le> bound}
[PROOF STEP]
obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y"
[PROOF STATE]
proof (prove)
using this:
\<not> Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>\<not> y \<le> bound; y \<in> Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> y \<le> bound
y \<in> Y

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<not> \<Squnion>Y \<le> bound"
[PROOF STATE]
proof (prove)
using this:
\<not> y \<le> bound
y \<in> Y

goal (1 subgoal):
 1. \<not> \<Squnion> Y \<le> bound
[PROOF STEP]
by (metis ccpo_Sup_upper chain order.trans)
[PROOF STATE]
proof (state)
this:
\<not> \<Squnion> Y \<le> bound

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "?g (\<Squnion>Y) = f (\<Squnion>Y)"
[PROOF STATE]
proof (prove)
using this:
\<not> \<Squnion> Y \<le> bound

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = f (\<Squnion> Y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = f (\<Squnion> Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = f (\<Squnion> Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "\<Squnion>Y \<le> \<Squnion>?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. \<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
proof(rule ccpo_Sup_least)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
assume x: "x \<in> Y"
[PROOF STATE]
proof (state)
this:
x \<in> Y

goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
show "x \<le> \<Squnion>?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
proof(cases "x \<le> bound")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
 2. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<le> bound

goal (2 subgoals):
 1. x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
 2. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
with chainD[OF chain x y]
[PROOF STATE]
proof (chain)
picking this:
x \<le> y \<or> y \<le> x
x \<le> bound
[PROOF STEP]
have "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
x \<le> y \<or> y \<le> x
x \<le> bound

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
using ybound
[PROOF STATE]
proof (prove)
using this:
x \<le> y \<or> y \<le> x
x \<le> bound
\<not> y \<le> bound

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

goal (2 subgoals):
 1. x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
 2. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
[PROOF STATE]
proof (state)
this:
x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
[PROOF STATE]
proof (state)
this:
x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<Squnion>Y = \<Squnion>?Y"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<Squnion> Y = \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
by(rule order.antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
[PROOF STATE]
proof (state)
this:
\<Squnion> Y = \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "f (\<Squnion>Y) = f (\<Squnion>?Y)"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y = \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. f (\<Squnion> Y) = f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (\<Squnion> Y) = f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (\<Squnion> Y) = f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
using chain'
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(rule cont)(insert y ybound, auto)
[PROOF STATE]
proof (state)
this:
f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
proof(cases "Y \<inter> {x. x \<le> bound} = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y \<inter> {x. x \<le> bound} = {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Y \<inter> {x. x \<le> bound} = {}

goal (2 subgoals):
 1. Y \<inter> {x. x \<le> bound} = {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "f ` ?Y = ?g ` Y"
[PROOF STATE]
proof (prove)
using this:
Y \<inter> {x. x \<le> bound} = {}

goal (1 subgoal):
 1. f ` (Y \<inter> {x. \<not> x \<le> bound}) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` (Y \<inter> {x. \<not> x \<le> bound}) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y

goal (2 subgoals):
 1. Y \<inter> {x. x \<le> bound} = {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` (Y \<inter> {x. \<not> x \<le> bound}) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y

goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
by(rule arg_cong)
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Y \<inter> {x. x \<le> bound} \<noteq> {}

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have chain'': "Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` ?Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))
[PROOF STEP]
by(auto intro!: chainI bot dest: chainD intro: mono)
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence chain''': "Complete_Partial_Order.chain (\<sqsubseteq>) (f ` ?Y)"
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<sqsubseteq>) (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(rule chain_subset) blast
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<sqsubseteq>) (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "bot \<sqsubseteq> \<Or>(f ` ?Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
using y ybound
[PROOF STATE]
proof (prove)
using this:
y \<in> Y
\<not> y \<le> bound

goal (1 subgoal):
 1. bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])
[PROOF STATE]
proof (state)
this:
bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)"
[PROOF STATE]
proof (prove)
using this:
bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
using chain''
[PROOF STATE]
proof (prove)
using this:
bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain'''])
[PROOF STATE]
proof (state)
this:
\<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
with _
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
\<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
have "\<dots> = \<Or>(insert bot (f ` ?Y))"
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
\<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))
[PROOF STEP]
by(rule c.order.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "insert bot (f ` ?Y) = ?g ` Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Y \<inter> {x. x \<le> bound} \<noteq> {}

goal (1 subgoal):
 1. insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_keysD: "k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> keys m \<Longrightarrow> \<exists>v. lookup m k = Some v
[PROOF STEP]
by transfer (fact domD)


[STATEMENT]
lemma add_eq_conv_ex:
  "(add_mset a M = add_mset b N) =
    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (add_mset a M = add_mset b N) = (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))
[PROOF STEP]
by (auto simp add: add_eq_conv_diff)


[STATEMENT]
lemma filter_mset_cong:
  assumes "M = M'" and "\<And>x. x \<in># M' \<Longrightarrow> f x \<longleftrightarrow> g x"
  shows "filter_mset f M = filter_mset g M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset f M = filter_mset g M'
[PROOF STEP]
unfolding \<open>M = M'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset f M' = filter_mset g M'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M = M'
?x \<in># M' \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. filter_mset f M' = filter_mset g M'
[PROOF STEP]
by (auto intro: filter_mset_cong0)


[STATEMENT]
lemma size_multiset_eq_0_iff_empty [iff]:
  "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (size_multiset f M = 0) = (M = {#})
[PROOF STEP]
by (auto simp add: size_multiset_eq count_eq_zero_iff)


[STATEMENT]
lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset [m..<n] = mset_set {m..<n}
[PROOF STEP]
by (induction n) (simp_all add: atLeastLessThanSuc)


[STATEMENT]
lemma mult1I:
  assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
  shows "(N, M) \<in> mult1 r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (N, M) \<in> mult1 r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M = add_mset a M0
N = M0 + K
?b \<in># K \<Longrightarrow> (?b, a) \<in> r

goal (1 subgoal):
 1. (N, M) \<in> mult1 r
[PROOF STEP]
unfolding mult1_def
[PROOF STATE]
proof (prove)
using this:
M = add_mset a M0
N = M0 + K
?b \<in># K \<Longrightarrow> (?b, a) \<in> r

goal (1 subgoal):
 1. (N, M) \<in> {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}
[PROOF STEP]
by blast


[STATEMENT]
lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> r' \<Longrightarrow> multp r \<le> multp r'
[PROOF STEP]
unfolding le_fun_def le_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. r x xa \<longrightarrow> r' x xa \<Longrightarrow> \<forall>x xa. multp r x xa \<longrightarrow> multp r' x xa
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
fix M N :: "'a multiset"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
[PROOF STATE]
proof (state)
this:
\<forall>x xa. r x xa \<longrightarrow> r' x xa

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x xa. r x xa \<longrightarrow> r' x xa

goal (1 subgoal):
 1. {(x, y). r x y} \<subseteq> {(x, y). r' x y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{(x, y). r x y} \<subseteq> {(x, y). r' x y}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
thus "multp r M N \<Longrightarrow> multp r' M N"
[PROOF STATE]
proof (prove)
using this:
{(x, y). r x y} \<subseteq> {(x, y). r' x y}

goal (1 subgoal):
 1. multp r M N \<Longrightarrow> multp r' M N
[PROOF STEP]
unfolding multp_def
[PROOF STATE]
proof (prove)
using this:
{(x, y). r x y} \<subseteq> {(x, y). r' x y}

goal (1 subgoal):
 1. (M, N) \<in> mult {(x, y). r x y} \<Longrightarrow> (M, N) \<in> mult {(x, y). r' x y}
[PROOF STEP]
by (fact mono_mult[THEN subsetD, rotated])
[PROOF STATE]
proof (state)
this:
multp r M N \<Longrightarrow> multp r' M N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fmdrop_idle': "x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B
[PROOF STEP]
by transfer' (auto simp: map_drop_def map_filter_def)


[STATEMENT]
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B \<subseteq> wp act B \<inter> awp F (B \<union> A) \<Longrightarrow> A \<subseteq> wens F act B
[PROOF STEP]
apply (simp add: wens_def wp_def awp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B \<subseteq> - act\<inverse> `` (- B) \<and> A - B \<subseteq> (\<Inter>x\<in>Acts F. - x\<inverse> `` (- B \<inter> - A)) \<Longrightarrow> A \<subseteq> gfp (\<lambda>X. - act\<inverse> `` (- B) \<inter> (\<Inter>x\<in>Acts F. - x\<inverse> `` (- B \<inter> - X)) \<union> B)
[PROOF STEP]
apply (rule gfp_upperbound, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma less_bot_Bot_Value [simp]: "Bot < Value x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bot < Value x
[PROOF STEP]
by (simp add: less_bot_def)


[STATEMENT]
lemma linear_eq_on:
  assumes l: "linear s1 s2 f" "linear s1 s2 g"
  assumes x: "x \<in> vs1.span B" and eq: "\<And>b. b \<in> B \<Longrightarrow> f b = g b"
  shows "f x = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
interpret d: linear s1 s2 "\<lambda>x. f x - g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (*a) (*b) (\<lambda>x. f x - g x)
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
linear (*a) (*b) f
linear (*a) (*b) g

goal (1 subgoal):
 1. linear (*a) (*b) (\<lambda>x. f x - g x)
[PROOF STEP]
by (intro linear_compose_sub) (auto simp: module_hom_iff_linear)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
have "f x - g x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x - g x = (0::'c)
[PROOF STEP]
by (rule d.eq_0_on_span[OF _ x]) (auto simp: eq)
[PROOF STATE]
proof (state)
this:
f x - g x = (0::'c)

goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x - g x = (0::'c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f x - g x = (0::'c)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_linear_imp_inv_linear:
  assumes "linear scale scale f" "inj f" shows "linear scale scale (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (*s) (*s) (inv f)
[PROOF STEP]
using assms inj_iff left_inverse_linear
[PROOF STATE]
proof (prove)
using this:
linear (*s) (*s) f
inj f
inj ?f = (inv ?f \<circ> ?f = id)
\<lbrakk>linear (*s) (*s) ?f; ?g \<circ> ?f = id\<rbrakk> \<Longrightarrow> linear (*s) (*s) ?g

goal (1 subgoal):
 1. linear (*s) (*s) (inv f)
[PROOF STEP]
by blast


[STATEMENT]
lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; b < 0\<rbrakk> \<Longrightarrow> a sdiv b = - (a div - b)
[PROOF STEP]
by (simp add: sdiv_def sgn_if)


[STATEMENT]
lemma constrains_Int:
    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<in> A co A'; F \<in> B co B'\<rbrakk> \<Longrightarrow> F \<in> A \<inter> B co A' \<inter> B'
[PROOF STEP]
by (unfold constrains_def, blast)


[STATEMENT]
lemma mirror_ex:
  assumes "iszlfm p"
  shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) p)"
  (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. Ifm bbs (x # bs) (mirror p)) = (\<exists>x. Ifm bbs (x # bs) p)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
assume "?I x ?mp"
[PROOF STATE]
proof (state)
this:
Ifm bbs (x # bs) (mirror p)

goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
have "?I (- x) p"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) (mirror p)

goal (1 subgoal):
 1. Ifm bbs (- x # bs) p
[PROOF STEP]
using mirror[OF assms]
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) (mirror p)
Ifm ?bbs (?x # ?bs) (mirror p) = Ifm ?bbs (- ?x # ?bs) p

goal (1 subgoal):
 1. Ifm bbs (- x # bs) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ifm bbs (- x # bs) p

goal (2 subgoals):
 1. \<And>x. Ifm bbs (x # bs) (mirror p) \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) p
 2. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (- x # bs) p
[PROOF STEP]
show "\<exists>x. ?I x p"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (- x # bs) p

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

goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
assume "?I x p"
[PROOF STATE]
proof (state)
this:
Ifm bbs (x # bs) p

goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (x # bs) p
[PROOF STEP]
have "?I (- x) ?mp"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) p

goal (1 subgoal):
 1. Ifm bbs (- x # bs) (mirror p)
[PROOF STEP]
using mirror[OF assms, where x="- x", symmetric]
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (x # bs) p
Ifm ?bbs (- (- x) # ?bs) p = Ifm ?bbs (- x # ?bs) (mirror p)

goal (1 subgoal):
 1. Ifm bbs (- x # bs) (mirror p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ifm bbs (- x # bs) (mirror p)

goal (1 subgoal):
 1. \<And>x. Ifm bbs (x # bs) p \<Longrightarrow> \<exists>x. Ifm bbs (x # bs) (mirror p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ifm bbs (- x # bs) (mirror p)
[PROOF STEP]
show "\<exists>x. ?I x ?mp"
[PROOF STATE]
proof (prove)
using this:
Ifm bbs (- x # bs) (mirror p)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_elem_multiplicity_prod_mset_distrib:
  assumes "prime_elem p" "0 \<notin># A"
  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (\<Prod>\<^sub># A) = \<Sum>\<^sub># (image_mset (multiplicity p) A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime_elem p
(0::'a) \<notin># A

goal (1 subgoal):
 1. multiplicity p (\<Prod>\<^sub># A) = \<Sum>\<^sub># (image_mset (multiplicity p) A)
[PROOF STEP]
by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)


[STATEMENT]
lemma Fract_less_zero_iff: "0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < b \<Longrightarrow> (Fract a b < 0) = (a < (0::'a))
[PROOF STEP]
by (auto simp add: Zero_fract_def mult_less_0_iff)


[STATEMENT]
lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (n choose k) = of_nat n gchoose k
[PROOF STEP]
by (simp add: gbinomial_binomial [symmetric] of_nat_gbinomial)


[STATEMENT]
lemma invar_delete: "invar t \<Longrightarrow> invar (delete xs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar t \<Longrightarrow> invar (Trie_Map.delete xs t)
[PROOF STEP]
apply(induction xs t rule: delete.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b m. invar (trie_map.Nd b m) \<Longrightarrow> invar (Trie_Map.delete [] (trie_map.Nd b m))
 2. \<And>x xs b m. \<lbrakk>\<And>x2. \<lbrakk>lookup m x = Some x2; invar x2\<rbrakk> \<Longrightarrow> invar (Trie_Map.delete xs x2); invar (trie_map.Nd b m)\<rbrakk> \<Longrightarrow> invar (Trie_Map.delete (x # xs) (trie_map.Nd b m))
[PROOF STEP]
apply(auto simp: M.map_specs split: option.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done