[STATEMENT]
lemma mset_le_add_iff1:
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i-j) u + m \<le> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i - j) u + m \<le> n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i - j) u + m \<le> n)
[PROOF STEP]
assume "j \<le> i"
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i - j) u + m \<le> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
[PROOF STEP]
have "j + (i - j) = i"
[PROOF STATE]
proof (prove)
using this:
j \<le> i

goal (1 subgoal):
 1. j + (i - j) = i
[PROOF STEP]
using le_add_diff_inverse
[PROOF STATE]
proof (prove)
using this:
j \<le> i
?b \<le> ?a \<Longrightarrow> ?b + (?a - ?b) = ?a

goal (1 subgoal):
 1. j + (i - j) = i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j + (i - j) = i

goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i - j) u + m \<le> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j + (i - j) = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j + (i - j) = i

goal (1 subgoal):
 1. (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i - j) u + m \<le> n)
[PROOF STEP]
by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
[PROOF STATE]
proof (state)
this:
(repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i - j) u + m \<le> n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma AnnCond1_atomics:
  "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow>
   interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>interfree_aux (Any, q, Some a1); interfree_aux (Any, q, Some a2)\<rbrakk> \<Longrightarrow> interfree_aux (Any, q, Some (AnnCond1 r b a1 a2))
[PROOF STEP]
apply(simp add: interfree_aux_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>atomics a1. case x of (r, a) \<Rightarrow> \<parallel>= (q \<inter> r)
 a
q \<and> (Any = None \<or> (\<forall>p\<in>assertions (the Any). \<parallel>= (p \<inter> r)
 a
p)); \<forall>x\<in>atomics a2. case x of (r, a) \<Rightarrow> \<parallel>= (q \<inter> r)
 a
q \<and> (Any = None \<or> (\<forall>p\<in>assertions (the Any). \<parallel>= (p \<inter> r)
 a
p))\<rbrakk> \<Longrightarrow> \<forall>(r, a)\<in>atomics a1 \<union> atomics a2. \<parallel>= (q \<inter> r)
 a
q \<and> (Any = None \<or> (\<forall>p\<in>assertions (the Any). \<parallel>= (p \<inter> r)
 a
p))
[PROOF STEP]
by force


[STATEMENT]
theorem lookup_eq:
  "lookup env xs =
    (case xs of
      [] \<Rightarrow> Some env
    | x # xs \<Rightarrow>
      (case env of
        Val a \<Rightarrow> None
      | Env b es \<Rightarrow>
          (case es x of
            None \<Rightarrow> None
          | Some e \<Rightarrow> lookup e xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup env xs = (case xs of [] \<Rightarrow> Some env | x # xs \<Rightarrow> case env of Val x \<Rightarrow> Map.empty x | Env b es \<Rightarrow> case es x of None \<Rightarrow> None | Some e \<Rightarrow> lookup e xs)
[PROOF STEP]
by (simp split: list.split env.split)


[STATEMENT]
lemma abs_summable_countable:
  assumes \<open>f abs_summable_on A\<close>
  shows \<open>countable {x\<in>A. f x \<noteq> 0}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
have fin: \<open>finite {x\<in>A. norm (f x) \<ge> t}\<close> if \<open>t > 0\<close> for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x \<in> A. t \<le> norm (f x)}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {x \<in> A. t \<le> norm (f x)} \<Longrightarrow> False
[PROOF STEP]
assume *: \<open>infinite {x \<in> A. t \<le> norm (f x)}\<close>
[PROOF STATE]
proof (state)
this:
infinite {x \<in> A. t \<le> norm (f x)}

goal (1 subgoal):
 1. infinite {x \<in> A. t \<le> norm (f x)} \<Longrightarrow> False
[PROOF STEP]
have \<open>infsum (\<lambda>x. norm (f x)) A \<ge> b\<close> for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
obtain b' where b': \<open>of_nat b' \<ge> b / t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b'. b / t \<le> real b' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson real_arch_simple)
[PROOF STATE]
proof (state)
this:
b / t \<le> real b'

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
infinite {x \<in> A. t \<le> norm (f x)}
[PROOF STEP]
obtain F where cardF: \<open>card F \<ge> b'\<close> and \<open>finite F\<close> and F: \<open>F \<subseteq> {x \<in> A. t \<le> norm (f x)}\<close>
[PROOF STATE]
proof (prove)
using this:
infinite {x \<in> A. t \<le> norm (f x)}

goal (1 subgoal):
 1. (\<And>F. \<lbrakk>b' \<le> card F; finite F; F \<subseteq> {x \<in> A. t \<le> norm (f x)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson finite_if_finite_subsets_card_bdd nle_le)
[PROOF STATE]
proof (state)
this:
b' \<le> card F
finite F
F \<subseteq> {x \<in> A. t \<le> norm (f x)}

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
have \<open>b \<le> of_nat b' * t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> real b' * t
[PROOF STEP]
using b' \<open>t > 0\<close>
[PROOF STATE]
proof (prove)
using this:
b / t \<le> real b'
0 < t

goal (1 subgoal):
 1. b \<le> real b' * t
[PROOF STEP]
by (simp add: field_simps split: if_splits)
[PROOF STATE]
proof (state)
this:
b \<le> real b' * t

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
b \<le> real b' * t

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
have \<open>\<dots> \<le> of_nat (card F) * t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real b' * t \<le> real (card F) * t
[PROOF STEP]
by (simp add: cardF that)
[PROOF STATE]
proof (state)
this:
real b' * t \<le> real (card F) * t

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real b' * t \<le> real (card F) * t

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
have \<open>\<dots> = sum (\<lambda>x. t) F\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card F) * t = (\<Sum>x\<in>F. t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (card F) * t = (\<Sum>x\<in>F. t)

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (card F) * t = (\<Sum>x\<in>F. t)

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
have \<open>\<dots> \<le> sum (\<lambda>x. norm (f x)) F\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>F. t) \<le> (\<Sum>x\<in>F. norm (f x))
[PROOF STEP]
by (metis (mono_tags, lifting) F in_mono mem_Collect_eq sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>F. t) \<le> (\<Sum>x\<in>F. norm (f x))

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>F. t) \<le> (\<Sum>x\<in>F. norm (f x))

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
have \<open>\<dots> = infsum (\<lambda>x. norm (f x)) F\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>F. norm (f x)) = (\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x))
[PROOF STEP]
using \<open>finite F\<close>
[PROOF STATE]
proof (prove)
using this:
finite F

goal (1 subgoal):
 1. (\<Sum>x\<in>F. norm (f x)) = (\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x))
[PROOF STEP]
by (rule infsum_finite[symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>F. norm (f x)) = (\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x))

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>F. norm (f x)) = (\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x))

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
have \<open>\<dots> \<le> infsum (\<lambda>x. norm (f x)) A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
by (rule infsum_mono_neutral) (use \<open>finite F\<close> assms F in auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>x\<in>F. norm (f x)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))

goal (1 subgoal):
 1. b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))

goal (1 subgoal):
 1. infinite {x \<in> A. t \<le> norm (f x)} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
?b \<le> (\<Sum>\<^sub>\<infinity>x\<in>A. norm (f x))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?t \<Longrightarrow> finite {x \<in> A. ?t \<le> norm (f x)}

goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
have \<open>countable (\<Union>i\<in>{1..}. {x\<in>A. norm (f x) \<ge> 1/of_nat i})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
by (rule countable_UN) (use fin in \<open>auto intro!: countable_finite\<close>)
[PROOF STATE]
proof (state)
this:
countable (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})

goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
countable (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})

goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
have \<open>\<dots> = {x\<in>A. f x \<noteq> 0}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)}) = {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
assume x: "x \<in> A" "f x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
x \<in> A
f x \<noteq> (0::'b)

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
define i where "i = max 1 (nat (ceiling (1 / norm (f x))))"
[PROOF STATE]
proof (state)
this:
i = max 1 (nat \<lceil>1 / norm (f x)\<rceil>)

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
have "i \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> i
[PROOF STEP]
by (simp add: i_def)
[PROOF STATE]
proof (state)
this:
1 \<le> i

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> i

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
have "real i \<ge> 1 / norm (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / norm (f x) \<le> real i
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / norm (f x) \<le> real (max 1 (nat \<lceil>1 / norm (f x)\<rceil>))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
1 / norm (f x) \<le> real i

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
hence "1 / real i \<le> norm (f x)"
[PROOF STATE]
proof (prove)
using this:
1 / norm (f x) \<le> real i

goal (1 subgoal):
 1. 1 / real i \<le> norm (f x)
[PROOF STEP]
using \<open>f x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 / norm (f x) \<le> real i
f x \<noteq> (0::'b)

goal (1 subgoal):
 1. 1 / real i \<le> norm (f x)
[PROOF STEP]
by (auto simp: divide_simps mult_ac)
[PROOF STATE]
proof (state)
this:
1 / real i \<le> norm (f x)

goal (2 subgoals):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<in> A; f x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> i
1 / real i \<le> norm (f x)
[PROOF STEP]
show "x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})"
[PROOF STATE]
proof (prove)
using this:
1 \<le> i
1 / real i \<le> norm (f x)

goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
using \<open>x \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> i
1 / real i \<le> norm (f x)
x \<in> A

goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)})

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>1 \<le> i; x \<in> A; 1 / real i \<le> norm (f x); f x = (0::'b)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{1..}. {x \<in> A. 1 / real i \<le> norm (f x)}) = {x \<in> A. f x \<noteq> (0::'b)}

goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
countable {x \<in> A. f x \<noteq> (0::'b)}

goal (1 subgoal):
 1. countable {x \<in> A. f x \<noteq> (0::'b)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
countable {x \<in> A. f x \<noteq> (0::'b)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
  (is "?P n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (fib n) (fib (n + 1))
[PROOF STEP]
proof (induct n rule: fib_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. coprime (fib 0) (fib (0 + 1))
 2. coprime (fib 1) (fib (1 + 1))
 3. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
show "?P 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (fib 0) (fib (0 + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coprime (fib 0) (fib (0 + 1))

goal (2 subgoals):
 1. coprime (fib 1) (fib (1 + 1))
 2. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
show "?P 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (fib 1) (fib (1 + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coprime (fib 1) (fib (1 + 1))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
[PROOF STATE]
proof (state)
this:
coprime (fib (n + 1)) (fib (n + 1 + 1))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
have "\<dots> = fib (n + 2) + fib (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fib (n + 1) + fib (n + 2) = fib (n + 2) + fib (n + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fib (n + 1) + fib (n + 2) = fib (n + 2) + fib (n + 1)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fib (n + 1) + fib (n + 2) = fib (n + 2) + fib (n + 1)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (fib (n + 2)) (fib (n + 2) + fib (n + 1)) = gcd (fib (n + 2)) (fib (n + 1))
[PROOF STEP]
by (rule gcd_add2)
[PROOF STATE]
proof (state)
this:
gcd (fib (n + 2)) (fib (n + 2) + fib (n + 1)) = gcd (fib (n + 2)) (fib (n + 1))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gcd (fib (n + 2)) (fib (n + 2) + fib (n + 1)) = gcd (fib (n + 2)) (fib (n + 1))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (fib (n + 2)) (fib (n + 1)) = gcd (fib (n + 1)) (fib (n + 1 + 1))
[PROOF STEP]
by (simp add: gcd.commute)
[PROOF STATE]
proof (state)
this:
gcd (fib (n + 2)) (fib (n + 1)) = gcd (fib (n + 1)) (fib (n + 1 + 1))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gcd (fib (n + 2)) (fib (n + 1)) = gcd (fib (n + 1)) (fib (n + 1 + 1))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (fib (n + 1)) (fib (n + 1 + 1)) = 1
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
coprime (fib (n + 1)) (fib (n + 1 + 1))

goal (1 subgoal):
 1. gcd (fib (n + 1)) (fib (n + 1 + 1)) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd (fib (n + 1)) (fib (n + 1 + 1)) = 1

goal (1 subgoal):
 1. \<And>n. \<lbrakk>coprime (fib (n + 1)) (fib (n + 1 + 1)); coprime (fib n) (fib (n + 1))\<rbrakk> \<Longrightarrow> coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gcd (fib (n + 2)) (fib (n + 2 + 1)) = 1
[PROOF STEP]
show "?P (n + 2)"
[PROOF STATE]
proof (prove)
using this:
gcd (fib (n + 2)) (fib (n + 2 + 1)) = 1

goal (1 subgoal):
 1. coprime (fib (n + 2)) (fib (n + 2 + 1))
[PROOF STEP]
by (simp add: coprime_iff_gcd_eq_1)
[PROOF STATE]
proof (state)
this:
coprime (fib (n + 2)) (fib (n + 2 + 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_powr_nat_le: "abs (powr_nat x y) \<le> powr_nat (abs x) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>powr_nat x y\<bar> \<le> powr_nat \<bar>x\<bar> y
[PROOF STEP]
by (simp add: powr_nat_def abs_mult)


[STATEMENT]
lemma l11: assumes "\<not> QuadRes p a"
  shows "card S2 = (p - 1) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S2 = (p - 1) div 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card S2 = (p - 1) div 2
[PROOF STEP]
have "sum card S2 = 2 * card S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum card S2 = 2 * card S2
[PROOF STEP]
using sum.cong[of S2 S2 card "\<lambda>x. 2"] l1 f_def S2_def assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S2 = S2; \<And>x. x \<in> S2 \<Longrightarrow> card x = 2\<rbrakk> \<Longrightarrow> sum card S2 = (\<Sum>x\<in>S2. 2)
\<lbrakk>\<not> QuadRes (int p) a; ?x \<in> S1\<rbrakk> \<Longrightarrow> ?x \<noteq> f_1 ?x
f ?x = {?x, f_1 ?x}
S2 = f ` S1
\<not> QuadRes (int p) a

goal (1 subgoal):
 1. sum card S2 = 2 * card S2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sum card S2 = 2 * card S2

goal (1 subgoal):
 1. card S2 = (p - 1) div 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum card S2 = 2 * card S2

goal (1 subgoal):
 1. card S2 = (p - 1) div 2
[PROOF STEP]
have "p - 1 = sum card S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p - 1 = sum card S2
[PROOF STEP]
using l4 card_UN_disjoint[of S2 "\<lambda>x. x"] l3 l5 S1_def S2_def
[PROOF STATE]
proof (prove)
using this:
S1 = \<Union> S2
\<lbrakk>finite S2; \<forall>i\<in>S2. finite i; \<forall>i\<in>S2. \<forall>j\<in>S2. i \<noteq> j \<longrightarrow> i \<inter> j = {}\<rbrakk> \<Longrightarrow> card (\<Union>x\<in>S2. x) = sum card S2
?x \<in> S2 \<Longrightarrow> finite ?x
\<lbrakk>?x \<in> S2; ?y \<in> S2; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> ?x \<inter> ?y = {}
S1 = {0<..int p - 1}
S2 = f ` S1

goal (1 subgoal):
 1. p - 1 = sum card S2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p - 1 = sum card S2

goal (1 subgoal):
 1. card S2 = (p - 1) div 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum card S2 = 2 * card S2
p - 1 = sum card S2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum card S2 = 2 * card S2
p - 1 = sum card S2

goal (1 subgoal):
 1. card S2 = (p - 1) div 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
card S2 = (p - 1) div 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_real_power [simp]:
  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_real (x ^ n) = of_real x ^ n
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma of_real_eq_minus_of_real_iff [simp]: "of_real x = -of_real y \<longleftrightarrow> x = -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_real x = - of_real y) = (x = - y)
[PROOF STEP]
using of_real_eq_iff[of x "-y"]
[PROOF STATE]
proof (prove)
using this:
(of_real x = of_real (- y)) = (x = - y)

goal (1 subgoal):
 1. (of_real x = - of_real y) = (x = - y)
[PROOF STEP]
by (simp only: of_real_minus)


[STATEMENT]
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_real = id
[PROOF STEP]
by (rule ext) (simp add: of_real_def)


[STATEMENT]
lemma norm_diff_triangle_le: "norm (x - z) \<le> e1 + e2"
  if "norm (x - y) \<le> e1"  "norm (y - z) \<le> e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x - z) \<le> e1 + e2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (x - z) \<le> e1 + e2
[PROOF STEP]
have "norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)
[PROOF STEP]
using norm_diff_triangle_ineq that diff_diff_eq2
[PROOF STATE]
proof (prove)
using this:
norm (?a + ?b - (?c + ?d)) \<le> norm (?a - ?c) + norm (?b - ?d)
norm (x - y) \<le> e1
norm (y - z) \<le> e2
?a - (?b - ?c) = ?a + ?c - ?b

goal (1 subgoal):
 1. norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)

goal (1 subgoal):
 1. norm (x - z) \<le> e1 + e2
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
norm (x - y) \<le> e1
norm (y - z) \<le> e2
norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (x - y) \<le> e1
norm (y - z) \<le> e2
norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)

goal (1 subgoal):
 1. norm (x - z) \<le> e1 + e2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (x - z) \<le> e1 + e2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma norm_neg_numeral [simp]: "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (- numeral w) = numeral w
[PROOF STEP]
by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)


[STATEMENT]
lemma Finite_stable_completion:
     "[| finite I;
         !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i);
         !!i. i \<in> I ==> F \<in> Stable (A' i) |]
      ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> F \<in> A i \<longmapsto>w A' i; \<And>i. i \<in> I \<Longrightarrow> F \<in> Stable (A' i)\<rbrakk> \<Longrightarrow> F \<in> \<Inter> (A ` I) \<longmapsto>w \<Inter> (A' ` I)
[PROOF STEP]
apply (unfold Stable_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> F \<in> A i \<longmapsto>w A' i; \<And>i. i \<in> I \<Longrightarrow> F \<in> A' i Co A' i\<rbrakk> \<Longrightarrow> F \<in> \<Inter> (A ` I) \<longmapsto>w \<Inter> (A' ` I)
[PROOF STEP]
apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> F \<in> A i \<longmapsto>w A' i; \<And>i. i \<in> I \<Longrightarrow> F \<in> A' i Co A' i\<rbrakk> \<Longrightarrow> finite I
 2. \<And>i. \<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> F \<in> A i \<longmapsto>w A' i; \<And>i. i \<in> I \<Longrightarrow> F \<in> A' i Co A' i; i \<in> I\<rbrakk> \<Longrightarrow> F \<in> A i \<longmapsto>w ?A'1 i \<union> {}
 3. \<And>i. \<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> F \<in> A i \<longmapsto>w A' i; \<And>i. i \<in> I \<Longrightarrow> F \<in> A' i Co A' i; i \<in> I\<rbrakk> \<Longrightarrow> F \<in> ?A'1 i Co ?A'1 i \<union> {}
 4. \<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> F \<in> A i \<longmapsto>w A' i; \<And>i. i \<in> I \<Longrightarrow> F \<in> A' i Co A' i\<rbrakk> \<Longrightarrow> \<Inter> (?A'1 ` I) \<union> {} \<subseteq> \<Inter> (A' ` I)
[PROOF STEP]
apply (simp_all, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asig_of (A || B) = asig_comp (asig_of A) (asig_of B)
[PROOF STEP]
apply (simp add: par_def ioa_projections)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Im_linepath': "Im (linepath a b x) = linepath (Im a) (Im b) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (linepath a b x) = linepath (Im a) (Im b) x
[PROOF STEP]
by (simp add: linepath_def)


[STATEMENT]
lemma midpoint_in_open_segment [simp]: "midpoint a b \<in> open_segment a b \<longleftrightarrow> a \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (midpoint a b \<in> open_segment a b) = (a \<noteq> b)
[PROOF STEP]
by (simp add: open_segment_def)


[STATEMENT]
lemma inv_max_hi_delete:
  "inv_max_hi t \<Longrightarrow> inv_max_hi (delete x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_max_hi t \<Longrightarrow> inv_max_hi (delete x t)
[PROOF STEP]
apply (induct t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inv_max_hi \<langle>\<rangle> \<Longrightarrow> inv_max_hi (delete x \<langle>\<rangle>)
 2. \<And>t1 x2 t2. \<lbrakk>inv_max_hi t1 \<Longrightarrow> inv_max_hi (delete x t1); inv_max_hi t2 \<Longrightarrow> inv_max_hi (delete x t2); inv_max_hi \<langle>t1, x2, t2\<rangle>\<rbrakk> \<Longrightarrow> inv_max_hi (delete x \<langle>t1, x2, t2\<rangle>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 x2 t2. \<lbrakk>inv_max_hi t1 \<Longrightarrow> inv_max_hi (delete x t1); inv_max_hi t2 \<Longrightarrow> inv_max_hi (delete x t2); inv_max_hi \<langle>t1, x2, t2\<rangle>\<rbrakk> \<Longrightarrow> inv_max_hi (delete x \<langle>t1, x2, t2\<rangle>)
[PROOF STEP]
using inv_max_hi_split_min
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t \<noteq> \<langle>\<rangle>; inv_max_hi ?t\<rbrakk> \<Longrightarrow> inv_max_hi (snd (split_min ?t))

goal (1 subgoal):
 1. \<And>t1 x2 t2. \<lbrakk>inv_max_hi t1 \<Longrightarrow> inv_max_hi (delete x t1); inv_max_hi t2 \<Longrightarrow> inv_max_hi (delete x t2); inv_max_hi \<langle>t1, x2, t2\<rangle>\<rbrakk> \<Longrightarrow> inv_max_hi (delete x \<langle>t1, x2, t2\<rangle>)
[PROOF STEP]
by (fastforce simp add: Let_def split: prod.splits)


[STATEMENT]
lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x\<rangle> = \<langle>y\<rangle> \<equiv> x = y
[PROOF STEP]
by (simp add: expr_list_inj_term_simp)


[STATEMENT]
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {m. 0 < m \<and> m < n} = n - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {m. 0 < m \<and> m < n} = n - 1
[PROOF STEP]
have "{ m. 0 < m \<and> m < n } = {1..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m. 0 < m \<and> m < n} = {1..<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{m. 0 < m \<and> m < n} = {1..<n}

goal (1 subgoal):
 1. card {m. 0 < m \<and> m < n} = n - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{m. 0 < m \<and> m < n} = {1..<n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{m. 0 < m \<and> m < n} = {1..<n}

goal (1 subgoal):
 1. card {m. 0 < m \<and> m < n} = n - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {m. 0 < m \<and> m < n} = n - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ord_eq_2_iff: "ord n (x :: nat) = 2 \<longleftrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ord n x = 2) = ([x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ord n x = 2 \<Longrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
 2. [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n) \<Longrightarrow> ord n x = 2
[PROOF STEP]
assume x: "[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
[PROOF STATE]
proof (state)
this:
[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)

goal (2 subgoals):
 1. ord n x = 2 \<Longrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
 2. [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n) \<Longrightarrow> ord n x = 2
[PROOF STEP]
hence "coprime n x"
[PROOF STATE]
proof (prove)
using this:
[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)

goal (1 subgoal):
 1. coprime n x
[PROOF STEP]
by (metis coprime_commute lucas_coprime_lemma zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
coprime n x

goal (2 subgoals):
 1. ord n x = 2 \<Longrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
 2. [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n) \<Longrightarrow> ord n x = 2
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
coprime n x
[PROOF STEP]
have "ord n x dvd 2" "ord n x \<noteq> 1" "ord n x > 0"
[PROOF STATE]
proof (prove)
using this:
[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
coprime n x

goal (1 subgoal):
 1. ord n x dvd 2 &&& ord n x \<noteq> 1 &&& 0 < ord n x
[PROOF STEP]
by (auto simp: ord_divides' ord_eq_Suc_0_iff)
[PROOF STATE]
proof (state)
this:
ord n x dvd 2
ord n x \<noteq> 1
0 < ord n x

goal (2 subgoals):
 1. ord n x = 2 \<Longrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
 2. [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n) \<Longrightarrow> ord n x = 2
[PROOF STEP]
thus "ord n x = 2"
[PROOF STATE]
proof (prove)
using this:
ord n x dvd 2
ord n x \<noteq> 1
0 < ord n x

goal (1 subgoal):
 1. ord n x = 2
[PROOF STEP]
by (auto dest!: dvd_imp_le simp del: ord_gt_0_iff)
[PROOF STATE]
proof (state)
this:
ord n x = 2

goal (1 subgoal):
 1. ord n x = 2 \<Longrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)
[PROOF STEP]
qed (use ord_divides[of _ 2] ord_divides[of _ 1] in auto)


[STATEMENT]
lemma  bilinear_cross: "bilinear(\<times>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear (\<times>)
[PROOF STEP]
apply (auto simp add: bilinear_def linear_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) ((\<times>) x)
 2. \<And>y. Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) (\<lambda>x. x \<times> y)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x b1 b2. x \<times> (b1 + b2) = x \<times> b1 + x \<times> b2
 2. \<And>x r b. x \<times> (r *\<^sub>R b) = r *\<^sub>R x \<times> b
 3. \<And>y b1 b2. (b1 + b2) \<times> y = b1 \<times> y + b2 \<times> y
 4. \<And>y r b. (r *\<^sub>R b) \<times> y = r *\<^sub>R b \<times> y
[PROOF STEP]
apply (simp add: cross_add_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x r b. x \<times> (r *\<^sub>R b) = r *\<^sub>R x \<times> b
 2. \<And>y b1 b2. (b1 + b2) \<times> y = b1 \<times> y + b2 \<times> y
 3. \<And>y r b. (r *\<^sub>R b) \<times> y = r *\<^sub>R b \<times> y
[PROOF STEP]
apply (simp add: cross_mult_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y b1 b2. (b1 + b2) \<times> y = b1 \<times> y + b2 \<times> y
 2. \<And>y r b. (r *\<^sub>R b) \<times> y = r *\<^sub>R b \<times> y
[PROOF STEP]
apply (simp add: cross_add_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y r b. (r *\<^sub>R b) \<times> y = r *\<^sub>R b \<times> y
[PROOF STEP]
apply (simp add: cross_mult_left)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace> \<in> set evs;
Guard n Ks (knows_max' C evs) |] ==> L \<in> guard n Ks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Says C A' \<lbrace>A'', r, I, L\<rbrace> \<in> set evs; Guard n Ks (knows_max' C evs)\<rbrakk> \<Longrightarrow> L \<in> guard n Ks
[PROOF STEP]
by (auto dest: Says_from_knows_max')


[STATEMENT]
lemma add_diff_add: "(a + c) - (b + d) = (a - b) + (c - d)"
  for a b c d :: "'a::ab_group_add"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + c - (b + d) = a - b + (c - d)
[PROOF STEP]
by simp


[STATEMENT]
lemma integer_of_nat_eq_of_nat [code]:
  "integer_of_nat = of_nat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integer_of_nat = of_nat
[PROOF STEP]
by transfer rule


[STATEMENT]
lemma mset_concat: "mset (concat xss) = sum_list (map mset xss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (concat xss) = sum_list (map mset xss)
[PROOF STEP]
by (induction xss) simp_all


[STATEMENT]
lemma (in algebra) increasing_additive_bound:
  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> ennreal"
  assumes f: "positive M f" and ad: "additive M f"
      and inc: "increasing M f"
      and A: "range A \<subseteq> M"
      and disj: "disjoint_family A"
  shows  "(\<Sum>i. f (A i)) \<le> f \<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i. f (A i)) \<le> f \<Omega>
[PROOF STEP]
proof (safe intro!: suminf_le_const)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>i. f (A i))
 2. \<And>n. (\<Sum>i<n. f (A i)) \<le> f \<Omega>
[PROOF STEP]
fix N
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>i. f (A i))
 2. \<And>n. (\<Sum>i<n. f (A i)) \<le> f \<Omega>
[PROOF STEP]
note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"]
[PROOF STATE]
proof (state)
this:
{..<N} \<subseteq> UNIV \<Longrightarrow> disjoint_family_on A {..<N}

goal (2 subgoals):
 1. summable (\<lambda>i. f (A i))
 2. \<And>n. (\<Sum>i<n. f (A i)) \<le> f \<Omega>
[PROOF STEP]
have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<N. f (A i)) = f (\<Union> (A ` {..<N}))
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
range A \<subseteq> M

goal (1 subgoal):
 1. (\<Sum>i<N. f (A i)) = f (\<Union> (A ` {..<N}))
[PROOF STEP]
by (intro additive_sum [OF f ad _ _]) (auto simp: disj_N)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<N. f (A i)) = f (\<Union> (A ` {..<N}))

goal (2 subgoals):
 1. summable (\<lambda>i. f (A i))
 2. \<And>n. (\<Sum>i<n. f (A i)) \<le> f \<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<N. f (A i)) = f (\<Union> (A ` {..<N}))

goal (2 subgoals):
 1. summable (\<lambda>i. f (A i))
 2. \<And>n. (\<Sum>i<n. f (A i)) \<le> f \<Omega>
[PROOF STEP]
have "... \<le> f \<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<Union> (A ` {..<N})) \<le> f \<Omega>
[PROOF STEP]
using space_closed A
[PROOF STATE]
proof (prove)
using this:
M \<subseteq> Pow \<Omega>
range A \<subseteq> M

goal (1 subgoal):
 1. f (\<Union> (A ` {..<N})) \<le> f \<Omega>
[PROOF STEP]
by (intro increasingD[OF inc] finite_UN) auto
[PROOF STATE]
proof (state)
this:
f (\<Union> (A ` {..<N})) \<le> f \<Omega>

goal (2 subgoals):
 1. summable (\<lambda>i. f (A i))
 2. \<And>n. (\<Sum>i<n. f (A i)) \<le> f \<Omega>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<N. f (A i)) \<le> f \<Omega>
[PROOF STEP]
show "(\<Sum>i<N. f (A i)) \<le> f \<Omega>"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<N. f (A i)) \<le> f \<Omega>

goal (1 subgoal):
 1. (\<Sum>i<N. f (A i)) \<le> f \<Omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<N. f (A i)) \<le> f \<Omega>

goal (1 subgoal):
 1. summable (\<lambda>i. f (A i))
[PROOF STEP]
qed (insert f A, auto simp: positive_def)


[STATEMENT]
lemma fmeasurable_Diff_D:
    assumes m: "T - S \<in> fmeasurable M" "S \<in> fmeasurable M" and sub: "S \<subseteq> T"
    shows "T \<in> fmeasurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<in> fmeasurable M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T \<in> fmeasurable M
[PROOF STEP]
have "T = S \<union> (T - S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T = S \<union> (T - S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
T - S \<in> fmeasurable M
S \<in> fmeasurable M
S \<subseteq> T

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

goal (1 subgoal):
 1. T \<in> fmeasurable M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = S \<union> (T - S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T = S \<union> (T - S)

goal (1 subgoal):
 1. T \<in> fmeasurable M
[PROOF STEP]
by (metis m fmeasurable.Un)
[PROOF STATE]
proof (state)
this:
T \<in> fmeasurable M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. memberid (fdecl (vn, f)) = fid vn
[PROOF STEP]
by (simp add: memberdecl_memberid_def)


[STATEMENT]
lemma "Rep_unit () = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_unit () = True
[PROOF STEP]
nitpick [expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_unit () = True
[PROOF STEP]
by (insert Rep_unit) simp


[STATEMENT]
lemma (in abelian_group) setadd_subset_G:
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G
[PROOF STEP]
by (rule group.setmult_subset_G [OF a_group,
    folded set_add_def, simplified monoid_record_simps])


[STATEMENT]
lemma at3:
  fixes a ::"'x"
  and   b ::"'x"
  and   c ::"'x"
  assumes a: "at TYPE('x)"
  shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap (a, b) c = (if a = c then b else if b = c then a else c)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
at TYPE('x)

goal (1 subgoal):
 1. swap (a, b) c = (if a = c then b else if b = c then a else c)
[PROOF STEP]
by (simp only: at_def)


[STATEMENT]
lemma at_swap:
  fixes a :: "'x"
  and   b :: "'x"
  and   c :: "'x"
  assumes at: "at TYPE('x)"
  shows "swap (a,b) (swap (a,b) c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swap (a, b) (swap (a, b) c) = c
[PROOF STEP]
by (auto simp add: at3[OF at])


[STATEMENT]
lemma pt_eqvt_fun1:
  fixes f     :: "'a\<Rightarrow>'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm). pi\<bullet>f = f)" (is "?LHS = ?RHS")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (supp f = {}) = (\<forall>pi. pi \<bullet> f = f)
[PROOF STEP]
by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b)


[STATEMENT]
lemma pt_eqvt_fun2:
  fixes f     :: "'a\<Rightarrow>'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (supp f = {}) = (\<forall>pi x. pi \<bullet> f x = f (pi \<bullet> x))
[PROOF STEP]
by (rule iffI,
    simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at],
    simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at])


[STATEMENT]
lemma MSC004_1:
 "(\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) --> in'(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Mid_part) | has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &
  (\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts(Big_part::'a,Number_of_mid_parts,Mid_part) & has_parts(object_in(Big_part::'a,Mid_part,Small_part,Number_of_mid_parts,Number_of_small_parts),Number_of_small_parts,Small_part) --> has_parts(Big_part::'a,mtimes(Number_of_mid_parts::'a,Number_of_small_parts),Small_part)) &
  (in'(john::'a,boy)) &
  (\<forall>X. in'(X::'a,boy) --> in'(X::'a,human)) &
  (\<forall>X. in'(X::'a,hand) --> has_parts(X::'a,num5,fingers)) &
  (\<forall>X. in'(X::'a,human) --> has_parts(X::'a,num2,arm)) &
  (\<forall>X. in'(X::'a,arm) --> has_parts(X::'a,num1,hand)) &
  (~has_parts(john::'a,mtimes(mtimes(num2::'a,num1),num5),fingers)) --> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>Number_of_small_parts Small_part Big_part Number_of_mid_parts Mid_part. has_parts (Big_part, Number_of_mid_parts, Mid_part) \<longrightarrow> in' (object_in (Big_part, Mid_part, Small_part, Number_of_mid_parts, Number_of_small_parts), Mid_part) \<or> has_parts (Big_part, mtimes (Number_of_mid_parts, Number_of_small_parts), Small_part)) \<and> (\<forall>Big_part Mid_part Number_of_mid_parts Number_of_small_parts Small_part. has_parts (Big_part, Number_of_mid_parts, Mid_part) \<and> has_parts (object_in (Big_part, Mid_part, Small_part, Number_of_mid_parts, Number_of_small_parts), Number_of_small_parts, Small_part) \<longrightarrow> has_parts (Big_part, mtimes (Number_of_mid_parts, Number_of_small_parts), Small_part)) \<and> in' (john, boy) \<and> (\<forall>X. in' (X, boy) \<longrightarrow> in' (X, human)) \<and> (\<forall>X. in' (X, hand) \<longrightarrow> has_parts (X, num5, fingers)) \<and> (\<forall>X. in' (X, human) \<longrightarrow> has_parts (X, num2, arm)) \<and> (\<forall>X. in' (X, arm) \<longrightarrow> has_parts (X, num1, hand)) \<and> \<not> has_parts (john, mtimes (mtimes (num2, num1), num5), fingers) \<longrightarrow> False
[PROOF STEP]
by meson


[STATEMENT]
lemma MSC006_1:
 "(\<forall>Y X Z. p(X::'a,Y) & p(Y::'a,Z) --> p(X::'a,Z)) &
  (\<forall>Y X Z. q(X::'a,Y) & q(Y::'a,Z) --> q(X::'a,Z)) &
  (\<forall>Y X. q(X::'a,Y) --> q(Y::'a,X)) &
  (\<forall>X Y. p(X::'a,Y) | q(X::'a,Y)) &
  (~p(a::'a,b)) &
  (~q(c::'a,d)) --> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>Y X Z. p (X, Y) \<and> p (Y, Z) \<longrightarrow> p (X, Z)) \<and> (\<forall>Y X Z. q (X, Y) \<and> q (Y, Z) \<longrightarrow> q (X, Z)) \<and> (\<forall>Y X. q (X, Y) \<longrightarrow> q (Y, X)) \<and> (\<forall>X Y. p (X, Y) \<or> q (X, Y)) \<and> \<not> p (a, b) \<and> \<not> q (c, d) \<longrightarrow> False
[PROOF STEP]
by meson


[STATEMENT]
lemma real_divr: "x / y \<le> real_divr prec x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x / y \<le> real_divr prec x y
[PROOF STEP]
by (simp add: real_divr_def truncate_up)


[STATEMENT]
lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. 2 * \<acute>N)) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>
[PROOF STEP]
by (rule assign)


[STATEMENT]
lemma prob_space_point_measure:
  "finite S \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s) \<Longrightarrow> (\<Sum>s\<in>S. p s) = 1 \<Longrightarrow> prob_space (point_measure S p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; \<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s; sum p S = 1\<rbrakk> \<Longrightarrow> prob_space (point_measure S p)
[PROOF STEP]
by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite)


[STATEMENT]
lemma "(3 :: int) + 1 = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 + 1 = 4
[PROOF STEP]
by smt


[STATEMENT]
lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2
[PROOF STEP]
using fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
fst (?x1.0, ?x2.0) = ?x1.0
snd (?x1.0, ?x2.0) = ?x2.0

goal (1 subgoal):
 1. p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2
[PROOF STEP]
by smt


[STATEMENT]
lemma mset_le_add_iff2:
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j-i) u + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j - i) u + n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j - i) u + n)
[PROOF STEP]
assume "i \<le> j"
[PROOF STATE]
proof (state)
this:
i \<le> j

goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j - i) u + n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
have "i + (j - i) = j"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. i + (j - i) = j
[PROOF STEP]
using le_add_diff_inverse
[PROOF STATE]
proof (prove)
using this:
i \<le> j
?b \<le> ?a \<Longrightarrow> ?b + (?a - ?b) = ?a

goal (1 subgoal):
 1. i + (j - i) = j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i + (j - i) = j

goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j - i) u + n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i + (j - i) = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i + (j - i) = j

goal (1 subgoal):
 1. (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j - i) u + n)
[PROOF STEP]
by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
[PROOF STATE]
proof (state)
this:
(repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j - i) u + n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cnj_prod [simp]:
  \<open>cnj (prod f s) = (\<Prod>x\<in>s. cnj (f x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj (prod f s) = (\<Prod>x\<in>s. cnj (f x))
[PROOF STEP]
by (induct s rule: infinite_finite_induct) auto


[STATEMENT]
lemma (in abelian_monoid) boundD_carrier:
  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bound \<zero> n f; n < m\<rbrakk> \<Longrightarrow> f m \<in> carrier G
[PROOF STEP]
by auto


[STATEMENT]
lemma (in ring_hom_ring) hom_finsum [simp]:
  "f \<in> A \<rightarrow> carrier R \<Longrightarrow>
  h (finsum R f A) = finsum S (h \<circ> f) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> A \<rightarrow> carrier R \<Longrightarrow> h (finsum R f A) = finsum S (h \<circ> f) A
[PROOF STEP]
by (induct A rule: infinite_finite_induct, auto simp: Pi_def)


[STATEMENT]
lemma eventually_at_left_field:
  "eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
  for x :: "'a::{linordered_field, linorder_topology}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (at_left x) = (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)
[PROOF STEP]
using linordered_field_no_lb[rule_format, of x]
[PROOF STATE]
proof (prove)
using this:
\<exists>y. y < x

goal (1 subgoal):
 1. eventually P (at_left x) = (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)
[PROOF STEP]
by (auto simp: eventually_at_left)


[STATEMENT]
lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow> \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> k <o g \<in> O(h)
[PROOF STEP]
apply (unfold lesso_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> (\<lambda>x. max (k x - g x) (0::'b)) \<in> O(h)
[PROOF STEP]
apply (rule bigo_lesseq4)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> ?f \<in> O(h)
 2. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> \<forall>x. (0::'b) \<le> max (k x - g x) (0::'b)
 3. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> \<forall>x. max (k x - g x) (0::'b) \<le> \<bar>?f x\<bar>
[PROOF STEP]
apply (erule set_plus_imp_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> \<forall>x. (0::'b) \<le> max (k x - g x) (0::'b)
 2. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> \<forall>x. max (k x - g x) (0::'b) \<le> \<bar>(f - g) x\<bar>
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> (0::'b) \<le> max (k x - g x) (0::'b)
 2. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> \<forall>x. max (k x - g x) (0::'b) \<le> \<bar>(f - g) x\<bar>
[PROOF STEP]
apply (rule max.cobounded2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> \<forall>x. max (k x - g x) (0::'b) \<le> \<bar>(f - g) x\<bar>
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>(f - g) x\<bar>
[PROOF STEP]
apply (subst fun_diff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (case_tac "0 \<le> k x - g x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x - g x \<le> \<bar>f x - g x\<bar>
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (subst abs_of_nonneg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> (0::'b) \<le> f x - g x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x - g x \<le> f x - g x
 3. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (drule_tac x = x in spec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. k x \<le> f x; g x \<le> k x; (0::'b) \<le> k x\<rbrakk> \<Longrightarrow> (0::'b) \<le> f x - g x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x - g x \<le> f x - g x
 3. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; g x \<le> k x; k x \<le> f x\<rbrakk> \<Longrightarrow> (0::'b) \<le> f x - g x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x - g x \<le> f x - g x
 3. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x - g x \<le> f x - g x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (subst diff_conv_add_uminus)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x + - g x \<le> f x + - g x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (rule add_right_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; g x \<le> k x\<rbrakk> \<Longrightarrow> k x \<le> f x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> ?y26 x
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> ?y26 x \<le> \<bar>f x - g x\<bar>
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> ?y26 x \<le> \<bar>f x - g x\<bar>
 2. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> ?y26 x
[PROOF STEP]
apply (rule abs_ge_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> g +o O(h); \<forall>x. (0::'b) \<le> k x; \<forall>x. k x \<le> f x; \<not> (0::'b) \<le> k x - g x\<rbrakk> \<Longrightarrow> max (k x - g x) (0::'b) \<le> (0::'b)
[PROOF STEP]
apply (simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Mapping_size_card_keys: (*FIXME*)
  "Mapping.size m = card (Mapping.keys m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.size m = card (Mapping.keys m)
[PROOF STEP]
unfolding size_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if finite (Mapping.keys m) then card (Mapping.keys m) else 0) = card (Mapping.keys m)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma parts_parts_parts: "[| X \<in> parts {Y}; Y \<in> parts {Z}; Z \<in> parts G |] ==> X \<in> parts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> parts {Y}; Y \<in> parts {Z}; Z \<in> parts G\<rbrakk> \<Longrightarrow> X \<in> parts G
[PROOF STEP]
by (auto dest: parts_parts)


[STATEMENT]
lemma LIMSEQ_realpow_zero:
  fixes x :: real
  assumes "0 \<le> x" "x < 1"
  shows "(\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
 2. x \<noteq> 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
 2. x \<noteq> 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
with \<open>0 \<le> x\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x
x \<noteq> 0
[PROOF STEP]
have x0: "0 < x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
x \<noteq> 0

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

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
 2. x \<noteq> 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x
[PROOF STEP]
have "1 < inverse x"
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. 1 < inverse x
[PROOF STEP]
using \<open>x < 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x
x < 1

goal (1 subgoal):
 1. 1 < inverse x
[PROOF STEP]
by (rule one_less_inverse)
[PROOF STATE]
proof (state)
this:
1 < inverse x

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
 2. x \<noteq> 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < inverse x
[PROOF STEP]
have "(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
1 < inverse x

goal (1 subgoal):
 1. (\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
by (rule LIMSEQ_inverse_realpow_zero)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
 2. x \<noteq> 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
by (simp add: power_inverse)
[PROOF STATE]
proof (state)
this:
(^) x \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (^) x \<longlonglongrightarrow> 0
[PROOF STEP]
by (rule LIMSEQ_imp_Suc) (simp add: True)
[PROOF STATE]
proof (state)
this:
(^) x \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma p_not_div_choose:
  assumes "k < K" and "k \<le> n"
      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "prime p"
    shows "multiplicity p (n choose k) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (n choose k) = 0
[PROOF STEP]
apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. Suc i < K \<Longrightarrow> multiplicity p (Suc i) = multiplicity p (Suc (n - k + i))
 2. True
 3. True
[PROOF STEP]
apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True
 2. True
[PROOF STEP]
apply (rule TrueI)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma approx_map_le:
  "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>approx t2 s; t1 \<subseteq>\<^sub>m t2\<rbrakk> \<Longrightarrow> approx t1 s
[PROOF STEP]
by (clarsimp simp: approx_def map_le_def dom_def)


[STATEMENT]
lemma suminf_pos: "summable f \<Longrightarrow> (\<And>n. 0 < f n) \<Longrightarrow> 0 < suminf f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>summable f; \<And>n. (0::'a) < f n\<rbrakk> \<Longrightarrow> (0::'a) < suminf f
[PROOF STEP]
by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le)


[STATEMENT]
lemma "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
apply match_test'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
oops


[STATEMENT]
lemma jumpNestingOk_eval_no_jump:
 assumes    eval: "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
           jmpOk: "jumpNestingOk {} t" and
          no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
              wt: "Env\<turnstile>t\<Colon>T" and
              wf: "wf_prog (prg Env)"
 shows "abrupt s1 \<noteq> Some (Jump j) \<and>
        (normal s1 \<longrightarrow> v=In2 (w,upd)
         \<longrightarrow> abrupt s \<noteq> Some (Jump j')
         \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
proof (cases "\<exists> j'. abrupt s0 = Some (Jump j')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
 2. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>j'. fst s0 = Some (Jump j')

goal (2 subgoals):
 1. \<exists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
 2. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j'. fst s0 = Some (Jump j')
[PROOF STEP]
obtain j' where jmp: "abrupt s0 = Some (Jump j')"
[PROOF STATE]
proof (prove)
using this:
\<exists>j'. fst s0 = Some (Jump j')

goal (1 subgoal):
 1. (\<And>j'. fst s0 = Some (Jump j') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
fst s0 = Some (Jump j')

goal (2 subgoals):
 1. \<exists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
 2. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
with no_jmp
[PROOF STATE]
proof (chain)
picking this:
fst s0 \<noteq> Some (Jump j)
fst s0 = Some (Jump j')
[PROOF STEP]
have "j'\<noteq>j"
[PROOF STATE]
proof (prove)
using this:
fst s0 \<noteq> Some (Jump j)
fst s0 = Some (Jump j')

goal (1 subgoal):
 1. j' \<noteq> j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j' \<noteq> j

goal (2 subgoals):
 1. \<exists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
 2. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
with eval jmp
[PROOF STATE]
proof (chain)
picking this:
prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)
fst s0 = Some (Jump j')
j' \<noteq> j
[PROOF STEP]
have "s1=s0"
[PROOF STATE]
proof (prove)
using this:
prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)
fst s0 = Some (Jump j')
j' \<noteq> j

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

goal (2 subgoals):
 1. \<exists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
 2. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
with no_jmp jmp
[PROOF STATE]
proof (chain)
picking this:
fst s0 \<noteq> Some (Jump j)
fst s0 = Some (Jump j')
s1 = s0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst s0 \<noteq> Some (Jump j)
fst s0 = Some (Jump j')
s1 = s0

goal (1 subgoal):
 1. fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>j'. fst s0 = Some (Jump j')

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
obtain G where G: "prg Env = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G. prg Env = G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases Env) simp
[PROOF STATE]
proof (state)
this:
prg Env = G

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
from G eval
[PROOF STATE]
proof (chain)
picking this:
prg Env = G
prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)
[PROOF STEP]
have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
[PROOF STATE]
proof (prove)
using this:
prg Env = G
prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)

goal (1 subgoal):
 1. G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
note jmpOk wt
[PROOF STATE]
proof (state)
this:
jumpNestingOk {} t
Env\<turnstile>t\<Colon>T

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
jumpNestingOk {} t
Env\<turnstile>t\<Colon>T

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
from G wf
[PROOF STATE]
proof (chain)
picking this:
prg Env = G
wf_prog (prg Env)
[PROOF STEP]
have "wf_prog G"
[PROOF STATE]
proof (prove)
using this:
prg Env = G
wf_prog (prg Env)

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

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_prog G

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
note G
[PROOF STATE]
proof (state)
this:
prg Env = G

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prg Env = G

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<nexists>j'. fst s0 = Some (Jump j')
[PROOF STEP]
have "\<And> j. abrupt s0 = Some (Jump j) \<Longrightarrow> j \<in> {}"
[PROOF STATE]
proof (prove)
using this:
\<nexists>j'. fst s0 = Some (Jump j')

goal (1 subgoal):
 1. \<And>j. fst s0 = Some (Jump j) \<Longrightarrow> j \<in> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst s0 = Some (Jump ?j) \<Longrightarrow> ?j \<in> {}

goal (1 subgoal):
 1. \<nexists>j'. fst s0 = Some (Jump j') \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)
jumpNestingOk {} t
Env\<turnstile>t\<Colon>T
wf_prog G
prg Env = G
fst s0 = Some (Jump ?j) \<Longrightarrow> ?j \<in> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)
jumpNestingOk {} t
Env\<turnstile>t\<Colon>T
wf_prog G
prg Env = G
fst s0 = Some (Jump ?j) \<Longrightarrow> ?j \<in> {}

goal (1 subgoal):
 1. fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
apply (rule jumpNestingOk_evalE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. fst s0 = Some (Jump j) \<Longrightarrow> fst s0 = Some (Jump j)
 2. \<lbrakk>\<And>j. fst s1 = Some (Jump j) \<Longrightarrow> j \<in> {}; \<And>w upd s j val. \<lbrakk>normal s1; v = In2 (w, upd); fst s \<noteq> Some (Jump j)\<rbrakk> \<Longrightarrow> fst (upd val s) \<noteq> Some (Jump j)\<rbrakk> \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>j. fst s1 = Some (Jump j) \<Longrightarrow> j \<in> {}; \<And>w upd s j val. \<lbrakk>normal s1; v = In2 (w, upd); fst s \<noteq> Some (Jump j)\<rbrakk> \<Longrightarrow> fst (upd val s) \<noteq> Some (Jump j)\<rbrakk> \<Longrightarrow> fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>j. fst s1 = Some (Jump j) \<Longrightarrow> False; \<And>w upd a b j val. \<lbrakk>fst s1 = None; v = In2 (w, upd); a \<noteq> Some (Jump j)\<rbrakk> \<Longrightarrow> fst (upd val (a, b)) \<noteq> Some (Jump j)\<rbrakk> \<Longrightarrow> fst s1 \<noteq> Some (Jump j)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
fst s1 \<noteq> Some (Jump j) \<and> (normal s1 \<longrightarrow> v = In2 (w, upd) \<longrightarrow> fst s \<noteq> Some (Jump j') \<longrightarrow> fst (upd val s) \<noteq> Some (Jump j'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_Intl: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C
[PROOF STEP]
by blast


[STATEMENT]
lemma permutes_not_in:
  \<open>x \<notin> S \<Longrightarrow> p x = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> S \<Longrightarrow> p x = x
[PROOF STEP]
using perm
[PROOF STATE]
proof (prove)
using this:
p permutes S

goal (1 subgoal):
 1. x \<notin> S \<Longrightarrow> p x = x
[PROOF STEP]
by (auto simp: permutes_def)


[STATEMENT]
lemma permutation_of_list_permutes [simp]:
  assumes "list_permutes xs A"
  shows "permutation_of_list xs permutes A"
    (is "?f permutes _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutation_of_list xs permutes A
[PROOF STEP]
proof (rule permutes_subset[OF bij_imp_permutes])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. bij_betw (permutation_of_list xs) ?S ?S
 2. \<And>x. x \<notin> ?S \<Longrightarrow> permutation_of_list xs x = x
 3. ?S \<subseteq> A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
list_permutes xs A
[PROOF STEP]
show "set (map fst xs) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
list_permutes xs A

goal (1 subgoal):
 1. set (map fst xs) \<subseteq> A
[PROOF STEP]
by (simp add: list_permutes_def)
[PROOF STATE]
proof (state)
this:
set (map fst xs) \<subseteq> A

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
list_permutes xs A
[PROOF STEP]
have "inj_on (the \<circ> map_of xs) (set (map fst xs))" (is ?P)
[PROOF STATE]
proof (prove)
using this:
list_permutes xs A

goal (1 subgoal):
 1. inj_on (the \<circ> map_of xs) (set (map fst xs))
[PROOF STEP]
by (intro inj_on_map_of') (simp_all add: list_permutes_def)
[PROOF STATE]
proof (state)
this:
inj_on (the \<circ> map_of xs) (set (map fst xs))

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inj_on (the \<circ> map_of xs) (set (map fst xs))

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
have "?P \<longleftrightarrow> inj_on ?f (set (map fst xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (the \<circ> map_of xs) (set (map fst xs)) = inj_on (permutation_of_list xs) (set (map fst xs))
[PROOF STEP]
by (intro inj_on_cong)
      (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)
[PROOF STATE]
proof (state)
this:
inj_on (the \<circ> map_of xs) (set (map fst xs)) = inj_on (permutation_of_list xs) (set (map fst xs))

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inj_on (permutation_of_list xs) (set (map fst xs))
[PROOF STEP]
have "bij_betw ?f (set (map fst xs)) (?f ` set (map fst xs))"
[PROOF STATE]
proof (prove)
using this:
inj_on (permutation_of_list xs) (set (map fst xs))

goal (1 subgoal):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (permutation_of_list xs ` set (map fst xs))
[PROOF STEP]
by (rule inj_on_imp_bij_betw)
[PROOF STATE]
proof (state)
this:
bij_betw (permutation_of_list xs) (set (map fst xs)) (permutation_of_list xs ` set (map fst xs))

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bij_betw (permutation_of_list xs) (set (map fst xs)) (permutation_of_list xs ` set (map fst xs))

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
list_permutes xs A
[PROOF STEP]
have "?f ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
list_permutes xs A

goal (1 subgoal):
 1. permutation_of_list xs ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)
[PROOF STEP]
by (intro image_cong refl)
      (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)
[PROOF STATE]
proof (state)
this:
permutation_of_list xs ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
permutation_of_list xs ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
list_permutes xs A
[PROOF STEP]
have "\<dots> = set (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
list_permutes xs A

goal (1 subgoal):
 1. (the \<circ> map_of xs) ` set (map fst xs) = set (map fst xs)
[PROOF STEP]
by (subst image_map_of') (simp_all add: list_permutes_def)
[PROOF STATE]
proof (state)
this:
(the \<circ> map_of xs) ` set (map fst xs) = set (map fst xs)

goal (2 subgoals):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
 2. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
[PROOF STEP]
show "bij_betw ?f (set (map fst xs)) (set (map fst xs))"
[PROOF STATE]
proof (prove)
using this:
bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))

goal (1 subgoal):
 1. bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
bij_betw (permutation_of_list xs) (set (map fst xs)) (set (map fst xs))

goal (1 subgoal):
 1. \<And>x. x \<notin> set (map fst xs) \<Longrightarrow> permutation_of_list xs x = x
[PROOF STEP]
qed (force simp: permutation_of_list_def dest!: map_of_SomeD split: option.splits)+


[STATEMENT]
lemma Serv_fresh_not_AKcryptSK:
 "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs
[PROOF STEP]
by (auto simp add: AKcryptSK_def)


[STATEMENT]
lemma Confidentiality_B:
     "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
           \<in> parts (spies evs);
         Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>
           \<in> parts (spies evs);
         Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>
           \<in> parts (spies evs);
         \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
         A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
      \<Longrightarrow> Key servK \<notin> analz (spies evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> Key servK \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (frule authK_authentic)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> A \<notin> bad
 2. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> evs \<in> kerbV
 3. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; \<exists>AT. Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> Key servK \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (erule_tac [3] exE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> A \<notin> bad
 2. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> evs \<in> kerbV
 3. \<And>AT. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> Key servK \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (frule_tac [3] Confidentiality_Kas)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> A \<notin> bad
 2. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV\<rbrakk> \<Longrightarrow> evs \<in> kerbV
 3. \<And>AT. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> \<not> expiredAK Ta evs
 4. \<And>AT. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> A \<notin> bad
 5. \<And>AT. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs\<rbrakk> \<Longrightarrow> evs \<in> kerbV
 6. \<And>AT. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs; Key authK \<notin> analz (knows Spy evs)\<rbrakk> \<Longrightarrow> Key servK \<notin> analz (knows Spy evs)
[PROOF STEP]
apply (frule_tac [6] servTicket_authentic, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AT Taa authKa. \<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace> \<in> parts (knows Spy evs); Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace> \<in> parts (knows Spy evs); \<not> expiredSK Ts evs; \<not> expiredAK Ta evs; A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta\<rbrace>, AT\<rbrace> \<in> set evs; Key authK \<notin> analz (knows Spy evs); Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Taa\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Taa\<rbrace>\<rbrace> \<in> set evs; Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servK, Agent B, Number Ts\<rbrace>, Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace> \<in> set evs; Key servK \<in> analz (knows Spy evs)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma append_rsp2_pre0:
  assumes a:"list_all2 (\<approx>) x x'"
  shows "list_all2 (\<approx>) (x @ z) (x' @ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<approx>) (x @ z) (x' @ z)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<approx>) x x'

goal (1 subgoal):
 1. list_all2 (\<approx>) (x @ z) (x' @ z)
[PROOF STEP]
apply (induct x x' rule: list_induct2')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. list_all2 (\<approx>) [] [] \<Longrightarrow> list_all2 (\<approx>) ([] @ z) ([] @ z)
 2. \<And>x xs. list_all2 (\<approx>) (x # xs) [] \<Longrightarrow> list_all2 (\<approx>) ((x # xs) @ z) ([] @ z)
 3. \<And>y ys. list_all2 (\<approx>) [] (y # ys) \<Longrightarrow> list_all2 (\<approx>) ([] @ z) ((y # ys) @ z)
 4. \<And>x xs y ys. \<lbrakk>list_all2 (\<approx>) xs ys \<Longrightarrow> list_all2 (\<approx>) (xs @ z) (ys @ z); list_all2 (\<approx>) (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> list_all2 (\<approx>) ((x # xs) @ z) ((y # ys) @ z)
[PROOF STEP]
by simp_all (rule list_all2_refl'[OF list_eq_equivp])