[STATEMENT]
lemma euler_60_decimals:
  "\<bar>exp 1 - 2.718281828459045235360287471352662497757247093699959574966968\<bar>
      \<le> inverse (10^60::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>exp 1 - 2718281828459045235360287471352662497757247093699959574966968 / 10 ^ 60\<bar> \<le> inverse (10 ^ 60)
[PROOF STEP]
by (rule approx_coarsen, rule exp_1_approx[of 48])
     (simp_all add: eval_euler_approx eval_fact)


[STATEMENT]
lemma nths_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> nths xs inds = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>inds. length xs \<le> i \<Longrightarrow> nths xs inds = []
[PROOF STEP]
apply (induct xs arbitrary: inds)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>inds. Ball inds ((\<le>) (length [])) \<Longrightarrow> nths [] inds = []
 2. \<And>a xs inds. \<lbrakk>\<And>inds. Ball inds ((\<le>) (length xs)) \<Longrightarrow> nths xs inds = []; Ball inds ((\<le>) (length (a # xs)))\<rbrakk> \<Longrightarrow> nths (a # xs) inds = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs inds. \<lbrakk>\<And>inds. Ball inds ((\<le>) (length xs)) \<Longrightarrow> nths xs inds = []; Ball inds ((\<le>) (length (a # xs)))\<rbrakk> \<Longrightarrow> nths (a # xs) inds = []
[PROOF STEP]
apply (simp add: nths_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs inds. \<lbrakk>\<And>inds. Ball inds ((\<le>) (length xs)) \<Longrightarrow> nths xs inds = []; Ball inds ((\<le>) (Suc (length xs)))\<rbrakk> \<Longrightarrow> 0 \<notin> inds \<and> (0 \<notin> inds \<longrightarrow> nths xs {j. Suc j \<in> inds} = [])
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs inds. \<lbrakk>\<And>inds. \<forall>x\<in>inds. length xs \<le> x \<Longrightarrow> nths xs inds = []; \<forall>x\<in>inds. Suc (length xs) \<le> x; 0 \<notin> inds\<rbrakk> \<Longrightarrow> nths xs {j. Suc j \<in> inds} = []
[PROOF STEP]
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs inds. \<lbrakk>\<forall>x\<in>inds. Suc (length xs) \<le> x; 0 \<notin> inds; \<forall>x\<in>{j. Suc j \<in> inds}. length xs \<le> x \<Longrightarrow> nths xs {j. Suc j \<in> inds} = []\<rbrakk> \<Longrightarrow> nths xs {j. Suc j \<in> inds} = []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rev_length:
  assumes "effect (rev a i j) h h' r"
  shows "Array.length h a = Array.length h' a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array.length h a = Array.length h' a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (Imperative_Reverse.rev a i j) h h' r

goal (1 subgoal):
 1. Array.length h a = Array.length h' a
[PROOF STEP]
proof (induct a i j arbitrary: h h' rule: rev.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a i j h h'. \<lbrakk>\<And>x h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a
[PROOF STEP]
case (1 a i j h h'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r

goal (1 subgoal):
 1. \<And>a i j h h'. \<lbrakk>\<And>x h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
proof (cases "i < j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
 2. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
 2. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
with 1[unfolded rev.simps[of a i j]]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
i < j
[PROOF STEP]
obtain h' where
      swp: "effect (swap a i j) h h' ()"
      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
i < j

goal (1 subgoal):
 1. (\<And>h'. \<lbrakk>effect (swap a i j) h h' (); effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: effect_elims)
[PROOF STATE]
proof (state)
this:
effect (swap a i j) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()

goal (2 subgoals):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
 2. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
from swp rev 1 True
[PROOF STATE]
proof (chain)
picking this:
effect (swap a i j) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r
i < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
effect (swap a i j) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r
i < j

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
unfolding swap.simps
[PROOF STATE]
proof (prove)
using this:
effect (Array.nth a i \<bind> (\<lambda>x. Array.nth a j \<bind> (\<lambda>y. Array.upd i y a \<bind> (\<lambda>_. Array.upd j x a \<bind> (\<lambda>_. return ()))))) h h' ()
effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h' h'' ()
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (Imperative_Reverse.rev a i j) h h'' r
i < j

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
by (elim effect_elims) fastforce
[PROOF STATE]
proof (state)
this:
Array.length h a = Array.length h'' a

goal (1 subgoal):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<lbrakk>\<And>h h'. \<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) h h' r\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h' a; effect (Imperative_Reverse.rev a i j) h h'' r; \<not> i < j\<rbrakk> \<Longrightarrow> Array.length h a = Array.length h'' a
[PROOF STEP]
with 1[unfolded rev.simps[of a i j]]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
\<not> i < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < j; effect (Imperative_Reverse.rev a (i + 1) (j - 1)) ?h ?h' r\<rbrakk> \<Longrightarrow> Array.length ?h a = Array.length ?h' a
effect (if i < j then swap a i j \<bind> (\<lambda>_. Imperative_Reverse.rev a (i + 1) (j - 1)) else return ()) h h'' r
\<not> i < j

goal (1 subgoal):
 1. Array.length h a = Array.length h'' a
[PROOF STEP]
by (auto elim: effect_elims)
[PROOF STATE]
proof (state)
this:
Array.length h a = Array.length h'' a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Array.length h a = Array.length h'' a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cbox_translation: "cbox (c + a) (c + b) = image (\<lambda>x. c + x) (cbox a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox (c + a) (c + b) = (+) c ` cbox a b
[PROOF STEP]
using image_affinity_cbox [of 1 c a b]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 1 *\<^sub>R x + c) ` cbox a b = (if cbox a b = {} then {} else if 0 \<le> 1 then cbox (1 *\<^sub>R a + c) (1 *\<^sub>R b + c) else cbox (1 *\<^sub>R b + c) (1 *\<^sub>R a + c))

goal (1 subgoal):
 1. cbox (c + a) (c + b) = (+) c ` cbox a b
[PROOF STEP]
using box_ne_empty [of "a+c" "b+c"]  box_ne_empty [of a b]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 1 *\<^sub>R x + c) ` cbox a b = (if cbox a b = {} then {} else if 0 \<le> 1 then cbox (1 *\<^sub>R a + c) (1 *\<^sub>R b + c) else cbox (1 *\<^sub>R b + c) (1 *\<^sub>R a + c))
(cbox (a + c) (b + c) \<noteq> {}) = (\<forall>i\<in>Basis. (a + c) \<bullet> i \<le> (b + c) \<bullet> i)
(box (a + c) (b + c) \<noteq> {}) = (\<forall>i\<in>Basis. (a + c) \<bullet> i < (b + c) \<bullet> i)
(cbox a b \<noteq> {}) = (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
(box a b \<noteq> {}) = (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)

goal (1 subgoal):
 1. cbox (c + a) (c + b) = (+) c ` cbox a b
[PROOF STEP]
by (auto simp: inner_left_distrib add.commute)


[STATEMENT]
lemma "(\<lambda>f x y. (curry o case_prod) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. curry \<circ> case_prod = (\<lambda>f. f)
[PROOF STEP]
nitpick [card = 1-12, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. curry \<circ> case_prod = (\<lambda>f. f)
[PROOF STEP]
by auto


[STATEMENT]
lemma "g = Let (A \<or> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = Let (A \<or> B)
[PROOF STEP]
nitpick [card = 1, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = Let (A \<or> B)
[PROOF STEP]
nitpick [card = 12, expect = genuine]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = Let (A \<or> B)
[PROOF STEP]
oops


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


[STATEMENT]
lemma last_fst_esp:
 "fst(((Some a,s)#xs)!(length xs))=None \<Longrightarrow> fst(xs!(length xs - (Suc 0)))=None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (((Some a, s) # xs) ! length xs) = None \<Longrightarrow> fst (xs ! (length xs - Suc 0)) = None
[PROOF STEP]
apply(erule last_fst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Some a, s) \<noteq> None
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma open_segment_Reals:
    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> open_segment x y = complex_of_real ` open_segment (Re x) (Re y)
[PROOF STEP]
by (metis open_segment_of_real of_real_Re)


[STATEMENT]
lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. between (a + y, a + z) (a + x) = between (y, z) x
[PROOF STEP]
by (auto simp: between_def)


[STATEMENT]
lemma "(a::int) * b + a * c = a * (b + c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b + a * c = a * (b + c)
[PROOF STEP]
by ring


[STATEMENT]
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bseq X = Bseq X
[PROOF STEP]
..


[STATEMENT]
lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq f"
  for f :: "nat \<Rightarrow> 'a::real_normed_vector"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bseq (\<lambda>x. f x + c) = Bseq f
[PROOF STEP]
using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"]
[PROOF STATE]
proof (prove)
using this:
Bseq f \<Longrightarrow> Bseq (\<lambda>x. f x + c)
Bseq (\<lambda>x. f x + c) \<Longrightarrow> Bseq (\<lambda>x. f x + c + - c)

goal (1 subgoal):
 1. Bseq (\<lambda>x. f x + c) = Bseq f
[PROOF STEP]
by auto


[STATEMENT]
lemma filterlim_pow_at_bot_even:
  fixes f :: "real \<Rightarrow> real"
  shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> even n \<Longrightarrow> LIM x F. (f x)^n :> at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; filterlim f at_bot F; even n\<rbrakk> \<Longrightarrow> LIM x F. f x ^ n :> at_top
[PROOF STEP]
using filterlim_pow_at_top[of n "\<lambda>x. - f x" F]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < n; LIM x F. - f x :> at_top\<rbrakk> \<Longrightarrow> LIM x F. (- f x) ^ n :> at_top

goal (1 subgoal):
 1. \<lbrakk>0 < n; filterlim f at_bot F; even n\<rbrakk> \<Longrightarrow> LIM x F. f x ^ n :> at_top
[PROOF STEP]
by (simp add: filterlim_uminus_at_top)


[STATEMENT]
lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re L
[PROOF STEP]
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)


[STATEMENT]
lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hypreal_of_real (Re x) = hRe (hcomplex_of_complex x)
[PROOF STEP]
by transfer (rule refl)


[STATEMENT]
lemma suffix_conc_snd[simp]:
  assumes "n \<ge> length u"
  shows "suffix n (u \<frown> v) = suffix (n - length u) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix n (u \<frown> v) = suffix (n - length u) v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. suffix n (u \<frown> v) x = suffix (n - length u) v x
[PROOF STEP]
show "suffix n (u \<frown> v) i = suffix (n - length u) v i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix n (u \<frown> v) i = suffix (n - length u) v i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length u \<le> n

goal (1 subgoal):
 1. suffix n (u \<frown> v) i = suffix (n - length u) v i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
suffix n (u \<frown> v) ?i = suffix (n - length u) v ?i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integral_split:
  assumes f: "continuous_on (closed_segment a b) f"
      and k: "0 \<le> k" "k \<le> 1"
      and c: "c - a = k *\<^sub>R (b - a)"
    shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (1 - k) *\<^sub>R a + k *\<^sub>R b
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
c - a = k *\<^sub>R (b - a)

goal (1 subgoal):
 1. c = (1 - k) *\<^sub>R a + k *\<^sub>R b
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
c = (1 - k) *\<^sub>R a + k *\<^sub>R b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
have "closed_segment a c \<subseteq> closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment a c \<subseteq> closed_segment a b
[PROOF STEP]
by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment)
[PROOF STATE]
proof (state)
this:
closed_segment a c \<subseteq> closed_segment a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
closed_segment a c \<subseteq> closed_segment a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
have "closed_segment c b \<subseteq> closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
by (metis c' ends_in_segment(2) in_segment(1) k subset_closed_segment)
[PROOF STATE]
proof (state)
this:
closed_segment c b \<subseteq> closed_segment a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
closed_segment a c \<subseteq> closed_segment a b
closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
have *: "continuous_on (closed_segment a c) f" "continuous_on (closed_segment c b) f"
[PROOF STATE]
proof (prove)
using this:
closed_segment a c \<subseteq> closed_segment a b
closed_segment c b \<subseteq> closed_segment a b

goal (1 subgoal):
 1. continuous_on (closed_segment a c) f &&& continuous_on (closed_segment c b) f
[PROOF STEP]
by (auto intro: continuous_on_subset [OF f])
[PROOF STATE]
proof (state)
this:
continuous_on (closed_segment a c) f
continuous_on (closed_segment c b) f

goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f
[PROOF STEP]
by (rule contour_integral_unique) (meson "*" c contour_integrable_continuous_linepath has_contour_integral_integral has_contour_integral_split k)
[PROOF STATE]
proof (state)
this:
contour_integral (linepath a b) f = contour_integral (linepath a c) f + contour_integral (linepath c b) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b
[PROOF STEP]
apply (induct set: fine, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b c D a x. \<lbrakk>fine \<delta> (b, c) D; D \<noteq> [] \<Longrightarrow> b < c; a < b; a \<le> x; x \<le> b; b - a < \<delta> x; (a, x, b) # D \<noteq> []\<rbrakk> \<Longrightarrow> a < c
[PROOF STEP]
apply (drule fine_imp_le, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma affine_hull_closed_segment [simp]:
     "affine hull (closed_segment a b) = affine hull {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. affine hull closed_segment a b = affine hull {a, b}
[PROOF STEP]
by (simp add: segment_convex_hull)


[STATEMENT]
lemma Int_convex_hull_insert_rel_exterior:
  fixes z :: "'a::euclidean_space"
  assumes "convex C" "T \<subseteq> C" and z: "z \<in> rel_interior C" and dis: "disjnt S (rel_interior C)"
  shows "S \<inter> (convex hull (insert z T)) = S \<inter> (convex hull T)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> convex hull insert z T = S \<inter> convex hull T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T
 2. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
have "T = {} \<Longrightarrow> z \<notin> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T = {} \<Longrightarrow> z \<notin> S
[PROOF STEP]
using dis z
[PROOF STATE]
proof (prove)
using this:
disjnt S (rel_interior C)
z \<in> rel_interior C

goal (1 subgoal):
 1. T = {} \<Longrightarrow> z \<notin> S
[PROOF STEP]
by (auto simp add: disjnt_def)
[PROOF STATE]
proof (state)
this:
T = {} \<Longrightarrow> z \<notin> S

goal (2 subgoals):
 1. S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T
 2. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = {} \<Longrightarrow> z \<notin> S
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
using this:
T = {} \<Longrightarrow> z \<notin> S

goal (1 subgoal):
 1. S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T
[PROOF STEP]
proof (clarsimp simp add: convex_hull_insert_segments)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
assume "x \<in> S" and y: "y \<in> convex hull T" and "x \<in> closed_segment z y"
[PROOF STATE]
proof (state)
this:
x \<in> S
y \<in> convex hull T
x \<in> closed_segment z y

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
have "y \<in> closure C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> closure C
[PROOF STEP]
by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
[PROOF STATE]
proof (state)
this:
y \<in> closure C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> closure C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
have "x \<notin> rel_interior C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> rel_interior C
[PROOF STEP]
by (meson \<open>x \<in> S\<close> dis disjnt_iff)
[PROOF STATE]
proof (state)
this:
x \<notin> rel_interior C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> rel_interior C

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
have "x \<in> open_segment z y \<union> {z, y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> open_segment z y \<union> {z, y}
[PROOF STEP]
using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment z y
closed_segment ?a ?b = open_segment ?a ?b \<union> {?a, ?b}

goal (1 subgoal):
 1. x \<in> open_segment z y \<union> {z, y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> open_segment z y \<union> {z, y}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>T \<noteq> {}; x \<in> S; xa \<in> convex hull T; x \<in> closed_segment z xa\<rbrakk> \<Longrightarrow> x \<in> convex hull T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}
[PROOF STEP]
show "x \<in> convex hull T"
[PROOF STATE]
proof (prove)
using this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}

goal (1 subgoal):
 1. x \<in> convex hull T
[PROOF STEP]
using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
[PROOF STATE]
proof (prove)
using this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}
?b \<in> closure C \<Longrightarrow> open_segment z ?b \<subseteq> rel_interior C

goal (1 subgoal):
 1. x \<in> convex hull T
[PROOF STEP]
using y z
[PROOF STATE]
proof (prove)
using this:
y \<in> closure C
x \<notin> rel_interior C
x \<in> open_segment z y \<union> {z, y}
?b \<in> closure C \<Longrightarrow> open_segment z ?b \<subseteq> rel_interior C
y \<in> convex hull T
z \<in> rel_interior C

goal (1 subgoal):
 1. x \<in> convex hull T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> convex hull T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
S \<inter> convex hull insert z T \<subseteq> S \<inter> convex hull T

goal (1 subgoal):
 1. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T
[PROOF STEP]
by (meson hull_mono inf_mono subset_insertI subset_refl)
[PROOF STATE]
proof (state)
this:
S \<inter> convex hull T \<subseteq> S \<inter> convex hull insert z T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_openin:
  fixes S :: "'a::euclidean_space set"
  assumes ope: "openin (top_of_set T) S" and "subspace T" "S \<noteq> {}"
  shows "dim S = dim T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim S = dim T
[PROOF STEP]
proof (rule order_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dim S \<le> dim T
 2. dim T \<le> dim S
[PROOF STEP]
show "dim S \<le> dim T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim S \<le> dim T
[PROOF STEP]
by (metis ope dim_subset openin_subset topspace_euclidean_subtopology)
[PROOF STATE]
proof (state)
this:
dim S \<le> dim T

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
have "dim T = aff_dim S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (dim T) = aff_dim S
[PROOF STEP]
using aff_dim_openin
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>openin (top_of_set ?T) ?S; affine ?T; ?S \<noteq> {}\<rbrakk> \<Longrightarrow> aff_dim ?S = aff_dim ?T

goal (1 subgoal):
 1. int (dim T) = aff_dim S
[PROOF STEP]
by (metis aff_dim_subspace \<open>subspace T\<close> \<open>S \<noteq> {}\<close> ope subspace_affine)
[PROOF STATE]
proof (state)
this:
int (dim T) = aff_dim S

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (dim T) = aff_dim S

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
have "... \<le> dim S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aff_dim S \<le> int (dim S)
[PROOF STEP]
by (metis aff_dim_subset aff_dim_subspace dim_span span_superset
        subspace_span)
[PROOF STATE]
proof (state)
this:
aff_dim S \<le> int (dim S)

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (dim T) \<le> int (dim S)
[PROOF STEP]
show "dim T \<le> dim S"
[PROOF STATE]
proof (prove)
using this:
int (dim T) \<le> int (dim S)

goal (1 subgoal):
 1. dim T \<le> dim S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim T \<le> dim S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qfree p; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)
[PROOF STEP]
using imp_def
[PROOF STATE]
proof (prove)
using this:
imp ?p ?q \<equiv> if ?p = F \<or> ?q = T \<or> ?p = ?q then T else if ?p = T then ?q else if ?q = F then MIR.not ?p else Imp ?p ?q

goal (1 subgoal):
 1. \<lbrakk>qfree p; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)
[PROOF STEP]
by (cases "p=F \<or> q=T",simp_all add: imp_def)


[STATEMENT]
lemma fst_inv_equalityI:
     assumes surj_h: "surj h"
         and prem:   "!! x y. g (h(x,y)) = x"
     shows "fst (inv h z) = g z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (inv h z) = g z
[PROOF STEP]
by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)


[STATEMENT]
lemma irreducibleE:
  fixes G (structure)
  assumes irr: "irreducible G a"
    and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
irreducible G a
\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
unfolding irreducible_def
[PROOF STATE]
proof (prove)
using this:
a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)
\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast


[STATEMENT]
lemma WhileRule:
 "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<subseteq> i; Valid (i \<inter> b) c (A 0) i; i \<inter> - b \<subseteq> q\<rbrakk> \<Longrightarrow> Valid p (While b c) (Awhile i v A) q
[PROOF STEP]
apply (clarsimp simp:Valid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; Sem (While b c) s s'; s \<in> p\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply(drule While_aux)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p\<rbrakk> \<Longrightarrow> \<forall>sa s'a. Sem c sa s'a \<longrightarrow> sa \<in> ?I9 s s' \<and> sa \<in> b \<longrightarrow> s'a \<in> ?I9 s s'
 2. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p\<rbrakk> \<Longrightarrow> s \<in> ?I9 s s'
 3. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p; s' \<in> ?I9 s s' \<and> s' \<notin> b\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p\<rbrakk> \<Longrightarrow> s \<in> i
 2. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p; s' \<in> i \<and> s' \<notin> b\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>p \<subseteq> i; \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> i \<and> s \<in> b \<longrightarrow> s' \<in> i; i \<inter> - b \<subseteq> q; s \<in> p; s' \<in> i \<and> s' \<notin> b\<rbrakk> \<Longrightarrow> s' \<in> q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma weak_sup_pres:
  "sup_pres X Y f \<Longrightarrow> weak_sup_pres X Y f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_pres X Y f \<Longrightarrow> weak_sup_pres X Y f
[PROOF STEP]
by (simp add: sup_pres_def weak_sup_pres_def)


[STATEMENT]
lemma Sigma_inj_lepoll_mono:
  assumes h: "inj_on h A" "h ` A \<subseteq> C" and "\<And>x. x \<in> A \<Longrightarrow> B x \<lesssim> D (h x)"
  shows "Sigma A B \<lesssim> Sigma C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
have "\<And>x. x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B x) \<and> f ` (B x) \<subseteq> D (h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B x) \<and> f ` B x \<subseteq> D (h x)
[PROOF STEP]
by (meson assms lepoll_def)
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B ?x) \<and> f ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B ?x) \<and> f ` B ?x \<subseteq> D (h ?x)
[PROOF STEP]
obtain f where  "\<And>x. x \<in> A \<Longrightarrow> inj_on (f x) (B x) \<and> f x ` B x \<subseteq> D (h x)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B ?x) \<and> f ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. (\<And>f. (\<And>x. x \<in> A \<Longrightarrow> inj_on (f x) (B x) \<and> f x ` B x \<subseteq> D (h x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> inj_on (f ?x) (B ?x) \<and> f ?x ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
with h
[PROOF STATE]
proof (chain)
picking this:
inj_on h A
h ` A \<subseteq> C
?x \<in> A \<Longrightarrow> inj_on (f ?x) (B ?x) \<and> f ?x ` B ?x \<subseteq> D (h ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on h A
h ` A \<subseteq> C
?x \<in> A \<Longrightarrow> inj_on (f ?x) (B ?x) \<and> f ?x ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
unfolding lepoll_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. h x = h y \<longrightarrow> x = y
h ` A \<subseteq> C
?x \<in> A \<Longrightarrow> (\<forall>x\<in>B ?x. \<forall>y\<in>B ?x. f ?x x = f ?x y \<longrightarrow> x = y) \<and> f ?x ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. \<exists>f. (\<forall>x\<in>Sigma A B. \<forall>y\<in>Sigma A B. f x = f y \<longrightarrow> x = y) \<and> f ` Sigma A B \<subseteq> Sigma C D
[PROOF STEP]
by (rule_tac x="\<lambda>(x,y). (h x, f x y)" in exI) force
[PROOF STATE]
proof (state)
this:
Sigma A B \<lesssim> Sigma C D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_one [simp]:
  "apply 1 = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>$\<rangle>) 1 = id
[PROOF STEP]
by (fact one_perm.rep_eq)


[STATEMENT]
lemma ImplLeadsto_gen: "\<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)
[PROOF STEP]
apply (unfold leadsto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> \<box>(Init F \<longrightarrow> \<diamond>G)
[PROOF STEP]
apply (auto intro!: InitDmd_gen [temp_use]
    elim!: STL4E_gen [temp_use] simp: Init_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fls_subdegree_deriv':
  fixes   f :: "'a::ring_1_no_zero_divisors fls"
  assumes "(of_int (fls_subdegree f) :: 'a) \<noteq> 0"
  shows   "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fls_subdegree (fls_deriv f) = fls_subdegree f - 1
[PROOF STEP]
using   assms nth_fls_subdegree_zero_iff[of f]
[PROOF STATE]
proof (prove)
using this:
of_int (fls_subdegree f) \<noteq> (0::'a)
(f $$ fls_subdegree f = (0::'a)) = (f = 0)

goal (1 subgoal):
 1. fls_subdegree (fls_deriv f) = fls_subdegree f - 1
[PROOF STEP]
by      (auto intro: fls_deriv_subdegree')


[STATEMENT]
lemma has_field_derivative_Im[derivative_intros]:
  "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_field_derivative (Im D)) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_real_derivative Im D) F
[PROOF STEP]
unfolding has_vector_derivative_complex_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. Re (f x)) has_real_derivative Re D) F \<and> ((\<lambda>x. Im (f x)) has_real_derivative Im D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_real_derivative Im D) F
[PROOF STEP]
by safe


[STATEMENT]
lemma fineD[dest]:
  assumes "d fine s"
  shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d fine s

goal (1 subgoal):
 1. \<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x
[PROOF STEP]
unfolding fine_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, k)\<in>s. k \<subseteq> d x

goal (1 subgoal):
 1. \<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x
[PROOF STEP]
by auto


[STATEMENT]
lemma Spy_dont_know_TTPKey_parts [simp]:
     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> certified_mail \<Longrightarrow> Key (privateKey b TTP) \<notin> parts (knows Spy evs)
[PROOF STEP]
by simp


[STATEMENT]
lemma sstart_sets: "sstart S xs \<in> sets (stream_space (count_space UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sstart S xs \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
sstart S xs \<in> sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
note Cons[measurable]
[PROOF STATE]
proof (state)
this:
sstart S xs \<in> sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
have "sstart S (x # xs) =
    {s\<in>space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sstart S (x # xs) = {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}
[PROOF STEP]
by (simp add: set_eq_iff space_stream_space)
[PROOF STATE]
proof (state)
this:
sstart S (x # xs) = {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sstart S (x # xs) = {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
have "\<dots> \<in> sets (stream_space (count_space UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs} \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
{s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs} \<in> sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))

goal (1 subgoal):
 1. sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))

goal (1 subgoal):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
qed (simp add: streams_sets)


[STATEMENT]
lemma less_eq_list_code [code]:
  "x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False"
  "[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True"
  "(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs \<le> []) = False &&& ([] \<le> xs) = True &&& (x # xs \<le> y # ys) = (x < y \<or> x = y \<and> xs \<le> ys)
[PROOF STEP]
by simp_all


[STATEMENT]
theorem sup_PTS_eq:
  "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<turnstile> OK (PrimT p) <=o X = (X = Err \<or> X = OK (PrimT p))
[PROOF STEP]
by (auto simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def
              split: err.splits)


[STATEMENT]
lemma DERIV_LIM_iff:
  fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a"
  shows "((\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0\<rightarrow> D) = ((\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D = (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D \<Longrightarrow> (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
 2. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D

goal (2 subgoals):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D \<Longrightarrow> (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
 2. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
have "(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>0 - - a\<rightarrow> D"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D
[PROOF STEP]
by (rule LIM_offset)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D

goal (2 subgoals):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D \<Longrightarrow> (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
 2. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f (a + (x + - a)) - f a) / (x + - a)) \<midarrow>(0::'a) - - a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D
[PROOF STEP]
have "(\<lambda>x. (f (x+a) - f a) / ((x+a) - a)) \<midarrow>a-a\<rightarrow> D"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D
[PROOF STEP]
by (rule LIM_offset)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>x. (f x - f a) / (x - a)) \<midarrow>a\<rightarrow> D \<Longrightarrow> (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f (x + a) - f a) / (x + a - a)) \<midarrow>a - a\<rightarrow> D

goal (1 subgoal):
 1. (\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
(\<lambda>h. (f (a + h) - f a) / h) \<midarrow>0::'a\<rightarrow> D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_nlists_Suc_iff: "(xs \<in> nlists (Suc n) A) = (\<exists>y\<in>A. \<exists>ys \<in> nlists n A. xs = y#ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> nlists (Suc n) A) = (\<exists>y\<in>A. \<exists>ys\<in>nlists n A. xs = y # ys)
[PROOF STEP]
unfolding nlists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> {xs. length xs = Suc n \<and> set xs \<subseteq> A}) = (\<exists>y\<in>A. \<exists>ys\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. xs = y # ys)
[PROOF STEP]
by (cases "xs") auto


[STATEMENT]
lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\<lambda>x. map_pmf f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf f (M \<bind> g) = M \<bind> (\<lambda>x. map_pmf f (g x))
[PROOF STEP]
by (simp add: map_pmf_def bind_assoc_pmf)


[STATEMENT]
lemma Infinitesimal_HFinite_mult:
  fixes x y :: "'a::real_normed_algebra star"
  assumes "x \<in> Infinitesimal" "y \<in> HFinite"
  shows "x * y \<in> Infinitesimal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in> Infinitesimal
[PROOF STEP]
proof (rule InfinitesimalI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm (x * y) < r
[PROOF STEP]
obtain t where "hnorm y < t" "t \<in> Reals"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>hnorm y < t; t \<in> \<real>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using HFiniteD \<open>y \<in> HFinite\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> HFinite \<Longrightarrow> \<exists>t\<in>\<real>. hnorm ?x < t
y \<in> HFinite

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

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm (x * y) < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hnorm y < t
t \<in> \<real>
[PROOF STEP]
have "t > 0"
[PROOF STATE]
proof (prove)
using this:
hnorm y < t
t \<in> \<real>

goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
using hnorm_ge_zero le_less_trans
[PROOF STATE]
proof (prove)
using this:
hnorm y < t
t \<in> \<real>
0 \<le> hnorm ?x
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < t

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm (x * y) < r
[PROOF STEP]
show "hnorm (x * y) < r"
    if "r \<in> \<real>" and "0 < r" for r :: "real star"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
have "hnorm x < r/t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hnorm x < r / t
[PROOF STEP]
by (meson InfinitesimalD Reals_divide \<open>hnorm y < t\<close> \<open>t \<in> \<real>\<close> assms(1) divide_pos_pos hnorm_ge_zero le_less_trans that)
[PROOF STATE]
proof (state)
this:
hnorm x < r / t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hnorm x < r / t
[PROOF STEP]
have "hnorm (x * y) < (r / t) * t"
[PROOF STATE]
proof (prove)
using this:
hnorm x < r / t

goal (1 subgoal):
 1. hnorm (x * y) < r / t * t
[PROOF STEP]
using \<open>hnorm y < t\<close> hnorm_mult_less
[PROOF STATE]
proof (prove)
using this:
hnorm x < r / t
hnorm y < t
\<lbrakk>hnorm ?x < ?r; hnorm ?y < ?s\<rbrakk> \<Longrightarrow> hnorm (?x * ?y) < ?r * ?s

goal (1 subgoal):
 1. hnorm (x * y) < r / t * t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hnorm (x * y) < r / t * t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hnorm (x * y) < r / t * t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hnorm (x * y) < r / t * t

goal (1 subgoal):
 1. hnorm (x * y) < r
[PROOF STEP]
using \<open>0 < t\<close>
[PROOF STATE]
proof (prove)
using this:
hnorm (x * y) < r / t * t
0 < t

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?r \<in> \<real>; 0 < ?r\<rbrakk> \<Longrightarrow> hnorm (x * y) < ?r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma approx_trans2: "r \<approx> x \<Longrightarrow> s \<approx> x \<Longrightarrow> r \<approx> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<approx> x; s \<approx> x\<rbrakk> \<Longrightarrow> r \<approx> s
[PROOF STEP]
by (blast intro: approx_sym approx_trans)


[STATEMENT]
lemma Infinitesimal_add_right_cancel: "y \<in> Infinitesimal \<Longrightarrow> x \<approx> z + y \<Longrightarrow> x \<approx> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> Infinitesimal; x \<approx> z + y\<rbrakk> \<Longrightarrow> x \<approx> z
[PROOF STEP]
by (metis Infinitesimal_add_approx_self approx_monad_iff)


[STATEMENT]
lemma fps_of_poly_nth [simp]: "fps_of_poly p $ n = coeff p n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fps_of_poly p $ n = coeff p n
[PROOF STEP]
by (simp add: fps_of_poly_def)


[STATEMENT]
lemma summable_diff: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n - g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>summable f; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. f n - g n)
[PROOF STEP]
unfolding summable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ex ((sums) f); Ex ((sums) g)\<rbrakk> \<Longrightarrow> Ex ((sums) (\<lambda>n. f n - g n))
[PROOF STEP]
by (auto intro: sums_diff)


[STATEMENT]
lemma telescope_sums:
  fixes c :: "'a::real_normed_vector"
  assumes "f \<longlonglongrightarrow> c"
  shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (Suc n) - f n) sums (c - f 0)
[PROOF STEP]
unfolding sums_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<Sum>n<n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
proof (subst filterlim_sequentially_Suc [symmetric])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)
[PROOF STEP]
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] sum_Suc_diff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
have "\<dots> \<longlonglongrightarrow> c - f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (Suc n) - f 0) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (Suc n) - f 0) \<longlonglongrightarrow> c - f 0

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) \<longlonglongrightarrow> c - f 0

goal (1 subgoal):
 1. (\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strict_Some [simp]:
  "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (strict f x = OK y) = (\<exists>z. x = OK z \<and> f z = OK y)
[PROOF STEP]
by (cases x, auto)


[STATEMENT]
lemma OK_le_err_OK:
  "(OK x <=_(le r) OK y) = (x <=_r y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (OK x \<sqsubseteq>\<^bsub>le r\<^esub> OK y) = (x \<sqsubseteq>\<^bsub>r\<^esub> y)
[PROOF STEP]
by (simp add: unfold_lesub_err le_def)


[STATEMENT]
lemma Nonce_notin_kparts [simplified]: "Guard n Ks H \<Longrightarrow> Nonce n \<notin> kparts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Guard n Ks H \<Longrightarrow> Nonce n \<notin> kparts H
[PROOF STEP]
by (auto simp: Guard_def dest: in_kparts Nonce_notin_kparts_msg)


[STATEMENT]
lemma digit3_ascii_of_iff [simp]:
  "digit3 (String.ascii_of c) \<longleftrightarrow> digit3 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit3 (ascii_of c) = digit3 c
[PROOF STEP]
by (simp add: String.ascii_of_def)