[STATEMENT]
theorem (in prob_space) median_bound:
  fixes n :: nat
  fixes I :: "('b :: {linorder_topology, second_countable_topology}) set"
  assumes "interval I"
  assumes "\<alpha> > 0"
  assumes "\<epsilon> \<in> {0<..<1}"
  assumes "indep_vars (\<lambda>_. borel) X {0..<n}"
  assumes "n \<ge> - ln \<epsilon> / (2 * \<alpha>\<^sup>2)"
  assumes "\<And>i. i < n \<Longrightarrow> \<P>(\<omega> in M. X i \<omega> \<in> I) \<ge> 1/2+\<alpha>"
  shows "\<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> I) \<ge> 1-\<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
define Y :: "nat \<Rightarrow> 'a \<Rightarrow> real" where "Y = (\<lambda>i. indicator I \<circ> (X i))"
[PROOF STATE]
proof (state)
this:
Y = (\<lambda>i. indicat_real I \<circ> X i)

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
define t where "t = (\<Sum>i = 0..<n. expectation (Y i)) - n/2"
[PROOF STATE]
proof (state)
this:
t = (\<Sum>i = 0..<n. expectation (Y i)) - real n / 2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "0 < -ln \<epsilon> / (2 * \<alpha>\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < - ln \<epsilon> / (2 * \<alpha>\<^sup>2)
[PROOF STEP]
apply (rule divide_pos_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < - ln \<epsilon>
 2. 0 < 2 * \<alpha>\<^sup>2
[PROOF STEP]
apply (simp, subst ln_less_zero_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < \<epsilon>
 2. \<epsilon> < 1
 3. 0 < 2 * \<alpha>\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
interval I
0 < \<alpha>
\<epsilon> \<in> {0<..<1}
indep_vars (\<lambda>_. borel) X {0..<n}
- ln \<epsilon> / (2 * \<alpha>\<^sup>2) \<le> real n
?i8 < n \<Longrightarrow> 1 / 2 + \<alpha> \<le> prob {\<omega> \<in> space M. X ?i8 \<omega> \<in> I}

goal (3 subgoals):
 1. 0 < \<epsilon>
 2. \<epsilon> < 1
 3. 0 < 2 * \<alpha>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < - ln \<epsilon> / (2 * \<alpha>\<^sup>2)

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < - ln \<epsilon> / (2 * \<alpha>\<^sup>2)

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... \<le> real n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - ln \<epsilon> / (2 * \<alpha>\<^sup>2) \<le> real n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
interval I
0 < \<alpha>
\<epsilon> \<in> {0<..<1}
indep_vars (\<lambda>_. borel) X {0..<n}
- ln \<epsilon> / (2 * \<alpha>\<^sup>2) \<le> real n
?i8 < n \<Longrightarrow> 1 / 2 + \<alpha> \<le> prob {\<omega> \<in> space M. X ?i8 \<omega> \<in> I}

goal (1 subgoal):
 1. - ln \<epsilon> / (2 * \<alpha>\<^sup>2) \<le> real n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- ln \<epsilon> / (2 * \<alpha>\<^sup>2) \<le> real n

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < real n
[PROOF STEP]
have "real n > 0"
[PROOF STATE]
proof (prove)
using this:
0 < real n

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

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
hence n_ge_1:"n \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
0 < real n

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

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
hence n_ge_0:"n > 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> n

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

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have ind_comp: "\<And>i. indicator I \<circ> (X i) = indicator {\<omega>. X i \<omega> \<in> I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. indicator I \<circ> X i = indicator {\<omega>. X i \<omega> \<in> I}
[PROOF STEP]
by (rule ext, simp add:indicator_def comp_def)
[PROOF STATE]
proof (state)
this:
indicator I \<circ> X ?i8 = indicator {\<omega>. X ?i8 \<omega> \<in> I}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "\<alpha> * n \<le> (\<Sum> i =0..<n. 1/2 + \<alpha>) - n/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> * real n \<le> (\<Sum>i = 0..<n. 1 / 2 + \<alpha>) - real n / 2
[PROOF STEP]
by (simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
\<alpha> * real n \<le> (\<Sum>i = 0..<n. 1 / 2 + \<alpha>) - real n / 2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> * real n \<le> (\<Sum>i = 0..<n. 1 / 2 + \<alpha>) - real n / 2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... \<le> (\<Sum> i = 0..<n. expectation (Y i)) - n/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. 1 / 2 + \<alpha>) - real n / 2 \<le> (\<Sum>i = 0..<n. expectation (Y i)) - real n / 2
[PROOF STEP]
apply (rule diff_right_mono, rule sum_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n} \<Longrightarrow> 1 / 2 + \<alpha> \<le> expectation (Y i)
[PROOF STEP]
using assms(6)
[PROOF STATE]
proof (prove)
using this:
?i8 < n \<Longrightarrow> 1 / 2 + \<alpha> \<le> prob {\<omega> \<in> space M. X ?i8 \<omega> \<in> I}

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n} \<Longrightarrow> 1 / 2 + \<alpha> \<le> expectation (Y i)
[PROOF STEP]
by (simp add:Y_def ind_comp Collect_conj_eq inf_commute)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. 1 / 2 + \<alpha>) - real n / 2 \<le> (\<Sum>i = 0..<n. expectation (Y i)) - real n / 2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. 1 / 2 + \<alpha>) - real n / 2 \<le> (\<Sum>i = 0..<n. expectation (Y i)) - real n / 2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. expectation (Y i)) - real n / 2 = t
[PROOF STEP]
by (simp add:t_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. expectation (Y i)) - real n / 2 = t

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<alpha> * real n \<le> t
[PROOF STEP]
have t_ge_a: "t \<ge> \<alpha> * n"
[PROOF STATE]
proof (prove)
using this:
\<alpha> * real n \<le> t

goal (1 subgoal):
 1. \<alpha> * real n \<le> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> * real n \<le> t

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have d: "0 \<le> \<alpha> * n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<alpha> * real n
[PROOF STEP]
apply (rule mult_nonneg_nonneg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> \<alpha>
 2. 0 \<le> real n
[PROOF STEP]
using assms(2) n_ge_0
[PROOF STATE]
proof (prove)
using this:
0 < \<alpha>
0 < n

goal (2 subgoals):
 1. 0 \<le> \<alpha>
 2. 0 \<le> real n
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
0 \<le> \<alpha> * real n

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> \<alpha> * real n

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... \<le> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> * real n \<le> t
[PROOF STEP]
using t_ge_a
[PROOF STATE]
proof (prove)
using this:
\<alpha> * real n \<le> t

goal (1 subgoal):
 1. \<alpha> * real n \<le> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> * real n \<le> t

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> t
[PROOF STEP]
have t_ge_0: "t \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t

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

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have  "(\<alpha> * n)\<^sup>2 \<le> t\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<alpha> * real n)\<^sup>2 \<le> t\<^sup>2
[PROOF STEP]
using t_ge_a d power_mono
[PROOF STATE]
proof (prove)
using this:
\<alpha> * real n \<le> t
0 \<le> \<alpha> * real n
\<lbrakk>?a \<le> ?b; (0::?'a) \<le> ?a\<rbrakk> \<Longrightarrow> ?a ^ ?n \<le> ?b ^ ?n

goal (1 subgoal):
 1. (\<alpha> * real n)\<^sup>2 \<le> t\<^sup>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<alpha> * real n)\<^sup>2 \<le> t\<^sup>2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
hence t_ge_a_sq: "\<alpha>\<^sup>2 * real n * real n \<le> t\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(\<alpha> * real n)\<^sup>2 \<le> t\<^sup>2

goal (1 subgoal):
 1. \<alpha>\<^sup>2 * real n * real n \<le> t\<^sup>2
[PROOF STEP]
by (simp add:algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<alpha>\<^sup>2 * real n * real n \<le> t\<^sup>2

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have Y_indep: "indep_vars (\<lambda>_. borel) Y {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_vars (\<lambda>_. borel) Y {0..<n}
[PROOF STEP]
apply (subst Y_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_vars (\<lambda>_. borel) (\<lambda>i. indicat_real I \<circ> X i) {0..<n}
[PROOF STEP]
apply (rule indep_vars_compose[where M'="(\<lambda>_. borel)", OF assms(4)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n} \<Longrightarrow> indicat_real I \<in> borel_measurable borel
[PROOF STEP]
using interval_borel[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
I \<in> sets borel

goal (1 subgoal):
 1. \<And>i. i \<in> {0..<n} \<Longrightarrow> indicat_real I \<in> borel_measurable borel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
indep_vars (\<lambda>_. borel) Y {0..<n}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
hence b:"Hoeffding_ineq M {0..<n} Y (\<lambda>i. 0) (\<lambda>i. 1)"
[PROOF STATE]
proof (prove)
using this:
indep_vars (\<lambda>_. borel) Y {0..<n}

goal (1 subgoal):
 1. Hoeffding_ineq M {0..<n} Y (\<lambda>i. 0) (\<lambda>i. 1)
[PROOF STEP]
apply (simp add:Hoeffding_ineq_def indep_interval_bounded_random_variables_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indep_vars (\<lambda>_. borel) Y {0..<n} \<Longrightarrow> prob_space M \<and> indep_interval_bounded_random_variables_axioms M {0..<n} Y (\<lambda>i. 0) (\<lambda>i. 1)
[PROOF STEP]
by (simp add:prob_space_axioms indep_interval_bounded_random_variables_axioms_def Y_def Y_indep)
[PROOF STATE]
proof (state)
this:
Hoeffding_ineq M {0..<n} Y (\<lambda>i. 0) (\<lambda>i. 1)

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have c: "\<And>\<omega>. (\<Sum>i = 0..<n. Y i \<omega>) > n/2 \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
assume "(\<Sum>i = 0..<n. Y i \<omega>) > n/2"
[PROOF STATE]
proof (state)
this:
real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)

goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
hence "n < 2 * card ({0..<n} \<inter> {i. X i \<omega> \<in> I})"
[PROOF STATE]
proof (prove)
using this:
real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)

goal (1 subgoal):
 1. n < 2 * card ({0..<n} \<inter> {i. X i \<omega> \<in> I})
[PROOF STEP]
by (simp add:Y_def indicator_def)
[PROOF STATE]
proof (state)
this:
n < 2 * card ({0..<n} \<inter> {i. X i \<omega> \<in> I})

goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n < 2 * card ({0..<n} \<inter> {i. X i \<omega> \<in> I})

goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
have "... = 2 * card {i. i < n \<and> X i \<omega> \<in> I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * card ({0..<n} \<inter> {i. X i \<omega> \<in> I}) = 2 * card {i. i < n \<and> X i \<omega> \<in> I}
[PROOF STEP]
apply (simp, rule arg_cong[where f="card"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<n} \<inter> {i. X i \<omega> \<in> I} = {i. i < n \<and> X i \<omega> \<in> I}
[PROOF STEP]
by (rule order_antisym, rule subsetI, simp, rule subsetI, simp)
[PROOF STATE]
proof (state)
this:
2 * card ({0..<n} \<inter> {i. X i \<omega> \<in> I}) = 2 * card {i. i < n \<and> X i \<omega> \<in> I}

goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n < 2 * card {i. i < n \<and> X i \<omega> \<in> I}
[PROOF STEP]
have "2 * card {i. i < n \<and> X i \<omega> \<in> I} > n"
[PROOF STATE]
proof (prove)
using this:
n < 2 * card {i. i < n \<and> X i \<omega> \<in> I}

goal (1 subgoal):
 1. n < 2 * card {i. i < n \<and> X i \<omega> \<in> I}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < 2 * card {i. i < n \<and> X i \<omega> \<in> I}

goal (1 subgoal):
 1. \<And>\<omega>. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>) \<Longrightarrow> median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
thus "median n (\<lambda>i. X i \<omega>) \<in> I"
[PROOF STATE]
proof (prove)
using this:
n < 2 * card {i. i < n \<and> X i \<omega> \<in> I}

goal (1 subgoal):
 1. median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
using median_est[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
n < 2 * card {i. i < n \<and> X i \<omega> \<in> I}
?n < 2 * card {k. k < ?n \<and> ?f k \<in> I} \<Longrightarrow> median ?n ?f \<in> I

goal (1 subgoal):
 1. median n (\<lambda>i. X i \<omega>) \<in> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
median n (\<lambda>i. X i \<omega>) \<in> I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real n / 2 < (\<Sum>i = 0..<n. Y i ?\<omega>9) \<Longrightarrow> median n (\<lambda>i. X i ?\<omega>9) \<in> I

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "1 - \<epsilon> \<le> 1- exp (- (2 * \<alpha>\<^sup>2 * real n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - \<epsilon> \<le> 1 - exp (- (2 * \<alpha>\<^sup>2 * real n))
[PROOF STEP]
apply (simp, subst ln_ge_iff[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < \<epsilon>
 2. - (2 * \<alpha>\<^sup>2 * real n) \<le> ln \<epsilon>
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<epsilon> \<in> {0<..<1}

goal (2 subgoals):
 1. 0 < \<epsilon>
 2. - (2 * \<alpha>\<^sup>2 * real n) \<le> ln \<epsilon>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (2 * \<alpha>\<^sup>2 * real n) \<le> ln \<epsilon>
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
- ln \<epsilon> / (2 * \<alpha>\<^sup>2) \<le> real n

goal (1 subgoal):
 1. - (2 * \<alpha>\<^sup>2 * real n) \<le> ln \<epsilon>
[PROOF STEP]
apply (subst (asm) pos_divide_le_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < 2 * \<alpha>\<^sup>2
 2. - ln \<epsilon> \<le> real n * (2 * \<alpha>\<^sup>2) \<Longrightarrow> - (2 * \<alpha>\<^sup>2 * real n) \<le> ln \<epsilon>
[PROOF STEP]
apply (simp add: assms(2) power2_eq_square)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - ln \<epsilon> \<le> real n * (2 * \<alpha>\<^sup>2) \<Longrightarrow> - (2 * \<alpha>\<^sup>2 * real n) \<le> ln \<epsilon>
[PROOF STEP]
by (simp add: mult_of_nat_commute)
[PROOF STATE]
proof (state)
this:
1 - \<epsilon> \<le> 1 - exp (- (2 * \<alpha>\<^sup>2 * real n))

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 - \<epsilon> \<le> 1 - exp (- (2 * \<alpha>\<^sup>2 * real n))

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... \<le> 1- exp (- (2 * t\<^sup>2 / real n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - exp (- (2 * \<alpha>\<^sup>2 * real n)) \<le> 1 - exp (- (2 * t\<^sup>2 / real n))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * \<alpha>\<^sup>2 * real n \<le> 2 * t\<^sup>2 / real n
[PROOF STEP]
apply (subst pos_le_divide_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < real n
 2. 2 * \<alpha>\<^sup>2 * real n * real n \<le> 2 * t\<^sup>2
[PROOF STEP]
using n_ge_0
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (2 subgoals):
 1. 0 < real n
 2. 2 * \<alpha>\<^sup>2 * real n * real n \<le> 2 * t\<^sup>2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * \<alpha>\<^sup>2 * real n * real n \<le> 2 * t\<^sup>2
[PROOF STEP]
using t_ge_a_sq
[PROOF STATE]
proof (prove)
using this:
\<alpha>\<^sup>2 * real n * real n \<le> t\<^sup>2

goal (1 subgoal):
 1. 2 * \<alpha>\<^sup>2 * real n * real n \<le> 2 * t\<^sup>2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
1 - exp (- (2 * \<alpha>\<^sup>2 * real n)) \<le> 1 - exp (- (2 * t\<^sup>2 / real n))

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 - exp (- (2 * \<alpha>\<^sup>2 * real n)) \<le> 1 - exp (- (2 * t\<^sup>2 / real n))

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... \<le> 1 - \<P>(\<omega> in M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> n/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - exp (- (2 * t\<^sup>2 / real n)) \<le> 1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}
[PROOF STEP]
using Hoeffding_ineq.Hoeffding_ineq_le[OF b, where \<epsilon>="t", simplified] n_ge_0 t_ge_0
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> t; 0 < n\<rbrakk> \<Longrightarrow> prob {x \<in> space M. (\<Sum>i = 0..<n. Y i x) \<le> (\<Sum>i = 0..<n. expectation (Y i)) - t} \<le> exp (- (2 * t\<^sup>2 / real n))
0 < n
0 \<le> t

goal (1 subgoal):
 1. 1 - exp (- (2 * t\<^sup>2 / real n)) \<le> 1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}
[PROOF STEP]
by (simp add:t_def)
[PROOF STATE]
proof (state)
this:
1 - exp (- (2 * t\<^sup>2 / real n)) \<le> 1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 - exp (- (2 * t\<^sup>2 / real n)) \<le> 1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... = \<P>(\<omega> in M. (\<Sum>i = 0..<n. Y i \<omega>) > n/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2} = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}
[PROOF STEP]
apply (subst prob_compl[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2} \<in> events
 2. prob (space M - {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}) = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> {0..<n} \<Longrightarrow> random_variable borel (Y i)
 2. prob (space M - {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}) = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}
[PROOF STEP]
using Y_indep
[PROOF STATE]
proof (prove)
using this:
indep_vars (\<lambda>_. borel) Y {0..<n}

goal (2 subgoals):
 1. \<And>i. i \<in> {0..<n} \<Longrightarrow> random_variable borel (Y i)
 2. prob (space M - {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}) = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}
[PROOF STEP]
apply (simp add:indep_vars_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob (space M - {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2}) = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}
[PROOF STEP]
apply (rule arg_cong2[where f="measure"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space M - {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2} = {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}
[PROOF STEP]
by (rule order_antisym, rule subsetI, simp add:not_le, rule subsetI, simp add:not_le)
[PROOF STATE]
proof (state)
this:
1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2} = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 - prob {\<omega> \<in> space M. (\<Sum>i = 0..<n. Y i \<omega>) \<le> real n / 2} = prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
have "... \<le> \<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)} \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
apply (rule finite_measure_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)} \<subseteq> {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
 2. {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I} \<in> events
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)} \<Longrightarrow> x \<in> {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
 2. {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I} \<in> events
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
real n / 2 < (\<Sum>i = 0..<n. Y i ?\<omega>9) \<Longrightarrow> median n (\<lambda>i. X i ?\<omega>9) \<in> I

goal (2 subgoals):
 1. \<And>x. x \<in> {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)} \<Longrightarrow> x \<in> {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
 2. {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I} \<in> events
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I} \<in> events
[PROOF STEP]
using interval_borel[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
I \<in> sets borel

goal (1 subgoal):
 1. {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I} \<in> events
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. random_variable borel (\<lambda>x. median n (\<lambda>i. X i x))
[PROOF STEP]
apply (rule median_measurable[OF n_ge_1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> random_variable borel (X i)
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
indep_vars (\<lambda>_. borel) X {0..<n}

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> random_variable borel (X i)
[PROOF STEP]
by (simp add:indep_vars_def)
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. real n / 2 < (\<Sum>i = 0..<n. Y i \<omega>)} \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}

goal (1 subgoal):
 1. 1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 - \<epsilon> \<le> prob {\<omega> \<in> space M. median n (\<lambda>i. X i \<omega>) \<in> I}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_mono_map:
  assumes "sorted xs"
  assumes "mono f"
  shows "sorted (map f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map f xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted xs
mono f

goal (1 subgoal):
 1. sorted (map f xs)
[PROOF STEP]
apply (simp add:sorted_wrt_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; mono f\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. f x \<le> f y) xs
[PROOF STEP]
apply (rule sorted_wrt_mono_rel[where P="(\<le>)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>sorted xs; mono f; x \<in> set xs; y \<in> set xs; x \<le> y\<rbrakk> \<Longrightarrow> f x \<le> f y
 2. \<lbrakk>sorted xs; mono f\<rbrakk> \<Longrightarrow> sorted xs
[PROOF STEP]
by (simp add:mono_def, simp)


[STATEMENT]
lemma map_sort:
  assumes "mono f"
  shows "sort (map f xs) = map f (sort xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort (map f xs) = map f (sort xs)
[PROOF STEP]
apply (rule properties_for_sort)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mset (map f (sort xs)) = mset (map f xs)
 2. sorted (map f (sort xs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map f (sort xs))
[PROOF STEP]
by (rule sorted_mono_map, simp, simp add:assms)


[STATEMENT]
lemma median_cong:
  assumes "\<And>i. i < n \<Longrightarrow> f i = g i"
  shows "median n f = median n g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median n f = median n g
[PROOF STEP]
apply (cases "n = 0", simp add:median_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> median n f = median n g
[PROOF STEP]
apply (simp add:median_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> sort (map f [0..<n]) ! (n div 2) = sort (map g [0..<n]) ! (n div 2)
[PROOF STEP]
apply (rule arg_cong2[where f="(!)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> sort (map f [0..<n]) = sort (map g [0..<n])
 2. 0 < n \<Longrightarrow> n div 2 = n div 2
[PROOF STEP]
apply (rule arg_cong[where f="sort"], rule map_cong, simp, simp add:assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> n div 2 = n div 2
[PROOF STEP]
by simp


[STATEMENT]
lemma median_restrict:
  "median n (\<lambda>i \<in> {0..<n}.f i) = median n f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median n (restrict f {0..<n}) = median n f
[PROOF STEP]
by (rule median_cong, simp)


[STATEMENT]
lemma median_commute_mono:
  assumes "n > 0"
  assumes "mono g"
  shows "g (median n f) = median n (g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (median n f) = median n (g \<circ> f)
[PROOF STEP]
apply (simp add: median_def del:map_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (sort (map f [0..<n]) ! (n div 2)) = sort (map (g \<circ> f) [0..<n]) ! (n div 2)
[PROOF STEP]
apply (subst map_map[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (sort (map f [0..<n]) ! (n div 2)) = sort (map g (map f [0..<n])) ! (n div 2)
[PROOF STEP]
apply (subst map_sort[OF assms(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (sort (map f [0..<n]) ! (n div 2)) = map g (sort (map f [0..<n])) ! (n div 2)
[PROOF STEP]
apply (subst nth_map, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n div 2 < n
 2. g (sort (map f [0..<n]) ! (n div 2)) = g (sort (map f [0..<n]) ! (n div 2))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < n
mono g

goal (2 subgoals):
 1. n div 2 < n
 2. g (sort (map f [0..<n]) ! (n div 2)) = g (sort (map f [0..<n]) ! (n div 2))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (sort (map f [0..<n]) ! (n div 2)) = g (sort (map f [0..<n]) ! (n div 2))
[PROOF STEP]
by simp


[STATEMENT]
lemma median_rat:
  assumes "n > 0"
  shows "real_of_rat (median n f) = median n (\<lambda>i. real_of_rat (f i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (median n f) = median n (\<lambda>i. real_of_rat (f i))
[PROOF STEP]
apply (subst (2) comp_def[where g="f", symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (median n f) = median n (real_of_rat \<circ> f)
[PROOF STEP]
apply (rule median_commute_mono[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono real_of_rat
[PROOF STEP]
by (simp add: mono_def of_rat_less_eq)


[STATEMENT]
lemma median_const:
  assumes "k > 0"
  shows "median k (\<lambda>i \<in> {0..<k}. a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
have b: "sorted (map (\<lambda>_. a) [0..<k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map (\<lambda>_. a) [0..<k])
[PROOF STEP]
by (subst sorted_wrt_map, simp)
[PROOF STATE]
proof (state)
this:
sorted (map (\<lambda>_. a) [0..<k])

goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
have a: "sort (map (\<lambda>_. a) [0..<k]) = map (\<lambda>_. a) [0..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort (map (\<lambda>_. a) [0..<k]) = map (\<lambda>_. a) [0..<k]
[PROOF STEP]
by (subst sorted_sort_id[OF b], simp)
[PROOF STATE]
proof (state)
this:
sort (map (\<lambda>_. a) [0..<k]) = map (\<lambda>_. a) [0..<k]

goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
have "median k (\<lambda>i \<in> {0..<k}. a) = median k (\<lambda>_. a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = median k (\<lambda>_. a)
[PROOF STEP]
by (subst median_restrict, simp)
[PROOF STATE]
proof (state)
this:
median k (\<lambda>i\<in>{0..<k}. a) = median k (\<lambda>_. a)

goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
median k (\<lambda>i\<in>{0..<k}. a) = median k (\<lambda>_. a)

goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
have "... = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median k (\<lambda>_. a) = a
[PROOF STEP]
apply (simp add:median_def a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>_. a) [0..<k] ! (k div 2) = a
[PROOF STEP]
apply (subst nth_map)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k div 2 < length [0..<k]
 2. a = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (2 subgoals):
 1. k div 2 < length [0..<k]
 2. a = a
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
median k (\<lambda>_. a) = a

goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
median k (\<lambda>i\<in>{0..<k}. a) = a

goal (1 subgoal):
 1. median k (\<lambda>i\<in>{0..<k}. a) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
median k (\<lambda>i\<in>{0..<k}. a) = a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma RID\<^sub>SI [intro]: "\<sigma> l = Some v \<Longrightarrow> r \<in> RID\<^sub>V v \<Longrightarrow> r \<in> RID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<sigma> l = Some v; r \<in> RID\<^sub>V v\<rbrakk> \<Longrightarrow> r \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
by (auto simp add: RID\<^sub>S_def ran_def)


[STATEMENT]
lemma RID\<^sub>SE [elim]: "r \<in> RID\<^sub>S \<sigma> \<Longrightarrow> (\<And>l v. \<sigma> l = Some v \<Longrightarrow> r \<in> RID\<^sub>V v \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> RID\<^sub>S \<sigma>; \<And>l v. \<lbrakk>\<sigma> l = Some v; r \<in> RID\<^sub>V v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto simp add: RID\<^sub>S_def ran_def)


[STATEMENT]
lemma RID\<^sub>LI [intro, consumes 1]:
  assumes "s = (\<sigma>, \<tau>, e)"
  shows
    "r \<in> RID\<^sub>S \<sigma> \<Longrightarrow> r \<in> RID\<^sub>L s"
    "r \<in> RID\<^sub>S \<tau> \<Longrightarrow> r \<in> RID\<^sub>L s"
    "r \<in> RID\<^sub>E e \<Longrightarrow> r \<in> RID\<^sub>L s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> RID\<^sub>S \<sigma> \<Longrightarrow> r \<in> RID\<^sub>L s) &&& (r \<in> RID\<^sub>S \<tau> \<Longrightarrow> r \<in> RID\<^sub>L s) &&& (r \<in> RID\<^sub>E e \<Longrightarrow> r \<in> RID\<^sub>L s)
[PROOF STEP]
by (auto simp add: RID\<^sub>L_def assms)


[STATEMENT]
lemma RID\<^sub>LE [elim]:
  "\<lbrakk> r \<in> RID\<^sub>L s; (\<And>\<sigma> \<tau> e. s = (\<sigma>, \<tau>, e) \<Longrightarrow> (r \<in> RID\<^sub>S \<sigma> \<Longrightarrow> P) \<Longrightarrow> (r \<in> RID\<^sub>S \<tau> \<Longrightarrow> P) \<Longrightarrow> (r \<in> RID\<^sub>E e \<Longrightarrow> P) \<Longrightarrow> P) \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> RID\<^sub>L s; (\<And>\<sigma> \<tau> e. \<lbrakk>s = (\<sigma>, \<tau>, e); r \<in> RID\<^sub>S \<sigma> \<Longrightarrow> P; r \<in> RID\<^sub>S \<tau> \<Longrightarrow> P; r \<in> RID\<^sub>E e \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cases s) (auto simp add: RID\<^sub>L_def)


[STATEMENT]
lemma RID\<^sub>GI [intro]:
  "s r = Some v \<Longrightarrow> r \<in> RID\<^sub>G s"
  "s r' = Some ls \<Longrightarrow> r \<in> RID\<^sub>L ls \<Longrightarrow> r \<in> RID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s r = Some v \<Longrightarrow> r \<in> RID\<^sub>G s) &&& (\<lbrakk>s r' = Some ls; r \<in> RID\<^sub>L ls\<rbrakk> \<Longrightarrow> r \<in> RID\<^sub>G s)
[PROOF STEP]
apply (simp add: RID\<^sub>G_def domI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s r' = Some ls; r \<in> RID\<^sub>L ls\<rbrakk> \<Longrightarrow> r \<in> RID\<^sub>G s
[PROOF STEP]
by (metis (no_types, lifting) RID\<^sub>G_def UN_I UnI2 ranI)


[STATEMENT]
lemma RID\<^sub>GE [elim]:
  assumes
    "r \<in> RID\<^sub>G s"
    "r \<in> dom s \<Longrightarrow> P"
    "\<And>r' ls. s r' = Some ls \<Longrightarrow> r \<in> RID\<^sub>L ls \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>G s
r \<in> dom s \<Longrightarrow> P
\<lbrakk>s ?r' = Some ?ls; r \<in> RID\<^sub>L ?ls\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (auto simp add: RID\<^sub>G_def ran_def)


[STATEMENT]
lemma LID\<^sub>SI [intro]:
  "\<sigma> l = Some v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma>"
  "\<sigma> l' = Some v \<Longrightarrow> l \<in> LID\<^sub>V v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma> l = Some v \<Longrightarrow> l \<in> LID\<^sub>S \<sigma>) &&& (\<lbrakk>\<sigma> l' = Some v; l \<in> LID\<^sub>V v\<rbrakk> \<Longrightarrow> l \<in> LID\<^sub>S \<sigma>)
[PROOF STEP]
by (auto simp add: LID\<^sub>S_def ran_def)


[STATEMENT]
lemma LID\<^sub>SE [elim]:
  assumes
    "l \<in> LID\<^sub>S \<sigma>"
    "l \<in> dom \<sigma> \<Longrightarrow> P"
    "\<And>l' v. \<sigma> l' = Some v \<Longrightarrow> l \<in> LID\<^sub>V v \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>S \<sigma>
l \<in> dom \<sigma> \<Longrightarrow> P
\<lbrakk>\<sigma> ?l' = Some ?v; l \<in> LID\<^sub>V ?v\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (auto simp add: LID\<^sub>S_def ran_def)


[STATEMENT]
lemma LID\<^sub>LI [intro]:
  assumes "s = (\<sigma>, \<tau>, e)"
  shows
    "r \<in> LID\<^sub>S \<sigma> \<Longrightarrow> r \<in> LID\<^sub>L s"
    "r \<in> LID\<^sub>S \<tau> \<Longrightarrow> r \<in> LID\<^sub>L s"
    "r \<in> LID\<^sub>E e \<Longrightarrow> r \<in> LID\<^sub>L s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> LID\<^sub>S \<sigma> \<Longrightarrow> r \<in> LID\<^sub>L s) &&& (r \<in> LID\<^sub>S \<tau> \<Longrightarrow> r \<in> LID\<^sub>L s) &&& (r \<in> LID\<^sub>E e \<Longrightarrow> r \<in> LID\<^sub>L s)
[PROOF STEP]
by (auto simp add: LID\<^sub>L_def assms)


[STATEMENT]
lemma LID\<^sub>LE [elim]:
  "\<lbrakk> l \<in> LID\<^sub>L s; (\<And>\<sigma> \<tau> e. s = (\<sigma>, \<tau>, e) \<Longrightarrow> (l \<in> LID\<^sub>S \<sigma> \<Longrightarrow> P) \<Longrightarrow> (l \<in> LID\<^sub>S \<tau> \<Longrightarrow> P) \<Longrightarrow> (l \<in> LID\<^sub>E e \<Longrightarrow> P) \<Longrightarrow> P) \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<in> LID\<^sub>L s; (\<And>\<sigma> \<tau> e. \<lbrakk>s = (\<sigma>, \<tau>, e); l \<in> LID\<^sub>S \<sigma> \<Longrightarrow> P; l \<in> LID\<^sub>S \<tau> \<Longrightarrow> P; l \<in> LID\<^sub>E e \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (cases s) (auto simp add: LID\<^sub>L_def)


[STATEMENT]
lemma LID\<^sub>GI [intro]: "s r = Some ls \<Longrightarrow> l \<in> LID\<^sub>L ls \<Longrightarrow> l \<in> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s r = Some ls; l \<in> LID\<^sub>L ls\<rbrakk> \<Longrightarrow> l \<in> LID\<^sub>G s
[PROOF STEP]
by (auto simp add: LID\<^sub>G_def LID\<^sub>L_def ran_def)


[STATEMENT]
lemma LID\<^sub>GE [elim]: "l \<in> LID\<^sub>G s \<Longrightarrow> (\<And>r ls. s r = Some ls \<Longrightarrow> l \<in> LID\<^sub>L ls \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<in> LID\<^sub>G s; \<And>r ls. \<lbrakk>s r = Some ls; l \<in> LID\<^sub>L ls\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto simp add: LID\<^sub>G_def ran_def)


[STATEMENT]
lemma ID_distr_completion [simp]:
  "RID\<^sub>E (\<E>[e]) = RID\<^sub>C \<E> \<union> RID\<^sub>E e"
  "LID\<^sub>E (\<E>[e]) = LID\<^sub>C \<E> \<union> LID\<^sub>E e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>E (\<E> [e]) = RID\<^sub>C \<E> \<union> RID\<^sub>E e &&& LID\<^sub>E (\<E> [e]) = LID\<^sub>C \<E> \<union> LID\<^sub>E e
[PROOF STEP]
by (induct rule: plug.induct) auto


[STATEMENT]
lemma ID_restricted_store_subset_store:
  "RID\<^sub>S (\<sigma>(l := None)) \<subseteq> RID\<^sub>S \<sigma>"
  "LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>S (\<sigma>(l := None)) \<subseteq> RID\<^sub>S \<sigma> &&& LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. RID\<^sub>S (\<sigma>(l := None)) \<subseteq> RID\<^sub>S \<sigma>
 2. LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>
[PROOF STEP]
show "RID\<^sub>S (\<sigma>(l := None)) \<subseteq> RID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>S (\<sigma>(l := None)) \<subseteq> RID\<^sub>S \<sigma>
[PROOF STEP]
proof (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
assume "r \<in> RID\<^sub>S (\<sigma>(l := None))"
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> RID\<^sub>S (\<sigma>(l := None))
[PROOF STEP]
obtain l' v where "(\<sigma>(l := None)) l' = Some v" and r_v: "r \<in> RID\<^sub>V v"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. (\<And>l' v. \<lbrakk>(\<sigma>(l := None)) l' = Some v; r \<in> RID\<^sub>V v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<sigma>(l := None)) l' = Some v
r \<in> RID\<^sub>V v

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
have "l' \<noteq> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' \<noteq> l
[PROOF STEP]
using \<open>(\<sigma>(l := None)) l' = Some v\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>(l := None)) l' = Some v

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

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
hence "\<sigma> l' = Some v"
[PROOF STATE]
proof (prove)
using this:
l' \<noteq> l

goal (1 subgoal):
 1. \<sigma> l' = Some v
[PROOF STEP]
using \<open>(\<sigma>(l := None)) l' = Some v\<close>
[PROOF STATE]
proof (prove)
using this:
l' \<noteq> l
(\<sigma>(l := None)) l' = Some v

goal (1 subgoal):
 1. \<sigma> l' = Some v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> l' = Some v

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
thus "r \<in> RID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> l' = Some v

goal (1 subgoal):
 1. r \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
using r_v
[PROOF STATE]
proof (prove)
using this:
\<sigma> l' = Some v
r \<in> RID\<^sub>V v

goal (1 subgoal):
 1. r \<in> RID\<^sub>S \<sigma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RID\<^sub>S (\<sigma>(l := None)) \<subseteq> RID\<^sub>S \<sigma>

goal (1 subgoal):
 1. LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>
[PROOF STEP]
show "LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>
[PROOF STEP]
proof (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
fix l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
assume "l' \<in> LID\<^sub>S (\<sigma>(l := None))"
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
hence "l' \<in> dom (\<sigma>(l := None)) \<or> (\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
using this:
l' \<in> LID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. l' \<in> dom (\<sigma>(l := None)) \<or> (\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l' \<in> dom (\<sigma>(l := None)) \<or> (\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v)

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> x \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
thus "l' \<in> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l' \<in> dom (\<sigma>(l := None)) \<or> (\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v)

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
proof (rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l' \<in> dom (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
 2. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
assume "l' \<in> dom (\<sigma>(l := None))"
[PROOF STATE]
proof (state)
this:
l' \<in> dom (\<sigma>(l := None))

goal (2 subgoals):
 1. l' \<in> dom (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
 2. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
thus "l' \<in> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l' \<in> dom (\<sigma>(l := None))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S \<sigma>

goal (1 subgoal):
 1. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
assume "\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v"
[PROOF STATE]
proof (state)
this:
\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v

goal (1 subgoal):
 1. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v
[PROOF STEP]
obtain l'' v where "(\<sigma>(l := None)) l'' = Some v" and l'_in_v: "l' \<in> LID\<^sub>V v"
[PROOF STATE]
proof (prove)
using this:
\<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v

goal (1 subgoal):
 1. (\<And>l'' v. \<lbrakk>(\<sigma>(l := None)) l'' = Some v; l' \<in> LID\<^sub>V v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<sigma>(l := None)) l'' = Some v
l' \<in> LID\<^sub>V v

goal (1 subgoal):
 1. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
hence "\<sigma> l'' = Some v"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>(l := None)) l'' = Some v
l' \<in> LID\<^sub>V v

goal (1 subgoal):
 1. \<sigma> l'' = Some v
[PROOF STEP]
by (cases "l = l''", auto)
[PROOF STATE]
proof (state)
this:
\<sigma> l'' = Some v

goal (1 subgoal):
 1. \<exists>l'' v. (\<sigma>(l := None)) l'' = Some v \<and> l' \<in> LID\<^sub>V v \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
thus "l' \<in> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> l'' = Some v

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
using l'_in_v
[PROOF STATE]
proof (prove)
using this:
\<sigma> l'' = Some v
l' \<in> LID\<^sub>V v

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S \<sigma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LID\<^sub>S (\<sigma>(l := None)) \<subseteq> LID\<^sub>S \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_restricted_store_in_unrestricted_store [intro]:
  "r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S \<sigma>"
  "l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S \<sigma>) &&& (l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S \<sigma>)
[PROOF STEP]
by (meson contra_subsetD ID_restricted_store_subset_store)+


[STATEMENT]
lemma in_restricted_store_in_updated_store [intro]:
  "r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))"
  "l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))) &&& (l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))
 2. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
assume "r \<in> RID\<^sub>S (\<sigma>(l := None))"
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<sigma>(l := None))

goal (2 subgoals):
 1. r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))
 2. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
hence "r \<in> RID\<^sub>S (\<sigma> |` (- {l}))"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. r \<in> RID\<^sub>S (\<sigma> |` (- {l}))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<sigma> |` (- {l}))

goal (2 subgoals):
 1. r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))
 2. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
hence "r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S (\<sigma> |` (- {l}))

goal (1 subgoal):
 1. r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))

goal (2 subgoals):
 1. r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))
 2. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
hence "r \<in> RID\<^sub>S (\<sigma>(l := Some v, l := None))"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))

goal (1 subgoal):
 1. r \<in> RID\<^sub>S ((\<sigma>(l \<mapsto> v))(l := None))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S ((\<sigma>(l \<mapsto> v))(l := None))

goal (2 subgoals):
 1. r \<in> RID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))
 2. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
thus "r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S ((\<sigma>(l \<mapsto> v))(l := None))

goal (1 subgoal):
 1. r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<sigma>(l \<mapsto> v))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
assume "l' \<in> LID\<^sub>S (\<sigma>(l := None))"
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
hence "l' \<in> LID\<^sub>S (\<sigma> |` (- {l}))"
[PROOF STATE]
proof (prove)
using this:
l' \<in> LID\<^sub>S (\<sigma>(l := None))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma> |` (- {l}))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S (\<sigma> |` (- {l}))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
hence "l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))"
[PROOF STATE]
proof (prove)
using this:
l' \<in> LID\<^sub>S (\<sigma> |` (- {l}))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
hence "l' \<in> LID\<^sub>S (\<sigma>(l := Some v, l := None))"
[PROOF STATE]
proof (prove)
using this:
l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v) |` (- {l}))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S ((\<sigma>(l \<mapsto> v))(l := None))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S ((\<sigma>(l \<mapsto> v))(l := None))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l := None)) \<Longrightarrow> l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
thus "l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))"
[PROOF STATE]
proof (prove)
using this:
l' \<in> LID\<^sub>S ((\<sigma>(l \<mapsto> v))(l := None))

goal (1 subgoal):
 1. l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S (\<sigma>(l \<mapsto> v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ID_distr_store [simp]:
  "RID\<^sub>S (\<tau>(l \<mapsto> v)) = RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v"
  "LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>S (\<tau>(l \<mapsto> v)) = RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v &&& LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. RID\<^sub>S (\<tau>(l \<mapsto> v)) = RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
 2. LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
show "RID\<^sub>S (\<tau>(l \<mapsto> v)) = RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>S (\<tau>(l \<mapsto> v)) = RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
[PROOF STEP]
proof (rule set_eqI, rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
 2. \<And>x. x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
 2. \<And>x. x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
assume "r \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))"
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))

goal (2 subgoals):
 1. \<And>x. x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
 2. \<And>x. x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
obtain l' v' where "(\<tau>(l \<mapsto> v)) l' = Some v'" "r \<in> RID\<^sub>V v'"
[PROOF STATE]
proof (prove)
using this:
r \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))

goal (1 subgoal):
 1. (\<And>l' v'. \<lbrakk>(\<tau>(l \<mapsto> v)) l' = Some v'; r \<in> RID\<^sub>V v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<tau>(l \<mapsto> v)) l' = Some v'
r \<in> RID\<^sub>V v'

goal (2 subgoals):
 1. \<And>x. x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
 2. \<And>x. x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
thus "r \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v"
[PROOF STATE]
proof (prove)
using this:
(\<tau>(l \<mapsto> v)) l' = Some v'
r \<in> RID\<^sub>V v'

goal (1 subgoal):
 1. r \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v
[PROOF STEP]
by (cases "l' = l") auto
[PROOF STATE]
proof (state)
this:
r \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v \<Longrightarrow> x \<in> RID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
RID\<^sub>S (\<tau>(l \<mapsto> v)) = RID\<^sub>S (\<tau>(l := None)) \<union> RID\<^sub>V v

goal (1 subgoal):
 1. LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
show "LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
proof (rule set_eqI, rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
 2. \<And>x. x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v) \<Longrightarrow> x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
fix l'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
 2. \<And>x. x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v) \<Longrightarrow> x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
assume "l' \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))"
[PROOF STATE]
proof (state)
this:
l' \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))

goal (2 subgoals):
 1. \<And>x. x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
 2. \<And>x. x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v) \<Longrightarrow> x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
hence "l' \<in> dom (\<tau>(l \<mapsto> v)) \<or> (\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v')"
[PROOF STATE]
proof (prove)
using this:
l' \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))

goal (1 subgoal):
 1. l' \<in> dom (\<tau>(l \<mapsto> v)) \<or> (\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l' \<in> dom (\<tau>(l \<mapsto> v)) \<or> (\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v')

goal (2 subgoals):
 1. \<And>x. x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v)) \<Longrightarrow> x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
 2. \<And>x. x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v) \<Longrightarrow> x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
thus "l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
using this:
l' \<in> dom (\<tau>(l \<mapsto> v)) \<or> (\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v')

goal (1 subgoal):
 1. l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
proof (rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l' \<in> dom (\<tau>(l \<mapsto> v)) \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
 2. \<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v' \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
assume "l' \<in> dom (\<tau>(l \<mapsto> v))"
[PROOF STATE]
proof (state)
this:
l' \<in> dom (\<tau>(l \<mapsto> v))

goal (2 subgoals):
 1. l' \<in> dom (\<tau>(l \<mapsto> v)) \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
 2. \<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v' \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
thus "l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
using this:
l' \<in> dom (\<tau>(l \<mapsto> v))

goal (1 subgoal):
 1. l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
by (cases "l' = l") auto
[PROOF STATE]
proof (state)
this:
l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)

goal (1 subgoal):
 1. \<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v' \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v' \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
assume "\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v'"
[PROOF STATE]
proof (state)
this:
\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v'

goal (1 subgoal):
 1. \<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v' \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v'
[PROOF STEP]
obtain l'' v' where "(\<tau>(l \<mapsto> v)) l'' = Some v'" "l' \<in> LID\<^sub>V v'"
[PROOF STATE]
proof (prove)
using this:
\<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v'

goal (1 subgoal):
 1. (\<And>l'' v'. \<lbrakk>(\<tau>(l \<mapsto> v)) l'' = Some v'; l' \<in> LID\<^sub>V v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<tau>(l \<mapsto> v)) l'' = Some v'
l' \<in> LID\<^sub>V v'

goal (1 subgoal):
 1. \<exists>l'' v'. (\<tau>(l \<mapsto> v)) l'' = Some v' \<and> l' \<in> LID\<^sub>V v' \<Longrightarrow> l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
thus "l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)"
[PROOF STATE]
proof (prove)
using this:
(\<tau>(l \<mapsto> v)) l'' = Some v'
l' \<in> LID\<^sub>V v'

goal (1 subgoal):
 1. l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)
[PROOF STEP]
by (cases "l = l''") auto
[PROOF STATE]
proof (state)
this:
l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l' \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)

goal (1 subgoal):
 1. \<And>x. x \<in> insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v) \<Longrightarrow> x \<in> LID\<^sub>S (\<tau>(l \<mapsto> v))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
LID\<^sub>S (\<tau>(l \<mapsto> v)) = insert l (LID\<^sub>S (\<tau>(l := None)) \<union> LID\<^sub>V v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ID_distr_local [simp]:
  "LID\<^sub>L (\<sigma>,\<tau>,e) = LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau> \<union> LID\<^sub>E e"
  "RID\<^sub>L (\<sigma>,\<tau>,e) = RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau> \<union> RID\<^sub>E e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>L (\<sigma>, \<tau>, e) = LID\<^sub>S \<sigma> \<union> LID\<^sub>S \<tau> \<union> LID\<^sub>E e &&& RID\<^sub>L (\<sigma>, \<tau>, e) = RID\<^sub>S \<sigma> \<union> RID\<^sub>S \<tau> \<union> RID\<^sub>E e
[PROOF STEP]
by (simp add: LID\<^sub>L_def RID\<^sub>L_def)+


[STATEMENT]
lemma ID_restricted_global_subset_unrestricted:
  "LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s"
  "RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s &&& RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s
 2. RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s
[PROOF STEP]
show "LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s
[PROOF STEP]
proof (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> LID\<^sub>G s
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> LID\<^sub>G s
[PROOF STEP]
assume "l \<in> LID\<^sub>G (s(r := None))"
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> LID\<^sub>G s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> LID\<^sub>G (s(r := None))
[PROOF STEP]
obtain r'' ls where "(s(r := None)) r'' = Some ls" and l_in_ls: "l \<in> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. (\<And>r'' ls. \<lbrakk>(s(r := None)) r'' = Some ls; l \<in> LID\<^sub>L ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(s(r := None)) r'' = Some ls
l \<in> LID\<^sub>L ls

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> LID\<^sub>G s
[PROOF STEP]
have "r'' \<noteq> r "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r'' \<noteq> r
[PROOF STEP]
using \<open>(s(r := None)) r'' = Some ls\<close>
[PROOF STATE]
proof (prove)
using this:
(s(r := None)) r'' = Some ls

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

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> LID\<^sub>G s
[PROOF STEP]
hence "s r'' = Some ls"
[PROOF STATE]
proof (prove)
using this:
r'' \<noteq> r

goal (1 subgoal):
 1. s r'' = Some ls
[PROOF STEP]
using \<open>(s(r := None)) r'' = Some ls\<close>
[PROOF STATE]
proof (prove)
using this:
r'' \<noteq> r
(s(r := None)) r'' = Some ls

goal (1 subgoal):
 1. s r'' = Some ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s r'' = Some ls

goal (1 subgoal):
 1. \<And>x. x \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> LID\<^sub>G s
[PROOF STEP]
thus "l \<in> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
using this:
s r'' = Some ls

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
using l_in_ls
[PROOF STATE]
proof (prove)
using this:
s r'' = Some ls
l \<in> LID\<^sub>L ls

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s

goal (1 subgoal):
 1. RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s
[PROOF STEP]
show "RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s
[PROOF STEP]
proof (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> RID\<^sub>G s
[PROOF STEP]
fix r'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> RID\<^sub>G s
[PROOF STEP]
assume "r' \<in> RID\<^sub>G (s(r := None))"
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> RID\<^sub>G s
[PROOF STEP]
hence "r' \<in> dom (s(r := None)) \<or> (\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls)"
[PROOF STATE]
proof (prove)
using this:
r' \<in> RID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. r' \<in> dom (s(r := None)) \<or> (\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r' \<in> dom (s(r := None)) \<or> (\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls)

goal (1 subgoal):
 1. \<And>x. x \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> x \<in> RID\<^sub>G s
[PROOF STEP]
thus "r' \<in> RID\<^sub>G s"
[PROOF STATE]
proof (prove)
using this:
r' \<in> dom (s(r := None)) \<or> (\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls)

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G s
[PROOF STEP]
proof (rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r' \<in> dom (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s
 2. \<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls \<Longrightarrow> r' \<in> RID\<^sub>G s
[PROOF STEP]
assume "\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls"
[PROOF STATE]
proof (state)
this:
\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls

goal (2 subgoals):
 1. r' \<in> dom (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s
 2. \<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls \<Longrightarrow> r' \<in> RID\<^sub>G s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls
[PROOF STEP]
obtain r'' ls where "(s(r := None)) r'' = Some ls" and r'_in_ls: "r' \<in> RID\<^sub>L ls"
[PROOF STATE]
proof (prove)
using this:
\<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls

goal (1 subgoal):
 1. (\<And>r'' ls. \<lbrakk>(s(r := None)) r'' = Some ls; r' \<in> RID\<^sub>L ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(s(r := None)) r'' = Some ls
r' \<in> RID\<^sub>L ls

goal (2 subgoals):
 1. r' \<in> dom (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s
 2. \<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls \<Longrightarrow> r' \<in> RID\<^sub>G s
[PROOF STEP]
have neq: "r'' \<noteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r'' \<noteq> r
[PROOF STEP]
using \<open>(s(r := None)) r'' = Some ls\<close>
[PROOF STATE]
proof (prove)
using this:
(s(r := None)) r'' = Some ls

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

goal (2 subgoals):
 1. r' \<in> dom (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s
 2. \<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls \<Longrightarrow> r' \<in> RID\<^sub>G s
[PROOF STEP]
hence "s r'' = Some ls"
[PROOF STATE]
proof (prove)
using this:
r'' \<noteq> r

goal (1 subgoal):
 1. s r'' = Some ls
[PROOF STEP]
using \<open>(s(r := None)) r'' = Some ls\<close>
[PROOF STATE]
proof (prove)
using this:
r'' \<noteq> r
(s(r := None)) r'' = Some ls

goal (1 subgoal):
 1. s r'' = Some ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s r'' = Some ls

goal (2 subgoals):
 1. r' \<in> dom (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s
 2. \<exists>r'' ls. (s(r := None)) r'' = Some ls \<and> r' \<in> RID\<^sub>L ls \<Longrightarrow> r' \<in> RID\<^sub>G s
[PROOF STEP]
thus "r' \<in> RID\<^sub>G s"
[PROOF STATE]
proof (prove)
using this:
s r'' = Some ls

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G s
[PROOF STEP]
using r'_in_ls
[PROOF STATE]
proof (prove)
using this:
s r'' = Some ls
r' \<in> RID\<^sub>L ls

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G s

goal (1 subgoal):
 1. r' \<in> dom (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RID\<^sub>G (s(r := None)) \<subseteq> RID\<^sub>G s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_restricted_global_in_unrestricted_global [intro]:
  "r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s"
  "l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G s) &&& (l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G s)
[PROOF STEP]
by (simp add: ID_restricted_global_subset_unrestricted rev_subsetD)+


[STATEMENT]
lemma in_restricted_global_in_updated_global [intro]:
  "r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))"
  "l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))) &&& (l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
 2. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
assume "r' \<in> RID\<^sub>G (s(r := None))"
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r := None))

goal (2 subgoals):
 1. r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
 2. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
hence "r' \<in> RID\<^sub>G (s |` (- {r}))"
[PROOF STATE]
proof (prove)
using this:
r' \<in> RID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G (s |` (- {r}))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s |` (- {r}))

goal (2 subgoals):
 1. r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
 2. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
hence "r' \<in> RID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))"
[PROOF STATE]
proof (prove)
using this:
r' \<in> RID\<^sub>G (s |` (- {r}))

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))

goal (2 subgoals):
 1. r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
 2. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
hence "r' \<in> RID\<^sub>G (s(r := Some ls, r := None))"
[PROOF STATE]
proof (prove)
using this:
r' \<in> RID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G ((s(r \<mapsto> ls))(r := None))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G ((s(r \<mapsto> ls))(r := None))

goal (2 subgoals):
 1. r' \<in> RID\<^sub>G (s(r := None)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
 2. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
thus "r' \<in> RID\<^sub>G (s(r \<mapsto> ls))"
[PROOF STATE]
proof (prove)
using this:
r' \<in> RID\<^sub>G ((s(r \<mapsto> ls))(r := None))

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r \<mapsto> ls))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
assume "l \<in> LID\<^sub>G (s(r := None))"
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
hence "l \<in> LID\<^sub>G (s |` (- {r}))"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s |` (- {r}))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s |` (- {r}))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
hence "l \<in> LID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G (s |` (- {r}))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
hence "l \<in> LID\<^sub>G (s(r := Some ls, r := None))"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G (s(r \<mapsto> ls) |` (- {r}))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G ((s(r \<mapsto> ls))(r := None))
[PROOF STEP]
by (simp add: restrict_complement_singleton_eq)
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G ((s(r \<mapsto> ls))(r := None))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
thus "l \<in> LID\<^sub>G (s(r \<mapsto> ls))"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G ((s(r \<mapsto> ls))(r := None))

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s(r \<mapsto> ls))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ID_distr_global [simp]:
  "RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)"
  "LID\<^sub>G (s(r \<mapsto> ls)) = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls) &&& LID\<^sub>G (s(r \<mapsto> ls)) = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
 2. LID\<^sub>G (s(r \<mapsto> ls)) = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
show "LID\<^sub>G (s(r \<mapsto> ls)) = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>G (s(r \<mapsto> ls)) = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
proof (rule set_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> LID\<^sub>G (s(r \<mapsto> ls))) = (x \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls)
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> LID\<^sub>G (s(r \<mapsto> ls))) = (x \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls)
[PROOF STEP]
show "(l \<in> LID\<^sub>G (s(r \<mapsto> ls))) = (l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l \<in> LID\<^sub>G (s(r \<mapsto> ls))) = (l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls)
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l \<in> LID\<^sub>G (s(r \<mapsto> ls)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
 2. l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
assume "l \<in> LID\<^sub>G (s(r \<mapsto> ls))"
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s(r \<mapsto> ls))

goal (2 subgoals):
 1. l \<in> LID\<^sub>G (s(r \<mapsto> ls)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
 2. l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
obtain r' ls' where "(s(r \<mapsto> ls)) r' = Some ls'" "l \<in> LID\<^sub>L ls'"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G (s(r \<mapsto> ls))

goal (1 subgoal):
 1. (\<And>r' ls'. \<lbrakk>(s(r \<mapsto> ls)) r' = Some ls'; l \<in> LID\<^sub>L ls'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s(r \<mapsto> ls)) r' = Some ls'
l \<in> LID\<^sub>L ls'

goal (2 subgoals):
 1. l \<in> LID\<^sub>G (s(r \<mapsto> ls)) \<Longrightarrow> l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
 2. l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
thus "l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
using this:
(s(r \<mapsto> ls)) r' = Some ls'
l \<in> LID\<^sub>L ls'

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls
[PROOF STEP]
by (cases "r = r'") auto
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls

goal (1 subgoal):
 1. l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls \<Longrightarrow> l \<in> LID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(l \<in> LID\<^sub>G (s(r \<mapsto> ls))) = (l \<in> LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LID\<^sub>G (s(r \<mapsto> ls)) = LID\<^sub>G (s(r := None)) \<union> LID\<^sub>L ls

goal (1 subgoal):
 1. RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
[PROOF STEP]
show "RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)
[PROOF STEP]
proof (rule set_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> RID\<^sub>G (s(r \<mapsto> ls))) = (x \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls))
[PROOF STEP]
fix r'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> RID\<^sub>G (s(r \<mapsto> ls))) = (x \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls))
[PROOF STEP]
show "(r' \<in> RID\<^sub>G (s(r \<mapsto> ls))) = (r' \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r' \<in> RID\<^sub>G (s(r \<mapsto> ls))) = (r' \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls))
[PROOF STEP]
proof (rule iffI, clarsimp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>r' \<in> RID\<^sub>G (s(r \<mapsto> ls)); r' \<noteq> r; r' \<notin> RID\<^sub>L ls\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
 2. r' \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
assume r'_g: "r' \<in> RID\<^sub>G (s(r \<mapsto> ls))" and neq: "r' \<noteq> r" and r'_l: "r' \<notin> RID\<^sub>L ls"
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
r' \<noteq> r
r' \<notin> RID\<^sub>L ls

goal (2 subgoals):
 1. \<lbrakk>r' \<in> RID\<^sub>G (s(r \<mapsto> ls)); r' \<noteq> r; r' \<notin> RID\<^sub>L ls\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
 2. r' \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
show "r' \<in> RID\<^sub>G (s(r := None))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
proof (rule RID\<^sub>GE[OF r'_g])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r' \<in> dom (s(r \<mapsto> ls)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
 2. \<And>r'a lsa. \<lbrakk>(s(r \<mapsto> ls)) r'a = Some lsa; r' \<in> RID\<^sub>L lsa\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
assume "r' \<in> dom (s(r \<mapsto> ls))"
[PROOF STATE]
proof (state)
this:
r' \<in> dom (s(r \<mapsto> ls))

goal (2 subgoals):
 1. r' \<in> dom (s(r \<mapsto> ls)) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
 2. \<And>r'a lsa. \<lbrakk>(s(r \<mapsto> ls)) r'a = Some lsa; r' \<in> RID\<^sub>L lsa\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r' \<in> dom (s(r \<mapsto> ls))

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
by (simp add: RID\<^sub>G_def neq)
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. \<And>r'a lsa. \<lbrakk>(s(r \<mapsto> ls)) r'a = Some lsa; r' \<in> RID\<^sub>L lsa\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r'a lsa. \<lbrakk>(s(r \<mapsto> ls)) r'a = Some lsa; r' \<in> RID\<^sub>L lsa\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
fix ls' r''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r'a lsa. \<lbrakk>(s(r \<mapsto> ls)) r'a = Some lsa; r' \<in> RID\<^sub>L lsa\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
assume r'_in_range:"(s(r \<mapsto> ls)) r'' = Some ls'" "r' \<in> RID\<^sub>L ls'"
[PROOF STATE]
proof (state)
this:
(s(r \<mapsto> ls)) r'' = Some ls'
r' \<in> RID\<^sub>L ls'

goal (1 subgoal):
 1. \<And>r'a lsa. \<lbrakk>(s(r \<mapsto> ls)) r'a = Some lsa; r' \<in> RID\<^sub>L lsa\<rbrakk> \<Longrightarrow> r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(s(r \<mapsto> ls)) r'' = Some ls'
r' \<in> RID\<^sub>L ls'

goal (1 subgoal):
 1. r' \<in> RID\<^sub>G (s(r := None))
[PROOF STEP]
by (cases "r'' = r") (use neq r'_l in auto)
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r := None))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r' \<in> RID\<^sub>G (s(r := None))

goal (1 subgoal):
 1. r' \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls) \<Longrightarrow> r' \<in> RID\<^sub>G (s(r \<mapsto> ls))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(r' \<in> RID\<^sub>G (s(r \<mapsto> ls))) = (r' \<in> insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RID\<^sub>G (s(r \<mapsto> ls)) = insert r (RID\<^sub>G (s(r := None)) \<union> RID\<^sub>L ls)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma restrictions_inwards [simp]:
  "x \<noteq> x' \<Longrightarrow> f(x := Some y, x' := None) = (f(x':= None, x := Some y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> (f(x \<mapsto> y))(x' := None) = f(x' := None)(x \<mapsto> y)
[PROOF STEP]
by (rule fun_upd_twist)