[STATEMENT]
lemma up_ray_borel:
  assumes "up_ray (I :: (('a :: linorder_topology) set))"
  shows "I \<in> borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
proof (cases "closed I")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. closed I \<Longrightarrow> I \<in> sets borel
 2. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
closed I

goal (2 subgoals):
 1. closed I \<Longrightarrow> I \<in> sets borel
 2. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
closed I

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
using borel_closed
[PROOF STATE]
proof (prove)
using this:
closed I
closed ?A \<Longrightarrow> ?A \<in> sets borel

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I \<in> sets borel

goal (1 subgoal):
 1. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> closed I

goal (1 subgoal):
 1. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
hence b:"\<not> closed I"
[PROOF STATE]
proof (prove)
using this:
\<not> closed I

goal (1 subgoal):
 1. \<not> closed I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> closed I

goal (1 subgoal):
 1. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
have "open I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open I
[PROOF STEP]
proof (rule Topological_Spaces.openI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
assume c:"x \<in> I"
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (1 subgoal):
 1. \<And>x. x \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
proof (cases "\<exists>y. y < x \<and> y \<in> I")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>y<x. y \<in> I

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y<x. y \<in> I
[PROOF STEP]
obtain y where a:"y < x \<and> y \<in> I"
[PROOF STATE]
proof (prove)
using this:
\<exists>y<x. y \<in> I

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

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
have "open {y<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open {y<..}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
open {y<..}

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
open {y<..}

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
have "x \<in> {y<..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {y<..}
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
y < x \<and> y \<in> I

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

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> {y<..}

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
have "{y<..} \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y<..} \<subseteq> I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {y<..} \<Longrightarrow> x \<in> I
[PROOF STEP]
using a assms(1)
[PROOF STATE]
proof (prove)
using this:
y < x \<and> y \<in> I
up_ray I

goal (1 subgoal):
 1. \<And>x. x \<in> {y<..} \<Longrightarrow> x \<in> I
[PROOF STEP]
apply (simp add: up_ray_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>y < xa; y < x \<and> y \<in> I; \<forall>x. x \<in> I \<longrightarrow> (\<forall>y\<ge>x. y \<in> I)\<rbrakk> \<Longrightarrow> xa \<in> I
[PROOF STEP]
by (metis less_le_not_le)
[PROOF STATE]
proof (state)
this:
{y<..} \<subseteq> I

goal (2 subgoals):
 1. \<exists>y<x. y \<in> I \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
 2. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
open {y<..}
x \<in> {y<..}
{y<..} \<subseteq> I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
open {y<..}
x \<in> {y<..}
{y<..} \<subseteq> I

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

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>y<x. y \<in> I)

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
hence "I \<subseteq> {x..}"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y<x. y \<in> I)

goal (1 subgoal):
 1. I \<subseteq> {x..}
[PROOF STEP]
using linorder_not_less
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y<x. y \<in> I)
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. I \<subseteq> {x..}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<subseteq> {x..}

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
I \<subseteq> {x..}

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
have "{x..} \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x..} \<subseteq> I
[PROOF STEP]
using c assms(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> I
up_ray I

goal (1 subgoal):
 1. {x..} \<subseteq> I
[PROOF STEP]
apply (simp add: up_ray_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> I; \<forall>x. x \<in> I \<longrightarrow> (\<forall>y\<ge>x. y \<in> I)\<rbrakk> \<Longrightarrow> {x..} \<subseteq> I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x..} \<subseteq> I

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
I \<subseteq> {x..}
{x..} \<subseteq> I
[PROOF STEP]
have "I = {x..}"
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> {x..}
{x..} \<subseteq> I

goal (1 subgoal):
 1. I = {x..}
[PROOF STEP]
by (rule order_antisym)
[PROOF STATE]
proof (state)
this:
I = {x..}

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
I = {x..}

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
have "closed {x..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {x..}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed {x..}

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
I = {x..}
closed {x..}
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
I = {x..}
closed {x..}

goal (1 subgoal):
 1. False
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
I = {x..}
closed {x..}
\<not> closed I

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

goal (1 subgoal):
 1. \<not> (\<exists>y<x. y \<in> I) \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I

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

goal (1 subgoal):
 1. \<not> closed I \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
open I

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I \<in> sets borel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma down_ray_borel:
  assumes "down_ray (I :: (('a :: linorder_topology) set))"
  shows "I \<in> borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
have "up_ray (-I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_ray (- I)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
down_ray I

goal (1 subgoal):
 1. up_ray (- I)
[PROOF STEP]
by (simp add: up_ray_def down_ray_def, blast)
[PROOF STATE]
proof (state)
this:
up_ray (- I)

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
hence "(-I) \<in> borel"
[PROOF STATE]
proof (prove)
using this:
up_ray (- I)

goal (1 subgoal):
 1. - I \<in> sets borel
[PROOF STEP]
using up_ray_borel
[PROOF STATE]
proof (prove)
using this:
up_ray (- I)
up_ray ?I \<Longrightarrow> ?I \<in> sets borel

goal (1 subgoal):
 1. - I \<in> sets borel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- I \<in> sets borel

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
thus "I \<in> borel"
[PROOF STATE]
proof (prove)
using this:
- I \<in> sets borel

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
by (metis borel_comp double_complement)
[PROOF STATE]
proof (state)
this:
I \<in> sets borel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interval_borel:
  assumes "interval (I :: (('a :: linorder_topology) set))"
  shows "I \<in> borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
proof (cases "I = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. I = {} \<Longrightarrow> I \<in> sets borel
 2. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
I = {}

goal (2 subgoals):
 1. I = {} \<Longrightarrow> I \<in> sets borel
 2. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I = {}

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I \<in> sets borel

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
I \<noteq> {}

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I \<noteq> {}
[PROOF STEP]
obtain x where a:"x \<in> I"
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {}

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

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
have "\<And>y z. y \<in> I \<union> {x..} \<Longrightarrow> y \<le> z \<Longrightarrow> z \<in> I \<union> {x..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>y \<in> I \<union> {x..}; y \<le> z\<rbrakk> \<Longrightarrow> z \<in> I \<union> {x..}
[PROOF STEP]
by (metis assms a interval_def  IntE UnE Un_Int_eq(1) Un_Int_eq(2) atLeast_iff nle_le order.trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> I \<union> {x..}; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?z \<in> I \<union> {x..}

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
hence "up_ray (I \<union> {x..})"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> I \<union> {x..}; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?z \<in> I \<union> {x..}

goal (1 subgoal):
 1. up_ray (I \<union> {x..})
[PROOF STEP]
using up_ray_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> I \<union> {x..}; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?z \<in> I \<union> {x..}
up_ray ?I = (\<forall>x y. x \<in> ?I \<longrightarrow> x \<le> y \<longrightarrow> y \<in> ?I)

goal (1 subgoal):
 1. up_ray (I \<union> {x..})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
up_ray (I \<union> {x..})

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
hence b:"I \<union> {x..} \<in> borel"
[PROOF STATE]
proof (prove)
using this:
up_ray (I \<union> {x..})

goal (1 subgoal):
 1. I \<union> {x..} \<in> sets borel
[PROOF STEP]
using up_ray_borel
[PROOF STATE]
proof (prove)
using this:
up_ray (I \<union> {x..})
up_ray ?I \<Longrightarrow> ?I \<in> sets borel

goal (1 subgoal):
 1. I \<union> {x..} \<in> sets borel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I \<union> {x..} \<in> sets borel

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
have "\<And>y z. y \<in> I \<union> {..x} \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> I \<union> {..x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>y \<in> I \<union> {..x}; z \<le> y\<rbrakk> \<Longrightarrow> z \<in> I \<union> {..x}
[PROOF STEP]
by (metis assms a interval_def UnE UnI1 UnI2 atMost_iff dual_order.trans linorder_le_cases)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> I \<union> {..x}; ?z \<le> ?y\<rbrakk> \<Longrightarrow> ?z \<in> I \<union> {..x}

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
hence "down_ray (I \<union> {..x})"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> I \<union> {..x}; ?z \<le> ?y\<rbrakk> \<Longrightarrow> ?z \<in> I \<union> {..x}

goal (1 subgoal):
 1. down_ray (I \<union> {..x})
[PROOF STEP]
using down_ray_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> I \<union> {..x}; ?z \<le> ?y\<rbrakk> \<Longrightarrow> ?z \<in> I \<union> {..x}
down_ray ?I = (\<forall>x y. y \<in> ?I \<longrightarrow> x \<le> y \<longrightarrow> x \<in> ?I)

goal (1 subgoal):
 1. down_ray (I \<union> {..x})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
down_ray (I \<union> {..x})

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
hence c:"I \<union> {..x} \<in> borel"
[PROOF STATE]
proof (prove)
using this:
down_ray (I \<union> {..x})

goal (1 subgoal):
 1. I \<union> {..x} \<in> sets borel
[PROOF STEP]
using down_ray_borel
[PROOF STATE]
proof (prove)
using this:
down_ray (I \<union> {..x})
down_ray ?I \<Longrightarrow> ?I \<in> sets borel

goal (1 subgoal):
 1. I \<union> {..x} \<in> sets borel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I \<union> {..x} \<in> sets borel

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
have "I = (I \<union> {x..}) \<inter> (I \<union> {..x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I = (I \<union> {x..}) \<inter> (I \<union> {..x})
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. I = (I \<union> {x..}) \<inter> (I \<union> {..x})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
I = (I \<union> {x..}) \<inter> (I \<union> {..x})

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> I \<in> sets borel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I = (I \<union> {x..}) \<inter> (I \<union> {..x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I = (I \<union> {x..}) \<inter> (I \<union> {..x})

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
using b c
[PROOF STATE]
proof (prove)
using this:
I = (I \<union> {x..}) \<inter> (I \<union> {..x})
I \<union> {x..} \<in> sets borel
I \<union> {..x} \<in> sets borel

goal (1 subgoal):
 1. I \<in> sets borel
[PROOF STEP]
by (metis sets.Int)
[PROOF STATE]
proof (state)
this:
I \<in> sets borel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sort_map_ind:
  "sort_map f (Suc n) = fold id [sort_primitive j n. j <- [0..<n]] (sort_map f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort_map f (Suc n) = fold id (map (\<lambda>j. sort_primitive j n) [0..<n]) (sort_map f n)
[PROOF STEP]
by simp


[STATEMENT]
lemma sort_map_strict_mono:
  fixes f :: "nat \<Rightarrow> 'b :: linorder"
  shows "j < n \<Longrightarrow> i < j \<Longrightarrow> sort_map f n i \<le> sort_map f n j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j
[PROOF STEP]
proof (induction n arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>j < 0; i < j\<rbrakk> \<Longrightarrow> sort_map f 0 i \<le> sort_map f 0 j
 2. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j < 0
i < j

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>j < 0; i < j\<rbrakk> \<Longrightarrow> sort_map f 0 i \<le> sort_map f 0 j
 2. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < 0
i < j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
j < 0
i < j

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

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j < n; ?i < ?j\<rbrakk> \<Longrightarrow> sort_map f n ?i \<le> sort_map f n ?j
j < Suc n
i < j

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
define g where "g = (\<lambda>k. fold id [sort_primitive j n. j <- [0..<k]] (sort_map f n))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>k. fold id (map (\<lambda>j. sort_primitive j n) [0..<k]) (sort_map f n))

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
define k where "k = n"
[PROOF STATE]
proof (state)
this:
k = n

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
have a:"(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l. l < k \<longrightarrow> g k l \<le> g k n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n)
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g 0 i \<le> g 0 j) \<and> (\<forall>l<0. g 0 l \<le> g 0 n)
 2. \<And>k. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n) \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g 0 i \<le> g 0 j) \<and> (\<forall>l<0. g 0 l \<le> g 0 n)
 2. \<And>k. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n) \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g 0 i \<le> g 0 j) \<and> (\<forall>l<0. g 0 l \<le> g 0 n)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j < n; ?i < ?j\<rbrakk> \<Longrightarrow> sort_map f n ?i \<le> sort_map f n ?j
j < Suc n
i < j

goal (1 subgoal):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g 0 i \<le> g 0 j) \<and> (\<forall>l<0. g 0 l \<le> g 0 n)
[PROOF STEP]
by (simp add:g_def del:sort_map.simps)
[PROOF STATE]
proof (state)
this:
(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g 0 i \<le> g 0 j) \<and> (\<forall>l<0. g 0 l \<le> g 0 n)

goal (1 subgoal):
 1. \<And>k. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n) \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n) \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n)

goal (1 subgoal):
 1. \<And>k. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n) \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
have "g (Suc k) = sort_primitive k n (g k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (Suc k) = sort_primitive k n (g k)
[PROOF STEP]
by (simp add:g_def)
[PROOF STATE]
proof (state)
this:
g (Suc k) = sort_primitive k n (g k)

goal (1 subgoal):
 1. \<And>k. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n) \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g (Suc k) = sort_primitive k n (g k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
g (Suc k) = sort_primitive k n (g k)

goal (1 subgoal):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
g (Suc k) = sort_primitive k n (g k)
(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n)

goal (1 subgoal):
 1. (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
apply (cases "g k k \<le> g k n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); g k k \<le> g k n\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
 2. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
apply (simp add:min_def max_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); g k k \<le> g k n\<rbrakk> \<Longrightarrow> n = k \<longrightarrow> (\<forall>l. l \<noteq> k \<longrightarrow> l < Suc k \<longrightarrow> g k l \<le> g k k)
 2. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
using less_antisym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> ?n < ?m; ?n < Suc ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (2 subgoals):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); g k k \<le> g k n\<rbrakk> \<Longrightarrow> n = k \<longrightarrow> (\<forall>l. l \<noteq> k \<longrightarrow> l < Suc k \<longrightarrow> g k l \<le> g k k)
 2. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
apply (cases "g k n \<le> g k k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n; g k n \<le> g k k\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
 2. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n; \<not> g k n \<le> g k k\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
apply (simp add:min_def max_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); g k k \<noteq> g k n; g k n \<le> g k k\<rbrakk> \<Longrightarrow> (n = k \<longrightarrow> (\<forall>l. l \<noteq> k \<longrightarrow> l < Suc k \<longrightarrow> g k l \<le> g k k)) \<and> (n \<noteq> k \<longrightarrow> (\<forall>j<n. k < j \<longrightarrow> g k n \<le> g k j) \<and> (\<forall>l. l \<noteq> n \<longrightarrow> l \<noteq> k \<longrightarrow> l < Suc k \<longrightarrow> g k l \<le> g k k))
 2. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n; \<not> g k n \<le> g k k\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
apply (metis less_antisym max.coboundedI2 max.orderE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g (Suc k) = sort_primitive k n (g k); (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n); \<not> g k k \<le> g k n; \<not> g k n \<le> g k k\<rbrakk> \<Longrightarrow> (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g (Suc k) i \<le> g (Suc k) j) \<and> (\<forall>l<Suc k. g (Suc k) l \<le> g (Suc k) n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n)

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
hence "\<And>i j. j < Suc n \<Longrightarrow> i < j \<Longrightarrow> g n i \<le> g n j"
[PROOF STATE]
proof (prove)
using this:
(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l<k. g k l \<le> g k n)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < Suc n; i < j\<rbrakk> \<Longrightarrow> g n i \<le> g n j
[PROOF STEP]
apply (simp add:k_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < Suc n; i < j; (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g n i \<le> g n j) \<and> (\<forall>l<n. g n l \<le> g n n)\<rbrakk> \<Longrightarrow> g n i \<le> g n j
[PROOF STEP]
using less_antisym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> ?n < ?m; ?n < Suc ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < Suc n; i < j; (\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g n i \<le> g n j) \<and> (\<forall>l<n. g n l \<le> g n n)\<rbrakk> \<Longrightarrow> g n i \<le> g n j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j < Suc n; ?i < ?j\<rbrakk> \<Longrightarrow> g n ?i \<le> g n ?j

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j < Suc n; ?i < ?j\<rbrakk> \<Longrightarrow> g n ?i \<le> g n ?j

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
have "sort_map f (Suc n) = g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort_map f (Suc n) = g n
[PROOF STEP]
by (simp add:sort_map_ind g_def del:sort_map.simps)
[PROOF STATE]
proof (state)
this:
sort_map f (Suc n) = g n

goal (1 subgoal):
 1. \<And>n i j. \<lbrakk>\<And>i j. \<lbrakk>j < n; i < j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j; j < Suc n; i < j\<rbrakk> \<Longrightarrow> sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?j < Suc n; ?i < ?j\<rbrakk> \<Longrightarrow> g n ?i \<le> g n ?j
sort_map f (Suc n) = g n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j < Suc n; ?i < ?j\<rbrakk> \<Longrightarrow> g n ?i \<le> g n ?j
sort_map f (Suc n) = g n

goal (1 subgoal):
 1. sort_map f (Suc n) i \<le> sort_map f (Suc n) j
[PROOF STEP]
apply (simp del:sort_map.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>j i. \<lbrakk>j < Suc n; i < j\<rbrakk> \<Longrightarrow> g n i \<le> g n j; sort_map f (Suc n) = g n\<rbrakk> \<Longrightarrow> g n i \<le> g n j
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j < n; ?i < ?j\<rbrakk> \<Longrightarrow> sort_map f n ?i \<le> sort_map f n ?j
j < Suc n
i < j

goal (1 subgoal):
 1. \<lbrakk>\<And>j i. \<lbrakk>j < Suc n; i < j\<rbrakk> \<Longrightarrow> g n i \<le> g n j; sort_map f (Suc n) = g n\<rbrakk> \<Longrightarrow> g n i \<le> g n j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sort_map f (Suc n) i \<le> sort_map f (Suc n) j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sort_map_mono:
  fixes f :: "nat \<Rightarrow> 'b :: linorder"
  shows "j < n \<Longrightarrow> i \<le> j \<Longrightarrow> sort_map f n i \<le> sort_map f n j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < n; i \<le> j\<rbrakk> \<Longrightarrow> sort_map f n i \<le> sort_map f n j
[PROOF STEP]
by (metis sort_map_strict_mono eq_iff le_imp_less_or_eq)


[STATEMENT]
lemma sort_map_perm:
  fixes f :: "nat \<Rightarrow> 'b :: linorder"
  shows "image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
define is_swap where "is_swap = (\<lambda>(ts :: ((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b)). \<exists>i < n. \<exists>j < n. ts = sort_primitive i j)"
[PROOF STATE]
proof (state)
this:
is_swap = (\<lambda>ts. \<exists>i<n. \<exists>j<n. ts = sort_primitive i j)

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
define t :: "((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b) list"
    where "t = [sort_primitive j i. i <- [0..<n], j <- [0..<i]]"
[PROOF STATE]
proof (state)
this:
t = concat (map (\<lambda>i. map (\<lambda>j. sort_primitive j i) [0..<i]) [0..<n])

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
have a: "\<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
fix f :: "nat \<Rightarrow> 'b :: linorder"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
assume "is_swap x"
[PROOF STATE]
proof (state)
this:
is_swap x

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_swap x
[PROOF STEP]
obtain i j where x_def: "x = sort_primitive i j" and i_bound: "i < n" and j_bound:"j < n"
[PROOF STATE]
proof (prove)
using this:
is_swap x

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>x = sort_primitive i j; i < n; j < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_swap_def
[PROOF STATE]
proof (prove)
using this:
is_swap x
is_swap = (\<lambda>ts. \<exists>i<n. \<exists>j<n. ts = sort_primitive i j)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>x = sort_primitive i j; i < n; j < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = sort_primitive i j
i < n
j < n

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
define inv where "inv = mset_set {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j}"
[PROOF STATE]
proof (state)
this:
inv = mset_set {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j}

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
have b:"{0..<n} = {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j} \<union> {i,j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<n} = {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j} \<union> {i, j}
[PROOF STEP]
apply (rule order_antisym, rule subsetI, simp, blast, rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x = i \<or> x = j \<or> x < n \<and> x \<noteq> i \<and> x \<noteq> j \<Longrightarrow> x < n
[PROOF STEP]
using i_bound j_bound
[PROOF STATE]
proof (prove)
using this:
i < n
j < n

goal (1 subgoal):
 1. \<And>x. x = i \<or> x = j \<or> x < n \<and> x \<noteq> i \<and> x \<noteq> j \<Longrightarrow> x < n
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
{0..<n} = {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j} \<union> {i, j}

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
have c:"\<And>k. k \<in># inv \<Longrightarrow> (x f) k = f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k \<in># inv \<Longrightarrow> x f k = f k
[PROOF STEP]
by (simp add:x_def inv_def)
[PROOF STATE]
proof (state)
this:
?k \<in># inv \<Longrightarrow> x f ?k = f ?k

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
have "image_mset (x f) inv = image_mset f inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset (x f) inv = image_mset f inv
[PROOF STEP]
apply (rule multiset_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. count (image_mset (x f) inv) xa = count (image_mset f inv) xa
[PROOF STEP]
using c multiset.map_cong0
[PROOF STATE]
proof (prove)
using this:
?k \<in># inv \<Longrightarrow> x f ?k = f ?k
(\<And>z. z \<in># ?x \<Longrightarrow> ?f z = ?g z) \<Longrightarrow> image_mset ?f ?x = image_mset ?g ?x

goal (1 subgoal):
 1. \<And>xa. count (image_mset (x f) inv) xa = count (image_mset f inv) xa
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
image_mset (x f) inv = image_mset f inv

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
image_mset (x f) inv = image_mset f inv

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
have "image_mset (x f) (mset_set {i,j}) = image_mset f (mset_set {i,j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})
[PROOF STEP]
apply (cases "i = j")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i = j \<Longrightarrow> image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})
 2. i \<noteq> j \<Longrightarrow> image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})
[PROOF STEP]
by (simp add:x_def max_def min_def)+
[PROOF STATE]
proof (state)
this:
image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
have "mset_set {0..<n} = inv + mset_set {i,j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set {0..<n} = inv + mset_set {i, j}
[PROOF STEP]
by (simp only:inv_def b, rule mset_set_Union, simp, simp, simp)
[PROOF STATE]
proof (state)
this:
mset_set {0..<n} = inv + mset_set {i, j}

goal (1 subgoal):
 1. \<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
image_mset (x f) inv = image_mset f inv
image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})
mset_set {0..<n} = inv + mset_set {i, j}
[PROOF STEP]
show "image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})"
[PROOF STATE]
proof (prove)
using this:
image_mset (x f) inv = image_mset f inv
image_mset (x f) (mset_set {i, j}) = image_mset f (mset_set {i, j})
mset_set {0..<n} = inv + mset_set {i, j}

goal (1 subgoal):
 1. image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_swap ?x \<Longrightarrow> image_mset (?x ?f) (mset_set {0..<n}) = image_mset ?f (mset_set {0..<n})

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
have "(\<forall>x \<in> set t. is_swap x) \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set t. is_swap x \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
by (induction t arbitrary:f, simp, simp add:a)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
have "\<And>x. x \<in> set t \<Longrightarrow> is_swap x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set t \<Longrightarrow> is_swap x
[PROOF STEP]
apply (simp add:t_def is_swap_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>xa\<in>{0..<n}. x \<in> (\<lambda>x. sort_primitive x xa) ` {0..<xa} \<Longrightarrow> \<exists>i<n. \<exists>j<n. x = sort_primitive i j
[PROOF STEP]
by (meson atLeastLessThan_iff imageE less_imp_le less_le_trans)
[PROOF STATE]
proof (state)
this:
?x \<in> set t \<Longrightarrow> is_swap ?x

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])
?x \<in> set t \<Longrightarrow> is_swap ?x
[PROOF STEP]
have "image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])
?x \<in> set t \<Longrightarrow> is_swap ?x

goal (1 subgoal):
 1. image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])

goal (1 subgoal):
 1. image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])
[PROOF STEP]
by (simp add:t_def)
[PROOF STATE]
proof (state)
this:
image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_eq_iff:
  assumes "mset xs = mset ys"
  assumes "sorted xs"
  assumes "sorted ys"
  shows "xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
using assms properties_for_sort
[PROOF STATE]
proof (prove)
using this:
mset xs = mset ys
sorted xs
sorted ys
\<lbrakk>mset ?ys = mset ?xs; sorted ?ys\<rbrakk> \<Longrightarrow> sort ?xs = ?ys

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
by blast


[STATEMENT]
lemma sort_map_eq_sort:
  fixes f :: "nat \<Rightarrow> ('b :: linorder)"
  shows "map (sort_map f n) [0..<n] = sort (map f [0..<n])" (is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
have "mset ?A = mset ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))
[PROOF STEP]
using sort_map_perm[where f="f" and n="n"]
[PROOF STATE]
proof (prove)
using this:
image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])

goal (1 subgoal):
 1. mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))
[PROOF STEP]
by (simp del:sort_map.simps)
[PROOF STATE]
proof (state)
this:
mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
have "sorted ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (sort (map f [0..<n]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted (sort (map f [0..<n]))

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (sort (map f [0..<n]))

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
have "sorted ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map (sort_map f n) [0..<n])
[PROOF STEP]
apply (subst sorted_wrt_iff_nth_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> j < length (map (sort_map f n) [0..<n]) \<longrightarrow> map (sort_map f n) [0..<n] ! i \<le> map (sort_map f n) [0..<n] ! j
[PROOF STEP]
apply (simp del:sort_map.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> j < n \<longrightarrow> sort_map f n i \<le> sort_map f n j
[PROOF STEP]
by (metis sort_map_mono nat_less_le)
[PROOF STATE]
proof (state)
this:
sorted (map (sort_map f n) [0..<n])

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))
sorted (sort (map f [0..<n]))
sorted (map (sort_map f n) [0..<n])
[PROOF STEP]
show "?A = ?B"
[PROOF STATE]
proof (prove)
using this:
mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))
sorted (sort (map f [0..<n]))
sorted (map (sort_map f n) [0..<n])

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
using list_eq_iff
[PROOF STATE]
proof (prove)
using this:
mset (map (sort_map f n) [0..<n]) = mset (sort (map f [0..<n]))
sorted (sort (map f [0..<n]))
sorted (map (sort_map f n) [0..<n])
\<lbrakk>mset ?xs = mset ?ys; sorted ?xs; sorted ?ys\<rbrakk> \<Longrightarrow> ?xs = ?ys

goal (1 subgoal):
 1. map (sort_map f n) [0..<n] = sort (map f [0..<n])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (sort_map f n) [0..<n] = sort (map f [0..<n])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma order_statistics_measurable_aux:
  fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> ('b :: {linorder_topology, second_countable_topology})"
  assumes "n \<ge> 1"
  assumes "j < n"
  assumes "\<And>i. i < n \<Longrightarrow> X i \<in> measurable M borel"
  shows "(\<lambda>x. (sort_map (\<lambda>i. X i x) n) j) \<in> measurable M borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
have n_ge_0:"n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> n
j < n
?i < n \<Longrightarrow> X ?i \<in> borel_measurable M

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

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
define is_swap where "is_swap = (\<lambda>(ts :: ((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b)). \<exists>i < n. \<exists>j < n. ts = sort_primitive i j)"
[PROOF STATE]
proof (state)
this:
is_swap = (\<lambda>ts. \<exists>i<n. \<exists>j<n. ts = sort_primitive i j)

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
define t :: "((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b) list"
    where "t = [sort_primitive j i. i <- [0..<n], j <- [0..<i]]"
[PROOF STATE]
proof (state)
this:
t = concat (map (\<lambda>i. map (\<lambda>j. sort_primitive j i) [0..<i]) [0..<n])

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
define meas_ptw :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
    where "meas_ptw = (\<lambda>f. (\<forall>k. k < n \<longrightarrow> f k \<in> borel_measurable M))"
[PROOF STATE]
proof (state)
this:
meas_ptw = (\<lambda>f. \<forall>k<n. f k \<in> borel_measurable M)

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
have ind_step:
    "\<And>x (g :: nat \<Rightarrow> 'a \<Rightarrow> 'b). meas_ptw g \<Longrightarrow> is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
fix x g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
assume "meas_ptw g"
[PROOF STATE]
proof (state)
this:
meas_ptw g

goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
hence a:"\<And>k. k < n \<Longrightarrow> g k \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
meas_ptw g

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> g k \<in> borel_measurable M
[PROOF STEP]
by (simp add:meas_ptw_def)
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> g ?k \<in> borel_measurable M

goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
assume "is_swap x"
[PROOF STATE]
proof (state)
this:
is_swap x

goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_swap x
[PROOF STEP]
obtain i j where x_def:"x=sort_primitive i j" and i_le:"i < n" and j_le:"j < n"
[PROOF STATE]
proof (prove)
using this:
is_swap x

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>x = sort_primitive i j; i < n; j < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add:is_swap_def, blast)
[PROOF STATE]
proof (state)
this:
x = sort_primitive i j
i < n
j < n

goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
have "\<And>k. k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M
[PROOF STEP]
assume "k < n"
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. \<And>k. k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M
[PROOF STEP]
thus " (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M
[PROOF STEP]
apply (simp add:x_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
apply (cases "k = i", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < n; k = i\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. min (g i \<omega>) (g j \<omega>)) \<in> borel_measurable M
 2. \<lbrakk>k < n; k \<noteq> i\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
using a i_le j_le borel_measurable_min
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> g ?k \<in> borel_measurable M
i < n
j < n
\<lbrakk>?f \<in> borel_measurable ?M; ?g \<in> borel_measurable ?M\<rbrakk> \<Longrightarrow> (\<lambda>x. min (?g x) (?f x)) \<in> borel_measurable ?M

goal (2 subgoals):
 1. \<lbrakk>i < n; k = i\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. min (g i \<omega>) (g j \<omega>)) \<in> borel_measurable M
 2. \<lbrakk>k < n; k \<noteq> i\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < n; k \<noteq> i\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
apply (cases "k = j", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>j < n; j \<noteq> i; k = j\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. max (g i \<omega>) (g j \<omega>)) \<in> borel_measurable M
 2. \<lbrakk>k < n; k \<noteq> i; k \<noteq> j\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
using a i_le j_le borel_measurable_max
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> g ?k \<in> borel_measurable M
i < n
j < n
\<lbrakk>?f \<in> borel_measurable ?M; ?g \<in> borel_measurable ?M\<rbrakk> \<Longrightarrow> (\<lambda>x. max (?g x) (?f x)) \<in> borel_measurable ?M

goal (2 subgoals):
 1. \<lbrakk>j < n; j \<noteq> i; k = j\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. max (g i \<omega>) (g j \<omega>)) \<in> borel_measurable M
 2. \<lbrakk>k < n; k \<noteq> i; k \<noteq> j\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < n; k \<noteq> i; k \<noteq> j\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> g ?k \<in> borel_measurable M

goal (1 subgoal):
 1. \<lbrakk>k < n; k \<noteq> i; k \<noteq> j\<rbrakk> \<Longrightarrow> (\<lambda>\<omega>. if k = i then min (g i \<omega>) (g j \<omega>) else if k = j then max (g i \<omega>) (g j \<omega>) else g k \<omega>) \<in> borel_measurable M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) ?k) \<in> borel_measurable M

goal (1 subgoal):
 1. \<And>x g. \<lbrakk>meas_ptw g; is_swap x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
thus "meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) ?k) \<in> borel_measurable M

goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)
[PROOF STEP]
by (simp add:meas_ptw_def)
[PROOF STATE]
proof (state)
this:
meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>meas_ptw ?g; is_swap ?x\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. ?x (\<lambda>i. ?g i \<omega>) k)

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
have "(\<forall>x \<in> set t. is_swap x) \<Longrightarrow> meas_ptw (\<lambda> k \<omega>. (fold id t (\<lambda>k. X k \<omega>)) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set t. is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id t (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
proof (induction t rule:rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (set []) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id [] (\<lambda>k. X k \<omega>) k)
 2. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set []. is_swap a

goal (2 subgoals):
 1. Ball (set []) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id [] (\<lambda>k. X k \<omega>) k)
 2. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set []. is_swap a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set []. is_swap a

goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. fold id [] (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set []. is_swap a
1 \<le> n
j < n
?i < n \<Longrightarrow> X ?i \<in> borel_measurable M

goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. fold id [] (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
by (simp add:meas_ptw_def)
[PROOF STATE]
proof (state)
this:
meas_ptw (\<lambda>k \<omega>. fold id [] (\<lambda>k. X k \<omega>) k)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set xs. is_swap a \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k)
\<forall>a\<in>set (xs @ [x]). is_swap a

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
have a:"meas_ptw (\<lambda>k \<omega>. fold (\<lambda>a. a) xs (\<lambda>k. X k \<omega>) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. fold (\<lambda>a. a) xs (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs. is_swap a \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k)
\<forall>a\<in>set (xs @ [x]). is_swap a

goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. fold (\<lambda>a. a) xs (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
meas_ptw (\<lambda>k \<omega>. fold (\<lambda>a. a) xs (\<lambda>k. X k \<omega>) k)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
have b:"is_swap x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_swap x
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs. is_swap a \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k)
\<forall>a\<in>set (xs @ [x]). is_swap a

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

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>Ball (set xs) is_swap \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id xs (\<lambda>k. X k \<omega>) k); Ball (set (xs @ [x])) is_swap\<rbrakk> \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
using ind_step[OF a b]
[PROOF STATE]
proof (prove)
using this:
meas_ptw (\<lambda>k \<omega>. x (fold (\<lambda>a. a) xs (\<lambda>k. X k \<omega>)) k)

goal (1 subgoal):
 1. meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
meas_ptw (\<lambda>k \<omega>. fold id (xs @ [x]) (\<lambda>k. X k \<omega>) k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id t (\<lambda>k. X k \<omega>) k)

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id t (\<lambda>k. X k \<omega>) k)

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
have "\<And>x. x \<in> set t \<Longrightarrow> is_swap x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set t \<Longrightarrow> is_swap x
[PROOF STEP]
apply (simp add:t_def is_swap_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>xa\<in>{0..<n}. x \<in> (\<lambda>x. sort_primitive x xa) ` {0..<xa} \<Longrightarrow> \<exists>i<n. \<exists>j<n. x = sort_primitive i j
[PROOF STEP]
by (meson atLeastLessThan_iff imageE less_imp_le less_le_trans)
[PROOF STATE]
proof (state)
this:
?x \<in> set t \<Longrightarrow> is_swap ?x

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id t (\<lambda>k. X k \<omega>) k)
?x \<in> set t \<Longrightarrow> is_swap ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id t (\<lambda>k. X k \<omega>) k)
?x \<in> set t \<Longrightarrow> is_swap ?x

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set t. is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. fold id t (\<lambda>k. X k \<omega>) k)
?x \<in> set t \<Longrightarrow> is_swap ?x
1 \<le> n
j < n
?i < n \<Longrightarrow> X ?i \<in> borel_measurable M

goal (1 subgoal):
 1. (\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M
[PROOF STEP]
by (simp add:t_def[symmetric] meas_ptw_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. sort_map (\<lambda>i. X i x) n j) \<in> borel_measurable M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma order_statistics_measurable:
  fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> ('b :: {linorder_topology, second_countable_topology})"
  assumes "n \<ge> 1"
  assumes "j < n"
  assumes "\<And>i. i < n \<Longrightarrow> X i \<in> measurable M borel"
  shows "(\<lambda>x. (sort (map (\<lambda>i. X i x) [0..<n])) ! j) \<in> measurable M borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sort (map (\<lambda>i. X i x) [0..<n]) ! j) \<in> borel_measurable M
[PROOF STEP]
apply (subst sort_map_eq_sort[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. map (sort_map (\<lambda>i. X i x) n) [0..<n] ! j) \<in> borel_measurable M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> n
j < n
?i < n \<Longrightarrow> X ?i \<in> borel_measurable M

goal (1 subgoal):
 1. (\<lambda>x. map (sort_map (\<lambda>i. X i x) n) [0..<n] ! j) \<in> borel_measurable M
[PROOF STEP]
by (simp add:order_statistics_measurable_aux del:sort_map.simps)


[STATEMENT]
lemma median_measurable:
  fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> ('b :: {linorder_topology, second_countable_topology})"
  assumes "n \<ge> 1"
  assumes "\<And>i. i < n \<Longrightarrow> X i \<in> measurable M borel"
  shows "(\<lambda>x. median n (\<lambda>i. X i x)) \<in> measurable M borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. median n (\<lambda>i. X i x)) \<in> borel_measurable M
[PROOF STEP]
apply (simp add:median_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sort (map (\<lambda>i. X i x) [0..<n]) ! (n div 2)) \<in> borel_measurable M
[PROOF STEP]
apply (rule order_statistics_measurable[OF assms(1) _ assms(2)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n div 2 < n
 2. \<And>i. i < n \<Longrightarrow> i < n
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
1 \<le> n

goal (2 subgoals):
 1. n div 2 < n
 2. \<And>i. i < n \<Longrightarrow> i < n
[PROOF STEP]
by force+


[STATEMENT]
lemma interval_rule:
  assumes "interval I"
  assumes "a \<le> x" "x \<le> b"
  assumes "a \<in> I"
  assumes "b \<in> I"
  shows "x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
interval I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
apply (simp add:interval_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> I \<longrightarrow> (\<forall>y z. z \<in> I \<longrightarrow> x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> y \<in> I) \<Longrightarrow> x \<in> I
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
interval I
a \<le> x
x \<le> b
a \<in> I
b \<in> I

goal (1 subgoal):
 1. \<forall>x. x \<in> I \<longrightarrow> (\<forall>y z. z \<in> I \<longrightarrow> x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> y \<in> I) \<Longrightarrow> x \<in> I
[PROOF STEP]
by blast


[STATEMENT]
lemma sorted_int:
  assumes "interval I"
  assumes "sorted xs"
  assumes "k < length xs" "i \<le> j" "j \<le> k "
  assumes "xs ! i \<in> I" "xs ! k \<in> I"
  shows "xs ! j \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! j \<in> I
[PROOF STEP]
apply (rule interval_rule[where a="xs ! i" and b="xs ! k"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. interval I
 2. xs ! i \<le> xs ! j
 3. xs ! j \<le> xs ! k
 4. xs ! i \<in> I
 5. xs ! k \<in> I
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
interval I
sorted xs
k < length xs
i \<le> j
j \<le> k
xs ! i \<in> I
xs ! k \<in> I

goal (5 subgoals):
 1. interval I
 2. xs ! i \<le> xs ! j
 3. xs ! j \<le> xs ! k
 4. xs ! i \<in> I
 5. xs ! k \<in> I
[PROOF STEP]
by (simp add: sorted_nth_mono)+


[STATEMENT]
lemma mid_in_interval:
  assumes "2*length (filter (\<lambda>x. x \<in> I) xs) > length xs"
  assumes "interval I"
  assumes "sorted xs"
  shows "xs ! (length xs div 2) \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
have "length (filter (\<lambda>x. x \<in> I) xs) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (filter (\<lambda>x. x \<in> I) xs)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
length xs < 2 * length (filter (\<lambda>x. x \<in> I) xs)

goal (1 subgoal):
 1. 0 < length (filter (\<lambda>x. x \<in> I) xs)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < length (filter (\<lambda>x. x \<in> I) xs)

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < length (filter (\<lambda>x. x \<in> I) xs)
[PROOF STEP]
obtain v where v_1: "v < length xs" and v_2: "xs ! v \<in> I"
[PROOF STATE]
proof (prove)
using this:
0 < length (filter (\<lambda>x. x \<in> I) xs)

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v < length xs; xs ! v \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis filter_False in_set_conv_nth length_greater_0_conv)
[PROOF STATE]
proof (state)
this:
v < length xs
xs ! v \<in> I

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
define J where "J = {k. k < length xs \<and> xs ! k \<in> I}"
[PROOF STATE]
proof (state)
this:
J = {k. k < length xs \<and> xs ! k \<in> I}

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
have card_J_min: "2*card J > length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs < 2 * card J
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
length xs < 2 * length (filter (\<lambda>x. x \<in> I) xs)

goal (1 subgoal):
 1. length xs < 2 * card J
[PROOF STEP]
by (simp add:J_def length_filter_conv_card)
[PROOF STATE]
proof (state)
this:
length xs < 2 * card J

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
consider
    (a) "xs ! (length xs div 2) \<in> I" |
    (b) "xs ! (length xs div 2) \<notin> I \<and> v > (length xs div 2)" |
    (c) "xs ! (length xs div 2) \<notin> I \<and> v < (length xs div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs ! (length xs div 2) \<in> I \<Longrightarrow> thesis; xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> thesis; xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis linorder_cases v_2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs ! (length xs div 2) \<in> I \<Longrightarrow> ?thesis; xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> ?thesis; xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xs ! (length xs div 2) \<in> I \<Longrightarrow> ?thesis; xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> ?thesis; xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs ! (length xs div 2) \<in> I \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 3. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<in> I

goal (3 subgoals):
 1. xs ! (length xs div 2) \<in> I \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 3. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs ! (length xs div 2) \<in> I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs ! (length xs div 2) \<in> I

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<in> I

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
have p:"\<And>k. k \<le> length xs div 2 \<Longrightarrow> xs ! k \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k \<le> length xs div 2 \<Longrightarrow> xs ! k \<notin> I
[PROOF STEP]
using b v_2 sorted_int[OF assms(2) assms(3) v_1, where j="length xs div 2"]
[PROOF STATE]
proof (prove)
using this:
xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v
xs ! v \<in> I
\<lbrakk>?i \<le> length xs div 2; length xs div 2 \<le> v; xs ! ?i \<in> I; xs ! v \<in> I\<rbrakk> \<Longrightarrow> xs ! (length xs div 2) \<in> I

goal (1 subgoal):
 1. \<And>k. k \<le> length xs div 2 \<Longrightarrow> xs ! k \<notin> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> length xs div 2; xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v; xs ! v \<in> I; \<And>i. \<lbrakk>i \<le> length xs div 2; xs ! i \<in> I\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> xs ! k \<notin> I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?k \<le> length xs div 2 \<Longrightarrow> xs ! ?k \<notin> I

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
have "card J \<le> card {Suc (length xs div 2)..<length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card J \<le> card {Suc (length xs div 2)..<length xs}
[PROOF STEP]
apply (rule card_mono, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<subseteq> {Suc (length xs div 2)..<length xs}
[PROOF STEP]
apply (rule subsetI, simp add:J_def not_less_eq_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length xs \<and> xs ! x \<in> I \<Longrightarrow> \<not> x \<le> length xs div 2
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
?k \<le> length xs div 2 \<Longrightarrow> xs ! ?k \<notin> I

goal (1 subgoal):
 1. \<And>x. x < length xs \<and> xs ! x \<in> I \<Longrightarrow> \<not> x \<le> length xs div 2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card J \<le> card {Suc (length xs div 2)..<length xs}

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
hence "card J \<le> length xs - (Suc (length xs div 2))"
[PROOF STATE]
proof (prove)
using this:
card J \<le> card {Suc (length xs div 2)..<length xs}

goal (1 subgoal):
 1. card J \<le> length xs - Suc (length xs div 2)
[PROOF STEP]
using card_atLeastLessThan
[PROOF STATE]
proof (prove)
using this:
card J \<le> card {Suc (length xs div 2)..<length xs}
card {?l..<?u} = ?u - ?l

goal (1 subgoal):
 1. card J \<le> length xs - Suc (length xs div 2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card J \<le> length xs - Suc (length xs div 2)

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
hence "length xs \<le> 2*( length xs - (Suc (length xs div 2)))"
[PROOF STATE]
proof (prove)
using this:
card J \<le> length xs - Suc (length xs div 2)

goal (1 subgoal):
 1. length xs \<le> 2 * (length xs - Suc (length xs div 2))
[PROOF STEP]
using card_J_min
[PROOF STATE]
proof (prove)
using this:
card J \<le> length xs - Suc (length xs div 2)
length xs < 2 * card J

goal (1 subgoal):
 1. length xs \<le> 2 * (length xs - Suc (length xs div 2))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length xs \<le> 2 * (length xs - Suc (length xs div 2))

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
hence "False"
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 2 * (length xs - Suc (length xs div 2))

goal (1 subgoal):
 1. False
[PROOF STEP]
apply (simp add:nat_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> 2 * length xs - Suc (Suc (2 * (length xs div 2))) \<Longrightarrow> False
[PROOF STEP]
apply (subst (asm) le_diff_conv2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Suc (Suc (2 * (length xs div 2))) \<le> 2 * length xs
 2. length xs + Suc (Suc (2 * (length xs div 2))) \<le> 2 * length xs \<Longrightarrow> False
[PROOF STEP]
using b v_1
[PROOF STATE]
proof (prove)
using this:
xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v
v < length xs

goal (2 subgoals):
 1. Suc (Suc (2 * (length xs div 2))) \<le> 2 * length xs
 2. length xs + Suc (Suc (2 * (length xs div 2))) \<le> 2 * length xs \<Longrightarrow> False
[PROOF STEP]
apply linarith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs + Suc (Suc (2 * (length xs div 2))) \<le> 2 * length xs \<Longrightarrow> False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. xs ! (length xs div 2) \<notin> I \<and> length xs div 2 < v \<Longrightarrow> xs ! (length xs div 2) \<in> I
 2. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<in> I

goal (1 subgoal):
 1. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
case c
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2

goal (1 subgoal):
 1. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
have p:"\<And>k. k \<ge> length xs div 2 \<Longrightarrow> k < length xs \<Longrightarrow> xs ! k \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>length xs div 2 \<le> k; k < length xs\<rbrakk> \<Longrightarrow> xs ! k \<notin> I
[PROOF STEP]
using c v_1 v_2 sorted_int[OF assms(2) assms(3), where i ="v" and j="length xs div 2"]
[PROOF STATE]
proof (prove)
using this:
xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2
v < length xs
xs ! v \<in> I
\<lbrakk>?k < length xs; v \<le> length xs div 2; length xs div 2 \<le> ?k; xs ! v \<in> I; xs ! ?k \<in> I\<rbrakk> \<Longrightarrow> xs ! (length xs div 2) \<in> I

goal (1 subgoal):
 1. \<And>k. \<lbrakk>length xs div 2 \<le> k; k < length xs\<rbrakk> \<Longrightarrow> xs ! k \<notin> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>length xs div 2 \<le> k; k < length xs; xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2; xs ! v \<in> I; \<And>k. \<lbrakk>k < length xs; length xs div 2 \<le> k; xs ! k \<in> I\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> xs ! k \<notin> I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>length xs div 2 \<le> ?k; ?k < length xs\<rbrakk> \<Longrightarrow> xs ! ?k \<notin> I

goal (1 subgoal):
 1. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
have "card J \<le> card {0..<(length xs div 2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card J \<le> card {0..<length xs div 2}
[PROOF STEP]
apply (rule card_mono, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<subseteq> {0..<length xs div 2}
[PROOF STEP]
apply (rule subsetI, simp add:J_def not_less_eq_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length xs \<and> xs ! x \<in> I \<Longrightarrow> x < length xs div 2
[PROOF STEP]
using p linorder_le_less_linear
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs div 2 \<le> ?k; ?k < length xs\<rbrakk> \<Longrightarrow> xs ! ?k \<notin> I
?x \<le> ?y \<or> ?y < ?x

goal (1 subgoal):
 1. \<And>x. x < length xs \<and> xs ! x \<in> I \<Longrightarrow> x < length xs div 2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card J \<le> card {0..<length xs div 2}

goal (1 subgoal):
 1. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
hence "card J \<le> (length xs div 2)"
[PROOF STATE]
proof (prove)
using this:
card J \<le> card {0..<length xs div 2}

goal (1 subgoal):
 1. card J \<le> length xs div 2
[PROOF STEP]
using card_atLeastLessThan
[PROOF STATE]
proof (prove)
using this:
card J \<le> card {0..<length xs div 2}
card {?l..<?u} = ?u - ?l

goal (1 subgoal):
 1. card J \<le> length xs div 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card J \<le> length xs div 2

goal (1 subgoal):
 1. xs ! (length xs div 2) \<notin> I \<and> v < length xs div 2 \<Longrightarrow> xs ! (length xs div 2) \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card J \<le> length xs div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card J \<le> length xs div 2

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
using card_J_min
[PROOF STATE]
proof (prove)
using this:
card J \<le> length xs div 2
length xs < 2 * card J

goal (1 subgoal):
 1. xs ! (length xs div 2) \<in> I
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<in> I

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xs ! (length xs div 2) \<in> I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma median_est:
  assumes "interval I"
  assumes "2*card {k. k < n \<and> f k \<in> I} > n"
  shows "median n f \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median n f \<in> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. median n f \<in> I
[PROOF STEP]
have a:"{k. k < n \<and> f k \<in> I} = {i. i < n \<and> map f [0..<n] ! i \<in> I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {k. k < n \<and> f k \<in> I} = {i. i < n \<and> map f [0..<n] ! i \<in> I}
[PROOF STEP]
apply (rule order_antisym, rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < n \<and> map f [0..<n] ! i \<in> I} \<subseteq> {k. k < n \<and> f k \<in> I}
[PROOF STEP]
by (rule subsetI, simp, metis add_0 diff_zero nth_map_upt)
[PROOF STATE]
proof (state)
this:
{k. k < n \<and> f k \<in> I} = {i. i < n \<and> map f [0..<n] ! i \<in> I}

goal (1 subgoal):
 1. median n f \<in> I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. median n f \<in> I
[PROOF STEP]
apply (simp add:median_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sort (map f [0..<n]) ! (n div 2) \<in> I
[PROOF STEP]
apply (rule mid_in_interval[where I="I" and xs="sort (map f [0..<n])", simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < 2 * length (filter (\<lambda>x. x \<in> I) (sort (map f [0..<n])))
 2. interval I
[PROOF STEP]
using assms a
[PROOF STATE]
proof (prove)
using this:
interval I
n < 2 * card {k. k < n \<and> f k \<in> I}
{k. k < n \<and> f k \<in> I} = {i. i < n \<and> map f [0..<n] ! i \<in> I}

goal (2 subgoals):
 1. n < 2 * length (filter (\<lambda>x. x \<in> I) (sort (map f [0..<n])))
 2. interval I
[PROOF STEP]
apply (simp add:filter_sort comp_def length_filter_conv_card)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval I
[PROOF STEP]
by (simp add:assms)
[PROOF STATE]
proof (state)
this:
median n f \<in> I

goal:
No subgoals!
[PROOF STEP]
qed