[STATEMENT]
lemma invc2_joinR:
  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
  invc2 (joinR l x r)
  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invc l; invh l; invc r; invh r; bheight r \<le> bheight l\<rbrakk> \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
proof (induct l x r rule: joinR.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l x r. \<lbrakk>\<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Red; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (joinR x23 x r)); \<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Black; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (joinR x23 x r)); invc l; invh l; invc r; invh r; bheight r \<le> bheight l\<rbrakk> \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
case (1 l x r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Red; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
invc l
invh l
invc r
invh r
bheight r \<le> bheight l

goal (1 subgoal):
 1. \<And>l x r. \<lbrakk>\<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Red; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (joinR x23 x r)); \<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Black; invc x23; invh x23; invc r; invh r; bheight r \<le> bheight x23\<rbrakk> \<Longrightarrow> invc2 (joinR x23 x r) \<and> (bheight x23 \<noteq> bheight r \<and> color x23 = Black \<longrightarrow> invc (joinR x23 x r)); invc l; invh l; invc r; invh r; bheight r \<le> bheight l\<rbrakk> \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Red; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; invc ?x23.0; invh ?x23.0; invc r; invh r; bheight r \<le> bheight ?x23.0\<rbrakk> \<Longrightarrow> invc2 (joinR ?x23.0 x r) \<and> (bheight ?x23.0 \<noteq> bheight r \<and> color ?x23.0 = Black \<longrightarrow> invc (joinR ?x23.0 x r))
invc l
invh l
invc r
invh r
bheight r \<le> bheight l

goal (1 subgoal):
 1. invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))
[PROOF STEP]
by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
[PROOF STATE]
proof (state)
this:
invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc (joinR l x r))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq># M; N < P\<rbrakk> \<Longrightarrow> M - P + N < M
[PROOF STEP]
by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)


[STATEMENT]
lemma component_le_infnorm_cart: "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x $ i\<bar> \<le> infnorm x
[PROOF STEP]
using Basis_le_infnorm[of "axis i 1" x]
[PROOF STATE]
proof (prove)
using this:
axis i 1 \<in> Basis \<Longrightarrow> \<bar>x \<bullet> axis i 1\<bar> \<le> infnorm x

goal (1 subgoal):
 1. \<bar>x $ i\<bar> \<le> infnorm x
[PROOF STEP]
by (simp add: Basis_vec_def axis_eq_axis inner_axis)


[STATEMENT]
lemma success_freezeI [success_intros]:
  "success (freeze a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (freeze a) h
[PROOF STEP]
by (auto intro: success_intros simp add: freeze_def)


[STATEMENT]
lemma nat_of_natural_numeral [simp]:
  "nat_of_natural (numeral k) = numeral k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_of_natural (numeral k) = numeral k
[PROOF STEP]
by transfer rule


[STATEMENT]
lemma eventually_filtercomap_at_topological:
  "eventually P (filtercomap f (at A within B)) \<longleftrightarrow>
     (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (filtercomap f (at A within B)) = (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))
[PROOF STEP]
unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal
          eventually_filtercomap_nhds eventually_principal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<longrightarrow> x \<in> f -` (B - {A}) \<longrightarrow> P x)) = (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))
[PROOF STEP]
by blast


[STATEMENT]
lemma seq_suble:
  assumes sf: "strict_mono (f :: nat \<Rightarrow> nat)"
  shows "n \<le> f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> f n
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> f 0
 2. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. 0 \<le> f 0
 2. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> f 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> f 0

goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n \<le> f n

goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
with sf [unfolded strict_mono_Suc_iff, rule_format, of n]
[PROOF STATE]
proof (chain)
picking this:
f n < f (Suc n)
n \<le> f n
[PROOF STEP]
have "n < f (Suc n)"
[PROOF STATE]
proof (prove)
using this:
f n < f (Suc n)
n \<le> f n

goal (1 subgoal):
 1. n < f (Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
n < f (Suc n)

goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < f (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n < f (Suc n)

goal (1 subgoal):
 1. Suc n \<le> f (Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
Suc n \<le> f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma connected_Ioo[simp]: "connected {a<..<b}"
  for a b :: "'a::linear_continuum_topology"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected {a<..<b}
[PROOF STEP]
unfolding connected_iff_interval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{a<..<b}. \<forall>y\<in>{a<..<b}. \<forall>z\<ge>x. z \<le> y \<longrightarrow> z \<in> {a<..<b}
[PROOF STEP]
by auto


[STATEMENT]
lemma cyclic_on_alldef:
  "cyclic_on f S \<longleftrightarrow> S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cyclic_on f S = (S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s))
[PROOF STEP]
unfolding cyclic_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s\<in>S. S = orbit f s) = (S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s))
[PROOF STEP]
by (auto intro: orbit.step orbit_swap orbit_trans)


[STATEMENT]
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bal t = (\<exists>n. full n t)
[PROOF STEP]
by (auto elim!: bal_imp_full full_imp_bal)


[STATEMENT]
lemma nn_integral_measure_spmf':
  "(\<integral>\<^sup>+ x. f x \<partial>measure_spmf p) = \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>count_space (set_spmf p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf p) f = \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>count_space (set_spmf p)
[PROOF STEP]
by(auto simp add: nn_integral_measure_spmf nn_integral_count_space_indicator in_set_spmf_iff_spmf intro!: nn_integral_cong split: split_indicator)


[STATEMENT]
lemma ord_spmf_map_spmf1: "ord_spmf R (map_spmf f p) = ord_spmf (\<lambda>x. R (f x)) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf R (map_spmf f p) = ord_spmf (\<lambda>x. R (f x)) p
[PROOF STEP]
by(simp add: pmf.rel_map[abs_def] ord_option_map1[abs_def])


[STATEMENT]
lemma gen_binomial_complex':
  fixes x y :: real and a :: complex
  assumes "\<bar>x\<bar> < \<bar>y\<bar>"
  shows   "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums
               of_real (x + y) powr a" (is "?P x y")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
fix x y :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
assume xy: "\<bar>x\<bar> < \<bar>y\<bar>" "y \<ge> 0"
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
hence "y > 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y

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

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note xy = xy this
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y
[PROOF STEP]
have "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n) sums (1 + of_real (x / y)) powr a"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n) sums (1 + complex_of_real (x / y)) powr a
[PROOF STEP]
by (intro gen_binomial_complex) (simp add: norm_divide)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n) sums (1 + complex_of_real (x / y)) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums
               ((1 + of_real (x / y)) powr a * y powr a)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n) sums (1 + complex_of_real (x / y)) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums ((1 + complex_of_real (x / y)) powr a * complex_of_real y powr a)
[PROOF STEP]
by (rule sums_mult2)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums ((1 + complex_of_real (x / y)) powr a * complex_of_real y powr a)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums ((1 + complex_of_real (x / y)) powr a * complex_of_real y powr a)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "(1 + complex_of_real (x / y)) = complex_of_real (1 + x/y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + complex_of_real (x / y) = complex_of_real (1 + x / y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 + complex_of_real (x / y) = complex_of_real (1 + x / y)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + complex_of_real (x / y) = complex_of_real (1 + x / y)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y
[PROOF STEP]
have "\<dots> powr a * of_real y powr a = (\<dots> * y) powr a"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. complex_of_real (1 + x / y) powr a * complex_of_real y powr a = (complex_of_real (1 + x / y) * complex_of_real y) powr a
[PROOF STEP]
by (subst powr_times_real[symmetric]) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
complex_of_real (1 + x / y) powr a * complex_of_real y powr a = (complex_of_real (1 + x / y) * complex_of_real y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real (1 + x / y) powr a * complex_of_real y powr a = (complex_of_real (1 + x / y) * complex_of_real y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y
[PROOF STEP]
have "complex_of_real (1 + x / y) * complex_of_real y = of_real (x + y)"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. complex_of_real (1 + x / y) * complex_of_real y = complex_of_real (x + y)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
complex_of_real (1 + x / y) * complex_of_real y = complex_of_real (x + y)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "?P x y"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums complex_of_real (x + y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
using xy
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (a gchoose n) * complex_of_real (x / y) ^ n * complex_of_real y powr a) sums complex_of_real (x + y) powr a
\<bar>x\<bar> < \<bar>y\<bar>
0 \<le> y
0 < y

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
by (simp add: field_simps powr_diff powr_nat)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<bar>?xa2\<bar> < \<bar>?ya2\<bar>; 0 \<le> ?ya2\<rbrakk> \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real ?xa2 ^ n * complex_of_real ?ya2 powr (a - of_nat n)) sums complex_of_real (?xa2 + ?ya2) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note A = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<bar>?xa2\<bar> < \<bar>?ya2\<bar>; 0 \<le> ?ya2\<rbrakk> \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real ?xa2 ^ n * complex_of_real ?ya2 powr (a - of_nat n)) sums complex_of_real (?xa2 + ?ya2) powr a

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
proof (cases "y < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
assume y: "y < 0"
[PROOF STATE]
proof (state)
this:
y < 0

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
y < 0
[PROOF STEP]
have xy: "x + y < 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
y < 0

goal (1 subgoal):
 1. x + y < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x + y < 0

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> < \<bar>y\<bar>
x + y < 0
[PROOF STEP]
have "\<bar>-x\<bar> < \<bar>-y\<bar>" "-y \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> < \<bar>y\<bar>
x + y < 0

goal (1 subgoal):
 1. \<bar>- x\<bar> < \<bar>- y\<bar> &&& 0 \<le> - y
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<bar>- x\<bar> < \<bar>- y\<bar>
0 \<le> - y

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note A[OF this]
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n)) sums complex_of_real (- x + - y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n)) sums complex_of_real (- x + - y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "complex_of_real (-x + -y) = - complex_of_real (x + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (- x + - y) = - complex_of_real (x + y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
complex_of_real (- x + - y) = - complex_of_real (x + y)

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real (- x + - y) = - complex_of_real (x + y)

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from xy assms
[PROOF STATE]
proof (chain)
picking this:
x + y < 0
\<bar>x\<bar> < \<bar>y\<bar>
[PROOF STEP]
have "... powr a = (-1) powr -a * of_real (x + y) powr a"
[PROOF STATE]
proof (prove)
using this:
x + y < 0
\<bar>x\<bar> < \<bar>y\<bar>

goal (1 subgoal):
 1. (- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a
[PROOF STEP]
by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
(- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(- complex_of_real (x + y)) powr a = (- 1) powr - a * complex_of_real (x + y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y < 0
[PROOF STEP]
have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
                       (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a"
[PROOF STATE]
proof (prove)
using this:
y < 0

goal (1 subgoal):
 1. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (a gchoose n) * (- complex_of_real x / - complex_of_real y) ^ n * (- complex_of_real y) powr a
[PROOF STEP]
by (subst power_divide) (simp add: powr_diff powr_nat)
[PROOF STATE]
proof (state)
this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (a gchoose n) * (- complex_of_real x / - complex_of_real y) ^ n * (- complex_of_real y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (a gchoose n) * (- complex_of_real x / - complex_of_real y) ^ n * (- complex_of_real y) powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y < 0
[PROOF STEP]
have "(- of_real y) powr a = (-1) powr -a * of_real y powr a"
[PROOF STATE]
proof (prove)
using this:
y < 0

goal (1 subgoal):
 1. (- complex_of_real y) powr a = (- 1) powr - a * complex_of_real y powr a
[PROOF STEP]
by (subst powr_neg_real_complex) simp
[PROOF STATE]
proof (state)
this:
(- complex_of_real y) powr a = (- 1) powr - a * complex_of_real y powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- complex_of_real y) powr a = (- 1) powr - a * complex_of_real y powr a

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - complex_of_real x / - complex_of_real y = complex_of_real x / complex_of_real y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- complex_of_real x / - complex_of_real y = complex_of_real x / complex_of_real y

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- complex_of_real x / - complex_of_real y = complex_of_real x / complex_of_real y

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "... ^ n = of_real x ^ n / of_real y ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complex_of_real x / complex_of_real y) ^ n = complex_of_real x ^ n / complex_of_real y ^ n
[PROOF STEP]
by (simp add: power_divide)
[PROOF STATE]
proof (state)
this:
(complex_of_real x / complex_of_real y) ^ n = complex_of_real x ^ n / complex_of_real y ^ n

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(complex_of_real x / complex_of_real y) ^ n = complex_of_real x ^ n / complex_of_real y ^ n

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
                   (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a gchoose n) * (complex_of_real x ^ n / complex_of_real y ^ n) * ((- 1) powr - a * complex_of_real y powr a) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))
[PROOF STEP]
by (simp add: algebra_simps powr_diff powr_nat)
[PROOF STATE]
proof (state)
this:
(a gchoose n) * (complex_of_real x ^ n / complex_of_real y ^ n) * ((- 1) powr - a * complex_of_real y powr a) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))
[PROOF STEP]
have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) =
                      (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))"
[PROOF STATE]
proof (prove)
using this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))

goal (1 subgoal):
 1. (a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(a gchoose n) * complex_of_real (- x) ^ n * complex_of_real (- y) powr (a - of_nat n) = (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(a gchoose ?n2) * complex_of_real (- x) ^ ?n2 * complex_of_real (- y) powr (a - of_nat ?n2) = (- 1) powr - a * ((a gchoose ?n2) * complex_of_real x ^ ?n2 * complex_of_real y powr (a - of_nat ?n2))

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
note sums_cong[OF this]
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose ?n3 n) * complex_of_real (- x) ^ ?n3 n * complex_of_real (- y) powr (a - of_nat (?n3 n))) sums ?c = (\<lambda>n. (- 1) powr - a * ((a gchoose ?n3 n) * complex_of_real x ^ ?n3 n * complex_of_real y powr (a - of_nat (?n3 n)))) sums ?c

goal (2 subgoals):
 1. y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
 2. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))) sums ((- 1) powr - a * complex_of_real (x + y) powr a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (- 1) powr - a * ((a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n))) sums ((- 1) powr - a * complex_of_real (x + y) powr a)

goal (1 subgoal):
 1. (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
by (simp add: sums_mult_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a

goal (1 subgoal):
 1. \<not> y < 0 \<Longrightarrow> (\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a
[PROOF STEP]
qed (insert A[of x y] assms, simp_all add: not_less)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (a gchoose n) * complex_of_real x ^ n * complex_of_real y powr (a - of_nat n)) sums complex_of_real (x + y) powr a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NC2_not_NonceCCA:
     "[|Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace>
          \<in> parts (knows Spy evs);
        Nonce N \<notin> analz (knows Spy evs);
       evs \<in> set_cr|]
      ==> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs); Nonce N \<notin> analz (knows Spy evs); evs \<in> set_cr\<rbrakk> \<Longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Nonce N \<notin> analz (knows Spy evs); evs \<in> set_cr\<rbrakk> \<Longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> set_cr \<Longrightarrow> Nonce N \<notin> analz (knows Spy evs) \<longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)
[PROOF STEP]
apply (erule set_cr.induct, analz_mono_contra, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evsf X. \<lbrakk>evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)); Nonce N \<notin> analz (knows Spy evsf); Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evsf)\<rbrakk> \<Longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (insert X (knows Spy evsf))
 2. \<And>evs3 Ca k NC2 KC1a SKi X NC1 i EKi. \<lbrakk>evs3 \<in> set_cr; Ca = Cardholder k; Nonce NC2 \<notin> used evs3; Key KC1a \<notin> used evs3; KC1a \<in> symKeys; Gets (Cardholder k) \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NC1\<rbrace>, cert (CA i) EKi onlyEnc (priSK RCA), cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs3; Says (Cardholder k) (CA i) \<lbrace>Agent (Cardholder k), Nonce NC1\<rbrace> \<in> set evs3; Nonce N \<notin> analz (knows Spy evs3); Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs3)\<rbrakk> \<Longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> N = NC2 \<longrightarrow> B = Cardholder k \<longrightarrow> KC1 = KC1a \<longrightarrow> p \<noteq> Pan (pan (Cardholder k))
 3. \<And>evs6 NonceCCA KC2 KC3 cardSK i Ca NC3 CardSecret. \<lbrakk>evs6 \<in> set_cr; Nonce NonceCCA \<notin> used evs6; KC2 \<in> symKeys; KC3 \<in> symKeys; cardSK \<notin> symKeys; Notes (CA i) (Key cardSK) \<notin> set evs6; Gets (CA i) \<lbrace>Crypt KC3 \<lbrace>Agent Ca, Nonce NC3, Key KC2, Key cardSK, Crypt (invKey cardSK) (Hash \<lbrace>Agent Ca, Nonce NC3, Key KC2, Key cardSK, Pan (pan Ca), Nonce CardSecret\<rbrace>)\<rbrace>, Crypt (pubEK (CA i)) \<lbrace>Key KC3, Pan (pan Ca), Nonce CardSecret\<rbrace>\<rbrace> \<in> set evs6; Nonce N \<notin> analz (knows Spy evs6); Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs6) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs6)\<rbrakk> \<Longrightarrow> C' = Ca \<and> N' = NC3 \<and> C = CA i \<and> N = NonceCCA \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce NonceCCA\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs6)
[PROOF STEP]
apply (blast dest: Hash_imp_parts2)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma stc_part_Ex:
  assumes "x \<in> HFinite"
  shows "\<exists>t \<in> SComplex. x \<approx> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
let ?t = "HComplex (st (hRe x)) (st (hIm x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
have "?t \<in> SComplex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
[PROOF STEP]
using HFinite_hIm HFinite_hRe Reals_eq_Standard assms st_SReal
[PROOF STATE]
proof (prove)
using this:
?x \<in> HFinite \<Longrightarrow> hIm ?x \<in> HFinite
?x \<in> HFinite \<Longrightarrow> hRe ?x \<in> HFinite
\<real> = Standard
x \<in> HFinite
?x \<in> HFinite \<Longrightarrow> st ?x \<in> \<real>

goal (1 subgoal):
 1. HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
have "x \<approx> ?t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<approx> HComplex (st (hRe x)) (st (hIm x))
[PROOF STEP]
by (simp add: HFinite_hIm HFinite_hRe assms hcomplex_approx_iff st_HFinite st_eq_approx)
[PROOF STATE]
proof (state)
this:
x \<approx> HComplex (st (hRe x)) (st (hIm x))

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
x \<approx> HComplex (st (hRe x)) (st (hIm x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HComplex (st (hRe x)) (st (hIm x)) \<in> SComplex
x \<approx> HComplex (st (hRe x)) (st (hIm x))

goal (1 subgoal):
 1. \<exists>t\<in>SComplex. x \<approx> t
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>SComplex. x \<approx> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group_hom) inj_on_one_iff:
   "inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on h (carrier G) = (\<forall>x. x \<in> carrier G \<longrightarrow> h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)
[PROOF STEP]
using G.solve_equation G.subgroup_self
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup ?H G; ?x \<in> ?H; ?y \<in> ?H\<rbrakk> \<Longrightarrow> \<exists>h\<in>?H. ?y = h \<otimes> ?x
subgroup (carrier G) G

goal (1 subgoal):
 1. inj_on h (carrier G) = (\<forall>x. x \<in> carrier G \<longrightarrow> h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)
[PROOF STEP]
by (force simp: inj_on_def)


[STATEMENT]
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZN ===> ZN ===> ZN) (*) (*)
[PROOF STEP]
unfolding rel_fun_def ZN_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x = int y \<longrightarrow> (\<forall>xa ya. xa = int ya \<longrightarrow> x * xa = int (y * ya))
[PROOF STEP]
by simp


[STATEMENT]
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<le> x
[PROOF STEP]
using while_option_stop[OF assms[simplified pfp_def]]
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> f x \<le> x

goal (1 subgoal):
 1. f x \<le> x
[PROOF STEP]
by simp


[STATEMENT]
lemma append_eq_cong: "\<lbrakk>eq xs ys; eq xs' ys'\<rbrakk> \<Longrightarrow> eq (xs @ xs') (ys @ ys')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivclp cancel1 xs ys; equivclp cancel1 xs' ys'\<rbrakk> \<Longrightarrow> equivclp cancel1 (xs @ xs') (ys @ ys')
[PROOF STEP]
by(induction rule: equivclp_induct)(auto intro: eq_append_same1 equivclp_into_equivclp cancel1_append_same2)


[STATEMENT]
lemma undual_bot_eq [simp]:
  "undual bot = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. undual bot = top
[PROOF STEP]
by (fact bot_dual.rep_eq)


[STATEMENT]
lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. c) has_vector_derivative (0::'a)) net
[PROOF STEP]
by (auto simp: has_vector_derivative_def)


[STATEMENT]
lemma "x - (0::int) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - 0 = x
[PROOF STEP]
nitpick [unary_ints, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - 0 = x
[PROOF STEP]
nitpick [binary_ints, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - 0 = x
[PROOF STEP]
sorry


[STATEMENT]
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keysFor (insert (Key K) H) = keysFor H
[PROOF STEP]
by (unfold keysFor_def, auto)


[STATEMENT]
lemma upper_max_interval[simp]: "upper (max_interval x y) = max (upper x) (upper y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper (max_interval x y) = max (upper x) (upper y)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma "(i + j + -12 + (k::int)) - -15 = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + j + - 12 + k - - 15 = y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 + (i + (j + k)) = y
[PROOF STEP]
oops


[STATEMENT]
lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w < x \<and> y < z \<Longrightarrow> w + y < x + z
[PROOF STEP]
by arith


[STATEMENT]
lemma "(x + -y < z) = (x < z + (y::real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + - y < z) = (x < z + y)
[PROOF STEP]
by arith


[STATEMENT]
lemma "(-x \<le> -y) = (y \<le> (x::real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- x \<le> - y) = (y \<le> x)
[PROOF STEP]
by arith


[STATEMENT]
lemma inv_1 [simp]: "inv \<one> = \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv \<one> = \<one>
[PROOF STEP]
by (rule inverse_unique) simp_all


[STATEMENT]
lemma integral_mult_right_zero[simp]:
  fixes c :: "_::{real_normed_field,second_countable_topology}"
  shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. c * f x = c * integral\<^sup>L M f
[PROOF STEP]
by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp


[STATEMENT]
lemma integrable_mult_indicator:
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> sets M; integrable M f\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. indicat_real A x *\<^sub>R f x)
[PROOF STEP]
by (rule integrable_bound[of M f]) (auto split: split_indicator)


[STATEMENT]
lemma map_upd_eqD1:
  assumes "m(a\<mapsto>x) = n(a\<mapsto>y)"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
m(a \<mapsto> x) = n(a \<mapsto> y)
[PROOF STEP]
have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a"
[PROOF STATE]
proof (prove)
using this:
m(a \<mapsto> x) = n(a \<mapsto> y)

goal (1 subgoal):
 1. (m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a

goal (1 subgoal):
 1. x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(m(a \<mapsto> x)) a = (n(a \<mapsto> y)) a

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_Pinfty:
  fixes f :: "'a \<Rightarrow> ereal"
  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum f P = \<infinity>) = (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sum f P = \<infinity> \<Longrightarrow> finite P
 2. sum f P = \<infinity> \<Longrightarrow> \<exists>i\<in>P. f i = \<infinity>
 3. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
assume *: "sum f P = \<infinity>"
[PROOF STATE]
proof (state)
this:
sum f P = \<infinity>

goal (3 subgoals):
 1. sum f P = \<infinity> \<Longrightarrow> finite P
 2. sum f P = \<infinity> \<Longrightarrow> \<exists>i\<in>P. f i = \<infinity>
 3. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
show "finite P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite P
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite P \<Longrightarrow> False
[PROOF STEP]
assume "\<not> finite P"
[PROOF STATE]
proof (state)
this:
infinite P

goal (1 subgoal):
 1. infinite P \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
sum f P = \<infinity>
infinite P
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sum f P = \<infinity>
infinite P

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

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

goal (2 subgoals):
 1. sum f P = \<infinity> \<Longrightarrow> \<exists>i\<in>P. f i = \<infinity>
 2. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
show "\<exists>i\<in>P. f i = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>P. f i = \<infinity>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<in>P. f i = \<infinity>)

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i\<in>P. f i = \<infinity>)
[PROOF STEP]
have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i\<in>P. f i = \<infinity>)

goal (1 subgoal):
 1. \<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in> P \<Longrightarrow> f ?i \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
with \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
finite P
?i \<in> P \<Longrightarrow> f ?i \<noteq> \<infinity>
[PROOF STEP]
have "sum f P \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
finite P
?i \<in> P \<Longrightarrow> f ?i \<noteq> \<infinity>

goal (1 subgoal):
 1. sum f P \<noteq> \<infinity>
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
sum f P \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>P. f i = \<infinity>) \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
sum f P = \<infinity>
sum f P \<noteq> \<infinity>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sum f P = \<infinity>
sum f P \<noteq> \<infinity>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>P. f i = \<infinity>

goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
assume "finite P" and "i \<in> P" and "f i = \<infinity>"
[PROOF STATE]
proof (state)
this:
finite P
i \<in> P
f i = \<infinity>

goal (1 subgoal):
 1. \<And>i. \<lbrakk>finite P; i \<in> P; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f P = \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite P
i \<in> P
f i = \<infinity>
[PROOF STEP]
show "sum f P = \<infinity>"
[PROOF STATE]
proof (prove)
using this:
finite P
i \<in> P
f i = \<infinity>

goal (1 subgoal):
 1. sum f P = \<infinity>
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<in> {}; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f {} = \<infinity>
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>i \<in> F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f F = \<infinity>; i \<in> insert x F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f (insert x F) = \<infinity>
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
\<lbrakk>i \<in> A; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f A = \<infinity>
i \<in> insert x A
f i = \<infinity>

goal (2 subgoals):
 1. \<lbrakk>i \<in> {}; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f {} = \<infinity>
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>i \<in> F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f F = \<infinity>; i \<in> insert x F; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f (insert x F) = \<infinity>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (insert x A) = \<infinity>
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
\<lbrakk>i \<in> A; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f A = \<infinity>
i \<in> insert x A
f i = \<infinity>

goal (1 subgoal):
 1. sum f (insert x A) = \<infinity>
[PROOF STEP]
by (cases "x = i") auto
[PROOF STATE]
proof (state)
this:
sum f (insert x A) = \<infinity>

goal (1 subgoal):
 1. \<lbrakk>i \<in> {}; f i = \<infinity>\<rbrakk> \<Longrightarrow> sum f {} = \<infinity>
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
sum f P = \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Inf_countable_INF:
  assumes "A \<noteq> {}" shows "\<exists>f::nat \<Rightarrow> ereal. decseq f \<and> range f \<subseteq> A \<and> Inf A = (INF i. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
obtain f where "incseq f" "range f \<subseteq> uminus`A" "Sup (uminus`A) = (SUP i. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>incseq f; range f \<subseteq> uminus ` A; Sup (uminus ` A) = Sup (range f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Sup_countable_SUP[of "uminus ` A"] \<open>A \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
uminus ` A \<noteq> {} \<Longrightarrow> \<exists>f. incseq f \<and> range f \<subseteq> uminus ` A \<and> Sup (uminus ` A) = Sup (range f)
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>incseq f; range f \<subseteq> uminus ` A; Sup (uminus ` A) = Sup (range f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
incseq f
range f \<subseteq> uminus ` A
Sup (uminus ` A) = Sup (range f)

goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
incseq f
range f \<subseteq> uminus ` A
Sup (uminus ` A) = Sup (range f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
incseq f
range f \<subseteq> uminus ` A
Sup (uminus ` A) = Sup (range f)

goal (1 subgoal):
 1. \<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)
[PROOF STEP]
by (intro exI[of _ "\<lambda>x. - f x"])
       (auto simp: ereal_Sup_uminus_image_eq ereal_INF_uminus_eq eq_commute[of "- _"])
[PROOF STATE]
proof (state)
this:
\<exists>f. decseq f \<and> range f \<subseteq> A \<and> Inf A = Inf (range f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_rat_ceiling [simp]:
  "\<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>
[PROOF STEP]
using of_rat_floor [of "- r"]
[PROOF STATE]
proof (prove)
using this:
\<lfloor>of_rat (- r)\<rfloor> = \<lfloor>- r\<rfloor>

goal (1 subgoal):
 1. \<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>
[PROOF STEP]
by (simp add: of_rat_minus ceiling_def)


[STATEMENT]
lemma exp_approx'':
  assumes "n > 0" "0 \<le> x" "x \<le> 1"
  shows   "\<bar>exp (x::real) - (\<Sum>k\<le>n. x^k / fact k)\<bar> \<le> 1 / fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
0 \<le> x
x \<le> 1
[PROOF STEP]
have "\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n"
[PROOF STATE]
proof (prove)
using this:
0 < n
0 \<le> x
x \<le> 1

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n
[PROOF STEP]
by (rule exp_approx')
[PROOF STATE]
proof (state)
this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
0 \<le> x
x \<le> 1
[PROOF STEP]
have "\<dots> \<le> 1 / fact n"
[PROOF STATE]
proof (prove)
using this:
0 < n
0 \<le> x
x \<le> 1

goal (1 subgoal):
 1. x ^ n / fact n \<le> 1 / fact n
[PROOF STEP]
by (simp add: field_split_simps power_le_one)
[PROOF STATE]
proof (state)
this:
x ^ n / fact n \<le> 1 / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eventually_at_Pair_within_TimesI2:
  fixes x::"'a::metric_space"
  assumes "\<forall>\<^sub>F y' in at y within Y. P y'" "P y"
  shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
from assms[unfolded eventually_at_topological]
[PROOF STATE]
proof (chain)
picking this:
\<exists>S. open S \<and> y \<in> S \<and> (\<forall>x\<in>S. x \<noteq> y \<longrightarrow> x \<in> Y \<longrightarrow> P x)
P y
[PROOF STEP]
obtain S where S: "open S" "y \<in> S" "\<And>y'. y' \<in> Y \<Longrightarrow> y' \<in> S \<Longrightarrow> P y'"
[PROOF STATE]
proof (prove)
using this:
\<exists>S. open S \<and> y \<in> S \<and> (\<forall>x\<in>S. x \<noteq> y \<longrightarrow> x \<in> Y \<longrightarrow> P x)
P y

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>open S; y \<in> S; \<And>y'. \<lbrakk>y' \<in> Y; y' \<in> S\<rbrakk> \<Longrightarrow> P y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
open S
y \<in> S
\<lbrakk>?y' \<in> Y; ?y' \<in> S\<rbrakk> \<Longrightarrow> P ?y'

goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
show "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'
[PROOF STEP]
unfolding eventually_at_topological
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S. open S \<and> (x, y) \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> (x, y) \<longrightarrow> xa \<in> X \<times> Y \<longrightarrow> (case xa of (x', x) \<Rightarrow> P x))
[PROOF STEP]
by (auto intro!: exI[where x="UNIV \<times> S"] S open_Times)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permutations_of_list_impl_aux_correct':
  "permutations_of_list_impl_aux acc xs =
     map (\<lambda>xs. rev xs @ acc) (permutations_of_list_impl xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutations_of_list_impl_aux acc xs = map (\<lambda>xs. rev xs @ acc) (permutations_of_list_impl xs)
[PROOF STEP]
by (induction acc xs rule: permutations_of_list_impl_aux.induct,
      subst permutations_of_list_impl_aux.simps, subst permutations_of_list_impl.simps)
     (auto simp: map_list_bind intro!: list_bind_cong)


[STATEMENT]
lemma (in ring) genideal_minimal:
  assumes "ideal I R" "S \<subseteq> I"
  shows "Idl S \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idl S \<subseteq> I
[PROOF STEP]
unfolding genideal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter> {I. ideal I R \<and> S \<subseteq> I} \<subseteq> I
[PROOF STEP]
by rule (elim InterD, simp add: assms)


[STATEMENT]
lemma one_smallo_powr: "e > (0::real) \<Longrightarrow> (\<lambda>_. 1) \<in> o(\<lambda>x. x powr e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e \<Longrightarrow> (\<lambda>_. 1) \<in> o(\<lambda>x. x powr e)
[PROOF STEP]
by (auto simp: smallomega_iff_smallo [symmetric] real_powr_at_top
                 smallomegaI_filterlim_at_top_norm)


[STATEMENT]
lemma not_trimmed_pos_MSLNil [simp]: "\<not>trimmed_pos (MS MSLNil f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> trimmed_pos (MS MSLNil f)
[PROOF STEP]
by (simp add: trimmed_pos_ms_iff)


[STATEMENT]
lemma eventually_int_real_at_top:
  assumes "eventually P (at_top :: real filter)"
  shows   "eventually (\<lambda>x. P (of_int x)) (at_top :: int filter)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (real_of_int x)
[PROOF STEP]
using assms filterlim_of_int_at_top filterlim_iff filterlim_real_of_int_at_top
[PROOF STATE]
proof (prove)
using this:
eventually P at_top
filterlim ?f ?F at_top \<Longrightarrow> LIM x at_top. ?f (real_of_int x) :> ?F
filterlim ?f ?F2.0 ?F1.0 = (\<forall>P. eventually P ?F2.0 \<longrightarrow> (\<forall>\<^sub>F x in ?F1.0. P (?f x)))
filterlim real_of_int at_top at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (real_of_int x)
[PROOF STEP]
by blast


[STATEMENT]
lemma (in topological_space) at_within_union:
  "at x within (S \<union> T) = sup (at x within S) (at x within T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. at x within S \<union> T = sup (at x within S) (at x within T)
[PROOF STEP]
unfolding filter_eq_iff eventually_sup eventually_at_filter
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. (\<forall>\<^sub>F xa in nhds x. xa \<noteq> x \<longrightarrow> xa \<in> S \<union> T \<longrightarrow> P xa) = ((\<forall>\<^sub>F xa in nhds x. xa \<noteq> x \<longrightarrow> xa \<in> S \<longrightarrow> P xa) \<and> (\<forall>\<^sub>F xa in nhds x. xa \<noteq> x \<longrightarrow> xa \<in> T \<longrightarrow> P xa))
[PROOF STEP]
by (auto elim!: eventually_rev_mp)


[STATEMENT]
lemma nhds_prod: "nhds (a, b) = nhds a \<times>\<^sub>F nhds b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nhds (a, b) = nhds a \<times>\<^sub>F nhds b
[PROOF STEP]
unfolding nhds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf (principal ` {S. open S \<and> (a, b) \<in> S}) = Inf (principal ` {S. open S \<and> a \<in> S}) \<times>\<^sub>F Inf (principal ` {S. open S \<and> b \<in> S})
[PROOF STEP]
proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>open x; a \<in> x; open xa; b \<in> xa\<rbrakk> \<Longrightarrow> Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (x \<times> xa)
 2. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
fix S T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>open x; a \<in> x; open xa; b \<in> xa\<rbrakk> \<Longrightarrow> Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (x \<times> xa)
 2. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
assume "open S" "a \<in> S" "open T" "b \<in> T"
[PROOF STATE]
proof (state)
this:
open S
a \<in> S
open T
b \<in> T

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>open x; a \<in> x; open xa; b \<in> xa\<rbrakk> \<Longrightarrow> Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (x \<times> xa)
 2. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open S
a \<in> S
open T
b \<in> T
[PROOF STEP]
show "(INF x \<in> {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
[PROOF STATE]
proof (prove)
using this:
open S
a \<in> S
open T
b \<in> T

goal (1 subgoal):
 1. Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (S \<times> T)
[PROOF STEP]
by (intro INF_lower) (auto intro!: open_Times)
[PROOF STATE]
proof (state)
this:
Inf (principal ` {S. open S \<and> (a, b) \<in> S}) \<le> principal (S \<times> T)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
fix S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
assume "open S'" "(a, b) \<in> S'"
[PROOF STATE]
proof (state)
this:
open S'
(a, b) \<in> S'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open S'
(a, b) \<in> S'
[PROOF STEP]
obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
[PROOF STATE]
proof (prove)
using this:
open S'
(a, b) \<in> S'

goal (1 subgoal):
 1. (\<And>S T. \<lbrakk>open S; a \<in> S; open T; b \<in> T; S \<times> T \<subseteq> S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: open_prod_elim)
[PROOF STATE]
proof (state)
this:
open S
a \<in> S
open T
b \<in> T
S \<times> T \<subseteq> S'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>open x; (a, b) \<in> x\<rbrakk> \<Longrightarrow> (INF x\<in>{S. open S \<and> a \<in> S}. INF xa\<in>{S. open S \<and> b \<in> S}. principal (x \<times> xa)) \<le> principal x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open S
a \<in> S
open T
b \<in> T
S \<times> T \<subseteq> S'
[PROOF STEP]
show "(INF x \<in> {S. open S \<and> a \<in> S}. INF y \<in> {S. open S \<and> b \<in> S}.
      principal (x \<times> y)) \<le> principal S'"
[PROOF STATE]
proof (prove)
using this:
open S
a \<in> S
open T
b \<in> T
S \<times> T \<subseteq> S'

goal (1 subgoal):
 1. (INF x\<in>{S. open S \<and> a \<in> S}. INF y\<in>{S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'
[PROOF STEP]
by (auto intro!: INF_lower2)
[PROOF STATE]
proof (state)
this:
(INF x\<in>{S. open S \<and> a \<in> S}. INF y\<in>{S. open S \<and> b \<in> S}. principal (x \<times> y)) \<le> principal S'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closedin_standard_simplex:
   "closedin (powertop_real UNIV) (standard_simplex p)"
    (is "closedin ?X ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
have eq: "standard_simplex p =
              (\<Inter>i. {x. x \<in> topspace ?X \<and> x i \<in> {0..1}}) \<inter>
              (\<Inter>i \<in> {p<..}. {x \<in> topspace ?X. x i \<in> {0}}) \<inter>
              {x \<in> topspace ?X. (\<Sum>i\<le>p. x i) \<in> {1}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. standard_simplex p = (\<Inter>i. {x \<in> topspace (powertop_real UNIV). x i \<in> {0..1}}) \<inter> (\<Inter>i\<in>{p<..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}) \<inter> {x \<in> topspace (powertop_real UNIV). sum x {..p} \<in> {1}}
[PROOF STEP]
by (auto simp: standard_simplex_def topspace_product_topology)
[PROOF STATE]
proof (state)
this:
standard_simplex p = (\<Inter>i. {x \<in> topspace (powertop_real UNIV). x i \<in> {0..1}}) \<inter> (\<Inter>i\<in>{p<..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}) \<inter> {x \<in> topspace (powertop_real UNIV). sum x {..p} \<in> {1}}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (standard_simplex p)
[PROOF STEP]
unfolding eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) ((\<Inter>i. {x \<in> topspace (powertop_real UNIV). x i \<in> {0..1}}) \<inter> (\<Inter>i\<in>{p<..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}) \<inter> {x \<in> topspace (powertop_real UNIV). sum x {..p} \<in> {1}})
[PROOF STEP]
by (rule closedin_Int closedin_Inter continuous_map_sum
             continuous_map_product_projection closedin_continuous_map_preimage | force | clarify)+
[PROOF STATE]
proof (state)
this:
closedin (powertop_real UNIV) (standard_simplex p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hypnat_diff_is_0_eq [simp]: "\<And>m n::hypnat. m - n = 0 \<longleftrightarrow> m \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. (m - n = 0) = (m \<le> n)
[PROOF STEP]
by transfer (rule diff_is_0_eq)


[STATEMENT]
lemma digit_7_code [code]:
  \<open>digit7 c \<longleftrightarrow> bit (integer_of_char c) 7\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit7 c = bit (integer_of_char c) 7
[PROOF STEP]
by (cases c) (simp add: integer_of_char_def)


[STATEMENT]
lemma asciis_of_zero [simp, code]:
  "asciis_of_literal 0 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asciis_of_literal STR '''' = []
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * (2 * x + y + 0 + 1) \<noteq> 0
[PROOF STEP]
apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inum (Mul 1 (Add (Add (Add (Mul 2 (Var (Suc (Suc (Suc 0))))) (Var (Suc (Suc 0)))) (Var (Suc 0))) (Var 0))) [1, 0, y, x] \<noteq> 0
[PROOF STEP]
oops


[STATEMENT]
lemma get_set[simp]: "bind get set = return ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get \<bind> local.set = return ()
[PROOF STEP]
unfolding bind_def get_def set_def return_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>s. case run_state (State (\<lambda>s. (s, s))) s of (a, x) \<Rightarrow> run_state (State (\<lambda>_. ((), a))) x) = State (Pair ())
[PROOF STEP]
by simp


[STATEMENT]
lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fps f (0::'a) = fps_nth f 0
[PROOF STEP]
by (simp add: eval_fps_def)


[STATEMENT]
lemma transitions_cons_eq:
  "root \<Midarrow>(x # xs)\<Rightarrow> root'' \<longleftrightarrow> (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root'' \<Longrightarrow> \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
 2. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
assume "root \<Midarrow>(x # xs)\<Rightarrow> root''"
[PROOF STATE]
proof (state)
this:
root \<Midarrow>(x # xs)\<Rightarrow> root''

goal (2 subgoals):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root'' \<Longrightarrow> \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
 2. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''"
[PROOF STATE]
proof (prove)
using this:
root \<Midarrow>(x # xs)\<Rightarrow> root''

goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''

goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''"
[PROOF STATE]
proof (state)
this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''

goal (1 subgoal):
 1. \<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''
[PROOF STEP]
show "root \<Midarrow>(x # xs)\<Rightarrow> root''"
[PROOF STATE]
proof (prove)
using this:
\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' \<Midarrow>xs\<Rightarrow> root''

goal (1 subgoal):
 1. root \<Midarrow>(x # xs)\<Rightarrow> root''
[PROOF STEP]
by (blast intro: transitions.cons)
[PROOF STATE]
proof (state)
this:
root \<Midarrow>(x # xs)\<Rightarrow> root''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CA_image_eq [simp]: "(CA x \<in> CA`A) = (x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (CA x \<in> CA ` A) = (x \<in> A)
[PROOF STEP]
by auto


[STATEMENT]
theorem prime_card_elements_with_ord_eq_totient:
  assumes "prime n"
  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
proof (cases "d dvd totient n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
 2. \<not> d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> d dvd totient n

goal (2 subgoals):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
 2. \<not> d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> d dvd totient n

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
using order_divides_totient[of n] assms
[PROOF STATE]
proof (prove)
using this:
\<not> d dvd totient n
coprime n ?a \<Longrightarrow> ord n ?a dvd totient n
prime n

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
[PROOF STATE]
proof (state)
this:
\<psi> d = (if d dvd n - 1 then totient d else 0)

goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
d dvd totient n

goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
have "\<psi> d = totient d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> d = totient d
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
assume neq: "\<psi> d \<noteq> totient d"
[PROOF STATE]
proof (state)
this:
\<psi> d \<noteq> totient d

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> d \<le> totient d
[PROOF STEP]
using prime_card_elements_with_ord[of d] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<psi> d \<noteq> 0; prime n\<rbrakk> \<Longrightarrow> \<psi> d = totient d
prime n

goal (1 subgoal):
 1. \<psi> d \<le> totient d
[PROOF STEP]
by (cases "\<psi> d = 0") auto
[PROOF STATE]
proof (state)
this:
?d dvd totient n \<Longrightarrow> \<psi> ?d \<le> totient ?d

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
from neq and le[of d] and True
[PROOF STATE]
proof (chain)
picking this:
\<psi> d \<noteq> totient d
d dvd totient n \<Longrightarrow> \<psi> d \<le> totient d
d dvd totient n
[PROOF STEP]
have less: "\<psi> d < totient d"
[PROOF STATE]
proof (prove)
using this:
\<psi> d \<noteq> totient d
d dvd totient n \<Longrightarrow> \<psi> d \<le> totient d
d dvd totient n

goal (1 subgoal):
 1. \<psi> d < totient d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<psi> d < totient d

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. totient n = (\<Sum>d | d dvd totient n. \<psi> d)
[PROOF STEP]
using prime_sum_card_elements_with_ord_eq_totient
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd totient n. \<psi> d) = totient n

goal (1 subgoal):
 1. totient n = (\<Sum>d | d dvd totient n. \<psi> d)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
totient n = (\<Sum>d | d dvd totient n. \<psi> d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
totient n = (\<Sum>d | d dvd totient n. \<psi> d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd totient n. \<psi> d) < (\<Sum>d | d dvd totient n. totient d)
[PROOF STEP]
by (rule sum_strict_mono_ex1)
         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd totient n. \<psi> d) < (\<Sum>d | d dvd totient n. totient d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd totient n. \<psi> d) < (\<Sum>d | d dvd totient n. totient d)

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = totient n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd totient n. totient d) = totient n
[PROOF STEP]
using totient_divisor_sum
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd ?n. totient d) = ?n

goal (1 subgoal):
 1. (\<Sum>d | d dvd totient n. totient d) = totient n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd totient n. totient d) = totient n

goal (1 subgoal):
 1. \<psi> d \<noteq> totient d \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
totient n < totient n
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
totient n < totient n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<psi> d = totient d

goal (1 subgoal):
 1. d dvd totient n \<Longrightarrow> \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
d dvd totient n
\<psi> d = totient d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d dvd totient n
\<psi> d = totient d

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d dvd totient n
\<psi> d = totient d
prime n

goal (1 subgoal):
 1. \<psi> d = (if d dvd n - 1 then totient d else 0)
[PROOF STEP]
by (simp add: totient_prime)
[PROOF STATE]
proof (state)
this:
\<psi> d = (if d dvd n - 1 then totient d else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Carmichael_eq_totient_imp_primroot:
  assumes "n > 0" and "Carmichael n = totient n"
  shows   "\<exists>g. residue_primroot n g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
from \<open>n > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> totatives n; ord n g = Carmichael n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Carmichael_root_exists[of n]
[PROOF STATE]
proof (prove)
using this:
0 < n
\<lbrakk>0 < n; \<And>g. \<lbrakk>g \<in> totatives n; ord n g = Carmichael n\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> totatives n; ord n g = Carmichael n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
g \<in> totatives n
ord n g = Carmichael n

goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
Carmichael n = totient n
g \<in> totatives n
ord n g = Carmichael n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < n
Carmichael n = totient n
g \<in> totatives n
ord n g = Carmichael n

goal (1 subgoal):
 1. \<exists>g. residue_primroot n g
[PROOF STEP]
by (auto simp: residue_primroot_def totatives_def coprime_commute)
[PROOF STATE]
proof (state)
this:
\<exists>g. residue_primroot n g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t k = Some x; C k x\<rbrakk> \<Longrightarrow> filter_tab C t k = Some x
[PROOF STEP]
by (simp add: filter_tab_def)


[STATEMENT]
lemma ignore_Inl_Inter:
  "\<lbrakk> S \<noteq> {}; \<Inter>S \<noteq> {} \<rbrakk> \<Longrightarrow> (\<Inter>A\<in>S. {(x, y). ignore_Inl x y} `` {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A}) \<subseteq> {(x, y). ignore_Inl x y} `` (\<Inter>A\<in>S. {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<noteq> {}; \<Inter> S \<noteq> {}\<rbrakk> \<Longrightarrow> (\<Inter>A\<in>S. {(x, y). ignore_Inl x y} `` {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A}) \<subseteq> {(x, y). ignore_Inl x y} `` (\<Inter>A\<in>S. {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A})
[PROOF STEP]
apply(clarsimp; safe; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; xa \<in> S; \<forall>x\<in>S. xb \<in> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for x A x'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule bspec[where x="Inl x'"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a\<rbrakk> \<Longrightarrow> Inl x' \<in> (\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x})
 2. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a; \<not> ignore_Inl (Inl x') x\<rbrakk> \<Longrightarrow> False
 3. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a; \<not> ignore_Inl (Inl x') x\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; \<forall>x\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. x \<noteq> Inr b; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule bspec[where x="Inr _"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> Inr (?uu12 b) \<in> (\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x})
 2. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b; Inr (?uu12 b) \<noteq> Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b; Inr b \<noteq> Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma floor_le_one [simp]: "\<lfloor>x\<rfloor> \<le> 1 \<longleftrightarrow> x < 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lfloor>x\<rfloor> \<le> 1) = (x < (2::'a))
[PROOF STEP]
by (simp add: floor_le_iff)


[STATEMENT]
lemma pos_minus_divideR_le_eq [field_simps]:
  "- (b /\<^sub>R c) \<le> a \<longleftrightarrow> - b \<le> c *\<^sub>R a" if "c > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (b /\<^sub>R c) \<le> a) = (- b \<le> c *\<^sub>R a)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (- (b /\<^sub>R c) \<le> a) = (- b \<le> c *\<^sub>R a)
[PROOF STEP]
by (metis pos_divideR_le_eq pos_le_minus_divideR_eq that
    inverse_positive_iff_positive le_imp_neg_le minus_minus)


[STATEMENT]
lemma all_LeadsTo_UN_UN:
     "\<forall>i. F \<in> (A i) LeadsTo (A' i)
      ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. F \<in> A i \<longmapsto>w A' i \<Longrightarrow> F \<in> \<Union> (range A) \<longmapsto>w \<Union> (range A')
[PROOF STEP]
by (blast intro: LeadsTo_UN_UN)


[STATEMENT]
lemma Basis_S_transfer[transfer_rule]: "rel_set cr_S Basis Basis_S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set cr_S Basis Basis_S
[PROOF STEP]
using Abs_inverse rep_inverse basis_subset
[PROOF STATE]
proof (prove)
using this:
?y \<in> S \<Longrightarrow> rep (Abs ?y) = ?y
Abs (rep ?x) = ?x
Basis \<subseteq> S

goal (1 subgoal):
 1. rel_set cr_S Basis Basis_S
[PROOF STEP]
by (force simp: rel_set_def Basis_S_def cr_S_def)


[STATEMENT]
lemma Some_in_opt [iff]:
  "(Some x \<in> opt A) = (x\<in>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some x \<in> opt A) = (x \<in> A)
[PROOF STEP]
apply (unfold opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Some x \<in> insert None {x. \<exists>y\<in>A. x = Some y}) = (x \<in> A)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma connected_disjoint_Union_open_subset:
  assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
      and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
      and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
      and eq [simp]: "\<Union>A = \<Union>B"
    shows "A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
assume "S \<in> A"
[PROOF STATE]
proof (state)
this:
S \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
obtain T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>T \<in> B; S \<subseteq> T; S \<inter> \<Union> (B - {T}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using SA SB \<open>S \<in> A\<close> connected_disjoint_Union_open_pick [OF B, of A] eq order_refl
[PROOF STATE]
proof (prove)
using this:
?S \<in> A \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
?S \<in> B \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
S \<in> A
\<lbrakk>\<And>S. S \<in> A \<Longrightarrow> connected S \<and> S \<noteq> {}; \<And>S. S \<in> B \<Longrightarrow> open S; \<Union> A \<subseteq> \<Union> B; ?S \<in> A; \<And>T. \<lbrakk>T \<in> B; ?S \<subseteq> T; ?S \<inter> \<Union> (B - {T}) = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<Union> A = \<Union> B
?x \<le> ?x

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>T \<in> B; S \<subseteq> T; S \<inter> \<Union> (B - {T}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
obtain S' where "S' \<in> A" "T \<subseteq> S'" "T \<inter> \<Union>(A - {S'}) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<in> A; T \<subseteq> S'; T \<inter> \<Union> (A - {S'}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using SA SB \<open>T \<in> B\<close> connected_disjoint_Union_open_pick [OF A, of B] eq order_refl
[PROOF STATE]
proof (prove)
using this:
?S \<in> A \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
?S \<in> B \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
T \<in> B
\<lbrakk>\<And>S. S \<in> B \<Longrightarrow> connected S \<and> S \<noteq> {}; \<And>S. S \<in> A \<Longrightarrow> open S; \<Union> B \<subseteq> \<Union> A; ?S \<in> B; \<And>T. \<lbrakk>T \<in> A; ?S \<subseteq> T; ?S \<inter> \<Union> (A - {T}) = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<Union> A = \<Union> B
?x \<le> ?x

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<in> A; T \<subseteq> S'; T \<inter> \<Union> (A - {S'}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> A
T \<subseteq> S'
T \<inter> \<Union> (A - {S'}) = {}

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}
S' \<in> A
T \<subseteq> S'
T \<inter> \<Union> (A - {S'}) = {}
[PROOF STEP]
have "S' = S"
[PROOF STATE]
proof (prove)
using this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}
S' \<in> A
T \<subseteq> S'
T \<inter> \<Union> (A - {S'}) = {}

goal (1 subgoal):
 1. S' = S
[PROOF STEP]
by (metis A Int_subset_iff SA \<open>S \<in> A\<close> disjnt_def inf.orderE pairwise_def)
[PROOF STATE]
proof (state)
this:
S' = S

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
with \<open>T \<subseteq> S'\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<subseteq> S'
S' = S
[PROOF STEP]
have "T \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> S'
S' = S

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

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
with \<open>S \<subseteq> T\<close>
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> T
T \<subseteq> S
[PROOF STEP]
have "S = T"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> T
T \<subseteq> S

goal (1 subgoal):
 1. S = T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S = T

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
with \<open>T \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<in> B
S = T
[PROOF STEP]
show "S \<in> B"
[PROOF STATE]
proof (prove)
using this:
T \<in> B
S = T

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  nmi_P[no_atp]: "\<forall>x. ~P \<and> P \<longrightarrow>  (\<exists>u\<in> U. u \<le> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<not> P \<and> P \<longrightarrow> (\<exists>u\<in>U. u \<le> x)
[PROOF STEP]
by auto