[STATEMENT]
lemma before_in_index1:
  fixes l
  assumes "set l = {x,y}" and "length l = 2" and "x\<noteq>y"
  shows "(if (x < y in l) then 0 else 1) = index l x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x < y in l then 0 else 1) = index l x
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if index l x < index l y \<and> y \<in> set l then 0 else 1) = index l x
[PROOF STEP]
proof (auto, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 3. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
(* bad style! *)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 3. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
index l x < index l y
y \<in> set l

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 3. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have "index l y < length l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

goal (1 subgoal):
 1. index l y < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y < length l

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 3. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
with assms(2) 1(1)
[PROOF STATE]
proof (chain)
picking this:
length l = 2
index l x < index l y
index l y < length l
[PROOF STEP]
show "index l x = 0"
[PROOF STATE]
proof (prove)
using this:
length l = 2
index l x < index l y
index l y < length l

goal (1 subgoal):
 1. index l x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l x = 0

goal (2 subgoals):
 1. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 2. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 2. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<not> index l x < index l y

goal (2 subgoals):
 1. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 2. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have a: "index l x < length l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

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

goal (2 subgoals):
 1. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 2. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
x \<noteq> y
[PROOF STEP]
have "index l y \<noteq> index l x"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
x \<noteq> y

goal (1 subgoal):
 1. index l y \<noteq> index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y \<noteq> index l x

goal (2 subgoals):
 1. \<not> index l x < index l y \<Longrightarrow> Suc 0 = index l x
 2. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
with assms(2) 2(1) a
[PROOF STATE]
proof (chain)
picking this:
length l = 2
\<not> index l x < index l y
index l x < length l
index l y \<noteq> index l x
[PROOF STEP]
show "Suc 0 = index l x"
[PROOF STATE]
proof (prove)
using this:
length l = 2
\<not> index l x < index l y
index l x < length l
index l y \<noteq> index l x

goal (1 subgoal):
 1. Suc 0 = index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc 0 = index l x

goal (1 subgoal):
 1. y \<notin> set l \<Longrightarrow> Suc 0 = index l x
[PROOF STEP]
qed (simp add: assms)


[STATEMENT]
lemma before_in_index2:
  fixes l
  assumes "set l = {x,y}" and "length l = 2" and "x\<noteq>y"
  shows "(if (x < y in l) then 1 else 0) = index l y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x < y in l then 1 else 0) = index l y
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if index l x < index l y \<and> y \<in> set l then 1 else 0) = index l y
[PROOF STEP]
proof (auto, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. \<not> index l x < index l y \<Longrightarrow> index l y = 0
 3. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
(* bad style! *)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. \<not> index l x < index l y \<Longrightarrow> index l y = 0
 3. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<not> index l x < index l y

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. \<not> index l x < index l y \<Longrightarrow> index l y = 0
 3. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
x \<noteq> y
[PROOF STEP]
have a: "index l y \<noteq> index l x"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
x \<noteq> y

goal (1 subgoal):
 1. index l y \<noteq> index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y \<noteq> index l x

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. \<not> index l x < index l y \<Longrightarrow> index l y = 0
 3. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have "index l x < length l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

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

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. \<not> index l x < index l y \<Longrightarrow> index l y = 0
 3. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
with assms(2) a 2(1)
[PROOF STATE]
proof (chain)
picking this:
length l = 2
index l y \<noteq> index l x
\<not> index l x < index l y
index l x < length l
[PROOF STEP]
show "index l y = 0"
[PROOF STATE]
proof (prove)
using this:
length l = 2
index l y \<noteq> index l x
\<not> index l x < index l y
index l x < length l

goal (1 subgoal):
 1. index l y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l y = 0

goal (2 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
index l x < index l y
y \<in> set l

goal (2 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have a: "index l y < length l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

goal (1 subgoal):
 1. index l y < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y < length l

goal (2 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
x \<noteq> y
[PROOF STEP]
have "index l y \<noteq> index l x"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
x \<noteq> y

goal (1 subgoal):
 1. index l y \<noteq> index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y \<noteq> index l x

goal (2 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> Suc 0 = index l y
 2. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
with assms(2) 1(1) a
[PROOF STATE]
proof (chain)
picking this:
length l = 2
index l x < index l y
index l y < length l
index l y \<noteq> index l x
[PROOF STEP]
show "Suc 0 = index l y"
[PROOF STATE]
proof (prove)
using this:
length l = 2
index l x < index l y
index l y < length l
index l y \<noteq> index l x

goal (1 subgoal):
 1. Suc 0 = index l y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc 0 = index l y

goal (1 subgoal):
 1. y \<notin> set l \<Longrightarrow> l = []
[PROOF STEP]
qed (simp add: assms)


[STATEMENT]
lemma before_in_index:
  fixes l
  assumes "set l = {x,y}" and "length l = 2" and "x\<noteq>y"
  shows "(x < y in l) = (index l x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in l = (index l x = 0)
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index l x < index l y \<and> y \<in> set l) = (index l x = 0)
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. index l x = 0 \<Longrightarrow> index l x < index l y
 3. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
index l x < index l y
y \<in> set l

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. index l x = 0 \<Longrightarrow> index l x < index l y
 3. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have "index l y < length l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

goal (1 subgoal):
 1. index l y < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y < length l

goal (3 subgoals):
 1. \<lbrakk>index l x < index l y; y \<in> set l\<rbrakk> \<Longrightarrow> index l x = 0
 2. index l x = 0 \<Longrightarrow> index l x < index l y
 3. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
with assms(2) 1(1)
[PROOF STATE]
proof (chain)
picking this:
length l = 2
index l x < index l y
index l y < length l
[PROOF STEP]
show "index l x = 0"
[PROOF STATE]
proof (prove)
using this:
length l = 2
index l x < index l y
index l y < length l

goal (1 subgoal):
 1. index l x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l x = 0

goal (2 subgoals):
 1. index l x = 0 \<Longrightarrow> index l x < index l y
 2. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. index l x = 0 \<Longrightarrow> index l x < index l y
 2. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
index l x = 0

goal (2 subgoals):
 1. index l x = 0 \<Longrightarrow> index l x < index l y
 2. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
x \<noteq> y
[PROOF STEP]
have "index l y \<noteq> index l x"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
x \<noteq> y

goal (1 subgoal):
 1. index l y \<noteq> index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y \<noteq> index l x

goal (2 subgoals):
 1. index l x = 0 \<Longrightarrow> index l x < index l y
 2. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
with 2(1)
[PROOF STATE]
proof (chain)
picking this:
index l x = 0
index l y \<noteq> index l x
[PROOF STEP]
show "index l x < index l y"
[PROOF STATE]
proof (prove)
using this:
index l x = 0
index l y \<noteq> index l x

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

goal (1 subgoal):
 1. index l x = 0 \<Longrightarrow> y \<in> set l
[PROOF STEP]
qed (simp add: assms)


[STATEMENT]
lemma T_on_n_no_paid:
      assumes
      nopaid: "\<And>s n. map_pmf (\<lambda>x. snd (fst x)) (snd A s n) = return_pmf []"
      shows "T_on_rand_n A init qs i = E (config'' A qs init i \<bind> (\<lambda>p. return_pmf (real(index (fst p) (qs ! i)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))
[PROOF STEP]
have "(\<lambda>s. snd A s (qs ! i) \<bind>
            (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! i) a))))
       =
        (\<lambda>s. (snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))))
              \<bind> (\<lambda>p. return_pmf
               (real (index (swaps p (fst s)) (qs ! i)) +
                real (length p))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! i) a)))) = (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))) \<bind> (\<lambda>p. return_pmf (real (index (swaps p (fst s)) (qs ! i)) + real (length p))))
[PROOF STEP]
by(simp add: t\<^sub>p_def split_def bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (state)
this:
(\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! i) a)))) = (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))) \<bind> (\<lambda>p. return_pmf (real (index (swaps p (fst s)) (qs ! i)) + real (length p))))

goal (1 subgoal):
 1. Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! i) a)))) = (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))) \<bind> (\<lambda>p. return_pmf (real (index (swaps p (fst s)) (qs ! i)) + real (length p))))

goal (1 subgoal):
 1. Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))
[PROOF STEP]
have "\<dots> = (\<lambda>p. return_pmf (real (index (fst p) (qs ! i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))) \<bind> (\<lambda>p. return_pmf (real (index (swaps p (fst s)) (qs ! i)) + real (length p)))) = (\<lambda>p. return_pmf (real (index (fst p) (qs ! i))))
[PROOF STEP]
using nopaid[unfolded map_pmf_def]
[PROOF STATE]
proof (prove)
using this:
snd A ?s ?n \<bind> (\<lambda>x. return_pmf (snd (fst x))) = return_pmf []

goal (1 subgoal):
 1. (\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))) \<bind> (\<lambda>p. return_pmf (real (index (swaps p (fst s)) (qs ! i)) + real (length p)))) = (\<lambda>p. return_pmf (real (index (fst p) (qs ! i))))
[PROOF STEP]
by(simp add: split_def bind_return_pmf)
[PROOF STATE]
proof (state)
this:
(\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>x. return_pmf (snd (fst x))) \<bind> (\<lambda>p. return_pmf (real (index (swaps p (fst s)) (qs ! i)) + real (length p)))) = (\<lambda>p. return_pmf (real (index (fst p) (qs ! i))))

goal (1 subgoal):
 1. Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! i) a)))) = (\<lambda>p. return_pmf (real (index (fst p) (qs ! i))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>s. snd A s (qs ! i) \<bind> (\<lambda>(a, is'). return_pmf (real (t\<^sub>p (fst s) (qs ! i) a)))) = (\<lambda>p. return_pmf (real (index (fst p) (qs ! i))))

goal (1 subgoal):
 1. Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Partial_Cost_Model.T_on_rand'_n A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) qs i = E (Partial_Cost_Model.config'_rand A (fst A init \<bind> (\<lambda>is. return_pmf (init, is))) (take i qs) \<bind> (\<lambda>p. return_pmf (real (index (fst p) (qs ! i)))))

goal:
No subgoals!
[PROOF STEP]
qed