[STATEMENT]
theorem (in group) trivial_derived_seq_imp_solvable:
  assumes "subgroup H G" and "((derived G) ^^ n) H = { \<one> }" shows "solvable_seq G H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgroup H G
(derived G ^^ n) H = {\<one>}

goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
proof (induct n arbitrary: H, simp add: unity[of G])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n H. \<lbrakk>\<And>H. \<lbrakk>subgroup H G; (derived G ^^ n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H; subgroup H G; (derived G ^^ Suc n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>subgroup ?H G; (derived G ^^ n) ?H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup H G
(derived G ^^ Suc n) H = {\<one>}

goal (1 subgoal):
 1. \<And>n H. \<lbrakk>\<And>H. \<lbrakk>subgroup H G; (derived G ^^ n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H; subgroup H G; (derived G ^^ Suc n) H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G H
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup ?H G; (derived G ^^ n) ?H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup H G
(derived G ^^ Suc n) H = {\<one>}

goal (1 subgoal):
 1. solvable_seq G H
[PROOF STEP]
using augment_solvable_seq derived_is_subgroup[OF subgroup.subset]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup ?H G; (derived G ^^ n) ?H = {\<one>}\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup H G
(derived G ^^ Suc n) H = {\<one>}
\<lbrakk>subgroup ?H G; solvable_seq G (derived G ?H)\<rbrakk> \<Longrightarrow> solvable_seq G ?H
subgroup ?H G \<Longrightarrow> subgroup (derived G ?H) G

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
quickcheck[exhaustive, expect = counterexample]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
oops


[STATEMENT]
lemma "((\<forall>x. P(x)) \<or> Q)  =  (\<forall>x. P(x) \<or> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>x. P x) \<or> Q) = (\<forall>x. P x \<or> Q)
[PROOF STEP]
by blast


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


[STATEMENT]
lemma "P \<or> \<not> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<or> \<not> P
[PROOF STEP]
by blast


[STATEMENT]
lemma eval_minus [simp]:
  "eval (P - Q) = eval P - eval Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (P - Q) = eval P - eval Q
[PROOF STEP]
by (simp add: minus_pred_def)


[STATEMENT]
lemma closure_of_eq_topspace:
   "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X closure_of S = topspace X) = (X interior_of (topspace X - S) = {})
[PROOF STEP]
using closure_of_subset_topspace [of X S] interior_of_complement
[PROOF STATE]
proof (prove)
using this:
X closure_of S \<subseteq> topspace X
?X interior_of (topspace ?X - ?S) = topspace ?X - ?X closure_of ?S

goal (1 subgoal):
 1. (X closure_of S = topspace X) = (X interior_of (topspace X - S) = {})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma homeomorphic_map_derived_set_of:
  assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
  shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` topspace X = topspace Y &&& inj_on f (topspace X)
[PROOF STEP]
using hom
[PROOF STATE]
proof (prove)
using this:
homeomorphic_map X Y f

goal (1 subgoal):
 1. f ` topspace X = topspace Y &&& inj_on f (topspace X)
[PROOF STEP]
by (auto simp: homeomorphic_eq_everything_map)
[PROOF STATE]
proof (state)
this:
f ` topspace X = topspace Y
inj_on f (topspace X)

goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
have iff: "(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) =
            (\<forall>T. T \<subseteq> topspace Y \<longrightarrow> f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))"
    if "x \<in> topspace X" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
have \<section>: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))
[PROOF STEP]
by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
[PROOF STATE]
proof (state)
this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
have "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)"  (is "?lhs = ?rhs")
      if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T \<Longrightarrow> \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T
 2. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
show "?lhs \<Longrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T \<Longrightarrow> \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T
[PROOF STEP]
by (meson \<section> imageI inj inj_on_eq_iff inj_on_subset that)
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T \<Longrightarrow> \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T

goal (1 subgoal):
 1. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
show "?rhs \<Longrightarrow> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
using S inj inj_onD that
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> topspace X
inj_on f (topspace X)
\<lbrakk>inj_on ?f ?A; ?f ?x = ?f ?y; ?x \<in> ?A; ?y \<in> ?A\<rbrakk> \<Longrightarrow> ?x = ?y
T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)

goal (1 subgoal):
 1. \<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T \<Longrightarrow> \<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T) \<Longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> ?T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` ?T)

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))
?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T) \<Longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> ?T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` ?T)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x \<in> ?T \<and> openin X ?T) = (?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T))
?T \<subseteq> topspace X \<and> f x \<in> f ` ?T \<and> openin Y (f ` ?T) \<Longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> ?T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` ?T)

goal (1 subgoal):
 1. (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))
[PROOF STEP]
by (auto simp flip: fim simp: all_subset_image)
[PROOF STATE]
proof (state)
this:
(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> topspace X \<Longrightarrow> (\<forall>T. ?x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> ?x \<and> y \<in> S \<and> y \<in> T)) = (\<forall>T\<subseteq>topspace Y. f ?x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f ?x \<and> y \<in> f ` S \<and> y \<in> T))

goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
have *: "\<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x \<longleftrightarrow> Q(f x)\<rbrakk> \<Longrightarrow> {y. y \<in> T \<and> Q y} = f ` {x \<in> S. P x}" for T S P Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x = Q (f x)\<rbrakk> \<Longrightarrow> {y \<in> T. Q y} = f ` {x \<in> S. P x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?T = f ` ?S; \<And>x. x \<in> ?S \<Longrightarrow> ?P x = ?Q (f x)\<rbrakk> \<Longrightarrow> {y \<in> ?T. ?Q y} = f ` {x \<in> ?S. ?P x}

goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y derived_set_of f ` S = f ` (X derived_set_of S)
[PROOF STEP]
unfolding derived_set_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> topspace Y. \<forall>T. x \<in> T \<and> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> f ` S \<and> y \<in> T)} = f ` {x \<in> topspace X. \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)}
[PROOF STEP]
by (rule *) (use fim iff openin_subset in force)+
[PROOF STATE]
proof (state)
this:
Y derived_set_of f ` S = f ` (X derived_set_of S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma perfect_map_id [simp]: "perfect_map X X id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perfect_map X X id
[PROOF STEP]
by (simp add: homeomorphic_imp_perfect_map)


[STATEMENT]
lemma connected_Iic[simp]: "connected {..a}"
  for a :: "'a::linear_continuum_topology"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected {..a}
[PROOF STEP]
by (auto simp: connected_iff_interval)


[STATEMENT]
lemma open_image_fst:
  assumes "open S"
  shows "open (fst ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (fst ` S)
[PROOF STEP]
proof (rule openI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
assume "x \<in> fst ` S"
[PROOF STATE]
proof (state)
this:
x \<in> fst ` S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> fst ` S
[PROOF STEP]
obtain y where "(x, y) \<in> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> fst ` S

goal (1 subgoal):
 1. (\<And>y. (x, y) \<in> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> S
[PROOF STEP]
obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> S

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>open A; open B; x \<in> A; y \<in> B; A \<times> B \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>open S\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> S
open S

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>open A; open B; x \<in> A; y \<in> B; A \<times> B \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding open_prod_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> S
\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>open A; open B; x \<in> A; y \<in> B; A \<times> B \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open A
open B
x \<in> A
y \<in> B
A \<times> B \<subseteq> S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<times> B \<subseteq> S
y \<in> B
[PROOF STEP]
have "A \<subseteq> fst ` S"
[PROOF STATE]
proof (prove)
using this:
A \<times> B \<subseteq> S
y \<in> B

goal (1 subgoal):
 1. A \<subseteq> fst ` S
[PROOF STEP]
by (rule subset_fst_imageI)
[PROOF STATE]
proof (state)
this:
A \<subseteq> fst ` S

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

goal (1 subgoal):
 1. open A \<and> x \<in> A \<and> A \<subseteq> fst ` S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
open A \<and> x \<in> A \<and> A \<subseteq> fst ` S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open A \<and> x \<in> A \<and> A \<subseteq> fst ` S
[PROOF STEP]
show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S"
[PROOF STATE]
proof (prove)
using this:
open A \<and> x \<in> A \<and> A \<subseteq> fst ` S

goal (1 subgoal):
 1. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_lim_then_eventually_real:
  assumes "(u \<longlongrightarrow> ereal l) F"
  shows "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
have "ereal l \<in> {-\<infinity><..<(\<infinity>::ereal)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ereal l \<in> {- \<infinity><..<\<infinity>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ereal l \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ereal l \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
have "open {-\<infinity><..<(\<infinity>::ereal)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open {- \<infinity><..<\<infinity>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
open {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ereal l \<in> {- \<infinity><..<\<infinity>}
open {- \<infinity><..<\<infinity>}
[PROOF STEP]
have "eventually (\<lambda>n. u n \<in> {-\<infinity><..<(\<infinity>::ereal)}) F"
[PROOF STATE]
proof (prove)
using this:
ereal l \<in> {- \<infinity><..<\<infinity>}
open {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
[PROOF STEP]
using assms tendsto_def
[PROOF STATE]
proof (prove)
using this:
ereal l \<in> {- \<infinity><..<\<infinity>}
open {- \<infinity><..<\<infinity>}
(u \<longlongrightarrow> ereal l) F
(?f \<longlongrightarrow> ?l) ?F = (\<forall>S. open S \<longrightarrow> ?l \<in> S \<longrightarrow> (\<forall>\<^sub>F x in ?F. ?f x \<in> S))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
have "\<And>x. x \<in> {-\<infinity><..<(\<infinity>::ereal)} \<Longrightarrow> x = ereal(real_of_ereal x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> x = ereal (real_of_ereal x)
[PROOF STEP]
using ereal_real
[PROOF STATE]
proof (prove)
using this:
ereal (real_of_ereal ?x) = (if \<bar>?x\<bar> = \<infinity> then 0 else ?x)

goal (1 subgoal):
 1. \<And>x. x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> x = ereal (real_of_ereal x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> ?x = ereal (real_of_ereal ?x)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
?x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> ?x = ereal (real_of_ereal ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in F. u n \<in> {- \<infinity><..<\<infinity>}
?x \<in> {- \<infinity><..<\<infinity>} \<Longrightarrow> ?x = ereal (real_of_ereal ?x)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))
[PROOF STEP]
by (metis (mono_tags, lifting) eventually_mono)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in F. u n = ereal (real_of_ereal (u n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strip_while_dropWhile_commute:
  "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])
 2. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])
 2. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q []) = dropWhile Q (strip_while P [])

goal (1 subgoal):
 1. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)

goal (1 subgoal):
 1. \<And>a xs. strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs) \<Longrightarrow> strip_while P (dropWhile Q (a # xs)) = dropWhile Q (strip_while P (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
proof (cases "\<forall>y\<in>set xs. P y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>y\<in>set xs. P y \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
 2. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set xs. P y

goal (2 subgoals):
 1. \<forall>y\<in>set xs. P y \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
 2. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
with dropWhile_append2 [of "rev xs"]
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> set (rev xs) \<Longrightarrow> ?P x) \<Longrightarrow> dropWhile ?P (rev xs @ ?ys) = dropWhile ?P ?ys
\<forall>y\<in>set xs. P y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set (rev xs) \<Longrightarrow> ?P x) \<Longrightarrow> dropWhile ?P (rev xs @ ?ys) = dropWhile ?P ?ys
\<forall>y\<in>set xs. P y

goal (1 subgoal):
 1. strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
by (auto simp add: strip_while_def dest: set_dropWhileD)
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))

goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y\<in>set xs. P y)

goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y\<in>set xs. P y)
[PROOF STEP]
obtain y where "y \<in> set xs" and "\<not> P y"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y\<in>set xs. P y)

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

goal (1 subgoal):
 1. \<not> (\<forall>y\<in>set xs. P y) \<Longrightarrow> strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
with Cons dropWhile_append3 [of P y "rev xs"]
[PROOF STATE]
proof (chain)
picking this:
strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)
\<not> P y \<Longrightarrow> dropWhile P (rev xs @ y # ?ys) = dropWhile P (rev xs) @ y # ?ys
y \<in> set xs
\<not> P y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)
\<not> P y \<Longrightarrow> dropWhile P (rev xs @ y # ?ys) = dropWhile P (rev xs) @ y # ?ys
y \<in> set xs
\<not> P y

goal (1 subgoal):
 1. strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))
[PROOF STEP]
by (simp add: strip_while_def)
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
strip_while P (dropWhile Q (x # xs)) = dropWhile Q (strip_while P (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length xs = 0) = (xs = [])
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma count_notin[simp]: "x \<notin> set xs \<Longrightarrow> count_list xs x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> count_list xs x = 0
[PROOF STEP]
by(simp add: count_list_0_iff)


[STATEMENT]
lemma sorted1: "sorted [x] = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted [x] = True
[PROOF STEP]
by simp


[STATEMENT]
lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))
[PROOF STEP]
by(induction zs) auto


[STATEMENT]
lemma uniformly_convergent_minus:
  "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
      uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uniformly_convergent_on A f; uniformly_convergent_on A g\<rbrakk> \<Longrightarrow> uniformly_convergent_on A (\<lambda>k x. f k x - g k x)
[PROOF STEP]
unfolding uniformly_convergent_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>l. uniform_limit A f l sequentially; \<exists>l. uniform_limit A g l sequentially\<rbrakk> \<Longrightarrow> \<exists>l. uniform_limit A (\<lambda>k x. f k x - g k x) l sequentially
[PROOF STEP]
by (blast dest: uniform_limit_minus)


[STATEMENT]
lemma emeasure_lborel_box_eq:
  "emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure lborel (box l u) = ennreal (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then prod ((\<bullet>) (u - l)) Basis else 0)
[PROOF STEP]
using box_eq_empty(1)[THEN iffD2, of u l]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>Basis. u \<bullet> i \<le> l \<bullet> i \<Longrightarrow> box l u = {}

goal (1 subgoal):
 1. emeasure lborel (box l u) = ennreal (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then prod ((\<bullet>) (u - l)) Basis else 0)
[PROOF STEP]
by (auto simp: not_le dest!: less_imp_le) force


[STATEMENT]
lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
have "emeasure lborel (cbox a b - box a b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure lborel (cbox a b - box a b) = 0
[PROOF STEP]
by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox)
[PROOF STATE]
proof (state)
this:
emeasure lborel (cbox a b - box a b) = 0

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure lborel (cbox a b - box a b) = 0
[PROOF STEP]
have "cbox a b - box a b \<in> null_sets lborel"
[PROOF STATE]
proof (prove)
using this:
emeasure lborel (cbox a b - box a b) = 0

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
by (auto simp: null_sets_def)
[PROOF STATE]
proof (state)
this:
cbox a b - box a b \<in> null_sets lborel

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cbox a b - box a b \<in> null_sets lborel

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
by (auto dest!: AE_not_in)
[PROOF STATE]
proof (state)
this:
cbox a b - box a b \<in> null_sets lborel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sets_lebesgue_inner_closed:
  fixes e::real
  assumes "S \<in> sets lebesgue" "e > 0"
  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "emeasure lebesgue (S - T) < ennreal e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "-S \<in> sets lebesgue"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - S \<in> sets lebesgue
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S \<in> sets lebesgue
0 < e

goal (1 subgoal):
 1. - S \<in> sets lebesgue
[PROOF STEP]
by (simp add: Compl_in_sets_lebesgue)
[PROOF STATE]
proof (state)
this:
- S \<in> sets lebesgue

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- S \<in> sets lebesgue
[PROOF STEP]
obtain T where "open T" "-S \<subseteq> T"
          and T: "(T - -S) \<in> lmeasurable" "emeasure lebesgue (T - -S) < e"
[PROOF STATE]
proof (prove)
using this:
- S \<in> sets lebesgue

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>open T; - S \<subseteq> T; T - - S \<in> lmeasurable; emeasure lebesgue (T - - S) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sets_lebesgue_outer_open assms
[PROOF STATE]
proof (prove)
using this:
- S \<in> sets lebesgue
\<lbrakk>?S \<in> sets lebesgue; 0 < ?e; \<And>T. \<lbrakk>open T; ?S \<subseteq> T; T - ?S \<in> lmeasurable; emeasure lebesgue (T - ?S) < ennreal ?e\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
S \<in> sets lebesgue
0 < e

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>open T; - S \<subseteq> T; T - - S \<in> lmeasurable; emeasure lebesgue (T - - S) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open T
- S \<subseteq> T
T - - S \<in> lmeasurable
emeasure lebesgue (T - - S) < ennreal e

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>closed T; T \<subseteq> S; S - T \<in> lmeasurable; emeasure lebesgue (S - T) < ennreal e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. closed ?T
 2. ?T \<subseteq> S
 3. S - ?T \<in> lmeasurable
 4. emeasure lebesgue (S - ?T) < ennreal e
[PROOF STEP]
show "closed (-T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (- T)
[PROOF STEP]
using \<open>open T\<close>
[PROOF STATE]
proof (prove)
using this:
open T

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

goal (3 subgoals):
 1. - T \<subseteq> S
 2. S - - T \<in> lmeasurable
 3. emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
show "-T \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - T \<subseteq> S
[PROOF STEP]
using \<open>- S \<subseteq> T\<close>
[PROOF STATE]
proof (prove)
using this:
- S \<subseteq> T

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

goal (2 subgoals):
 1. S - - T \<in> lmeasurable
 2. emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
show "S - ( -T) \<in> lmeasurable" "emeasure lebesgue (S - (- T)) < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - - T \<in> lmeasurable &&& emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
using T
[PROOF STATE]
proof (prove)
using this:
T - - S \<in> lmeasurable
emeasure lebesgue (T - - S) < ennreal e

goal (1 subgoal):
 1. S - - T \<in> lmeasurable &&& emeasure lebesgue (S - - T) < ennreal e
[PROOF STEP]
by (auto simp: Int_commute)
[PROOF STATE]
proof (state)
this:
S - - T \<in> lmeasurable
emeasure lebesgue (S - - T) < ennreal e

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sets_Collect_Cauchy[measurable]:
  fixes f :: "nat \<Rightarrow> 'a => 'b::{metric_space, second_countable_topology}"
  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
  shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. Cauchy (\<lambda>i. f i x)} \<in> sets M
[PROOF STEP]
unfolding metric_Cauchy_iff2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. \<forall>j. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < inverse (real (Suc j))} \<in> sets M
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f ?i \<in> borel_measurable M

goal (1 subgoal):
 1. {x \<in> space M. \<forall>j. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < inverse (real (Suc j))} \<in> sets M
[PROOF STEP]
by auto


[STATEMENT]
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> M < {#}
[PROOF STEP]
using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M
[PROOF STATE]
proof (prove)
using this:
(?n \<subseteq># {#}) = (?n = {#})
(?M < ?N) = multp (<) ?M ?N
multp ?r ?M ?N = ((?M, ?N) \<in> mult {(x, y). ?r x y})
(?M < ?N) = (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># ?N \<and> ?M = ?N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))

goal (1 subgoal):
 1. \<not> M < {#}
[PROOF STEP]
by blast


[STATEMENT]
lemma int_pow_def2: "a [^]\<^bsub>G\<^esub> z =
   (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> (nat (-z))) else a [^]\<^bsub>G\<^esub> (nat z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^]\<^bsub>G\<^esub> z = (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> nat (- z)) else a [^]\<^bsub>G\<^esub> nat z)
[PROOF STEP]
by (simp add: int_pow_def nat_pow_def)


[STATEMENT]
lemma succs_iexec1:
  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
  shows "fst c' \<in> succs P 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst c' \<in> succs P 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c' = iexec (P !! i) (i, s, stk)
0 \<le> i
i < size P

goal (1 subgoal):
 1. fst c' \<in> succs P 0
[PROOF STEP]
by (auto simp: succs_def isuccs_def split: instr.split)


[STATEMENT]
lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lub Y cl \<in> A
[PROOF STEP]
by (rule Y_subset_A [THEN lub_in_lattice])


[STATEMENT]
lemma (in domain) ring_iso_imp_img_domain:
  assumes "h \<in> ring_iso R S"
  shows "domain (S \<lparr> zero := h \<zero> \<rparr>)" (is "domain ?h_img")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
note aux = m_closed integral one_not_zero one_closed zero_closed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> carrier R; ?y \<in> carrier R\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier R
\<lbrakk>?a \<otimes> ?b = \<zero>; ?a \<in> carrier R; ?b \<in> carrier R\<rbrakk> \<Longrightarrow> ?a = \<zero> \<or> ?b = \<zero>
\<one> \<noteq> \<zero>
\<one> \<in> carrier R
\<zero> \<in> carrier R

goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
interpret h_img?: cring ?h_img
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
using ring_iso_imp_img_cring[OF assms]
[PROOF STATE]
proof (prove)
using this:
cring (S\<lparr>zero := h \<zero>\<rparr>)

goal (1 subgoal):
 1. cring (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
proof (unfold_locales)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
have "\<one>\<^bsub>?h_img\<^esub> = \<zero>\<^bsub>?h_img\<^esub> \<Longrightarrow> h \<one> = h \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
[PROOF STEP]
using ring_iso_memE(4)[OF assms]
[PROOF STATE]
proof (prove)
using this:
h \<one> = \<one>\<^bsub>S\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>

goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>

goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
have "h \<one> \<noteq> h \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<one> \<noteq> h \<zero>
[PROOF STEP]
using ring_iso_memE(5)[OF assms] aux(3-4)
[PROOF STATE]
proof (prove)
using this:
bij_betw h (carrier R) (carrier S)
\<one> \<noteq> \<zero>
\<one> \<in> carrier R

goal (1 subgoal):
 1. h \<one> \<noteq> h \<zero>
[PROOF STEP]
unfolding bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. h x = h y \<longrightarrow> x = y) \<and> h ` carrier R = carrier S
\<one> \<noteq> \<zero>
\<one> \<in> carrier R

goal (1 subgoal):
 1. h \<one> \<noteq> h \<zero>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
h \<one> \<noteq> h \<zero>

goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
h \<one> \<noteq> h \<zero>
[PROOF STEP]
show "\<one>\<^bsub>?h_img\<^esub> \<noteq> \<zero>\<^bsub>?h_img\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
h \<one> \<noteq> h \<zero>

goal (1 subgoal):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
assume A: "a \<otimes>\<^bsub>?h_img\<^esub> b = \<zero>\<^bsub>?h_img\<^esub>" "a \<in> carrier ?h_img" "b \<in> carrier ?h_img"
[PROOF STATE]
proof (state)
this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
obtain r1 r2
      where r1: "r1 \<in> carrier R" "a = h r1"
        and r2: "r2 \<in> carrier R" "b = h r2"
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> carrier R; a = h r1; r2 \<in> carrier R; b = h r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms image_iff[where ?f = h and ?A = "carrier R"]
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
h \<in> ring_iso R S
(?z \<in> h ` carrier R) = (\<exists>x\<in>carrier R. ?z = h x)

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> carrier R; a = h r1; r2 \<in> carrier R; b = h r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ring_iso_def bij_betw_def
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
h \<in> {h \<in> ring_hom R S. inj_on h (carrier R) \<and> h ` carrier R = carrier S}
(?z \<in> h ` carrier R) = (\<exists>x\<in>carrier R. ?z = h x)

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> carrier R; a = h r1; r2 \<in> carrier R; b = h r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "a \<otimes>\<^bsub>?h_img\<^esub> b = h (r1 \<otimes> r2)"
[PROOF STATE]
proof (prove)
using this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
[PROOF STEP]
using assms r1 r2
[PROOF STATE]
proof (prove)
using this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2
h \<in> ring_iso R S
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
[PROOF STEP]
unfolding ring_iso_def ring_hom_def
[PROOF STATE]
proof (prove)
using this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2
h \<in> {h \<in> {h \<in> carrier R \<rightarrow> carrier S. (\<forall>x y. x \<in> carrier R \<and> y \<in> carrier R \<longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y \<and> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) \<and> h \<one> = \<one>\<^bsub>S\<^esub>}. bij_betw h (carrier R) (carrier S)}
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "h (r1 \<otimes> r2) = h \<zero>"
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)

goal (1 subgoal):
 1. h (r1 \<otimes> r2) = h \<zero>
[PROOF STEP]
using A(1)
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>

goal (1 subgoal):
 1. h (r1 \<otimes> r2) = h \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h (r1 \<otimes> r2) = h \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "r1 \<otimes> r2 = \<zero>"
[PROOF STATE]
proof (prove)
using this:
h (r1 \<otimes> r2) = h \<zero>

goal (1 subgoal):
 1. r1 \<otimes> r2 = \<zero>
[PROOF STEP]
using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5)
[PROOF STATE]
proof (prove)
using this:
h (r1 \<otimes> r2) = h \<zero>
bij_betw h (carrier R) (carrier S)
r1 \<otimes> r2 \<in> carrier R
\<zero> \<in> carrier R

goal (1 subgoal):
 1. r1 \<otimes> r2 = \<zero>
[PROOF STEP]
unfolding bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
h (r1 \<otimes> r2) = h \<zero>
(\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. h x = h y \<longrightarrow> x = y) \<and> h ` carrier R = carrier S
r1 \<otimes> r2 \<in> carrier R
\<zero> \<in> carrier R

goal (1 subgoal):
 1. r1 \<otimes> r2 = \<zero>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
r1 \<otimes> r2 = \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "r1 = \<zero> \<or> r2 = \<zero>"
[PROOF STATE]
proof (prove)
using this:
r1 \<otimes> r2 = \<zero>

goal (1 subgoal):
 1. r1 = \<zero> \<or> r2 = \<zero>
[PROOF STEP]
using aux(2)[OF _ r1(1) r2(1)]
[PROOF STATE]
proof (prove)
using this:
r1 \<otimes> r2 = \<zero>
r1 \<otimes> r2 = \<zero> \<Longrightarrow> r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. r1 = \<zero> \<or> r2 = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
thus "a = \<zero>\<^bsub>?h_img\<^esub> \<or> b = \<zero>\<^bsub>?h_img\<^esub>"
[PROOF STATE]
proof (prove)
using this:
r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
unfolding r1 r2
[PROOF STATE]
proof (prove)
using this:
r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. h r1 = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> h r2 = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain (S\<lparr>zero := h \<zero>\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma leadsTo_Union:
    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. A \<in> S \<Longrightarrow> F \<in> A \<longmapsto> B) \<Longrightarrow> F \<in> \<Union> S \<longmapsto> B
[PROOF STEP]
apply (unfold leadsTo_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. A \<in> S \<Longrightarrow> F \<in> {F. (A, B) \<in> leads F}) \<Longrightarrow> F \<in> {F. (\<Union> S, B) \<in> leads F}
[PROOF STEP]
apply (blast intro: leads.Union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "x \<in> undefinedSet"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> undefinedSet
[PROOF STEP]
nitpick [expect = genuine]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> undefinedSet
[PROOF STEP]
oops


[STATEMENT]
lemma smallo_real_nat_transfer:
  "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> o(g) \<Longrightarrow> (\<lambda>x. f (real x)) \<in> o(\<lambda>x. g (real x))
[PROOF STEP]
by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])


[STATEMENT]
lemma asymp_equiv_transfer:
  assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
  shows   "f2 \<sim>[F] g2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2 \<sim>[F] g2
[PROOF STEP]
using assms(1) asymp_equiv_cong[OF assms(2,3)]
[PROOF STATE]
proof (prove)
using this:
f1 \<sim>[F] g1
(f1 \<sim>[F] g1) = (f2 \<sim>[F] g2)

goal (1 subgoal):
 1. f2 \<sim>[F] g2
[PROOF STEP]
by simp


[STATEMENT]
lemma continuous_on_components:
 fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
  assumes "locally connected S " "\<And>C. C \<in> components S \<Longrightarrow> continuous_on C f"
  shows "continuous_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
proof (rule continuous_on_components_gen)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
assume "C \<in> components S"
[PROOF STATE]
proof (state)
this:
C \<in> components S

goal (1 subgoal):
 1. \<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> components S
[PROOF STEP]
show "openin (top_of_set S) C \<and> continuous_on C f"
[PROOF STATE]
proof (prove)
using this:
C \<in> components S

goal (1 subgoal):
 1. openin (top_of_set S) C \<and> continuous_on C f
[PROOF STEP]
by (simp add: assms openin_components_locally_connected)
[PROOF STATE]
proof (state)
this:
openin (top_of_set S) C \<and> continuous_on C f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nullhomotopic_from_contractible_space:
  assumes f: "continuous_map X Y f" and X: "contractible_space X"
  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nullhomotopic_through_contractible_space [OF _ f X]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_map ?X X ?f; \<And>c. homotopic_with (\<lambda>h. True) ?X Y (f \<circ> ?f) (\<lambda>x. c) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c. homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis comp_id continuous_map_id)


[STATEMENT]
lemma length_compTpExpr_Exprs [rule_format]: "
  (\<forall>sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
  \<and> (\<forall>sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>sttp. length (fst (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)) \<and> (\<forall>sttp. length (fst (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs))
[PROOF STEP]
apply (rule compat_expr_expr_list.induct)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (NewC x) sttp)) = length (compExpr jmb (NewC x))
 2. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (Cast x1 x2) sttp)) = length (compExpr jmb (Cast x1 x2))
 3. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (Lit x) sttp)) = length (compExpr jmb (Lit x))
 4. \<And>x1 x2 x3. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x3 sttp)) = length (compExpr jmb x3)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp x1 x2 x3) sttp)) = length (compExpr jmb (BinOp x1 x2 x3))
 5. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (LAcc x) sttp)) = length (compExpr jmb (LAcc x))
 6. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (x1::=x2) sttp)) = length (compExpr jmb (x1::=x2))
 7. \<And>x1 x2 x3. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3) sttp)) = length (compExpr jmb ({x1}x2..x3))
 8. \<And>x1 x2 x3 x4. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x4 sttp)) = length (compExpr jmb x4)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3:=x4) sttp)) = length (compExpr jmb ({x1}x2..x3:=x4))
 9. \<And>x1 x2 x3 x4 x5. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExprs jmb G x5 sttp)) = length (compExprs jmb x5)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3( {x4}x5)) sttp)) = length (compExpr jmb ({x1}x2..x3( {x4}x5)))
 10. \<forall>sttp. length (fst (compTpExprs jmb G [] sttp)) = length (compExprs jmb [])
A total of 11 subgoals...
[PROOF STEP]
apply (simp_all)[3]
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x3 sttp)) = length (compExpr jmb x3)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp x1 x2 x3) sttp)) = length (compExpr jmb (BinOp x1 x2 x3))
 2. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (LAcc x) sttp)) = length (compExpr jmb (LAcc x))
 3. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (x1::=x2) sttp)) = length (compExpr jmb (x1::=x2))
 4. \<And>x1 x2 x3. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3) sttp)) = length (compExpr jmb ({x1}x2..x3))
 5. \<And>x1 x2 x3 x4. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x4 sttp)) = length (compExpr jmb x4)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3:=x4) sttp)) = length (compExpr jmb ({x1}x2..x3:=x4))
 6. \<And>x1 x2 x3 x4 x5. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExprs jmb G x5 sttp)) = length (compExprs jmb x5)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3( {x4}x5)) sttp)) = length (compExpr jmb ({x1}x2..x3( {x4}x5)))
 7. \<forall>sttp. length (fst (compTpExprs jmb G [] sttp)) = length (compExprs jmb [])
 8. \<And>x1 x2. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x1 sttp)) = length (compExpr jmb x1); \<forall>sttp. length (fst (compTpExprs jmb G x2 sttp)) = length (compExprs jmb x2)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExprs jmb G (x1 # x2) sttp)) = length (compExprs jmb (x1 # x2))
[PROOF STEP]
apply (rename_tac binop a b, case_tac binop)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>binop a b. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G a sttp)) = length (compExpr jmb a); \<forall>sttp. length (fst (compTpExpr jmb G b sttp)) = length (compExpr jmb b); binop = Eq\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp binop a b) sttp)) = length (compExpr jmb (BinOp binop a b))
 2. \<And>binop a b. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G a sttp)) = length (compExpr jmb a); \<forall>sttp. length (fst (compTpExpr jmb G b sttp)) = length (compExpr jmb b); binop = Add\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp binop a b) sttp)) = length (compExpr jmb (BinOp binop a b))
 3. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (LAcc x) sttp)) = length (compExpr jmb (LAcc x))
 4. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (x1::=x2) sttp)) = length (compExpr jmb (x1::=x2))
 5. \<And>x1 x2 x3. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3) sttp)) = length (compExpr jmb ({x1}x2..x3))
 6. \<And>x1 x2 x3 x4. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x4 sttp)) = length (compExpr jmb x4)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3:=x4) sttp)) = length (compExpr jmb ({x1}x2..x3:=x4))
 7. \<And>x1 x2 x3 x4 x5. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExprs jmb G x5 sttp)) = length (compExprs jmb x5)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3( {x4}x5)) sttp)) = length (compExpr jmb ({x1}x2..x3( {x4}x5)))
 8. \<forall>sttp. length (fst (compTpExprs jmb G [] sttp)) = length (compExprs jmb [])
 9. \<And>x1 x2. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x1 sttp)) = length (compExpr jmb x1); \<forall>sttp. length (fst (compTpExprs jmb G x2 sttp)) = length (compExprs jmb x2)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExprs jmb G (x1 # x2) sttp)) = length (compExprs jmb (x1 # x2))
[PROOF STEP]
apply (auto simp add: pushST_def split_beta)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Auth_A_to_B_lemma [rule_format]:
     "evs \<in> yahalom
      \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow>
          K \<in> symKeys \<longrightarrow>
          Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow>
          Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>
            \<in> parts (knows Spy evs) \<longrightarrow>
          B \<notin> bad \<longrightarrow>
          (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> yahalom \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)
[PROOF STEP]
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>evsf X Ba. \<lbrakk>evsf \<in> yahalom; Key K \<notin> analz (knows Spy evsf) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsf) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsf); X \<in> synth (analz (knows Spy evsf))\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Spy Ba X # evsf))
 2. \<And>evsr Aa Ba X. \<lbrakk>evsr \<in> yahalom; Key K \<notin> analz (knows Spy evsr) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsr) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsr) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsr); Says Aa Ba X \<in> set evsr\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Gets Ba X # evsr)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Gets Ba X # evsr)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Gets Ba X # evsr)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set (Gets Ba X # evsr))
 3. \<And>evs1 NA Aa Ba. \<lbrakk>evs1 \<in> yahalom; Key K \<notin> analz (knows Spy evs1) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs1) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs1) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs1); Nonce NA \<notin> used evs1\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> # evs1))
 4. \<And>evs2 NBa Ba Aa NA. \<lbrakk>evs2 \<in> yahalom; Key K \<notin> analz (knows Spy evs2) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs2) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs2); Nonce NBa \<notin> used evs2; Gets Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Ba Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> # evs2))
 5. \<And>evs3 KAB Ba NBa Aa NA. \<lbrakk>evs3 \<in> yahalom; Key K \<notin> analz (knows Spy evs3) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3); Key KAB \<notin> used evs3; Gets Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> \<in> set evs3\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key KAB, Nonce NA\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent Aa, Agent Ba, Key KAB, Nonce NBa\<rbrace>\<rbrace> # evs3))
 6. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Key K \<notin> analz (knows Spy evs4) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4); Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> \<Longrightarrow> evs4 \<in> yahalom
 7. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Key K \<notin> analz (knows Spy evs4) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4); Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4)\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set (Says Aa Ba \<lbrace>X, Crypt Ka (Nonce NBa)\<rbrace> # evs4))
 8. \<And>evso Aa NBa Ba Ka NA X. \<lbrakk>evso \<in> yahalom; Key K \<notin> analz (knows Spy evso) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evso) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evso) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evso); Says Server Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evso\<rbrakk> \<Longrightarrow> Key K \<notin> analz (knows Spy (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso)) \<longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set (Notes Spy \<lbrace>Nonce NA, Nonce NBa, Key Ka\<rbrace> # evso))
[PROOF STEP]
apply (analz_mono_contra, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evsf X Ba. \<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)); Key K \<notin> analz (knows Spy evsf); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsf) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Spy \<and> B = Ba \<and> \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> = X \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evsf)
 2. \<And>evs3 KAB Ba NBa Aa NA. \<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; Gets Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> \<in> set evs3; Key K \<notin> analz (knows Spy evs3); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> B = Ba \<and> A = Aa \<and> B = Ba \<and> K = KAB \<and> NB = NBa \<longrightarrow> Ba \<notin> bad \<longrightarrow> (\<exists>X. Says Aa Ba \<lbrace>X, Crypt KAB (Nonce NBa)\<rbrace> \<in> set evs3)
 3. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4); Key K \<notin> analz (knows Spy evs4); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka \<and> NB = NBa \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka, Nonce NBa\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<or> Says A B \<lbrace>Xa, Crypt Ka (Nonce NBa)\<rbrace> \<in> set evs4)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<and> K = Ka \<and> NB = NBa \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4))
[PROOF STEP]
subgoal \<comment> \<open>Fake\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evsf_ \<in> yahalom; X_ \<in> synth (analz (knows Spy evsf_)); Key K \<notin> analz (knows Spy evsf_); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evsf_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evsf_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evsf_)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (insert X_ (knows Spy evsf_)) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (insert X_ (knows Spy evsf_)) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Spy \<and> B = Ba_ \<and> \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> = X_ \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evsf_)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>evs3 KAB Ba NBa Aa NA. \<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; Gets Server \<lbrace>Agent Ba, Nonce NBa, Crypt (shrK Ba) \<lbrace>Agent Aa, Nonce NA\<rbrace>\<rbrace> \<in> set evs3; Key K \<notin> analz (knows Spy evs3); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3) \<longrightarrow> B = Ba \<and> A = Aa \<and> B = Ba \<and> K = KAB \<and> NB = NBa \<longrightarrow> Ba \<notin> bad \<longrightarrow> (\<exists>X. Says Aa Ba \<lbrace>X, Crypt KAB (Nonce NBa)\<rbrace> \<in> set evs3)
 2. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4); Key K \<notin> analz (knows Spy evs4); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka \<and> NB = NBa \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka, Nonce NBa\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<or> Says A B \<lbrace>Xa, Crypt Ka (Nonce NBa)\<rbrace> \<in> set evs4)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<and> K = Ka \<and> NB = NBa \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4))
[PROOF STEP]
subgoal \<comment> \<open>YM3 because the message \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs3_ \<in> yahalom; Key KAB_ \<notin> used evs3_; Gets Server \<lbrace>Agent Ba_, Nonce NBa_, Crypt (shrK Ba_) \<lbrace>Agent Aa_, Nonce NA_\<rbrace>\<rbrace> \<in> set evs3_; Key K \<notin> analz (knows Spy evs3_); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs3_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs3_)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs3_) \<longrightarrow> B = Ba_ \<and> A = Aa_ \<and> B = Ba_ \<and> K = KAB_ \<and> NB = NBa_ \<longrightarrow> Ba_ \<notin> bad \<longrightarrow> (\<exists>X. Says Aa_ Ba_ \<lbrace>X, Crypt KAB_ (Nonce NBa_)\<rbrace> \<in> set evs3_)
[PROOF STEP]
by (force dest!: Crypt_imp_keysFor)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Aa NBa Ba Ka NA X. \<lbrakk>evs4 \<in> yahalom; Gets Aa \<lbrace>Nonce NBa, Crypt (shrK Aa) \<lbrace>Agent Ba, Key Ka, Nonce NA\<rbrace>, X\<rbrace> \<in> set evs4; Says Aa Ba \<lbrace>Agent Aa, Nonce NA\<rbrace> \<in> set evs4; X \<in> parts (knows Spy evs4); Key K \<notin> analz (knows Spy evs4); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka \<and> NB = NBa \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka, Nonce NBa\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<or> Says A B \<lbrace>Xa, Crypt Ka (Nonce NBa)\<rbrace> \<in> set evs4)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa \<and> B = Ba \<and> Xa = X \<and> K = Ka \<and> NB = NBa \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4))
[PROOF STEP]
subgoal \<comment> \<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? If not, use the induction hypothesis,
             otherwise by unicity of session keys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs4_ \<in> yahalom; Gets Aa_ \<lbrace>Nonce NBa_, Crypt (shrK Aa_) \<lbrace>Agent Ba_, Key Ka_, Nonce NA_\<rbrace>, X_\<rbrace> \<in> set evs4_; Says Aa_ Ba_ \<lbrace>Agent Aa_, Nonce NA_\<rbrace> \<in> set evs4_; X_ \<in> parts (knows Spy evs4_); Key K \<notin> analz (knows Spy evs4_); K \<in> symKeys \<longrightarrow> Crypt K (Nonce NB) \<in> parts (knows Spy evs4_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs4_)\<rbrakk> \<Longrightarrow> K \<in> symKeys \<longrightarrow> (K = Ka_ \<and> NB = NBa_ \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key Ka_, Nonce NBa_\<rbrace> \<in> parts (knows Spy evs4_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa_ \<and> B = Ba_ \<and> Xa = X_ \<or> Says A B \<lbrace>Xa, Crypt Ka_ (Nonce NBa_)\<rbrace> \<in> set evs4_)) \<and> (Crypt K (Nonce NB) \<in> parts (knows Spy evs4_) \<longrightarrow> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> \<in> parts (knows Spy evs4_) \<longrightarrow> B \<notin> bad \<longrightarrow> (\<exists>Xa. A = Aa_ \<and> B = Ba_ \<and> Xa = X_ \<and> K = Ka_ \<and> NB = NBa_ \<or> Says A B \<lbrace>Xa, Crypt K (Nonce NB)\<rbrace> \<in> set evs4_))
[PROOF STEP]
by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)
[PROOF STEP]
by (auto simp add: prefix_def)


[STATEMENT]
lemma prefixes_append:
  "prefixes (xs @ ys) = prefixes xs @ map (\<lambda>ys'. xs @ ys') (tl (prefixes ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys))
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))
 2. \<And>a xs. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys)) \<Longrightarrow> prefixes ((a # xs) @ ys) = prefixes (a # xs) @ map ((@) (a # xs)) (tl (prefixes ys))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))
 2. \<And>a xs. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys)) \<Longrightarrow> prefixes ((a # xs) @ ys) = prefixes (a # xs) @ map ((@) (a # xs)) (tl (prefixes ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))
[PROOF STEP]
by (cases ys) auto
[PROOF STATE]
proof (state)
this:
prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))

goal (1 subgoal):
 1. \<And>a xs. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys)) \<Longrightarrow> prefixes ((a # xs) @ ys) = prefixes (a # xs) @ map ((@) (a # xs)) (tl (prefixes ys))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma right_total_semigroup_add_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total A" "bi_unique A"
  shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add
[PROOF STEP]
proof (intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (A ===> A ===> A) x y \<Longrightarrow> semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (A ===> A ===> A) x y \<Longrightarrow> semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
assume xy[transfer_rule]: "(A ===> A ===> A) x y"
[PROOF STATE]
proof (state)
this:
(A ===> A ===> A) x y

goal (1 subgoal):
 1. \<And>x y. (A ===> A ===> A) x y \<Longrightarrow> semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
show "semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
unfolding semigroup_add_on_with_def class.semigroup_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>a b c. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> c \<in> Collect (Domainp A) \<longrightarrow> x (x a b) c = x a (x b c)) \<and> (\<forall>a b. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> x a b \<in> Collect (Domainp A))) = (\<forall>a b c. y (y a b) c = y a (y b c))
[PROOF STEP]
by transfer (auto intro!: Domainp_apply2I[OF xy])
[PROOF STATE]
proof (state)
this:
semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ln_inverse: assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0" shows "Ln(inverse z) = -(Ln z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (inverse z) = - Ln z
[PROOF STEP]
proof (cases "z=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Ln (inverse z) = - Ln z
 2. z \<noteq> 0 \<Longrightarrow> Ln (inverse z) = - Ln z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Ln (inverse z) = - Ln z
 2. z \<noteq> 0 \<Longrightarrow> Ln (inverse z) = - Ln z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (inverse z) = - Ln z
[PROOF STEP]
proof (rule exp_complex_eqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
have "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>
[PROOF STEP]
by (rule abs_triangle_ineq4)
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>

goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>

goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
have "\<dots> < pi + pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
have "\<bar>Im (Ln (inverse z))\<bar> < pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> < pi
[PROOF STEP]
by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> < pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> < pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
have "\<bar>Im (- Ln z)\<bar> \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Im (- Ln z)\<bar> \<le> pi
[PROOF STEP]
using False Im_Ln_le_pi mpi_less_Im_Ln
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
?z \<noteq> 0 \<Longrightarrow> Im (Ln ?z) \<le> pi
?z \<noteq> 0 \<Longrightarrow> - pi < Im (Ln ?z)

goal (1 subgoal):
 1. \<bar>Im (- Ln z)\<bar> \<le> pi
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<bar>Im (- Ln z)\<bar> \<le> pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>Im (Ln (inverse z))\<bar> < pi
\<bar>Im (- Ln z)\<bar> \<le> pi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>Im (Ln (inverse z))\<bar> < pi
\<bar>Im (- Ln z)\<bar> \<le> pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar> < pi + pi

goal (2 subgoals):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
 2. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < pi + pi
[PROOF STEP]
show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
[PROOF STATE]
proof (prove)
using this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < pi + pi

goal (1 subgoal):
 1. \<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi

goal (1 subgoal):
 1. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
show "exp (Ln (inverse z)) = exp (- Ln z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (Ln (inverse z)) = exp (- Ln z)
[PROOF STEP]
by (simp add: False exp_minus)
[PROOF STATE]
proof (state)
this:
exp (Ln (inverse z)) = exp (- Ln z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ln (inverse z) = - Ln z

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> Ln (inverse z) = - Ln z
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
have  "Ln(-\<i>) = Ln(inverse \<i>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (- \<i>) = Ln (inverse \<i>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ln (- \<i>) = Ln (inverse \<i>)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ln (- \<i>) = Ln (inverse \<i>)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
have "\<dots> = - (Ln \<i>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ln (inverse \<i>) = - Ln \<i>
[PROOF STEP]
using Ln_inverse
[PROOF STATE]
proof (prove)
using this:
?z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln (inverse ?z) = - Ln ?z

goal (1 subgoal):
 1. Ln (inverse \<i>) = - Ln \<i>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ln (inverse \<i>) = - Ln \<i>

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ln (inverse \<i>) = - Ln \<i>

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
have "\<dots> = - (\<i> * pi/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Ln \<i> = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- Ln \<i> = - (\<i> * complex_of_real pi / 2)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)

goal (1 subgoal):
 1. Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Ln (- \<i>) = - (\<i> * complex_of_real pi / 2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Arg_exp: "-pi < Im z \<Longrightarrow> Im z \<le> pi \<Longrightarrow> Arg(exp z) = Im z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- pi < Im z; Im z \<le> pi\<rbrakk> \<Longrightarrow> Arg (exp z) = Im z
[PROOF STEP]
by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)


[STATEMENT]
lemma pi_gt3: "pi > 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 < pi
[PROOF STEP]
using pi_approx
[PROOF STATE]
proof (prove)
using this:
3141592653588 / 10 ^ 12 \<le> pi
pi \<le> 31415926535899 / 10 ^ 13

goal (1 subgoal):
 1. 3 < pi
[PROOF STEP]
by simp