[STATEMENT]
lemma sums_Suc:
  assumes "(\<lambda>n. f (Suc n)) sums l"
  shows "f sums (l + f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f sums (l + f 0)
[PROOF STEP]
proof  -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f sums (l + f 0)
[PROOF STEP]
have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f (Suc n)) sums l

goal (1 subgoal):
 1. (\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0
[PROOF STEP]
by (auto intro!: tendsto_add simp: sums_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0

goal (1 subgoal):
 1. f sums (l + f 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0

goal (1 subgoal):
 1. f sums (l + f 0)
[PROOF STEP]
have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. f (Suc i)) + f 0 = sum f {..<Suc n}
[PROOF STEP]
unfolding lessThan_Suc_eq_insert_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. f (Suc i)) + f 0 = sum f (insert 0 (Suc ` {..<n}))
[PROOF STEP]
by (simp add: ac_simps sum.atLeast1_atMost_eq image_Suc_lessThan)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<?n. f (Suc i)) + f 0 = sum f {..<Suc ?n}

goal (1 subgoal):
 1. f sums (l + f 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0
(\<Sum>i<?n. f (Suc i)) + f 0 = sum f {..<Suc ?n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0
(\<Sum>i<?n. f (Suc i)) + f 0 = sum f {..<Suc ?n}

goal (1 subgoal):
 1. f sums (l + f 0)
[PROOF STEP]
by (auto simp: sums_def simp del: sum.lessThan_Suc intro: filterlim_sequentially_Suc[THEN iffD1])
[PROOF STATE]
proof (state)
this:
f sums (l + f 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem S\<^sub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> S\<^sub>4p w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> S\<^sub>4p w
[PROOF STEP]
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> S\<^sub>4p w
[PROOF STEP]
oops


[STATEMENT]
lemma (in comm_ring_1) lemma_poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
proof (induct t arbitrary: h)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>h. \<exists>q r. [h] = [r] +++ [- a, 1::'a] *** q
 2. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>h. \<exists>q r. [h] = [r] +++ [- a, 1::'a] *** q
 2. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
have "[h] = [h] +++ [- a, 1] *** []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [h] = [h] +++ [- a, 1::'a] *** []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[h] = [h] +++ [- a, 1::'a] *** []

goal (2 subgoals):
 1. \<And>h. \<exists>q r. [h] = [r] +++ [- a, 1::'a] *** q
 2. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[h] = [h] +++ [- a, 1::'a] *** []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[h] = [h] +++ [- a, 1::'a] *** []

goal (1 subgoal):
 1. \<exists>q r. [h] = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q r. [h] = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
case (Cons  x xs)
[PROOF STATE]
proof (state)
this:
\<exists>q r. ?h1 # xs = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
have "\<exists>q r. h # x # xs = [r] +++ [-a, 1] *** q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<exists>q r. ?h1 # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
obtain q r where qr: "x # xs = [r] +++ [- a, 1] *** q"
[PROOF STATE]
proof (prove)
using this:
\<exists>q r. ?h1 # xs = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. (\<And>r q. x # xs = [r] +++ [- a, 1::'a] *** q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x # xs = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. \<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
have "h # x # xs = [a * r + h] +++ [-a, 1] *** (r # q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h # x # xs = [a * r + h] +++ [- a, 1::'a] *** (r # q)
[PROOF STEP]
using qr
[PROOF STATE]
proof (prove)
using this:
x # xs = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. h # x # xs = [a * r + h] +++ [- a, 1::'a] *** (r # q)
[PROOF STEP]
by (cases q) (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
h # x # xs = [a * r + h] +++ [- a, 1::'a] *** (r # q)

goal (1 subgoal):
 1. \<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h # x # xs = [a * r + h] +++ [- a, 1::'a] *** (r # q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h # x # xs = [a * r + h] +++ [- a, 1::'a] *** (r # q)

goal (1 subgoal):
 1. \<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. \<And>aa t h. (\<And>h. \<exists>q r. h # t = [r] +++ [- a, 1::'a] *** q) \<Longrightarrow> \<exists>q r. h # aa # t = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q

goal (1 subgoal):
 1. \<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q r. h # x # xs = [r] +++ [- a, 1::'a] *** q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) ord_mul_divides:
  assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
  shows "ord (x \<otimes> y) dvd (ord x * ord y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord (x \<otimes> y) dvd ord x * ord y
[PROOF STEP]
apply (simp add: xy flip: pow_eq_id eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<otimes> y) [^] (ord x * ord y) = \<one>
[PROOF STEP]
by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy)


[STATEMENT]
lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n choose k = 0) = (n < k)
[PROOF STEP]
by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)


[STATEMENT]
lemma gbinomial_mult_1':
  "(a gchoose k) * a = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose (Suc k))"
  for a :: "'a::field_char_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a gchoose k) * a = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose Suc k)
[PROOF STEP]
by (simp add: mult.commute gbinomial_mult_1)


[STATEMENT]
lemma finite_extensionalD_funcset[simp, intro]:
  assumes "finite A" "finite B"
  shows "finite (extensionalD d A \<inter> (A \<rightarrow> B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (extensionalD d A \<inter> (A \<rightarrow> B))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. finite (extensionalD d A \<inter> (A \<rightarrow> B))
[PROOF STEP]
by induct auto


[STATEMENT]
lemma set_like_Elem: "set_like is_Elem_of"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_like is_Elem_of
[PROOF STEP]
by (auto simp add: set_like_def image_def Ext_Elem)


[STATEMENT]
lemma above_Field: "above r a \<le> Field r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. above r a \<subseteq> Field r
[PROOF STEP]
by(unfold above_def Field_def, auto)


[STATEMENT]
lemma underS_UnderS_singl: "underS r a = UnderS r {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. underS r a = UnderS r {a}
[PROOF STEP]
by(unfold UnderS_def underS_def, auto simp add: Field_def)


[STATEMENT]
lemma integer_of_int_eq_of_int [simp, code_abbrev]:
  "integer_of_int = of_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integer_of_int = of_int
[PROOF STEP]
by transfer (simp add: fun_eq_iff)


[STATEMENT]
lemma "(\<lambda>x::real. x^2) \<in> o[at_right 0](\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power2 \<in> o[at_right 0](\<lambda>x. x)
[PROOF STEP]
by real_asymp


[STATEMENT]
lemma LIMSEQ_Suc: "f \<longlonglongrightarrow> l \<Longrightarrow> (\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<longlonglongrightarrow> l \<Longrightarrow> (\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l
[PROOF STEP]
by (drule LIMSEQ_ignore_initial_segment [where k="Suc 0"]) simp


[STATEMENT]
lemma continuous_on_sing [simp]: "continuous_on {x} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {x} f
[PROOF STEP]
by (simp add: continuous_on_def at_within_def)


[STATEMENT]
lemma K3_msg_in_parts_spies:
     "Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>)
               \<in> set evs \<Longrightarrow> authTicket \<in> parts (spies evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs \<Longrightarrow> authTicket \<in> parts (knows Spy evs)
[PROOF STEP]
by blast


[STATEMENT]
lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPMF.lub_spmf {} = return_pmf None
[PROOF STEP]
by(simp add: SPMF.lub_spmf_def bot_ereal_def)


[STATEMENT]
lemma set_scale_spmf: "set_spmf (scale_spmf r p) = (if r > 0 then set_spmf p else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (scale_spmf r p) = (if 0 < r then set_spmf p else {})
[PROOF STEP]
apply(auto simp add: in_set_spmf_iff_spmf spmf_scale_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0 < r; spmf p x \<noteq> 0; min (inverse (weight_spmf p)) r = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add: max_def min_def not_le weight_spmf_lt_0 weight_spmf_eq_0 split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}
[PROOF STEP]
proof(induction C arbitrary: Q)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>Q. vc SKIP Q \<Longrightarrow> \<turnstile>\<^sub>t {pre SKIP Q} strip SKIP {Q}
 2. \<And>x1 x2 Q. vc (x1 ::= x2) Q \<Longrightarrow> \<turnstile>\<^sub>t {pre (x1 ::= x2) Q} strip (x1 ::= x2) {Q}
 3. \<And>C1 C2 Q. \<lbrakk>\<And>Q. vc C1 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C1 Q} strip C1 {Q}; \<And>Q. vc C2 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C2 Q} strip C2 {Q}; vc (C1;; C2) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre (C1;; C2) Q} strip (C1;; C2) {Q}
 4. \<And>x1 C1 C2 Q. \<lbrakk>\<And>Q. vc C1 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C1 Q} strip C1 {Q}; \<And>Q. vc C2 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C2 Q} strip C2 {Q}; vc (IF x1 THEN C1 ELSE C2) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre (IF x1 THEN C1 ELSE C2) Q} strip (IF x1 THEN C1 ELSE C2) {Q}
 5. \<And>x1 x2 x3 C Q. \<lbrakk>\<And>Q. vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}; vc ({x1/x2} WHILE x3 DO C) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre ({x1/x2} WHILE x3 DO C) Q} strip ({x1/x2} WHILE x3 DO C) {Q}
[PROOF STEP]
case (Awhile I x b C)
[PROOF STATE]
proof (state)
this:
vc C ?Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C ?Q} strip C {?Q}
vc ({I/x} WHILE b DO C) Q

goal (5 subgoals):
 1. \<And>Q. vc SKIP Q \<Longrightarrow> \<turnstile>\<^sub>t {pre SKIP Q} strip SKIP {Q}
 2. \<And>x1 x2 Q. vc (x1 ::= x2) Q \<Longrightarrow> \<turnstile>\<^sub>t {pre (x1 ::= x2) Q} strip (x1 ::= x2) {Q}
 3. \<And>C1 C2 Q. \<lbrakk>\<And>Q. vc C1 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C1 Q} strip C1 {Q}; \<And>Q. vc C2 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C2 Q} strip C2 {Q}; vc (C1;; C2) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre (C1;; C2) Q} strip (C1;; C2) {Q}
 4. \<And>x1 C1 C2 Q. \<lbrakk>\<And>Q. vc C1 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C1 Q} strip C1 {Q}; \<And>Q. vc C2 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C2 Q} strip C2 {Q}; vc (IF x1 THEN C1 ELSE C2) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre (IF x1 THEN C1 ELSE C2) Q} strip (IF x1 THEN C1 ELSE C2) {Q}
 5. \<And>x1 x2 x3 C Q. \<lbrakk>\<And>Q. vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}; vc ({x1/x2} WHILE x3 DO C) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre ({x1/x2} WHILE x3 DO C) Q} strip ({x1/x2} WHILE x3 DO C) {Q}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<^sub>t {pre ({I/x} WHILE b DO C) Q} strip ({I/x} WHILE b DO C) {Q}
[PROOF STEP]
proof(simp, rule weaken_post[OF While[of I x]], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<turnstile>\<^sub>t {\<lambda>l. I (l(x := Suc (l x)))} strip C {I}
 2. \<forall>l s. 0 < l x \<and> I l s \<longrightarrow> bval b s
 3. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
 4. \<forall>l s. I (l(x := 0)) s \<longrightarrow> Q l s
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<turnstile>\<^sub>t {\<lambda>l. I (l(x := Suc (l x)))} strip C {I}
 2. \<forall>l s. 0 < l x \<and> I l s \<longrightarrow> bval b s
 3. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
 4. \<forall>l s. I (l(x := 0)) s \<longrightarrow> Q l s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile>\<^sub>t {\<lambda>l. I (l(x := Suc (l x)))} strip C {I}
[PROOF STEP]
using Awhile.IH[of "I"] Awhile.prems
[PROOF STATE]
proof (prove)
using this:
vc C I \<Longrightarrow> \<turnstile>\<^sub>t {pre C I} strip C {I}
vc ({I/x} WHILE b DO C) Q

goal (1 subgoal):
 1. \<turnstile>\<^sub>t {\<lambda>l. I (l(x := Suc (l x)))} strip C {I}
[PROOF STEP]
by (auto intro: strengthen_pre)
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>t {\<lambda>l. I (l(x := Suc (l x)))} strip C {I}

goal (3 subgoals):
 1. \<forall>l s. 0 < l x \<and> I l s \<longrightarrow> bval b s
 2. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
 3. \<forall>l s. I (l(x := 0)) s \<longrightarrow> Q l s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>l s. 0 < l x \<and> I l s \<longrightarrow> bval b s
 2. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
 3. \<forall>l s. I (l(x := 0)) s \<longrightarrow> Q l s
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<forall>l s. 0 < l x \<and> I l s \<longrightarrow> bval b s
 2. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
 3. \<forall>l s. I (l(x := 0)) s \<longrightarrow> Q l s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
[PROOF STEP]
using Awhile.prems
[PROOF STATE]
proof (prove)
using this:
vc ({I/x} WHILE b DO C) Q

goal (1 subgoal):
 1. \<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s
[PROOF STEP]
by (simp) (metis fun_upd_triv)
[PROOF STATE]
proof (state)
this:
\<forall>l s. l x = 0 \<and> I l s \<longrightarrow> \<not> bval b s

goal (2 subgoals):
 1. \<forall>l s. 0 < l x \<and> I l s \<longrightarrow> bval b s
 2. \<forall>l s. I (l(x := 0)) s \<longrightarrow> Q l s
[PROOF STEP]
qed (insert Awhile.prems, auto)
[PROOF STATE]
proof (state)
this:
\<turnstile>\<^sub>t {pre ({I/x} WHILE b DO C) Q} strip ({I/x} WHILE b DO C) {Q}

goal (4 subgoals):
 1. \<And>Q. vc SKIP Q \<Longrightarrow> \<turnstile>\<^sub>t {pre SKIP Q} strip SKIP {Q}
 2. \<And>x1 x2 Q. vc (x1 ::= x2) Q \<Longrightarrow> \<turnstile>\<^sub>t {pre (x1 ::= x2) Q} strip (x1 ::= x2) {Q}
 3. \<And>C1 C2 Q. \<lbrakk>\<And>Q. vc C1 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C1 Q} strip C1 {Q}; \<And>Q. vc C2 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C2 Q} strip C2 {Q}; vc (C1;; C2) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre (C1;; C2) Q} strip (C1;; C2) {Q}
 4. \<And>x1 C1 C2 Q. \<lbrakk>\<And>Q. vc C1 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C1 Q} strip C1 {Q}; \<And>Q. vc C2 Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C2 Q} strip C2 {Q}; vc (IF x1 THEN C1 ELSE C2) Q\<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {pre (IF x1 THEN C1 ELSE C2) Q} strip (IF x1 THEN C1 ELSE C2) {Q}
[PROOF STEP]
qed (auto intro: conseq Seq If simp: Skip Assign)


[STATEMENT]
lemma continuous_map_snd_of [continuous_intros]:
   "continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z Y (snd \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z Y (snd \<circ> f)
[PROOF STEP]
by (simp add: continuous_map_pairwise)


[STATEMENT]
lemma "x + y \<ge> (x::int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x + y
[PROOF STEP]
nitpick [unary_ints, expect = genuine]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x + y
[PROOF STEP]
nitpick [binary_ints, expect = genuine]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x + y
[PROOF STEP]
oops


[STATEMENT]
lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (analz G \<subseteq> analz H) = (G \<subseteq> analz H)
[PROOF STEP]
by (metis analz_idem analz_increasing analz_mono subset_trans)


[STATEMENT]
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (synth H) = analz H \<union> synth H
[PROOF STEP]
by (metis Un_empty_right analz_synth_Un)


[STATEMENT]
lemma lookup_filter_aux:
  assumes "distinct (List.map fst xs)"
  shows   "lookup (List.fold (\<lambda>(k, v) t. if P k v then insert k v t else t) xs t) k =
             (case map_of xs k of
                None \<Rightarrow> lookup t k
              | Some v \<Rightarrow> if P k v then Some v else lookup t k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (List.fold (\<lambda>(k, v) t. if P k v then RBT.insert k v t else t) xs t) k = (case map_of xs k of None \<Rightarrow> lookup t k | Some v \<Rightarrow> if P k v then Some v else lookup t k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (list.map fst xs)

goal (1 subgoal):
 1. lookup (List.fold (\<lambda>(k, v) t. if P k v then RBT.insert k v t else t) xs t) k = (case map_of xs k of None \<Rightarrow> lookup t k | Some v \<Rightarrow> if P k v then Some v else lookup t k)
[PROOF STEP]
by (induction xs arbitrary: t) (force split: option.splits)+


[STATEMENT]
lemma le_floor_add: "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> \<le> \<lfloor>x + y\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> \<le> \<lfloor>x + y\<rfloor>
[PROOF STEP]
by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)


[STATEMENT]
lemma sdrop_wait:
assumes "ev \<phi> xs"  shows "\<phi> (sdrop (wait \<phi> xs) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (sdrop (wait \<phi> xs) xs)
[PROOF STEP]
using nxt_wait[OF assms]
[PROOF STATE]
proof (prove)
using this:
(nxt ^^ wait \<phi> xs) \<phi> xs

goal (1 subgoal):
 1. \<phi> (sdrop (wait \<phi> xs) xs)
[PROOF STEP]
unfolding nxt_sdrop
[PROOF STATE]
proof (prove)
using this:
\<phi> (sdrop (wait \<phi> xs) xs)

goal (1 subgoal):
 1. \<phi> (sdrop (wait \<phi> xs) xs)
[PROOF STEP]
.


[STATEMENT]
lemma "(10::int) div -3 = -4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 10 div - 3 = - 4
[PROOF STEP]
by simp


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


[STATEMENT]
lemma nonzero_mult_divide_mult_cancel_left [simp]:
  assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
    and "b \<noteq> \<zero>" "c \<noteq> \<zero>"
  shows "(c \<otimes> a) \<oslash> (c \<otimes> b) = a \<oslash> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>
[PROOF STEP]
have "(c \<otimes> a) \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)"
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)
[PROOF STEP]
by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff)
[PROOF STATE]
proof (state)
this:
c \<otimes> a \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c \<otimes> a \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>
[PROOF STEP]
have "\<dots> =  a \<otimes> inv b \<otimes> (inv c \<otimes> c)"
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>

goal (1 subgoal):
 1. c \<otimes> a \<otimes> (inv b \<otimes> inv c) = a \<otimes> inv b \<otimes> (inv c \<otimes> c)
[PROOF STEP]
by (simp add: m_ac)
[PROOF STATE]
proof (state)
this:
c \<otimes> a \<otimes> (inv b \<otimes> inv c) = a \<otimes> inv b \<otimes> (inv c \<otimes> c)

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c \<otimes> a \<otimes> (inv b \<otimes> inv c) = a \<otimes> inv b \<otimes> (inv c \<otimes> c)

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>
[PROOF STEP]
have "\<dots> =  a \<otimes> inv b"
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>

goal (1 subgoal):
 1. a \<otimes> inv b \<otimes> (inv c \<otimes> c) = a \<otimes> inv b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<otimes> inv b \<otimes> (inv c \<otimes> c) = a \<otimes> inv b

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c \<otimes> a \<oslash> (c \<otimes> b) = a \<otimes> inv b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<otimes> a \<oslash> (c \<otimes> b) = a \<otimes> inv b

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c \<otimes> a \<oslash> (c \<otimes> b) = a \<otimes> inv b
a \<in> carrier R
b \<in> carrier R
c \<in> carrier R
b \<noteq> \<zero>
c \<noteq> \<zero>

goal (1 subgoal):
 1. c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b
[PROOF STEP]
by (simp add: m_div_def)
[PROOF STATE]
proof (state)
this:
c \<otimes> a \<oslash> (c \<otimes> b) = a \<oslash> b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma B_keydist_to_A:
     "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate,
                             (Crypt (pairK(A,B)) (Nonce Nb))\<rbrace> \<in> set evs;
         Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;
         B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B);
         evs \<in> sr \<rbrakk>
     \<Longrightarrow> Key K \<in> analz (knows A evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> Key K \<in> analz (knows A evs)
[PROOF STEP]
apply (frule B_authenticates_A)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> B \<noteq> Spy
 2. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card A)
 3. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card B)
 4. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> evs \<in> sr
 5. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> Key K \<in> analz (knows A evs)
[PROOF STEP]
apply (drule_tac [5] Outpts_B_Card_form_7)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> B \<noteq> Spy
 2. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card A)
 3. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card B)
 4. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> evs \<in> sr
 5. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> evs \<in> sr
 6. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; \<exists>Aa Na. K = sesK (Nb, pairK (Aa, B)) \<and> Certificate = Crypt (pairK (Aa, B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<and> Crypt (pairK (A, B)) (Nonce Nb) = Crypt (pairK (Aa, B)) (Nonce Nb)\<rbrakk> \<Longrightarrow> Key K \<in> analz (knows A evs)
[PROOF STEP]
apply (rule_tac [6] Outpts_imp_knows_agents_secureM_sr [THEN analz.Inj, THEN analz.Fst])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> B \<noteq> Spy
 2. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card A)
 3. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card B)
 4. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> evs \<in> sr
 5. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> evs \<in> sr
 6. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; \<exists>Aa Na. K = sesK (Nb, pairK (Aa, B)) \<and> Certificate = Crypt (pairK (Aa, B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<and> Crypt (pairK (A, B)) (Nonce Nb) = Crypt (pairK (Aa, B)) (Nonce Nb)\<rbrakk> \<Longrightarrow> Outpts (Card A) A \<lbrace>Key K, ?Y7\<rbrace> \<in> set evs
 7. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; \<exists>Aa Na. K = sesK (Nb, pairK (Aa, B)) \<and> Certificate = Crypt (pairK (Aa, B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<and> Crypt (pairK (A, B)) (Nonce Nb) = Crypt (pairK (Aa, B)) (Nonce Nb)\<rbrakk> \<Longrightarrow> evs \<in> sr
[PROOF STEP]
prefer 6
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; \<exists>Aa Na. K = sesK (Nb, pairK (Aa, B)) \<and> Certificate = Crypt (pairK (Aa, B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<and> Crypt (pairK (A, B)) (Nonce Nb) = Crypt (pairK (Aa, B)) (Nonce Nb)\<rbrakk> \<Longrightarrow> Outpts (Card A) A \<lbrace>Key K, ?Y7\<rbrace> \<in> set evs
 2. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> B \<noteq> Spy
 3. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card A)
 4. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card B)
 5. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> evs \<in> sr
 6. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> evs \<in> sr
 7. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; \<exists>Aa Na. K = sesK (Nb, pairK (Aa, B)) \<and> Certificate = Crypt (pairK (Aa, B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<and> Crypt (pairK (A, B)) (Nonce Nb) = Crypt (pairK (Aa, B)) (Nonce Nb)\<rbrakk> \<Longrightarrow> evs \<in> sr
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> B \<noteq> Spy
 2. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card A)
 3. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> \<not> illegalUse (Card B)
 4. \<lbrakk>Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr\<rbrakk> \<Longrightarrow> evs \<in> sr
 5. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> evs \<in> sr
 6. \<lbrakk>Gets B (Crypt (pairK (A, B)) (Nonce Nb)) \<in> set evs; B \<noteq> Spy; \<not> illegalUse (Card A); \<not> illegalUse (Card B); evs \<in> sr; Outpts (Card A) A \<lbrace>Key (sesK (Nb, pairK (A, B))), Crypt (pairK (A, B)) (Nonce Nb)\<rbrace> \<in> set evs; \<exists>Aa Na. K = sesK (Nb, pairK (Aa, B)) \<and> Certificate = Crypt (pairK (Aa, B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<and> Crypt (pairK (A, B)) (Nonce Nb) = Crypt (pairK (Aa, B)) (Nonce Nb)\<rbrakk> \<Longrightarrow> evs \<in> sr
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> iterates_above a; a \<in> Field leq\<rbrakk> \<Longrightarrow> x \<in> Field leq
[PROOF STEP]
by(drule (1) iterates_above_le_f)(rule FieldI1)


[STATEMENT]
lemma lift_forall [rule_format]:
  "\<And>x. (\<forall>x. A x) = True \<Longrightarrow> (A x) = True"
  "\<And>x. (\<exists>x. A x) = False \<Longrightarrow> (A x) = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (\<forall>x. A x) = True \<Longrightarrow> A x = True) &&& (\<And>x. (\<exists>x. A x) = False \<Longrightarrow> A x = False)
[PROOF STEP]
by auto


[STATEMENT]
lemma less_ereal_le: "a < ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a < ereal y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < ereal x; x \<le> y\<rbrakk> \<Longrightarrow> a < ereal y
[PROOF STEP]
using ereal_less_ereal_Ex
[PROOF STATE]
proof (prove)
using this:
(?x < ereal ?r) = (?x = - \<infinity> \<or> (\<exists>p<?r. ?x = ereal p))

goal (1 subgoal):
 1. \<lbrakk>a < ereal x; x \<le> y\<rbrakk> \<Longrightarrow> a < ereal y
[PROOF STEP]
by auto


[STATEMENT]
lemma ereal_le_mult_one_interval:
  fixes x y :: ereal
  assumes y: "y \<noteq> -\<infinity>"
  assumes z: "\<And>z. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> z * x \<le> y"
  shows "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> x \<le> y
 2. x = \<infinity> \<Longrightarrow> x \<le> y
 3. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
x = \<infinity>

goal (3 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> x \<le> y
 2. x = \<infinity> \<Longrightarrow> x \<le> y
 3. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
with z[of "1 / 2"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < 1 / 2; 1 / 2 < 1\<rbrakk> \<Longrightarrow> 1 / 2 * x \<le> y
x = \<infinity>
[PROOF STEP]
show "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < 1 / 2; 1 / 2 < 1\<rbrakk> \<Longrightarrow> 1 / 2 * x \<le> y
x = \<infinity>

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (simp add: one_ereal_def)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> x \<le> y
 2. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> x \<le> y
 2. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
case (real r)
[PROOF STATE]
proof (state)
this:
x = ereal r

goal (2 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> x \<le> y
 2. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
note r = this
[PROOF STATE]
proof (state)
this:
x = ereal r

goal (2 subgoals):
 1. \<And>r. x = ereal r \<Longrightarrow> x \<le> y
 2. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
show "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
proof (cases y)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>r. y = ereal r \<Longrightarrow> x \<le> y
 2. y = \<infinity> \<Longrightarrow> x \<le> y
 3. y = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
case (real p)
[PROOF STATE]
proof (state)
this:
y = ereal p

goal (3 subgoals):
 1. \<And>r. y = ereal r \<Longrightarrow> x \<le> y
 2. y = \<infinity> \<Longrightarrow> x \<le> y
 3. y = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
note p = this
[PROOF STATE]
proof (state)
this:
y = ereal p

goal (3 subgoals):
 1. \<And>r. y = ereal r \<Longrightarrow> x \<le> y
 2. y = \<infinity> \<Longrightarrow> x \<le> y
 3. y = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
have "r \<le> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> p
[PROOF STEP]
proof (rule field_le_mult_one_interval)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>0 < z; z < 1\<rbrakk> \<Longrightarrow> z * r \<le> p
[PROOF STEP]
fix z :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>0 < z; z < 1\<rbrakk> \<Longrightarrow> z * r \<le> p
[PROOF STEP]
assume "0 < z" and "z < 1"
[PROOF STATE]
proof (state)
this:
0 < z
z < 1

goal (1 subgoal):
 1. \<And>z. \<lbrakk>0 < z; z < 1\<rbrakk> \<Longrightarrow> z * r \<le> p
[PROOF STEP]
with z[of "ereal z"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < ereal z; ereal z < 1\<rbrakk> \<Longrightarrow> ereal z * x \<le> y
0 < z
z < 1
[PROOF STEP]
show "z * r \<le> p"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ereal z; ereal z < 1\<rbrakk> \<Longrightarrow> ereal z * x \<le> y
0 < z
z < 1

goal (1 subgoal):
 1. z * r \<le> p
[PROOF STEP]
using p r
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ereal z; ereal z < 1\<rbrakk> \<Longrightarrow> ereal z * x \<le> y
0 < z
z < 1
y = ereal p
x = ereal r

goal (1 subgoal):
 1. z * r \<le> p
[PROOF STEP]
by (auto simp: zero_le_mult_iff one_ereal_def)
[PROOF STATE]
proof (state)
this:
z * r \<le> p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<le> p

goal (3 subgoals):
 1. \<And>r. y = ereal r \<Longrightarrow> x \<le> y
 2. y = \<infinity> \<Longrightarrow> x \<le> y
 3. y = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<le> p
[PROOF STEP]
show "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
r \<le> p

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
using p r
[PROOF STATE]
proof (prove)
using this:
r \<le> p
y = ereal p
x = ereal r

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

goal (2 subgoals):
 1. y = \<infinity> \<Longrightarrow> x \<le> y
 2. y = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
qed (insert y, simp_all)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. x = - \<infinity> \<Longrightarrow> x \<le> y
[PROOF STEP]
qed simp


[STATEMENT]
lemma SUP_ereal_minus_right:
  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
  shows "(SUP i\<in>I. c - f i :: ereal) = c - (INF i\<in>I. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP i\<in>I. c - f i) = c - Inf (f ` I)
[PROOF STEP]
using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
[PROOF STATE]
proof (prove)
using this:
(SUP i\<in>I. c + - f i) = c + (SUP i\<in>I. - f i)

goal (1 subgoal):
 1. (SUP i\<in>I. c - f i) = c - Inf (f ` I)
[PROOF STEP]
by (simp add: ereal_SUP_uminus minus_ereal_def)


[STATEMENT]
lemma suminf_ereal_eq_SUP:
  fixes f :: "nat \<Rightarrow> ereal"
  assumes "\<And>i. 0 \<le> f i"
  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. f x) = (SUP n. sum f {..<n})
[PROOF STEP]
using sums_ereal_positive[of f, OF assms, THEN sums_unique]
[PROOF STATE]
proof (prove)
using this:
(SUP n. sum f {..<n}) = suminf f

goal (1 subgoal):
 1. (\<Sum>x. f x) = (SUP n. sum f {..<n})
[PROOF STEP]
by simp


[STATEMENT]
lemma analz_insert_Number [simp]:
     "analz (insert (Number N) H) = insert (Number N) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Number N) H) = insert (Number N) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Number N) H) \<Longrightarrow> x \<in> insert (Number N) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pi_approx2:
  fixes n :: nat assumes n: "even n" and "n > 0"
  shows   "\<bar>pi - pi_approx2 n\<bar> \<le> inverse (2^(46*n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
even n
[PROOF STEP]
have n': "even (6*n)" "even (4*n)" "even (3*n)"
[PROOF STATE]
proof (prove)
using this:
even n

goal (1 subgoal):
 1. even (6 * n) &&& even (4 * n) &&& even (3 * n)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
even (6 * n)
even (4 * n)
even (3 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
from machin'
[PROOF STATE]
proof (chain)
picking this:
pi / 4 = 12 * arctan (1 / 18) + 8 * arctan (1 / 57) - 5 * arctan (1 / 239)
[PROOF STEP]
have "pi = 48 * arctan (1/18) + 32 * arctan (1/57) - 20 * arctan (1/239::real)"
[PROOF STATE]
proof (prove)
using this:
pi / 4 = 12 * arctan (1 / 18) + 8 * arctan (1 / 57) - 5 * arctan (1 / 239)

goal (1 subgoal):
 1. pi = 48 * arctan (1 / 18) + 32 * arctan (1 / 57) - 20 * arctan (1 / 239)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pi = 48 * arctan (1 / 18) + 32 * arctan (1 / 57) - 20 * arctan (1 / 239)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
hence "pi - pi_approx2 n = 48 * (arctan (1/18) - arctan_approx (6*n) (1/18)) +
                                 32 * (arctan (1/57) - arctan_approx (4*n) (1/57)) -
                                 20 * (arctan (1/239) - arctan_approx (3*n) (1/239))"
[PROOF STATE]
proof (prove)
using this:
pi = 48 * arctan (1 / 18) + 32 * arctan (1 / 57) - 20 * arctan (1 / 239)

goal (1 subgoal):
 1. pi - pi_approx2 n = 48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239))
[PROOF STEP]
by (simp add: pi_approx2_def)
[PROOF STATE]
proof (state)
this:
pi - pi_approx2 n = 48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239))

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pi - pi_approx2 n = 48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239))

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
have "\<dots> \<in> {-((20/239/(1-(1/239)^4)) * (1/239)^(6*n))..
              (48/18 / (1-(1/18)^4))*(1/18)^(12*n) + (32/57/(1-(1/57)^4)) * (1/57)^(8*n)}"
    (is "_ \<in> {-?l..?u1 + ?u2}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239)) \<in> {- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)}
[PROOF STEP]
apply ((rule combine_bounds(1,2))+; (rule combine_bounds(3); (rule arctan_approx)?)?)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. 0 \<le> 48
 2. 0 \<le> 1 / 18
 3. 1 / 18 < 1
 4. even (6 * n)
 5. 0 \<le> 32
 6. 0 \<le> 1 / 57
 7. 1 / 57 < 1
 8. even (4 * n)
 9. ?a1.1 = 48 * 0 + 32 * 0
 10. ?b1.1 = 48 * ((1 / 18) ^ (2 * (6 * n) + 1) / (1 - (1 / 18) ^ 4)) + 32 * ((1 / 57) ^ (2 * (4 * n) + 1) / (1 - (1 / 57) ^ 4))
A total of 16 subgoals...
[PROOF STEP]
apply (simp_all add: n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 8 * (1 / 18) ^ (12 * n) / (3 - 3 * (1 / 18) ^ 4) = 48 * (1 / 18) ^ (12 * n) / (18 - 18 * (1 / 18) ^ 4)
[PROOF STEP]
apply (simp_all add: field_split_simps)?
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239)) \<in> {- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)}

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239)) \<in> {- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)}

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
48 * (arctan (1 / 18) - arctan_approx (6 * n) (1 / 18)) + 32 * (arctan (1 / 57) - arctan_approx (4 * n) (1 / 57)) - 20 * (arctan (1 / 239) - arctan_approx (3 * n) (1 / 239)) \<in> {- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)}

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
have "?l \<le> (1/8) * (1/2)^(46*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> 1 / 8 * (1 / 2) ^ (46 * n)
[PROOF STEP]
unfolding power_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 20 / 239 / (1 - (1 / 239) ^ 4) * ((1 / 239) ^ 6) ^ n \<le> 1 / 8 * ((1 / 2) ^ 46) ^ n
[PROOF STEP]
by (intro mult_mono power_mono) (simp_all add: field_split_simps)
[PROOF STATE]
proof (state)
this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> 1 / 8 * (1 / 2) ^ (46 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> 1 / 8 * (1 / 2) ^ (46 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
have "\<dots> \<le> (1/2) ^ (46 * n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 8 * (1 / 2) ^ (46 * n) \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
by (cases n; simp_all add: power_add field_split_simps)
[PROOF STATE]
proof (state)
this:
1 / 8 * (1 / 2) ^ (46 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
have "?l \<le> (1/2) ^ (46 * n - 1)"
[PROOF STATE]
proof (prove)
using this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. 20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
have "?u1 + ?u2 \<le> 4 * (1/2)^(48*n) + 1 * (1/2)^(46*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> 4 * (1 / 2) ^ (48 * n) + 1 * (1 / 2) ^ (46 * n)
[PROOF STEP]
unfolding power_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 48 / 18 / (1 - (1 / 18) ^ 4) * ((1 / 18) ^ 12) ^ n + 32 / 57 / (1 - (1 / 57) ^ 4) * ((1 / 57) ^ 8) ^ n \<le> 4 * ((1 / 2) ^ 48) ^ n + 1 * ((1 / 2) ^ 46) ^ n
[PROOF STEP]
by (intro add_mono mult_mono power_mono) (simp_all add: field_split_simps)
[PROOF STATE]
proof (state)
this:
48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> 4 * (1 / 2) ^ (48 * n) + 1 * (1 / 2) ^ (46 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> 4 * (1 / 2) ^ (48 * n) + 1 * (1 / 2) ^ (46 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
from \<open>n > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "4 * (1/2::real)^(48*n) \<le> (1/2)^(46*n)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. 4 * (1 / 2) ^ (48 * n) \<le> (1 / 2) ^ (46 * n)
[PROOF STEP]
by (cases n) (simp_all add: field_simps power_add)
[PROOF STATE]
proof (state)
this:
4 * (1 / 2) ^ (48 * n) \<le> (1 / 2) ^ (46 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
4 * (1 / 2) ^ (48 * n) \<le> (1 / 2) ^ (46 * n)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
from \<open>n > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "(1/2::real) ^ (46 * n) + 1 * (1 / 2) ^ (46 * n) = (1/2) ^ (46 * n - 1)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (1 / 2) ^ (46 * n) + 1 * (1 / 2) ^ (46 * n) = (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
by (cases n; simp_all add: power_add power_divide)
[PROOF STATE]
proof (state)
this:
(1 / 2) ^ (46 * n) + 1 * (1 / 2) ^ (46 * n) = (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 1 * (1 / 2) ^ (46 * n) \<le> y + 1 * (1 / 2) ^ (46 * n)) \<Longrightarrow> 48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
have "?u1 + ?u2 \<le> (1/2) ^ (46 * n - 1)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 1 * (1 / 2) ^ (46 * n) \<le> y + 1 * (1 / 2) ^ (46 * n)) \<Longrightarrow> 48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. 48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
by - simp
[PROOF STATE]
proof (state)
this:
48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)
48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
have "{-?l..?u1 + ?u2} \<subseteq> {-((1/2)^(46*n-1))..(1/2)^(46*n-1)}"
[PROOF STATE]
proof (prove)
using this:
20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n) \<le> (1 / 2) ^ (46 * n - 1)
48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n) \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. {- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)} \<subseteq> {- ((1 / 2) ^ (46 * n - 1))..(1 / 2) ^ (46 * n - 1)}
[PROOF STEP]
by (subst atLeastatMost_subset_iff) simp_all
[PROOF STATE]
proof (state)
this:
{- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)} \<subseteq> {- ((1 / 2) ^ (46 * n - 1))..(1 / 2) ^ (46 * n - 1)}

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
{- (20 / 239 / (1 - (1 / 239) ^ 4) * (1 / 239) ^ (6 * n))..48 / 18 / (1 - (1 / 18) ^ 4) * (1 / 18) ^ (12 * n) + 32 / 57 / (1 - (1 / 57) ^ 4) * (1 / 57) ^ (8 * n)} \<subseteq> {- ((1 / 2) ^ (46 * n - 1))..(1 / 2) ^ (46 * n - 1)}

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pi - pi_approx2 n \<in> {- ((1 / 2) ^ (46 * n - 1))..(1 / 2) ^ (46 * n - 1)}
[PROOF STEP]
have "\<bar>pi - pi_approx2 n\<bar> \<le> ((1/2) ^ (46 * n - 1))"
[PROOF STATE]
proof (prove)
using this:
pi - pi_approx2 n \<in> {- ((1 / 2) ^ (46 * n - 1))..(1 / 2) ^ (46 * n - 1)}

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> (1 / 2) ^ (46 * n - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>pi - pi_approx2 n\<bar> \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>pi - pi_approx2 n\<bar> \<le> (1 / 2) ^ (46 * n - 1)

goal (1 subgoal):
 1. \<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))
[PROOF STEP]
by (simp add: field_split_simps)
[PROOF STATE]
proof (state)
this:
\<bar>pi - pi_approx2 n\<bar> \<le> inverse (2 ^ (46 * n - 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma downset_on_empty [simp]: "downset_on {} p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. downset_on {} p
[PROOF STEP]
by (auto simp: downset_on_def)


[STATEMENT]
lemma finite_enumerate_Suc'':
  fixes S :: "'a::wellorder set"
  assumes "finite S" "Suc n < card S"
  shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
Suc n < card S

goal (1 subgoal):
 1. wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s)
[PROOF STEP]
proof (induction n arbitrary: S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S. \<lbrakk>finite S; Suc 0 < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc 0) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S 0 < s)
 2. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
finite S
Suc 0 < card S

goal (2 subgoals):
 1. \<And>S. \<lbrakk>finite S; Suc 0 < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc 0) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S 0 < s)
 2. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite S
Suc 0 < card S
[PROOF STEP]
have "\<forall>s \<in> S. enumerate S 0 \<le> s"
[PROOF STATE]
proof (prove)
using this:
finite S
Suc 0 < card S

goal (1 subgoal):
 1. \<forall>s\<in>S. wellorder_class.enumerate S 0 \<le> s
[PROOF STEP]
by (auto simp: enumerate.simps intro: Least_le)
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. wellorder_class.enumerate S 0 \<le> s

goal (2 subgoals):
 1. \<And>S. \<lbrakk>finite S; Suc 0 < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc 0) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S 0 < s)
 2. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. wellorder_class.enumerate S 0 \<le> s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. wellorder_class.enumerate S 0 \<le> s

goal (1 subgoal):
 1. wellorder_class.enumerate S (Suc 0) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S 0 < s)
[PROOF STEP]
unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. wellorder_class.enumerate S 0 \<le> s

goal (1 subgoal):
 1. (LEAST n. n \<in> S - {wellorder_class.enumerate S 0}) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S 0 < s)
[PROOF STEP]
by (metis Diff_iff dual_order.strict_iff_order singletonD singletonI)
[PROOF STATE]
proof (state)
this:
wellorder_class.enumerate S (Suc 0) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S 0 < s)

goal (1 subgoal):
 1. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
case (Suc n S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S; Suc n < card ?S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate ?S (Suc n) = (LEAST s. s \<in> ?S \<and> wellorder_class.enumerate ?S n < s)
finite S
Suc (Suc n) < card S

goal (1 subgoal):
 1. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite ?S; Suc n < card ?S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate ?S (Suc n) = (LEAST s. s \<in> ?S \<and> wellorder_class.enumerate ?S n < s)
finite S
Suc (Suc n) < card S
[PROOF STEP]
have "Suc n < card (S - {enumerate S 0})"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?S; Suc n < card ?S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate ?S (Suc n) = (LEAST s. s \<in> ?S \<and> wellorder_class.enumerate ?S n < s)
finite S
Suc (Suc n) < card S

goal (1 subgoal):
 1. Suc n < card (S - {wellorder_class.enumerate S 0})
[PROOF STEP]
using Suc.prems(2) finite_enumerate_in_set
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?S; Suc n < card ?S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate ?S (Suc n) = (LEAST s. s \<in> ?S \<and> wellorder_class.enumerate ?S n < s)
finite S
Suc (Suc n) < card S
Suc (Suc n) < card S
\<lbrakk>finite ?S; ?n < card ?S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate ?S ?n \<in> ?S

goal (1 subgoal):
 1. Suc n < card (S - {wellorder_class.enumerate S 0})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Suc n < card (S - {wellorder_class.enumerate S 0})

goal (1 subgoal):
 1. \<And>n S. \<lbrakk>\<And>S. \<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S n < s); finite S; Suc (Suc n) < card S\<rbrakk> \<Longrightarrow> wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc n < card (S - {wellorder_class.enumerate S 0})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Suc n < card (S - {wellorder_class.enumerate S 0})

goal (1 subgoal):
 1. wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)
[PROOF STEP]
apply (subst (1 2) enumerate_Suc')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n < card (S - {wellorder_class.enumerate S 0}) \<Longrightarrow> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) (Suc n) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s)
[PROOF STEP]
apply (simp add: Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n < card (S - {wellorder_class.enumerate S 0}) \<Longrightarrow> (LEAST s. s \<in> S \<and> s \<noteq> wellorder_class.enumerate S 0 \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s)
[PROOF STEP]
apply (intro arg_cong[where f = Least] HOL.ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. Suc n < card (S - {wellorder_class.enumerate S 0}) \<Longrightarrow> (s \<in> S \<and> s \<noteq> wellorder_class.enumerate S 0 \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s) = (s \<in> S \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s)
[PROOF STEP]
using finite_enumerate_mono[OF zero_less_Suc \<open>finite S\<close>, of n] Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc n < card S \<Longrightarrow> wellorder_class.enumerate S 0 < wellorder_class.enumerate S (Suc n)
finite S
Suc (Suc n) < card S

goal (1 subgoal):
 1. \<And>s. Suc n < card (S - {wellorder_class.enumerate S 0}) \<Longrightarrow> (s \<in> S \<and> s \<noteq> wellorder_class.enumerate S 0 \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s) = (s \<in> S \<and> wellorder_class.enumerate (S - {wellorder_class.enumerate S 0}) n < s)
[PROOF STEP]
by (auto simp flip: enumerate_Suc')
[PROOF STATE]
proof (state)
this:
wellorder_class.enumerate S (Suc (Suc n)) = (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ring) carrier_is_subalgebra:
  assumes "K \<subseteq> carrier R" shows "subalgebra K (carrier R) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subalgebra K (carrier R) R
[PROOF STEP]
using assms subalgebra.intro[OF add.group_incl_imp_subgroup[of "carrier R"], of K] add.group_axioms
[PROOF STATE]
proof (prove)
using this:
K \<subseteq> carrier R
\<lbrakk>carrier R \<subseteq> carrier R; Group.group (add_monoid R\<lparr>carrier := carrier R\<rparr>); subalgebra_axioms K (carrier R) R\<rbrakk> \<Longrightarrow> subalgebra K (carrier R) R
Group.group (add_monoid R)

goal (1 subgoal):
 1. subalgebra K (carrier R) R
[PROOF STEP]
unfolding subalgebra_axioms_def
[PROOF STATE]
proof (prove)
using this:
K \<subseteq> carrier R
\<lbrakk>carrier R \<subseteq> carrier R; Group.group (add_monoid R\<lparr>carrier := carrier R\<rparr>); \<forall>k v. k \<in> K \<longrightarrow> v \<in> carrier R \<longrightarrow> k \<otimes> v \<in> carrier R\<rbrakk> \<Longrightarrow> subalgebra K (carrier R) R
Group.group (add_monoid R)

goal (1 subgoal):
 1. subalgebra K (carrier R) R
[PROOF STEP]
by auto


[STATEMENT]
lemma isomorphic_group_relative_homology_of_contractible:
   "\<lbrakk>contractible_space X; topspace X \<inter> S \<noteq> {}\<rbrakk>
        \<Longrightarrow> relative_homology_group p X S \<cong>
            reduced_homology_group(p - 1) (subtopology X S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>contractible_space X; topspace X \<inter> S \<noteq> {}\<rbrakk> \<Longrightarrow> relative_homology_group p X S \<cong> reduced_homology_group (p - 1) (subtopology X S)
[PROOF STEP]
by (meson iso_relative_homology_of_contractible is_isoI)


[STATEMENT]
lemma differentiable_bound_linearization:
  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  assumes S: "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
  assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
  assumes B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x - f' x0) \<le> B"
  assumes "x0 \<in> S"
  shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B
[PROOF STEP]
define g where [abs_def]: "g x = f x - f' x0 x" for x
[PROOF STATE]
proof (state)
this:
g \<equiv> \<lambda>x. f x - f' x0 x

goal (1 subgoal):
 1. norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B
[PROOF STEP]
have g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. f x - f' x0 x) has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..1} \<Longrightarrow> a + ?t *\<^sub>R (b - a) \<in> S
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?x \<in> S \<Longrightarrow> onorm (f' ?x - f' x0) \<le> B
x0 \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> ((\<lambda>x. f x - f' x0 x) has_derivative (\<lambda>i. f' x i - f' x0 i)) (at x within S)
[PROOF STEP]
by (auto intro!: derivative_eq_intros
      bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> (g has_derivative (\<lambda>i. f' ?x i - f' x0 i)) (at ?x within S)

goal (1 subgoal):
 1. norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B
[PROOF STEP]
from B
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> onorm (f' ?x - f' x0) \<le> B
[PROOF STEP]
have "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> onorm (f' ?x - f' x0) \<le> B

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> onorm (f' ?x - f' x0) \<le> B
?t \<in> {0..1} \<Longrightarrow> a + ?t *\<^sub>R (b - a) \<in> S
?x \<in> S \<Longrightarrow> (f has_derivative f' ?x) (at ?x within S)
?x \<in> S \<Longrightarrow> onorm (f' ?x - f' x0) \<le> B
x0 \<in> S

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B
[PROOF STEP]
by (auto simp: fun_diff_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B

goal (1 subgoal):
 1. norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B
[PROOF STEP]
with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>t. t \<in> {0..1} \<Longrightarrow> t \<in> {0..1}; \<And>x. x \<in> S \<Longrightarrow> x \<in> S; \<And>x. x \<in> {0..1} \<Longrightarrow> onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> ?B\<rbrakk> \<Longrightarrow> norm (g (a + (b - a)) - g a) \<le> norm (b - a) * ?B
x0 \<in> S
\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>t. t \<in> {0..1} \<Longrightarrow> t \<in> {0..1}; \<And>x. x \<in> S \<Longrightarrow> x \<in> S; \<And>x. x \<in> {0..1} \<Longrightarrow> onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> ?B\<rbrakk> \<Longrightarrow> norm (g (a + (b - a)) - g a) \<le> norm (b - a) * ?B
x0 \<in> S
\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B

goal (1 subgoal):
 1. norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B
[PROOF STEP]
by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
[PROOF STATE]
proof (state)
this:
norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arctan_series_stream_aux_code:
  "arctan_series_stream_aux True n = MSSCons (-inverse n) (arctan_series_stream_aux False (n + 2))"
  "arctan_series_stream_aux False n = MSSCons (inverse n) (arctan_series_stream_aux True (n + 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arctan_series_stream_aux True n = MSSCons (- inverse n) (arctan_series_stream_aux False (n + 2)) &&& arctan_series_stream_aux False n = MSSCons (inverse n) (arctan_series_stream_aux True (n + 2))
[PROOF STEP]
by (subst arctan_series_stream_aux.code; simp)+


[STATEMENT]
lemma even_uminusI: "even a \<Longrightarrow> even (-a :: 'a :: unique_euclidean_ring_with_nat)"
  and odd_uminusI:  "odd a \<Longrightarrow> odd (-a :: 'a :: unique_euclidean_ring_with_nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (even a \<Longrightarrow> even (- a)) &&& (odd a \<Longrightarrow> odd (- a))
[PROOF STEP]
by auto


[STATEMENT]
lemma closed_insert [continuous_intros, simp]:
  assumes "closed S"
  shows "closed (insert a S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (insert a S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed (insert a S)
[PROOF STEP]
from closed_singleton assms
[PROOF STATE]
proof (chain)
picking this:
closed {?a}
closed S
[PROOF STEP]
have "closed ({a} \<union> S)"
[PROOF STATE]
proof (prove)
using this:
closed {?a}
closed S

goal (1 subgoal):
 1. closed ({a} \<union> S)
[PROOF STEP]
by (rule closed_Un)
[PROOF STATE]
proof (state)
this:
closed ({a} \<union> S)

goal (1 subgoal):
 1. closed (insert a S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed ({a} \<union> S)
[PROOF STEP]
show "closed (insert a S)"
[PROOF STATE]
proof (prove)
using this:
closed ({a} \<union> S)

goal (1 subgoal):
 1. closed (insert a S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed (insert a S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LIMSEQ_le_const2: "X \<longlonglongrightarrow> x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X n \<le> a \<Longrightarrow> x \<le> a"
  for a x :: "'a::linorder_topology"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<longlonglongrightarrow> x; \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a
[PROOF STEP]
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto


[STATEMENT]
lemma (in linorder_topology) compact_attains_sup:
  assumes "compact S" "S \<noteq> {}"
  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
proof (rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)

goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)
[PROOF STEP]
obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>\<forall>s\<in>S. t s \<in> S; \<forall>s\<in>S. s < t s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis not_le)
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. t s \<in> S
\<forall>s\<in>S. s < t s

goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. t s \<in> S
\<forall>s\<in>S. s < t s
[PROOF STEP]
have "\<And>s. s\<in>S \<Longrightarrow> open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. t s \<in> S
\<forall>s\<in>S. s < t s

goal (1 subgoal):
 1. (\<And>s. s \<in> S \<Longrightarrow> open {..<t s}) &&& S \<subseteq> (\<Union>s\<in>S. {..<t s})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?s \<in> S \<Longrightarrow> open {..<t ?s}
S \<subseteq> (\<Union>s\<in>S. {..<t s})

goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
with \<open>compact S\<close>
[PROOF STATE]
proof (chain)
picking this:
compact S
?s \<in> S \<Longrightarrow> open {..<t ?s}
S \<subseteq> (\<Union>s\<in>S. {..<t s})
[PROOF STEP]
obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
[PROOF STATE]
proof (prove)
using this:
compact S
?s \<in> S \<Longrightarrow> open {..<t ?s}
S \<subseteq> (\<Union>s\<in>S. {..<t s})

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<subseteq> S; finite C; S \<subseteq> (\<Union>s\<in>C. {..<t s})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis compactE_image)
[PROOF STATE]
proof (state)
this:
C \<subseteq> S
finite C
S \<subseteq> (\<Union>s\<in>C. {..<t s})

goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
with \<open>S \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
C \<subseteq> S
finite C
S \<subseteq> (\<Union>s\<in>C. {..<t s})
[PROOF STEP]
have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}
C \<subseteq> S
finite C
S \<subseteq> (\<Union>s\<in>C. {..<t s})

goal (1 subgoal):
 1. Max (t ` C) \<in> t ` C &&& \<forall>s\<in>t ` C. s \<le> Max (t ` C)
[PROOF STEP]
by (auto intro!: Max_in)
[PROOF STATE]
proof (state)
this:
Max (t ` C) \<in> t ` C
\<forall>s\<in>t ` C. s \<le> Max (t ` C)

goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
with C
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> (\<Union>s\<in>C. {..<t s})
Max (t ` C) \<in> t ` C
\<forall>s\<in>t ` C. s \<le> Max (t ` C)
[PROOF STEP]
have "S \<subseteq> {..< Max (t`C)}"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> (\<Union>s\<in>C. {..<t s})
Max (t ` C) \<in> t ` C
\<forall>s\<in>t ` C. s \<le> Max (t ` C)

goal (1 subgoal):
 1. S \<subseteq> {..<Max (t ` C)}
[PROOF STEP]
by (auto intro: less_le_trans simp: subset_eq)
[PROOF STATE]
proof (state)
this:
S \<subseteq> {..<Max (t ` C)}

goal (1 subgoal):
 1. \<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s) \<Longrightarrow> \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
with t Max \<open>C \<subseteq> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. t s \<in> S
Max (t ` C) \<in> t ` C
C \<subseteq> S
S \<subseteq> {..<Max (t ` C)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. t s \<in> S
Max (t ` C) \<in> t ` C
C \<subseteq> S
S \<subseteq> {..<Max (t ` C)}

goal (1 subgoal):
 1. \<exists>s\<in>S. \<forall>t\<in>S. t \<le> s
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singular_relcycle_restrict [simp]:
   "singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S
[PROOF STEP]
have eq: "subtopology X (topspace X \<inter> S) = subtopology X S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtopology X (topspace X \<inter> S) = subtopology X S
[PROOF STEP]
by (metis subtopology_subtopology subtopology_topspace)
[PROOF STATE]
proof (state)
this:
subtopology X (topspace X \<inter> S) = subtopology X S

goal (1 subgoal):
 1. singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S
[PROOF STEP]
by (force simp: singular_relcycle_def eq)
[PROOF STATE]
proof (state)
this:
singular_relcycle p X (topspace X \<inter> S) = singular_relcycle p X S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_map_eq:
   "\<lbrakk>singular_chain p X c; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
    \<Longrightarrow> chain_map p f c = chain_map p g c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>singular_chain p X c; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f c = chain_map p g c
[PROOF STEP]
unfolding singular_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Poly_Mapping.keys c \<subseteq> singular_simplex_set p X; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f c = chain_map p g c
[PROOF STEP]
proof (induction rule: frag_induction)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f 0 = chain_map p g 0
 2. \<And>x. \<lbrakk>x \<in> singular_simplex_set p X; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f (frag_of x) = chain_map p g (frag_of x)
 3. \<And>a b. \<lbrakk>(\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f a = chain_map p g a; (\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f b = chain_map p g b; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f (a - b) = chain_map p g (a - b)
[PROOF STEP]
case (one x)
[PROOF STATE]
proof (state)
this:
x \<in> singular_simplex_set p X
?x \<in> topspace X \<Longrightarrow> f ?x = g ?x

goal (3 subgoals):
 1. (\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f 0 = chain_map p g 0
 2. \<And>x. \<lbrakk>x \<in> singular_simplex_set p X; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f (frag_of x) = chain_map p g (frag_of x)
 3. \<And>a b. \<lbrakk>(\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f a = chain_map p g a; (\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f b = chain_map p g b; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f (a - b) = chain_map p g (a - b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> singular_simplex_set p X
?x \<in> topspace X \<Longrightarrow> f ?x = g ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> singular_simplex_set p X
?x \<in> topspace X \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. chain_map p f (frag_of x) = chain_map p g (frag_of x)
[PROOF STEP]
by (metis (no_types, lifting) chain_map_of mem_Collect_eq simplex_map_eq)
[PROOF STATE]
proof (state)
this:
chain_map p f (frag_of x) = chain_map p g (frag_of x)

goal (2 subgoals):
 1. (\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f 0 = chain_map p g 0
 2. \<And>a b. \<lbrakk>(\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f a = chain_map p g a; (\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x) \<Longrightarrow> chain_map p f b = chain_map p g b; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> chain_map p f (a - b) = chain_map p g (a - b)
[PROOF STEP]
qed (auto simp: chain_map_diff)


[STATEMENT]
lemma kparts_has_no_pair [iff]: "has_no_pair (kparts H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_no_pair (kparts H)
[PROOF STEP]
by auto


[STATEMENT]
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsplit c (x # xs) = c x xs
[PROOF STEP]
by (simp add: lsplit_def)


[STATEMENT]
lemma reflp_list_eq: "reflp list_eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflp list_eq
[PROOF STEP]
unfolding reflp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. list_eq x x
[PROOF STEP]
by simp


[STATEMENT]
lemma star_of_le_HNatInfinite: "N \<in> HNatInfinite \<Longrightarrow> star_of n \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N \<in> HNatInfinite \<Longrightarrow> hypnat_of_nat n \<le> N
[PROOF STEP]
by (rule star_of_less_HNatInfinite [THEN order_less_imp_le])


[STATEMENT]
lemma of_hypnat_add [simp]: "\<And>m n. of_hypnat (m + n) = of_hypnat m + of_hypnat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. of_hypnat (m + n) = of_hypnat m + of_hypnat n
[PROOF STEP]
by transfer (rule of_nat_add)


[STATEMENT]
lemma fps_mult_fps_X_power_commute: "fps_X ^ k * a = a * fps_X ^ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fps_X ^ k * a = a * fps_X ^ k
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fps_X ^ 0 * a = a * fps_X ^ 0
 2. \<And>k. fps_X ^ k * a = a * fps_X ^ k \<Longrightarrow> fps_X ^ Suc k * a = a * fps_X ^ Suc k
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
fps_X ^ k * a = a * fps_X ^ k

goal (2 subgoals):
 1. fps_X ^ 0 * a = a * fps_X ^ 0
 2. \<And>k. fps_X ^ k * a = a * fps_X ^ k \<Longrightarrow> fps_X ^ Suc k * a = a * fps_X ^ Suc k
[PROOF STEP]
hence "fps_X ^ Suc k * a = a * fps_X * fps_X ^ k"
[PROOF STATE]
proof (prove)
using this:
fps_X ^ k * a = a * fps_X ^ k

goal (1 subgoal):
 1. fps_X ^ Suc k * a = a * fps_X * fps_X ^ k
[PROOF STEP]
by (simp add: mult.assoc fps_mult_fps_X_commute[symmetric])
[PROOF STATE]
proof (state)
this:
fps_X ^ Suc k * a = a * fps_X * fps_X ^ k

goal (2 subgoals):
 1. fps_X ^ 0 * a = a * fps_X ^ 0
 2. \<And>k. fps_X ^ k * a = a * fps_X ^ k \<Longrightarrow> fps_X ^ Suc k * a = a * fps_X ^ Suc k
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
fps_X ^ Suc k * a = a * fps_X * fps_X ^ k

goal (1 subgoal):
 1. fps_X ^ Suc k * a = a * fps_X ^ Suc k
[PROOF STEP]
by (simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
fps_X ^ Suc k * a = a * fps_X ^ Suc k

goal (1 subgoal):
 1. fps_X ^ 0 * a = a * fps_X ^ 0
[PROOF STEP]
qed simp


[STATEMENT]
lemma fps_integral0_of_nat:
  "fps_integral0 (of_nat n :: 'a::division_ring fps) = of_nat n * fps_X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fps_integral0 (of_nat n) = of_nat n * fps_X
[PROOF STEP]
using fps_integral0_fps_const[of "of_nat n :: 'a"]
[PROOF STATE]
proof (prove)
using this:
fps_integral0 (fps_const (of_nat n)) = fps_const (of_nat n) * fps_X

goal (1 subgoal):
 1. fps_integral0 (of_nat n) = of_nat n * fps_X
[PROOF STEP]
by (simp add: fps_of_nat)


[STATEMENT]
lemma natlist_trivial_Suc0 [simp]: "natpermute n (Suc 0) = {[n]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. natpermute n (Suc 0) = {[n]}
[PROOF STEP]
using natlist_trivial_1
[PROOF STATE]
proof (prove)
using this:
natpermute ?n 1 = {[?n]}

goal (1 subgoal):
 1. natpermute n (Suc 0) = {[n]}
[PROOF STEP]
by force


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


[STATEMENT]
lemma "(0::real) < 1 + (1 + x)\<^sup>2 * \<bar>x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 + (1 + x)\<^sup>2 * \<bar>x\<bar>
[PROOF STEP]
by (sos "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))")


[STATEMENT]
lemma Nonce_Pan_image_eq [simp]: "(Nonce x \<notin> Pan`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nonce x \<notin> Pan ` A
[PROOF STEP]
by auto


[STATEMENT]
lemma path_connectedin_discrete_topology:
  "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_connectedin (discrete_topology U) S = (S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a}))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>path_connectedin (discrete_topology U) S; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> U
 2. path_connectedin (discrete_topology U) S \<Longrightarrow> \<exists>a. S \<subseteq> {a}
 3. \<And>a. \<lbrakk>S \<subseteq> U; S \<subseteq> {a}\<rbrakk> \<Longrightarrow> path_connectedin (discrete_topology U) S
[PROOF STEP]
using path_connectedin_subset_topspace
[PROOF STATE]
proof (prove)
using this:
path_connectedin ?X ?S \<Longrightarrow> ?S \<subseteq> topspace ?X

goal (3 subgoals):
 1. \<And>x. \<lbrakk>path_connectedin (discrete_topology U) S; x \<in> S\<rbrakk> \<Longrightarrow> x \<in> U
 2. path_connectedin (discrete_topology U) S \<Longrightarrow> \<exists>a. S \<subseteq> {a}
 3. \<And>a. \<lbrakk>S \<subseteq> U; S \<subseteq> {a}\<rbrakk> \<Longrightarrow> path_connectedin (discrete_topology U) S
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. path_connectedin (discrete_topology U) S \<Longrightarrow> \<exists>a. S \<subseteq> {a}
 2. \<And>a. \<lbrakk>S \<subseteq> U; S \<subseteq> {a}\<rbrakk> \<Longrightarrow> path_connectedin (discrete_topology U) S
[PROOF STEP]
apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>S \<subseteq> U; S \<subseteq> {a}\<rbrakk> \<Longrightarrow> path_connectedin (discrete_topology U) S
[PROOF STEP]
using subset_singletonD
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> {?x} \<Longrightarrow> ?A = {} \<or> ?A = {?x}

goal (1 subgoal):
 1. \<And>a. \<lbrakk>S \<subseteq> U; S \<subseteq> {a}\<rbrakk> \<Longrightarrow> path_connectedin (discrete_topology U) S
[PROOF STEP]
by fastforce


[STATEMENT]
lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) \<longleftrightarrow> n \<in> {1, 2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue_primroot n (Suc 0) = (n \<in> {1, 2})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. residue_primroot n (Suc 0) \<Longrightarrow> n \<in> {1, 2}
 2. n \<in> {1, 2} \<Longrightarrow> residue_primroot n (Suc 0)
[PROOF STEP]
assume *: "residue_primroot n (Suc 0)"
[PROOF STATE]
proof (state)
this:
residue_primroot n (Suc 0)

goal (2 subgoals):
 1. residue_primroot n (Suc 0) \<Longrightarrow> n \<in> {1, 2}
 2. n \<in> {1, 2} \<Longrightarrow> residue_primroot n (Suc 0)
[PROOF STEP]
with totient_gt_1[of n]
[PROOF STATE]
proof (chain)
picking this:
2 < n \<Longrightarrow> 1 < totient n
residue_primroot n (Suc 0)
[PROOF STEP]
have "n \<le> 2"
[PROOF STATE]
proof (prove)
using this:
2 < n \<Longrightarrow> 1 < totient n
residue_primroot n (Suc 0)

goal (1 subgoal):
 1. n \<le> 2
[PROOF STEP]
by (cases "n \<le> 2") (auto simp: residue_primroot_def)
[PROOF STATE]
proof (state)
this:
n \<le> 2

goal (2 subgoals):
 1. residue_primroot n (Suc 0) \<Longrightarrow> n \<in> {1, 2}
 2. n \<in> {1, 2} \<Longrightarrow> residue_primroot n (Suc 0)
[PROOF STEP]
hence "n \<in> {0, 1, 2}"
[PROOF STATE]
proof (prove)
using this:
n \<le> 2

goal (1 subgoal):
 1. n \<in> {0, 1, 2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> {0, 1, 2}

goal (2 subgoals):
 1. residue_primroot n (Suc 0) \<Longrightarrow> n \<in> {1, 2}
 2. n \<in> {1, 2} \<Longrightarrow> residue_primroot n (Suc 0)
[PROOF STEP]
thus "n \<in> {1, 2}"
[PROOF STATE]
proof (prove)
using this:
n \<in> {0, 1, 2}

goal (1 subgoal):
 1. n \<in> {1, 2}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n \<in> {0, 1, 2}
residue_primroot n (Suc 0)

goal (1 subgoal):
 1. n \<in> {1, 2}
[PROOF STEP]
by (auto simp: residue_primroot_def)
[PROOF STATE]
proof (state)
this:
n \<in> {1, 2}

goal (1 subgoal):
 1. n \<in> {1, 2} \<Longrightarrow> residue_primroot n (Suc 0)
[PROOF STEP]
qed (auto simp: residue_primroot_def)


[STATEMENT]
lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y
[PROOF STEP]
by (simp add: hidings_entails_def)


[STATEMENT]
lemma continuous_on_joinpaths_D2:
    "\<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} g2
[PROOF STEP]
apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> (\<lambda>x. inverse 2*x + 1/2)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on {0..1} (g1 +++ g2 \<circ> (\<lambda>x. inverse 2 * x + 1 / 2))
 2. \<And>x. \<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2; x \<in> {0..1}\<rbrakk> \<Longrightarrow> (g1 +++ g2 \<circ> (\<lambda>x. inverse 2 * x + 1 / 2)) x = g2 x
[PROOF STEP]
apply (rule continuous_intros | simp)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> continuous_on ((\<lambda>x. x / 2 + 1 / 2) ` {0..1}) (g1 +++ g2)
 2. \<And>x. \<lbrakk>continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2; x \<in> {0..1}\<rbrakk> \<Longrightarrow> (g1 +++ g2 \<circ> (\<lambda>x. inverse 2 * x + 1 / 2)) x = g2 x
[PROOF STEP]
apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma single_inheritance:
"\<lbrakk>G\<turnstile>A \<prec>\<^sub>C1 B; G\<turnstile>A \<prec>\<^sub>C1 C\<rbrakk> \<Longrightarrow> B = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G\<turnstile>A\<prec>\<^sub>C1B; G\<turnstile>A\<prec>\<^sub>C1C\<rbrakk> \<Longrightarrow> B = C
[PROOF STEP]
by (auto simp add: subcls1_def)