[STATEMENT]
lemma less_eq_multiset_empty_right[simp]: "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}
[PROOF STEP]
by (metis less_eq_multiset_empty_left antisym)


[STATEMENT]
lemma Rat_induct_pos [case_names Fract, induct type: rat]:
  assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)"
  shows "P q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P q
[PROOF STEP]
proof (cases q)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>q = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
case (Fract a b)
[PROOF STATE]
proof (state)
this:
q = Fract a b
0 < b
coprime a b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>q = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
have step': "P (Fract a b)" if b: "b < 0" for a b :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
b < 0
[PROOF STEP]
have "0 < - b"
[PROOF STATE]
proof (prove)
using this:
b < 0

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

goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < - b
[PROOF STEP]
have "P (Fract (- a) (- b))"
[PROOF STATE]
proof (prove)
using this:
0 < - b

goal (1 subgoal):
 1. P (Fract (- a) (- b))
[PROOF STEP]
by (rule step)
[PROOF STATE]
proof (state)
this:
P (Fract (- a) (- b))

goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P (Fract (- a) (- b))
[PROOF STEP]
show "P (Fract a b)"
[PROOF STATE]
proof (prove)
using this:
P (Fract (- a) (- b))

goal (1 subgoal):
 1. P (Fract a b)
[PROOF STEP]
by (simp add: order_less_imp_not_eq [OF b])
[PROOF STATE]
proof (state)
this:
P (Fract a b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?b < 0 \<Longrightarrow> P (Fract ?a ?b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>q = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> P q
[PROOF STEP]
from Fract
[PROOF STATE]
proof (chain)
picking this:
q = Fract a b
0 < b
coprime a b
[PROOF STEP]
show "P q"
[PROOF STATE]
proof (prove)
using this:
q = Fract a b
0 < b
coprime a b

goal (1 subgoal):
 1. P q
[PROOF STEP]
by (auto simp add: linorder_neq_iff step step')
[PROOF STATE]
proof (state)
this:
P q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int z \<in> \<rat>
[PROOF STEP]
by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat)


[STATEMENT]
lemma rat_minus_code [code abstract]:
  "quotient_of (p - q) =
    (let (a, c) = quotient_of p; (b, d) = quotient_of q
     in normalize (a * d - b * c, c * d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q in Rat.normalize (a * d - b * c, c * d))
[PROOF STEP]
by (cases p, cases q) (simp add: quotient_of_Fract)


[STATEMENT]
lemma graph_map_of_if_distinct_dom: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al
[PROOF STEP]
unfolding graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> {(a, b) |a b. map_of al a = Some b} = set al
[PROOF STEP]
by auto


[STATEMENT]
lemma empty_code [code]:
  "empty = Lazy_Sequence (\<lambda>_. None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lazy_Sequence.empty = Lazy_Sequence Map.empty
[PROOF STEP]
by (simp add: lazy_sequence_eq_iff)


[STATEMENT]
lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (n div x) \<le> real n / real x
[PROOF STEP]
using real_of_nat_div2 [of n x]
[PROOF STATE]
proof (prove)
using this:
0 \<le> real n / real x - real (n div x)

goal (1 subgoal):
 1. real (n div x) \<le> real n / real x
[PROOF STEP]
by simp


[STATEMENT]
lemma Rats_dense_in_real:
  fixes x :: real
  assumes "x < y"
  shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from \<open>x < y\<close>
[PROOF STATE]
proof (chain)
picking this:
x < y
[PROOF STEP]
have "0 < y - x"
[PROOF STATE]
proof (prove)
using this:
x < y

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

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
with reals_Archimedean
[PROOF STATE]
proof (chain)
picking this:
(0::?'a) < ?x \<Longrightarrow> \<exists>n. inverse (of_nat (Suc n)) < ?x
0 < y - x
[PROOF STEP]
obtain q :: nat where q: "inverse (real q) < y - x" and "0 < q"
[PROOF STATE]
proof (prove)
using this:
(0::?'a) < ?x \<Longrightarrow> \<exists>n. inverse (of_nat (Suc n)) < ?x
0 < y - x

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>inverse (real q) < y - x; 0 < q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverse (real q) < y - x
0 < q

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
define p where "p = \<lceil>y * real q\<rceil> - 1"
[PROOF STATE]
proof (state)
this:
p = \<lceil>y * real q\<rceil> - 1

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
define r where "r = of_int p / real q"
[PROOF STATE]
proof (state)
this:
r = real_of_int p / real q

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
inverse (real q) < y - x
[PROOF STEP]
have "x < y - inverse (real q)"
[PROOF STATE]
proof (prove)
using this:
inverse (real q) < y - x

goal (1 subgoal):
 1. x < y - inverse (real q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y - inverse (real q)

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y - inverse (real q)

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from \<open>0 < q\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < q
[PROOF STEP]
have "y - inverse (real q) \<le> r"
[PROOF STATE]
proof (prove)
using this:
0 < q

goal (1 subgoal):
 1. y - inverse (real q) \<le> r
[PROOF STEP]
by (simp add: r_def p_def le_divide_eq left_diff_distrib)
[PROOF STATE]
proof (state)
this:
y - inverse (real q) \<le> r

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < r
[PROOF STEP]
have "x < r"
[PROOF STATE]
proof (prove)
using this:
x < r

goal (1 subgoal):
 1. x < r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x < r

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x < r

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
from \<open>0 < q\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < q
[PROOF STEP]
have "r < y"
[PROOF STATE]
proof (prove)
using this:
0 < q

goal (1 subgoal):
 1. r < y
[PROOF STEP]
by (simp add: r_def p_def divide_less_eq diff_less_eq less_ceiling_iff [symmetric])
[PROOF STATE]
proof (state)
this:
r < y

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r < y

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
have "r \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> \<rat>
[PROOF STEP]
by (simp add: r_def)
[PROOF STATE]
proof (state)
this:
r \<in> \<rat>

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x < r
r < y
r \<in> \<rat>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < r
r < y
r \<in> \<rat>

goal (1 subgoal):
 1. \<exists>r\<in>\<rat>. x < r \<and> r < y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>\<rat>. x < r \<and> r < y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma integer_of_num [code]:
  "integer_of_num Num.One = 1"
  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integer_of_num num.One = 1 &&& integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k) &&& integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)
[PROOF STEP]
by (simp_all only: integer_of_num_def numeral.simps Let_def)


[STATEMENT]
lemma nat_of_integer_non_positive [simp]:
  "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> 0 \<Longrightarrow> nat_of_integer k = 0
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma integer_of_nat_1: "integer_of_nat 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integer_of_nat 1 = 1
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma mset_filter_mono:
  assumes "A \<subseteq># B" "\<And>x. x \<in># A \<Longrightarrow> P x \<Longrightarrow> Q x"
  shows   "filter_mset P A \<subseteq># filter_mset Q B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset P A \<subseteq># filter_mset Q B
[PROOF STEP]
by (rule mset_subset_eqI) (insert assms, auto simp: mset_subset_eq_count count_eq_zero_iff)


[STATEMENT]
lemma hd_sort:
  fixes xs :: "'a :: linorder list"
  shows "xs \<noteq> [] \<Longrightarrow> hd (sort xs) = Min (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> hd (sort xs) = Min (set xs)
[PROOF STEP]
by (subst Min_set_sorted [symmetric]) auto


[STATEMENT]
lemma AE_ball_countable:
  assumes [intro]: "countable X"
  shows "(AE x in M. \<forall>y\<in>X. P x y) \<longleftrightarrow> (\<forall>y\<in>X. AE x in M. P x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (AE x in M. \<forall>y\<in>X. P x y) = (\<forall>y\<in>X. AE x in M. P x y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
assume "\<forall>y\<in>X. AE x in M. P x y"
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>X. AE x in M. P x y

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
from this[unfolded eventually_ae_filter Bex_def, THEN bchoice]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x\<in>X. f x \<in> null_sets M \<and> {xa \<in> space M. \<not> P xa x} \<subseteq> f x
[PROOF STEP]
obtain N where N: "\<And>y. y \<in> X \<Longrightarrow> N y \<in> null_sets M" "\<And>y. y \<in> X \<Longrightarrow> {x\<in>space M. \<not> P x y} \<subseteq> N y"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x\<in>X. f x \<in> null_sets M \<and> {xa \<in> space M. \<not> P xa x} \<subseteq> f x

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<And>y. y \<in> X \<Longrightarrow> N y \<in> null_sets M; \<And>y. y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x y} \<subseteq> N y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
have "{x\<in>space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x\<in>space M. \<not> P x y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x \<in> space M. \<not> P x y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x \<in> space M. \<not> P x y})

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x \<in> space M. \<not> P x y})

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
have "\<dots> \<subseteq> (\<Union>y\<in>X. N y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>y\<in>X. {x \<in> space M. \<not> P x y}) \<subseteq> \<Union> (N ` X)
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y

goal (1 subgoal):
 1. (\<Union>y\<in>X. {x \<in> space M. \<not> P x y}) \<subseteq> \<Union> (N ` X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>y\<in>X. {x \<in> space M. \<not> P x y}) \<subseteq> \<Union> (N ` X)

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
[PROOF STEP]
have "{x\<in>space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. N y)"
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)

goal (1 subgoal):
 1. {x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y
[PROOF STEP]
have "(\<Union>y\<in>X. N y) \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
?y \<in> X \<Longrightarrow> N ?y \<in> null_sets M
?y \<in> X \<Longrightarrow> {x \<in> space M. \<not> P x ?y} \<subseteq> N ?y

goal (1 subgoal):
 1. \<Union> (N ` X) \<in> null_sets M
[PROOF STEP]
by (intro null_sets_UN') auto
[PROOF STATE]
proof (state)
this:
\<Union> (N ` X) \<in> null_sets M

goal (2 subgoals):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
 2. \<forall>y\<in>X. AE x in M. P x y \<Longrightarrow> AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
\<Union> (N ` X) \<in> null_sets M
[PROOF STEP]
show "AE x in M. \<forall>y\<in>X. P x y"
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
\<Union> (N ` X) \<in> null_sets M

goal (1 subgoal):
 1. AE x in M. \<forall>y\<in>X. P x y
[PROOF STEP]
unfolding eventually_ae_filter
[PROOF STATE]
proof (prove)
using this:
{x \<in> space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> \<Union> (N ` X)
\<Union> (N ` X) \<in> null_sets M

goal (1 subgoal):
 1. Bex (null_sets M) ((\<subseteq>) {x \<in> space M. \<not> Ball X (P x)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<forall>y\<in>X. P x y

goal (1 subgoal):
 1. AE x in M. \<forall>y\<in>X. P x y \<Longrightarrow> \<forall>y\<in>X. AE x in M. P x y
[PROOF STEP]
qed auto


[STATEMENT]
lemma (in finite_measure) finite_measure_Diff:
  assumes sets: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
  shows "measure M (A - B) = measure M A - measure M B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure M (A - B) = Sigma_Algebra.measure M A - Sigma_Algebra.measure M B
[PROOF STEP]
using measure_Diff[OF _ assms]
[PROOF STATE]
proof (prove)
using this:
emeasure M A \<noteq> \<infinity> \<Longrightarrow> Sigma_Algebra.measure M (A - B) = Sigma_Algebra.measure M A - Sigma_Algebra.measure M B

goal (1 subgoal):
 1. Sigma_Algebra.measure M (A - B) = Sigma_Algebra.measure M A - Sigma_Algebra.measure M B
[PROOF STEP]
by simp


[STATEMENT]
lemma oconf_init_obj:
 "\<lbrakk>wf_prog G;
 (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog G; case r of Inl a \<Rightarrow> is_type G (obj_ty obj) | Inr C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<lparr>values := init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r
[PROOF STEP]
apply (auto intro!: oconf_init_obj_lemma unique_fields)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs
[PROOF STEP]
apply (rule Nonce_supply_lemma [THEN exE])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>n\<ge>x. Nonce n \<notin> used ?evs1 \<Longrightarrow> Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs
[PROOF STEP]
apply (rule someI, fast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_decode_triangle_add: "prod_decode (triangle k + m) = prod_decode_aux k m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_decode (triangle k + m) = prod_decode_aux k m
[PROOF STEP]
proof (induct k arbitrary: m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. prod_decode (triangle 0 + m) = prod_decode_aux 0 m
 2. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>m. prod_decode (triangle 0 + m) = prod_decode_aux 0 m
 2. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_decode (triangle 0 + m) = prod_decode_aux 0 m
[PROOF STEP]
by (simp add: prod_decode_def)
[PROOF STATE]
proof (state)
this:
prod_decode (triangle 0 + m) = prod_decode_aux 0 m

goal (1 subgoal):
 1. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
prod_decode (triangle k + ?m) = prod_decode_aux k ?m

goal (1 subgoal):
 1. \<And>k m. (\<And>m. prod_decode (triangle k + m) = prod_decode_aux k m) \<Longrightarrow> prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod_decode (triangle k + ?m) = prod_decode_aux k ?m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prod_decode (triangle k + ?m) = prod_decode_aux k ?m

goal (1 subgoal):
 1. prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m
[PROOF STEP]
by (metis ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add1 not_less_eq_eq prod_decode_aux.simps triangle_Suc)
[PROOF STATE]
proof (state)
this:
prod_decode (triangle (Suc k) + m) = prod_decode_aux (Suc k) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Union_supports_set:
  fixes X::"('a set)"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (supp ` X) supports X
[PROOF STEP]
apply(simp add: supports_def fresh_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (\<forall>x\<in>X. a \<sharp> x) \<and> (\<forall>x\<in>X. b \<sharp> x) \<longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(rule allI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<forall>x\<in>X. a \<sharp> x) \<and> (\<forall>x\<in>X. b \<sharp> x) \<longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (\<forall>x\<in>X. a \<sharp> x) \<and> (\<forall>x\<in>X. b \<sharp> x) \<Longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> X = X
[PROOF STEP]
apply(simp add: perm_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x\<rbrakk> \<Longrightarrow> {[(a, b)] \<bullet> x |x. x \<in> X} = X
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa \<in> X
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X; [(a, b)] \<bullet> xa = xa\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa \<in> X
 2. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa = xa
 3. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> xa = xa
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(rule pt_fresh_fresh[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> a \<sharp> xa
 2. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> b \<sharp> xa
 3. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b xa. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; xa \<in> X\<rbrakk> \<Longrightarrow> b \<sharp> xa
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>xa. x = [(a, b)] \<bullet> xa \<and> xa \<in> X
[PROOF STEP]
apply(rule_tac x="x" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> x = [(a, b)] \<bullet> x \<and> x \<in> X
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> x = [(a, b)] \<bullet> x
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> [(a, b)] \<bullet> x = x
[PROOF STEP]
apply(rule pt_fresh_fresh[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> a \<sharp> x
 2. \<And>a b x. \<lbrakk>\<forall>x\<in>X. a \<sharp> x; \<forall>x\<in>X. b \<sharp> x; x \<in> X\<rbrakk> \<Longrightarrow> b \<sharp> x
[PROOF STEP]
apply(force)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fresh_abs_funI2:
  fixes a :: "'x"
  and   x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f: "finite ((supp x)::'x set)"
  shows "a\<sharp>([a].x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
have "\<exists>c::'x. c\<sharp>(a,x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<sharp> (a, x)
[PROOF STEP]
by  (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
[PROOF STATE]
proof (state)
this:
\<exists>c. c \<sharp> (a, x)

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<sharp> (a, x)
[PROOF STEP]
obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a"
                and   fr2: "c\<sharp>x"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<sharp> (a, x)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>a \<noteq> c; c \<noteq> a; c \<sharp> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp add: fresh_prod at_fresh[OF at])
[PROOF STATE]
proof (state)
this:
a \<noteq> c
c \<noteq> a
c \<sharp> x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
have "c\<sharp>([a].x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sharp> [a].x
[PROOF STEP]
using f fr1 fr2
[PROOF STATE]
proof (prove)
using this:
finite (supp x)
a \<noteq> c
c \<sharp> x

goal (1 subgoal):
 1. c \<sharp> [a].x
[PROOF STEP]
by (simp add: fresh_abs_funI1[OF pt, OF at])
[PROOF STATE]
proof (state)
this:
c \<sharp> [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))"
[PROOF STATE]
proof (prove)
using this:
c \<sharp> [a].x

goal (1 subgoal):
 1. [(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x
[PROOF STEP]
using fr1
[PROOF STATE]
proof (prove)
using this:
c \<sharp> [a].x
a \<noteq> c

goal (1 subgoal):
 1. [(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x
[PROOF STEP]
by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
[PROOF STATE]
proof (state)
this:
[(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))"
[PROOF STATE]
proof (prove)
using this:
[(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x

goal (1 subgoal):
 1. a \<sharp> [c].([(c, a)] \<bullet> x)
[PROOF STEP]
using fr1_sym
[PROOF STATE]
proof (prove)
using this:
[(c, a)] \<bullet> c \<sharp> [(c, a)] \<bullet> [a].x
c \<noteq> a

goal (1 subgoal):
 1. a \<sharp> [c].([(c, a)] \<bullet> x)
[PROOF STEP]
by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
[PROOF STATE]
proof (state)
this:
a \<sharp> [c].([(c, a)] \<bullet> x)

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
have "[c].([(c,a)]\<bullet>x) = ([a].x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [c].([(c, a)] \<bullet> x) = [a].x
[PROOF STEP]
using fr1_sym fr2
[PROOF STATE]
proof (prove)
using this:
c \<noteq> a
c \<sharp> x

goal (1 subgoal):
 1. [c].([(c, a)] \<bullet> x) = [a].x
[PROOF STEP]
by (simp add: abs_fun_eq[OF pt, OF at])
[PROOF STATE]
proof (state)
this:
[c].([(c, a)] \<bullet> x) = [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[c].([(c, a)] \<bullet> x) = [a].x

goal (1 subgoal):
 1. a \<sharp> [a].x
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
[c].([(c, a)] \<bullet> x) = [a].x
a \<sharp> [c].([(c, a)] \<bullet> x)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma System_sum_bounded:
    "System \<in> Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
            \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. System \<in> Always {s. (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocGiv) s) \<le> NbT + (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocRel) s)}
[PROOF STEP]
apply (simp add: o_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. System \<in> Always {s. (\<Sum>x<Nclients. sum_list (allocGiv s x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel s x))}
[PROOF STEP]
apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename sysOfAlloc Alloc \<in> rename sysOfAlloc ` (\<Inter>i<Nclients. Increasing (sub i \<circ> allocRel)) guarantees rename sysOfAlloc ` Always {s. (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocGiv) s) \<le> NbT + (\<Sum>i<Nclients. (sum_list \<circ> sub i \<circ> allocRel) s)} \<Longrightarrow> System \<in> Always {s. (\<Sum>x<Nclients. sum_list (allocGiv s x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel s x))}
[PROOF STEP]
apply (simp add: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rename sysOfAlloc Alloc \<in> (\<Inter>x<Nclients. Increasing (\<lambda>xa. allocRel xa x)) guarantees Always {y. (\<Sum>x<Nclients. sum_list (allocGiv y x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel y x))} \<Longrightarrow> System \<in> Always {s. (\<Sum>x<Nclients. sum_list (allocGiv s x)) \<le> NbT + (\<Sum>x<Nclients. sum_list (allocRel s x))}
[PROOF STEP]
apply (erule component_guaranteesD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. rename sysOfAlloc Alloc \<squnion> ?G19 = System
 2. System \<in> (\<Inter>x<Nclients. Increasing (\<lambda>xa. allocRel xa x))
 3. rename sysOfAlloc Alloc ok ?G19
[PROOF STEP]
apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma topological_space_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((rel_set T ===> (=)) ===> (=)) (topological_space_on_with (Collect (Domainp T)))
    class.topological_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_set T ===> (=)) ===> (=)) (topological_space_on_with (Collect (Domainp T))) class.topological_space
[PROOF STEP]
unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_set T ===> (=)) ===> (=)) (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<subseteq>Collect (Domainp T). \<forall>Ta\<subseteq>Collect (Domainp T). open S \<longrightarrow> open Ta \<longrightarrow> open (S \<inter> Ta)) \<and> (\<forall>K\<subseteq>Pow (Collect (Domainp T)). Ball K open \<longrightarrow> open (\<Union> K))) (\<lambda>open. open UNIV \<and> (\<forall>S T. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) \<and> (\<forall>K. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union> K)))
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. Transfer.Rel (?Rl27 ===> rel_set T) ?ak27 \<Union>
 2. Transfer.Rel (?Rl27 ===> (rel_set T ===> (=)) ===> ?Rn27) ?aj27 Ball
 3. Transfer.Rel (?Rn27 ===> (=) ===> ?Rm27) ?ai27 (\<longrightarrow>)
 4. Transfer.Rel ((?Rl27 ===> ?Rm27) ===> ?Rh27) ?ah27 All
 5. Transfer.Rel (rel_set T ===> rel_set T ===> rel_set T) ?ag27 (\<inter>)
 6. Transfer.Rel ((=) ===> (=) ===> ?Rk27) ?af27 (\<longrightarrow>)
 7. Transfer.Rel ((=) ===> ?Rk27 ===> ?Rj27) ?ae27 (\<longrightarrow>)
 8. Transfer.Rel ((rel_set T ===> ?Rj27) ===> ?Ri27) ?ad27 All
 9. Transfer.Rel ((rel_set T ===> ?Ri27) ===> ?Rg27) ?ac27 All
 10. Transfer.Rel (?Rg27 ===> ?Rh27 ===> ?Re27) ?ab27 (\<and>)
A total of 13 subgoals...
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<subseteq>Collect (Domainp T). \<forall>Ta\<subseteq>Collect (Domainp T). open S \<longrightarrow> open Ta \<longrightarrow> open (S \<inter> Ta)) \<and> (\<forall>K\<subseteq>Pow (Collect (Domainp T)). Ball K open \<longrightarrow> open (\<Union> K))) = (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<in>{A. Ball A (Domainp T)}. \<forall>T\<in>{A. Ball A (Domainp T)}. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) \<and> (\<forall>K\<in>{A. \<forall>A\<in>A. Ball A (Domainp T)}. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union> K)))
[PROOF STEP]
unfolding Pow_def Ball_Collect[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S. Ball S (Domainp T) \<longrightarrow> (\<forall>Ta. Ball Ta (Domainp T) \<longrightarrow> open S \<longrightarrow> open Ta \<longrightarrow> open (S \<inter> Ta))) \<and> (\<forall>K. (\<forall>B\<in>K. Ball B (Domainp T)) \<longrightarrow> Ball K open \<longrightarrow> open (\<Union> K))) = (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<in>{A. Ball A (Domainp T)}. \<forall>T\<in>{A. Ball A (Domainp T)}. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) \<and> (\<forall>K\<in>{A. \<forall>A\<in>A. Ball A (Domainp T)}. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union> K)))
[PROOF STEP]
by blast


[STATEMENT]
lemma (in prob_space) simple_distributed_joint:
  assumes X: "simple_distributed M (\<lambda>x. (X x, Y x)) Px"
  defines "S \<equiv> count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)"
  defines "P \<equiv> (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then Px x else 0)"
  shows "distributed M S (\<lambda>x. (X x, Y x)) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
from simple_distributed_joint_finite[OF X, simp]
[PROOF STATE]
proof (chain)
picking this:
finite (X ` space M)
finite (Y ` space M)
[PROOF STEP]
have S_eq: "S = count_space (X`space M \<times> Y`space M)"
[PROOF STATE]
proof (prove)
using this:
finite (X ` space M)
finite (Y ` space M)

goal (1 subgoal):
 1. S = count_space (X ` space M \<times> Y ` space M)
[PROOF STEP]
by (simp add: S_def pair_measure_count_space)
[PROOF STATE]
proof (state)
this:
S = count_space (X ` space M \<times> Y ` space M)

goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))
[PROOF STEP]
unfolding S_eq P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M (count_space (X ` space M \<times> Y ` space M)) (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Px x else 0))
[PROOF STEP]
proof (rule distributed_simple_function_superset)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. simple_function M (\<lambda>x. (X x, Y x))
 2. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 3. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 4. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
show "simple_function M (\<lambda>x. (X x, Y x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_function M (\<lambda>x. (X x, Y x))
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
simple_distributed M (\<lambda>x. (X x, Y x)) Px

goal (1 subgoal):
 1. simple_function M (\<lambda>x. (X x, Y x))
[PROOF STEP]
by (rule simple_distributed_simple_function)
[PROOF STATE]
proof (state)
this:
simple_function M (\<lambda>x. (X x, Y x))

goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 2. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 3. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 2. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 3. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
assume "x \<in> (\<lambda>x. (X x, Y x)) ` space M"
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. (X x, Y x)) ` space M

goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (X x, Y x)) ` space M \<Longrightarrow> Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
 2. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 3. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
from simple_distributed_measure[OF X this]
[PROOF STATE]
proof (chain)
picking this:
Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
[PROOF STEP]
show "Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)"
[PROOF STATE]
proof (prove)
using this:
Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)

goal (1 subgoal):
 1. Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Px x = prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)

goal (2 subgoals):
 1. (\<lambda>x. (X x, Y x)) ` space M \<subseteq> X ` space M \<times> Y ` space M
 2. finite (X ` space M \<times> Y ` space M)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
distributed M S (\<lambda>x. (X x, Y x)) (\<lambda>x. ennreal (P x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_eq_0:
  \<open>z = 0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z = 0) = ((Re z)\<^sup>2 + (Im z)\<^sup>2 = 0)
[PROOF STEP]
by (simp add: gauss_eq_iff sum_power2_eq_zero_iff)


[STATEMENT]
lemma ACI_set_eq:
  fixes r s :: "'a rexp"
  assumes "r ~ s"
  shows "set_rexp r = set_rexp s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_rexp r = set_rexp s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r ~ s

goal (1 subgoal):
 1. set_rexp r = set_rexp s
[PROOF STEP]
by (induct r s rule: ACI.induct) auto


[STATEMENT]
lemma Inputs_A_Card_form_9:

     "\<lbrakk> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
                             Cert1, Cert2, Cert3\<rbrace> \<in> set evs;
         evs \<in> srb \<rbrakk>
  \<Longrightarrow>    Cert3 = Crypt (crdK (Card A)) (Nonce Na)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs; evs \<in> srb\<rbrakk> \<Longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> srb \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
[PROOF STEP]
apply (erule srb.induct)
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set [] \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 2. \<And>evsF X Ba Aa. \<lbrakk>evsF \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsF \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); X \<in> synth (analz (knows Spy evsF)); illegalUse (Card Ba)\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Spy Aa X # Inputs Spy (Card Ba) X # evsF) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 3. \<And>evsFo Nba Aa Ba. \<lbrakk>evsFo \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsFo \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Nonce Nba \<in> analz (knows Spy evsFo); Key (pairK (Aa, Ba)) \<in> knows Spy evsFo\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Notes Spy (Key (sesK (Nba, pairK (Aa, Ba)))) # evsFo) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 4. \<And>evsrb Aa Ba X. \<lbrakk>evsrb \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsrb \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Says Aa Ba X \<in> set evsrb\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Gets Ba X # evsrb) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 5. \<And>evs1 Aa Ba. \<lbrakk>evs1 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs1 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Aa \<noteq> Server\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Aa Server \<lbrace>Agent Aa, Agent Ba\<rbrace> # evs1) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 6. \<And>evs2 Aa Ba. \<lbrakk>evs2 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs2 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Gets Server \<lbrace>Agent Aa, Agent Ba\<rbrace> \<in> set evs2\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Server Aa \<lbrace>Nonce (Pairkey (Aa, Ba)), Crypt (shrK Aa) \<lbrace>Nonce (Pairkey (Aa, Ba)), Agent Ba\<rbrace>\<rbrace> # evs2) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 7. \<And>evs3 Aa Ba Pka Certificate. \<lbrakk>evs3 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs3 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); legalUse Card Aa; Says Aa Server \<lbrace>Agent Aa, Agent Ba\<rbrace> \<in> set evs3; Gets Aa \<lbrace>Nonce Pka, Certificate\<rbrace> \<in> set evs3\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Inputs Aa (Card Aa) (Agent Aa) # evs3) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 8. \<And>evs4 Naa Aa. \<lbrakk>evs4 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs4 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Nonce Naa \<notin> used evs4; legalUse Card Aa; Aa \<noteq> Server; Inputs Aa (Card Aa) (Agent Aa) \<in> set evs4\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Crypt (crdK (Card Aa)) (Nonce Naa)\<rbrace> # evs4) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 9. \<And>evs4F Naa Aa. \<lbrakk>evs4F \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs4F \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Nonce Naa \<notin> used evs4F; illegalUse (Card Aa); Inputs Spy (Card Aa) (Agent Aa) \<in> set evs4F\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Outpts (Card Aa) Spy \<lbrace>Nonce Naa, Crypt (crdK (Card Aa)) (Nonce Naa)\<rbrace> # evs4F) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 10. \<And>evs5 Aa Naa Certificate Ba. \<lbrakk>evs5 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs5 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Certificate\<rbrace> \<in> set evs5; \<forall>p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Aa Ba \<lbrace>Agent Aa, Nonce Naa\<rbrace> # evs5) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
A total of 20 subgoals...
[PROOF STEP]
apply (simp_all (no_asm_simp))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>evsF X Ba. \<lbrakk>evsF \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsF \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); X \<in> synth (analz (knows Spy evsF)); illegalUse (Card Ba)\<rbrakk> \<Longrightarrow> A = Spy \<and> A = Ba \<and> \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> = X \<longrightarrow> Cert3 = Crypt (crdK (Card Spy)) (Nonce Na)
 2. \<And>evs9 Aa Pka Cert1a Naa Cert2a Nba Cert3a Ba. \<lbrakk>evs9 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs9 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); legalUse Card Aa; Gets Aa \<lbrace>Nonce Pka, Cert1a\<rbrace> \<in> set evs9; Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Cert2a\<rbrace> \<in> set evs9; Gets Aa \<lbrace>Nonce Nba, Cert3a\<rbrace> \<in> set evs9; \<forall>p q. Cert2a \<noteq> \<lbrace>p, q\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> Na = Naa \<and> Nb = Nba \<and> Pk = Pka \<and> Cert1 = Cert1a \<and> Cert2 = Cert3a \<and> Cert3 = Cert2a \<longrightarrow> Cert2a = Crypt (crdK (Card Aa)) (Nonce Naa)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs9 Aa Pka Cert1a Naa Cert2a Nba Cert3a Ba. \<lbrakk>evs9 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs9 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); legalUse Card Aa; Gets Aa \<lbrace>Nonce Pka, Cert1a\<rbrace> \<in> set evs9; Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Cert2a\<rbrace> \<in> set evs9; Gets Aa \<lbrace>Nonce Nba, Cert3a\<rbrace> \<in> set evs9; \<forall>p q. Cert2a \<noteq> \<lbrace>p, q\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> Na = Naa \<and> Nb = Nba \<and> Pk = Pka \<and> Cert1 = Cert1a \<and> Cert2 = Cert3a \<and> Cert3 = Cert2a \<longrightarrow> Cert2a = Crypt (crdK (Card Aa)) (Nonce Naa)
[PROOF STEP]
apply (blast dest!: Outpts_A_Card_form_4)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nhds_imp_cauchy_filter:
  assumes *: "F \<le> nhds x"
  shows "cauchy_filter F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x
[PROOF STEP]
by (intro prod_filter_mono *)
[PROOF STATE]
proof (state)
this:
F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
have "\<dots> \<le> uniformity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nhds x \<times>\<^sub>F nhds x \<le> uniformity
[PROOF STEP]
unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. eventually P uniformity \<longrightarrow> (\<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
assume "eventually P uniformity"
[PROOF STATE]
proof (state)
this:
eventually P uniformity

goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eventually P uniformity
[PROOF STEP]
obtain Ql where ev: "eventually Ql uniformity"
      and "Ql (x, y) \<Longrightarrow> Ql (y, z) \<Longrightarrow> P (x, z)" for x y z
[PROOF STATE]
proof (prove)
using this:
eventually P uniformity

goal (1 subgoal):
 1. (\<And>Ql. \<lbrakk>eventually Ql uniformity; \<And>x y z. \<lbrakk>Ql (x, y); Ql (y, z)\<rbrakk> \<Longrightarrow> P (x, z)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule uniformity_transE) simp
[PROOF STATE]
proof (state)
this:
eventually Ql uniformity
\<lbrakk>Ql (?x, ?y); Ql (?y, ?z)\<rbrakk> \<Longrightarrow> P (?x, ?z)

goal (1 subgoal):
 1. \<And>P. eventually P uniformity \<Longrightarrow> \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
with ev[THEN uniformity_sym]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F (x, y) in uniformity. Ql (y, x)
eventually Ql uniformity
\<lbrakk>Ql (?x, ?y); Ql (?y, ?z)\<rbrakk> \<Longrightarrow> P (?x, ?z)
[PROOF STEP]
show "\<exists>Q. eventually (\<lambda>(x', y). x' = x \<longrightarrow> Q y) uniformity \<and>
        (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F (x, y) in uniformity. Ql (y, x)
eventually Ql uniformity
\<lbrakk>Ql (?x, ?y); Ql (?y, ?z)\<rbrakk> \<Longrightarrow> P (?x, ?z)

goal (1 subgoal):
 1. \<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))
[PROOF STEP]
by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
[PROOF STATE]
proof (state)
this:
\<exists>Q. (\<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> Q y) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nhds x \<times>\<^sub>F nhds x \<le> uniformity

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
F \<times>\<^sub>F F \<le> uniformity
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F \<times>\<^sub>F F \<le> uniformity

goal (1 subgoal):
 1. cauchy_filter F
[PROOF STEP]
by (simp add: cauchy_filter_def)
[PROOF STATE]
proof (state)
this:
cauchy_filter F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcd_mult_unit1:
  assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
have "gcd (b * a) c dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (b * a) c dvd b
[PROOF STEP]
using assms dvd_mult_unit_iff
[PROOF STATE]
proof (prove)
using this:
is_unit a
is_unit ?b \<Longrightarrow> (?a dvd ?c * ?b) = (?a dvd ?c)

goal (1 subgoal):
 1. gcd (b * a) c dvd b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gcd (b * a) c dvd b

goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gcd (b * a) c dvd b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gcd (b * a) c dvd b

goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
by (rule gcdI) simp_all
[PROOF STATE]
proof (state)
this:
gcd (b * a) c = gcd b c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd m (k * m + n) = gcd m n
[PROOF STEP]
by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)


[STATEMENT]
lemma Lcm_fin_eq_Lcm [simp]:
  "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A
[PROOF STEP]
by induct simp_all


[STATEMENT]
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj nat_to_rat_surj
[PROOF STEP]
unfolding surj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. y = nat_to_rat_surj x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = nat_to_rat_surj x
[PROOF STEP]
fix r::rat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = nat_to_rat_surj x
[PROOF STEP]
show "\<exists>n. r = nat_to_rat_surj n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
assume [simp]: "r = Fract i j" and "j > 0"
[PROOF STATE]
proof (state)
this:
r = Fract i j
0 < j

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
have "r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))
[PROOF STEP]
by (simp add: Let_def nat_to_rat_surj_def)
[PROOF STATE]
proof (state)
this:
r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
thus "\<exists>n. r = nat_to_rat_surj n"
[PROOF STATE]
proof (prove)
using this:
r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))

goal (1 subgoal):
 1. \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
by(auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
\<exists>n. r = nat_to_rat_surj n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. r = nat_to_rat_surj n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasisym_not_greater:
  "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp a b = Equiv
[PROOF STEP]
using that comp.exhaust greater_iff_sym_less
[PROOF STATE]
proof (prove)
using this:
cmp a b \<noteq> Greater
cmp b a \<noteq> Greater
\<lbrakk>?y = Less \<Longrightarrow> ?P; ?y = Equiv \<Longrightarrow> ?P; ?y = Greater \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(cmp ?b ?a = Greater) = (cmp ?a ?b = Less)

goal (1 subgoal):
 1. cmp a b = Equiv
[PROOF STEP]
by auto


[STATEMENT]
lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma Methd_sound:
  assumes recursive: "G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
  shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
assume recursive: "\<And> n. \<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>n\<Colon>t
                              \<Longrightarrow>  \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>?n\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
have "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball A (triple_valid2 G 0) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G 0)
 2. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>A. G\<Turnstile>0\<Colon>a

goal (2 subgoals):
 1. Ball A (triple_valid2 G 0) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G 0)
 2. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>0\<Colon>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
fix C sig
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
assume "(C,sig) \<in> ms"
[PROOF STATE]
proof (state)
this:
(C, sig) \<in> ms

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
have "G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
by (rule Methd_triple_valid2_0)
[PROOF STATE]
proof (state)
this:
G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>0\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>0\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t
[PROOF STEP]
by (simp add: mtriples_def split_def)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>0\<Colon>t

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>A. G\<Turnstile>m\<Colon>a \<Longrightarrow> \<forall>a\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>a
\<forall>a\<in>A. G\<Turnstile>Suc m\<Colon>a

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
note hyp = \<open>\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t\<close>
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
note prem = \<open>\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t\<close>
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ball A (triple_valid2 G n) \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G n); Ball A (triple_valid2 G (Suc n))\<rbrakk> \<Longrightarrow> Ball ({{P} Methd-\<succ> {Q} | ms}) (triple_valid2 G (Suc n))
[PROOF STEP]
show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
fix C sig
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
assume m: "(C,sig) \<in> ms"
[PROOF STATE]
proof (state)
this:
(C, sig) \<in> ms

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
have "G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
from prem
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
have prem_m: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>A. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (rule triples_valid2_Suc)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
hence "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (rule hyp)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
with prem_m
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
have "\<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A. G\<Turnstile>m\<Colon>t
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (simp add: ball_Un)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
hence "\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
by (rule recursive)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
(C, sig) \<in> ms
\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t
[PROOF STEP]
have "G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}"
[PROOF STATE]
proof (prove)
using this:
(C, sig) \<in> ms
\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t

goal (1 subgoal):
 1. G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}
[PROOF STEP]
by (auto simp add: mtriples_def split_def)
[PROOF STATE]
proof (state)
this:
G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}
[PROOF STEP]
by (rule Methd_triple_valid2_SucI)
[PROOF STATE]
proof (state)
this:
G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>Suc m\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?C2, ?sig2) \<in> ms \<Longrightarrow> G\<Turnstile>Suc m\<Colon>{Normal (P ?C2 ?sig2)} Methd ?C2 ?sig2-\<succ> {Q ?C2 ?sig2}

goal (1 subgoal):
 1. \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t
[PROOF STEP]
by (simp add: mtriples_def split_def)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>n. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t; \<forall>t\<in>A. G\<Turnstile>?n2\<Colon>t\<rbrakk> \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n2\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
with recursive
[PROOF STATE]
proof (chain)
picking this:
G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}
\<lbrakk>\<And>n. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t; \<forall>t\<in>A. G\<Turnstile>?n2\<Colon>t\<rbrakk> \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n2\<Colon>t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}
\<lbrakk>\<And>n. \<forall>t\<in>A \<union> {{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t; \<forall>t\<in>A. G\<Turnstile>?n2\<Colon>t\<rbrakk> \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>?n2\<Colon>t

goal (1 subgoal):
 1. G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}
[PROOF STEP]
by (unfold ax_valids2_def) blast
[PROOF STATE]
proof (state)
this:
G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
          (if A\<in>bad then insert X (spies evs) else spies evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows Spy (evs @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy evs) else knows Spy evs)
[PROOF STEP]
apply (induct_tac "evs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. knows Spy ([] @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy []) else knows Spy [])
 2. \<And>a list. knows Spy (list @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy list) else knows Spy list) \<Longrightarrow> knows Spy ((a # list) @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy (a # list)) else knows Spy (a # list))
[PROOF STEP]
apply (rename_tac [2] a b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. knows Spy ([] @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy []) else knows Spy [])
 2. \<And>a b. knows Spy (b @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy b) else knows Spy b) \<Longrightarrow> knows Spy ((a # b) @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy (a # b)) else knows Spy (a # b))
[PROOF STEP]
apply (induct_tac [2] "a", auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma servK_authentic:
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
           \<in> parts (spies evs);
         Key authK \<notin> analz (spies evs);
         authK \<notin> range shrK;
         evs \<in> kerbV \<rbrakk>
 \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace>
       \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs); Key authK \<notin> analz (knows Spy evs); authK \<notin> range shrK; evs \<in> kerbV\<rbrakk> \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Key authK \<notin> analz (knows Spy evs); authK \<notin> range shrK; evs \<in> kerbV\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>authK \<notin> range shrK; evs \<in> kerbV\<rbrakk> \<Longrightarrow> Key authK \<notin> analz (knows Spy evs) \<longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs)
[PROOF STEP]
apply (erule kerbV.induct, analz_mono_contra)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. authK \<notin> range shrK \<Longrightarrow> Key authK \<notin> analz (knows Spy []) \<longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy []) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set [])
 2. \<And>evsf X Ba. \<lbrakk>authK \<notin> range shrK; evsf \<in> kerbV; X \<in> synth (analz (knows Spy evsf)); Key authK \<notin> analz (knows Spy evsf); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Spy Ba X # evsf))
 3. \<And>evs1 A. \<lbrakk>authK \<notin> range shrK; evs1 \<in> kerbV; Key authK \<notin> analz (knows Spy evs1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1))
 4. \<And>evs2 authKa A' A T1. \<lbrakk>authK \<notin> range shrK; evs2 \<in> kerbV; Key authKa \<notin> used evs2; authKa \<in> symKeys; Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2; Key authK \<notin> analz (knows Spy evs2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2))
 5. \<And>evs3 A T1 Kas' authKa Ta authTicket Ba. \<lbrakk>authK \<notin> range shrK; evs3 \<in> kerbV; A \<noteq> Kas; A \<noteq> Tgs; Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3; Says Kas' A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evs3; valid Ta wrt T1; Key authK \<notin> analz (knows Spy evs3); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3))
 6. \<And>evs4 servKa Ba authKa A' A Ta T2. \<lbrakk>authK \<notin> range shrK; evs4 \<in> kerbV; Key servKa \<notin> used evs4; servKa \<in> symKeys; Ba \<noteq> Tgs; authKa \<in> symKeys; Says A' Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Ta\<rbrace>, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs4; \<not> expiredAK Ta evs4; \<not> expiredA T2 evs4; servKlife + CT evs4 \<le> authKlife + Ta; Key authK \<notin> analz (knows Spy evs4); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4))
 7. \<And>evs5 authKa servKa A authTicket T2 Ba Tgs' Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evs5 \<in> kerbV; authKa \<in> symKeys; servKa \<in> symKeys; A \<noteq> Kas; A \<noteq> Tgs; Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs5; Says Tgs' A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evs5; valid Tsa wrt T2; Key authK \<notin> analz (knows Spy evs5); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs5) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs5)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5))
 8. \<And>evs6 Ba A' A servKa Tsa T3 Ta2. \<lbrakk>authK \<notin> range shrK; evs6 \<in> kerbV; Ba \<noteq> Kas; Ba \<noteq> Tgs; Says A' Ba \<lbrace>Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number Tsa\<rbrace>, Crypt servKa \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs6; \<not> expiredSK Tsa evs6; \<not> expiredA T3 evs6; Key authK \<notin> analz (knows Spy evs6); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs6) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs6)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Ba A (Crypt servKa (Number Ta2)) # evs6)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Ba A (Crypt servKa (Number Ta2)) # evs6))
 9. \<And>evsO1 A authKa Ta authTicket. \<lbrakk>authK \<notin> range shrK; evsO1 \<in> kerbV; A \<noteq> Spy; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evsO1; expiredAK Ta evsO1; Key authK \<notin> analz (knows Spy evsO1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1))
 10. \<And>evsO2 A authKa servKa Ba Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evsO2 \<in> kerbV; A \<noteq> Spy; Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evsO2; expiredSK Tsa evsO2; Key authK \<notin> analz (knows Spy evsO2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2))
[PROOF STEP]
apply (frule_tac [7] Says_ticket_parts)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. authK \<notin> range shrK \<Longrightarrow> Key authK \<notin> analz (knows Spy []) \<longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy []) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set [])
 2. \<And>evsf X Ba. \<lbrakk>authK \<notin> range shrK; evsf \<in> kerbV; X \<in> synth (analz (knows Spy evsf)); Key authK \<notin> analz (knows Spy evsf); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Spy Ba X # evsf))
 3. \<And>evs1 A. \<lbrakk>authK \<notin> range shrK; evs1 \<in> kerbV; Key authK \<notin> analz (knows Spy evs1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1))
 4. \<And>evs2 authKa A' A T1. \<lbrakk>authK \<notin> range shrK; evs2 \<in> kerbV; Key authKa \<notin> used evs2; authKa \<in> symKeys; Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2; Key authK \<notin> analz (knows Spy evs2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2))
 5. \<And>evs3 A T1 Kas' authKa Ta authTicket Ba. \<lbrakk>authK \<notin> range shrK; evs3 \<in> kerbV; A \<noteq> Kas; A \<noteq> Tgs; Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3; Says Kas' A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evs3; valid Ta wrt T1; Key authK \<notin> analz (knows Spy evs3); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3))
 6. \<And>evs4 servKa Ba authKa A' A Ta T2. \<lbrakk>authK \<notin> range shrK; evs4 \<in> kerbV; Key servKa \<notin> used evs4; servKa \<in> symKeys; Ba \<noteq> Tgs; authKa \<in> symKeys; Says A' Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Ta\<rbrace>, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs4; \<not> expiredAK Ta evs4; \<not> expiredA T2 evs4; servKlife + CT evs4 \<le> authKlife + Ta; Key authK \<notin> analz (knows Spy evs4); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4))
 7. \<And>evs5 authKa servKa A authTicket T2 Ba Tgs' Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evs5 \<in> kerbV; authKa \<in> symKeys; servKa \<in> symKeys; A \<noteq> Kas; A \<noteq> Tgs; Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs5; Says Tgs' A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evs5; valid Tsa wrt T2; Key authK \<notin> analz (knows Spy evs5); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs5) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs5); servTicket \<in> parts (knows Spy evs5)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5))
 8. \<And>evs6 Ba A' A servKa Tsa T3 Ta2. \<lbrakk>authK \<notin> range shrK; evs6 \<in> kerbV; Ba \<noteq> Kas; Ba \<noteq> Tgs; Says A' Ba \<lbrace>Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number Tsa\<rbrace>, Crypt servKa \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs6; \<not> expiredSK Tsa evs6; \<not> expiredA T3 evs6; Key authK \<notin> analz (knows Spy evs6); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs6) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs6)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Ba A (Crypt servKa (Number Ta2)) # evs6)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Ba A (Crypt servKa (Number Ta2)) # evs6))
 9. \<And>evsO1 A authKa Ta authTicket. \<lbrakk>authK \<notin> range shrK; evsO1 \<in> kerbV; A \<noteq> Spy; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evsO1; expiredAK Ta evsO1; Key authK \<notin> analz (knows Spy evsO1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1))
 10. \<And>evsO2 A authKa servKa Ba Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evsO2 \<in> kerbV; A \<noteq> Spy; Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evsO2; expiredSK Tsa evsO2; Key authK \<notin> analz (knows Spy evsO2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2))
[PROOF STEP]
apply (frule_tac [5] Says_ticket_parts, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evsf X. \<lbrakk>authK \<notin> range shrK; evsf \<in> kerbV; X \<in> synth (analz (knows Spy evsf)); Key authK \<notin> analz (knows Spy evsf); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)
 2. \<And>evs2 authKa A' A T1. \<lbrakk>authK \<notin> range shrK; evs2 \<in> kerbV; Key authKa \<notin> used evs2; authKa \<in> symKeys; Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2; Key authK \<notin> analz (knows Spy evs2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs2)\<rbrakk> \<Longrightarrow> authK = shrK A \<and> servK = authKa \<and> B = Tgs \<and> Ts = Number (CT evs2) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, ST\<rbrace> \<in> set evs2)
 3. \<And>evs4 servKa Ba authKa A' A Ta T2. \<lbrakk>authK \<notin> range shrK; evs4 \<in> kerbV; Key servKa \<notin> used evs4; servKa \<in> symKeys; Ba \<noteq> Tgs; authKa \<in> symKeys; Says A' Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Ta\<rbrace>, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs4; \<not> expiredA T2 evs4; servKlife + CT evs4 \<le> authKlife + Ta; Key authK \<notin> analz (knows Spy evs4); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> (authK = authKa \<and> servK = servKa \<and> B = Ba \<and> Ts = Number (CT evs4) \<longrightarrow> (\<exists>Aa ST. Aa = A \<and> ST = Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace> \<or> Says Tgs Aa \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, ST\<rbrace> \<in> set evs4)) \<and> (Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>Aa ST. Aa = A \<and> authK = authKa \<and> servK = servKa \<and> B = Ba \<and> Ts = Number (CT evs4) \<and> ST = Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace> \<or> Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4))
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Oops2_not_AKcryptSK:
     "\<lbrakk> evs \<in> kerbV;
         Says Tgs A \<lbrace>Crypt authK
                     \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace>
           \<in> set evs \<rbrakk>
      \<Longrightarrow> \<not> AKcryptSK servK SK evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs \<in> kerbV; Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, servTicket\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> \<not> AKcryptSK servK SK evs
[PROOF STEP]
by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)


[STATEMENT]
lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumj I i (s(C := x)) = sumj I i s
[PROOF STEP]
by (induct I) (auto simp add: sum_upd_C [unfolded fun_upd_def])


[STATEMENT]
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3
[PROOF STEP]
by (metis (full_types) rax)


[STATEMENT]
lemma [code]:
  "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card_UNIV TYPE('a) = card (set enum)
[PROOF STEP]
by (simp only: card_UNIV_def enum_UNIV)


[STATEMENT]
lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convex S \<Longrightarrow> S exposed_face_of S
[PROOF STEP]
by simp


[STATEMENT]
lemma extreme_point_of_empty [simp]: "\<not> (x extreme_point_of {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x extreme_point_of {}
[PROOF STEP]
by (simp add: extreme_point_of_def)


[STATEMENT]
lemma finite_polytope_facets:
  assumes "polytope S"
  shows "finite {T. T facet_of S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {T. T facet_of S}
[PROOF STEP]
by (simp add: assms facet_of_def finite_polytope_faces)


[STATEMENT]
lemma simplex_segment:
   "\<exists>n. n simplex closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. n simplex closed_segment a b
[PROOF STEP]
using simplex_segment_cases
[PROOF STATE]
proof (prove)
using this:
(if ?a = ?b then 0 else 1) simplex closed_segment ?a ?b

goal (1 subgoal):
 1. \<exists>n. n simplex closed_segment a b
[PROOF STEP]
by metis