[STATEMENT]
lemma index_surj:
  assumes "k \<ge> index l"
  shows "\<exists>i j. k = index i + j \<and> index i + j < index (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. k = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i j. k = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
index l \<le> k
[PROOF STEP]
have "k = index l + (k - index l)"
[PROOF STATE]
proof (prove)
using this:
index l \<le> k

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

goal (1 subgoal):
 1. \<exists>i j. k = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = index l + (k - index l)
[PROOF STEP]
obtain u where k: "k = index l + u"
[PROOF STATE]
proof (prove)
using this:
k = index l + (k - index l)

goal (1 subgoal):
 1. (\<And>u. k = index l + u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = index l + u

goal (1 subgoal):
 1. \<exists>i j. k = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. k = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
unfolding k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
proof (induct u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i j. index l + 0 = index i + j \<and> index i + j < index (Suc i)
 2. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>i j. index l + 0 = index i + j \<and> index i + j < index (Suc i)
 2. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. index l + 0 = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
by (intro exI conjI, rule refl, insert index_ordered[of l], simp)
[PROOF STATE]
proof (state)
this:
\<exists>i j. index l + 0 = index i + j \<and> index i + j < index (Suc i)

goal (1 subgoal):
 1. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
case (Suc u)
[PROOF STATE]
proof (state)
this:
\<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i)

goal (1 subgoal):
 1. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
obtain i j
      where lu: "index l + u = index i + j" and lt: "index i + j < index (Suc i)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>index l + u = index i + j; index i + j < index (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l + u = index i + j
index i + j < index (Suc i)

goal (1 subgoal):
 1. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
hence "index l + u < index (Suc i)"
[PROOF STATE]
proof (prove)
using this:
index l + u = index i + j
index i + j < index (Suc i)

goal (1 subgoal):
 1. index l + u < index (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l + u < index (Suc i)

goal (1 subgoal):
 1. \<And>u. \<exists>i j. index l + u = index i + j \<and> index i + j < index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
proof (cases "index l + (Suc u) = index (Suc i)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. index l + Suc u = index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
 2. index l + Suc u \<noteq> index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
index l + Suc u \<noteq> index (Suc i)

goal (2 subgoals):
 1. index l + Suc u = index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
 2. index l + Suc u \<noteq> index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
by (rule exI[of _ i], rule exI[of _ "Suc j"], insert lu lt False, auto)
[PROOF STATE]
proof (state)
this:
\<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)

goal (1 subgoal):
 1. index l + Suc u = index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index l + Suc u = index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
index l + Suc u = index (Suc i)

goal (1 subgoal):
 1. index l + Suc u = index (Suc i) \<Longrightarrow> \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)
[PROOF STEP]
by (rule exI[of _ "Suc i"], rule exI[of _ 0], insert True index_ordered[of "Suc i"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i j. index l + Suc u = index i + j \<and> index i + j < index (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i j. k = index i + j \<and> index i + j < index (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_ordered_less:
  assumes "i < j" shows "index i < index j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index i < index j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index i < index j
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < j
[PROOF STEP]
have "Suc i \<le> j"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. Suc i \<le> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i \<le> j

goal (1 subgoal):
 1. index i < index j
[PROOF STEP]
from index_ordered_le[OF this]
[PROOF STATE]
proof (chain)
picking this:
index (Suc i) \<le> index j
[PROOF STEP]
have "index (Suc i) \<le> index j"
[PROOF STATE]
proof (prove)
using this:
index (Suc i) \<le> index j

goal (1 subgoal):
 1. index (Suc i) \<le> index j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
index (Suc i) \<le> index j

goal (1 subgoal):
 1. index i < index j
[PROOF STEP]
with index_ordered[of i]
[PROOF STATE]
proof (chain)
picking this:
index i < index (Suc i)
index (Suc i) \<le> index j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
index i < index (Suc i)
index (Suc i) \<le> index j

goal (1 subgoal):
 1. index i < index j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index i < index j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_not_p_start: assumes i: "i < index 0" shows "\<not> p i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> p i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p i
[PROOF STEP]
from i[simplified index.simps]
[PROOF STATE]
proof (chain)
picking this:
i < Least p
[PROOF STEP]
have "i < Least p"
[PROOF STATE]
proof (prove)
using this:
i < Least p

goal (1 subgoal):
 1. i < Least p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i < Least p

goal (1 subgoal):
 1. \<not> p i
[PROOF STEP]
from not_less_Least[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<not> p i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> p i

goal (1 subgoal):
 1. \<not> p i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> p i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_simple_add:
  assumes ck: "inf_concat_simple f k = (i, j)"
    and jl: "j + l < f i"
  shows "inf_concat_simple f (k + l) = (i,j + l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_concat_simple f (k + l) = (i, j + l)
[PROOF STEP]
using jl
[PROOF STATE]
proof (prove)
using this:
j + l < f i

goal (1 subgoal):
 1. inf_concat_simple f (k + l) = (i, j + l)
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j + 0 < f i \<Longrightarrow> inf_concat_simple f (k + 0) = (i, j + 0)
 2. \<And>l. \<lbrakk>j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l); j + Suc l < f i\<rbrakk> \<Longrightarrow> inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j + 0 < f i

goal (2 subgoals):
 1. j + 0 < f i \<Longrightarrow> inf_concat_simple f (k + 0) = (i, j + 0)
 2. \<And>l. \<lbrakk>j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l); j + Suc l < f i\<rbrakk> \<Longrightarrow> inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
j + 0 < f i

goal (1 subgoal):
 1. inf_concat_simple f (k + 0) = (i, j + 0)
[PROOF STEP]
using ck
[PROOF STATE]
proof (prove)
using this:
j + 0 < f i
inf_concat_simple f k = (i, j)

goal (1 subgoal):
 1. inf_concat_simple f (k + 0) = (i, j + 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inf_concat_simple f (k + 0) = (i, j + 0)

goal (1 subgoal):
 1. \<And>l. \<lbrakk>j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l); j + Suc l < f i\<rbrakk> \<Longrightarrow> inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l); j + Suc l < f i\<rbrakk> \<Longrightarrow> inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l)
j + Suc l < f i

goal (1 subgoal):
 1. \<And>l. \<lbrakk>j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l); j + Suc l < f i\<rbrakk> \<Longrightarrow> inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
hence c: "inf_concat_simple f (k + l) = (i, j+ l)"
[PROOF STATE]
proof (prove)
using this:
j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l)
j + Suc l < f i

goal (1 subgoal):
 1. inf_concat_simple f (k + l) = (i, j + l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat_simple f (k + l) = (i, j + l)

goal (1 subgoal):
 1. \<And>l. \<lbrakk>j + l < f i \<Longrightarrow> inf_concat_simple f (k + l) = (i, j + l); j + Suc l < f i\<rbrakk> \<Longrightarrow> inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_concat_simple f (k + Suc l) = (i, j + Suc l)
[PROOF STEP]
by (simp add: c, insert Suc(2), auto)
[PROOF STATE]
proof (state)
this:
inf_concat_simple f (k + Suc l) = (i, j + Suc l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_simple_surj_zero: "\<exists> k. inf_concat_simple f k = (i,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (i, 0)
[PROOF STEP]
proof (induct i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>k. inf_concat_simple f k = (0, 0)
 2. \<And>i. \<exists>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>k. inf_concat_simple f k = (0, 0)
 2. \<And>i. \<exists>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (0, 0)
[PROOF STEP]
by (rule exI[of _ 0], simp)
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat_simple f k = (0, 0)

goal (1 subgoal):
 1. \<And>i. \<exists>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<exists>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat_simple f k = (i, 0)

goal (1 subgoal):
 1. \<And>i. \<exists>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. inf_concat_simple f k = (i, 0)
[PROOF STEP]
obtain k where ck: "inf_concat_simple f k = (i,0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. inf_concat_simple f k = (i, 0)

goal (1 subgoal):
 1. (\<And>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat_simple f k = (i, 0)

goal (1 subgoal):
 1. \<And>i. \<exists>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
proof (cases "f i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f i = 0 \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
 2. \<And>nat. f i = Suc nat \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
f i = 0

goal (2 subgoals):
 1. f i = 0 \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
 2. \<And>nat. f i = Suc nat \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
by (rule exI[of _ "Suc k"], simp add: ck 0)
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat_simple f k = (Suc i, 0)

goal (1 subgoal):
 1. \<And>nat. f i = Suc nat \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. f i = Suc nat \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
f i = Suc n

goal (1 subgoal):
 1. \<And>nat. f i = Suc nat \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
hence "0 + n < f i"
[PROOF STATE]
proof (prove)
using this:
f i = Suc n

goal (1 subgoal):
 1. 0 + n < f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 + n < f i

goal (1 subgoal):
 1. \<And>nat. f i = Suc nat \<Longrightarrow> \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
from inf_concat_simple_add[OF ck, OF this] Suc
[PROOF STATE]
proof (chain)
picking this:
inf_concat_simple f (k + n) = (i, 0 + n)
f i = Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inf_concat_simple f (k + n) = (i, 0 + n)
f i = Suc n

goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (Suc i, 0)
[PROOF STEP]
by (intro exI[of _ "k + Suc n"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat_simple f k = (Suc i, 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat_simple f k = (Suc i, 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_simple_surj:
  assumes "j < f i"
  shows "\<exists> k. inf_concat_simple f k = (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (i, j)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
j < f i
[PROOF STEP]
have j: "0 + j < f i"
[PROOF STATE]
proof (prove)
using this:
j < f i

goal (1 subgoal):
 1. 0 + j < f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 + j < f i

goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (i, j)
[PROOF STEP]
from inf_concat_simple_surj_zero
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. inf_concat_simple ?f k = (?i, 0)
[PROOF STEP]
obtain k where "inf_concat_simple f k = (i,0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. inf_concat_simple ?f k = (?i, 0)

goal (1 subgoal):
 1. (\<And>k. inf_concat_simple f k = (i, 0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat_simple f k = (i, 0)

goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (i, j)
[PROOF STEP]
from inf_concat_simple_add[OF this, OF j]
[PROOF STATE]
proof (chain)
picking this:
inf_concat_simple f (k + j) = (i, 0 + j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inf_concat_simple f (k + j) = (i, 0 + j)

goal (1 subgoal):
 1. \<exists>k. inf_concat_simple f k = (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat_simple f k = (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_simple_mono:
  assumes "k \<le> k'" shows "fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
k \<le> k'
[PROOF STEP]
have "k' = k + (k' - k)"
[PROOF STATE]
proof (prove)
using this:
k \<le> k'

goal (1 subgoal):
 1. k' = k + (k' - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' = k + (k' - k)

goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' = k + (k' - k)
[PROOF STEP]
obtain l where k': "k' = k + l"
[PROOF STATE]
proof (prove)
using this:
k' = k + (k' - k)

goal (1 subgoal):
 1. (\<And>l. k' = k + l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' = k + l

goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')
[PROOF STEP]
unfolding k'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l))
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
 2. \<And>l. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l)) \<Longrightarrow> fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l))

goal (2 subgoals):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
 2. \<And>l. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l)) \<Longrightarrow> fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
obtain i j where ckl: "inf_concat_simple f (k+l) = (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i j. inf_concat_simple f (k + l) = (i, j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "inf_concat_simple f (k+l)", auto)
[PROOF STATE]
proof (state)
this:
inf_concat_simple f (k + l) = (i, j)

goal (2 subgoals):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
 2. \<And>l. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l)) \<Longrightarrow> fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l))
inf_concat_simple f (k + l) = (i, j)
[PROOF STEP]
have "fst (inf_concat_simple f k) \<le> i"
[PROOF STATE]
proof (prove)
using this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l))
inf_concat_simple f (k + l) = (i, j)

goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (inf_concat_simple f k) \<le> i

goal (2 subgoals):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
 2. \<And>l. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l)) \<Longrightarrow> fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst (inf_concat_simple f k) \<le> i

goal (2 subgoals):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
 2. \<And>l. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l)) \<Longrightarrow> fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
have "... \<le> fst (inf_concat_simple f (k + Suc l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
by (simp add: ckl)
[PROOF STATE]
proof (state)
this:
i \<le> fst (inf_concat_simple f (k + Suc l))

goal (2 subgoals):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
 2. \<And>l. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + l)) \<Longrightarrow> fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))

goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + Suc l))

goal (1 subgoal):
 1. fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f (k + 0))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_bounds:
  assumes inf: "INFM i. n i > 0"
    and res: "inf_concat n k = (i,j)"
  shows "j < n i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < n i
[PROOF STEP]
proof (cases k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> j < n i
 2. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> j < n i
 2. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
inf_concat n k = (i, j)
k = 0
[PROOF STEP]
have i: "i = (LEAST i. n i > 0)" and j: "j = 0"
[PROOF STATE]
proof (prove)
using this:
inf_concat n k = (i, j)
k = 0

goal (1 subgoal):
 1. i = (LEAST i. 0 < n i) &&& j = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = (LEAST i. 0 < n i)
j = 0

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> j < n i
 2. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
from inf[unfolded INFM_nat_le]
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. \<exists>na\<ge>m. 0 < n na
[PROOF STEP]
obtain i' where i': "0 < n i'"
[PROOF STATE]
proof (prove)
using this:
\<forall>m. \<exists>na\<ge>m. 0 < n na

goal (1 subgoal):
 1. (\<And>i'. 0 < n i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n i'

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> j < n i
 2. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
have "0 < n (LEAST i. n i > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n (LEAST i. 0 < n i)
[PROOF STEP]
by (rule LeastI, rule i')
[PROOF STATE]
proof (state)
this:
0 < n (LEAST i. 0 < n i)

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> j < n i
 2. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
with i j
[PROOF STATE]
proof (chain)
picking this:
i = (LEAST i. 0 < n i)
j = 0
0 < n (LEAST i. 0 < n i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = (LEAST i. 0 < n i)
j = 0
0 < n (LEAST i. 0 < n i)

goal (1 subgoal):
 1. j < n i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < n i

goal (1 subgoal):
 1. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
case (Suc k')
[PROOF STATE]
proof (state)
this:
k = Suc k'

goal (1 subgoal):
 1. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
obtain i' j' where res': "inf_concat n k' = (i',j')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i' j'. inf_concat n k' = (i', j') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inf_concat n k' = (i', j')

goal (1 subgoal):
 1. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
note res = res[unfolded Suc inf_concat.simps res' Let_def split]
[PROOF STATE]
proof (state)
this:
(if Suc j' < n i' then (i', Suc j') else (LEAST i'a. i' < i'a \<and> 0 < n i'a, 0)) = (i, j)

goal (1 subgoal):
 1. \<And>nat. k = Suc nat \<Longrightarrow> j < n i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < n i
[PROOF STEP]
proof (cases "Suc j' < n i'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc j' < n i' \<Longrightarrow> j < n i
 2. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc j' < n i'

goal (2 subgoals):
 1. Suc j' < n i' \<Longrightarrow> j < n i
 2. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
(if Suc j' < n i' then (i', Suc j') else (LEAST i'a. i' < i'a \<and> 0 < n i'a, 0)) = (i, j)
Suc j' < n i'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if Suc j' < n i' then (i', Suc j') else (LEAST i'a. i' < i'a \<and> 0 < n i'a, 0)) = (i, j)
Suc j' < n i'

goal (1 subgoal):
 1. j < n i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < n i

goal (1 subgoal):
 1. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Suc j' < n i'

goal (1 subgoal):
 1. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
(if Suc j' < n i' then (i', Suc j') else (LEAST i'a. i' < i'a \<and> 0 < n i'a, 0)) = (i, j)
\<not> Suc j' < n i'
[PROOF STEP]
have i: "i = (LEAST f. i' < f \<and> 0 < n f)" and j: "j = 0"
[PROOF STATE]
proof (prove)
using this:
(if Suc j' < n i' then (i', Suc j') else (LEAST i'a. i' < i'a \<and> 0 < n i'a, 0)) = (i, j)
\<not> Suc j' < n i'

goal (1 subgoal):
 1. i = (LEAST f. i' < f \<and> 0 < n f) &&& j = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = (LEAST f. i' < f \<and> 0 < n f)
j = 0

goal (1 subgoal):
 1. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
from inf[unfolded INFM_nat]
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. \<exists>na>m. 0 < n na
[PROOF STEP]
obtain f where f: "i' < f \<and> 0 < n f"
[PROOF STATE]
proof (prove)
using this:
\<forall>m. \<exists>na>m. 0 < n na

goal (1 subgoal):
 1. (\<And>f. i' < f \<and> 0 < n f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' < f \<and> 0 < n f

goal (1 subgoal):
 1. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
have "0 < n (LEAST f. i' < f \<and> 0 < n f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n (LEAST f. i' < f \<and> 0 < n f)
[PROOF STEP]
using LeastI[of "\<lambda> f. i' < f \<and> 0 < n f", OF f]
[PROOF STATE]
proof (prove)
using this:
i' < (LEAST x. i' < x \<and> 0 < n x) \<and> 0 < n (LEAST x. i' < x \<and> 0 < n x)

goal (1 subgoal):
 1. 0 < n (LEAST f. i' < f \<and> 0 < n f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n (LEAST f. i' < f \<and> 0 < n f)

goal (1 subgoal):
 1. \<not> Suc j' < n i' \<Longrightarrow> j < n i
[PROOF STEP]
with i j
[PROOF STATE]
proof (chain)
picking this:
i = (LEAST f. i' < f \<and> 0 < n f)
j = 0
0 < n (LEAST f. i' < f \<and> 0 < n f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = (LEAST f. i' < f \<and> 0 < n f)
j = 0
0 < n (LEAST f. i' < f \<and> 0 < n f)

goal (1 subgoal):
 1. j < n i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < n i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
j < n i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_add:
  assumes res: "inf_concat n k = (i,j)"
    and j: "j + m < n i"
  shows "inf_concat n (k + m) = (i,j+m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_concat n (k + m) = (i, j + m)
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j + m < n i

goal (1 subgoal):
 1. inf_concat n (k + m) = (i, j + m)
[PROOF STEP]
proof (induct m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j + 0 < n i \<Longrightarrow> inf_concat n (k + 0) = (i, j + 0)
 2. \<And>m. \<lbrakk>j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m); j + Suc m < n i\<rbrakk> \<Longrightarrow> inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j + 0 < n i

goal (2 subgoals):
 1. j + 0 < n i \<Longrightarrow> inf_concat n (k + 0) = (i, j + 0)
 2. \<And>m. \<lbrakk>j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m); j + Suc m < n i\<rbrakk> \<Longrightarrow> inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_concat n (k + 0) = (i, j + 0)
[PROOF STEP]
using res
[PROOF STATE]
proof (prove)
using this:
inf_concat n k = (i, j)

goal (1 subgoal):
 1. inf_concat n (k + 0) = (i, j + 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat n (k + 0) = (i, j + 0)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m); j + Suc m < n i\<rbrakk> \<Longrightarrow> inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m); j + Suc m < n i\<rbrakk> \<Longrightarrow> inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m)
j + Suc m < n i

goal (1 subgoal):
 1. \<And>m. \<lbrakk>j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m); j + Suc m < n i\<rbrakk> \<Longrightarrow> inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
hence "inf_concat n (k + m) = (i, j+m)"
[PROOF STATE]
proof (prove)
using this:
j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m)
j + Suc m < n i

goal (1 subgoal):
 1. inf_concat n (k + m) = (i, j + m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat n (k + m) = (i, j + m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>j + m < n i \<Longrightarrow> inf_concat n (k + m) = (i, j + m); j + Suc m < n i\<rbrakk> \<Longrightarrow> inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
with Suc(2)
[PROOF STATE]
proof (chain)
picking this:
j + Suc m < n i
inf_concat n (k + m) = (i, j + m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
j + Suc m < n i
inf_concat n (k + m) = (i, j + m)

goal (1 subgoal):
 1. inf_concat n (k + Suc m) = (i, j + Suc m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat n (k + Suc m) = (i, j + Suc m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_step:
  assumes res: "inf_concat n k = (i,j)"
    and j: "Suc (j + m) = n i"
  shows "inf_concat n (k + Suc m) = (LEAST i'. i' > i \<and> 0 < n i', 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_concat n (k + Suc m) = (LEAST i'. i < i' \<and> 0 < n i', 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inf_concat n (k + Suc m) = (LEAST i'. i < i' \<and> 0 < n i', 0)
[PROOF STEP]
from j
[PROOF STATE]
proof (chain)
picking this:
Suc (j + m) = n i
[PROOF STEP]
have "j + m < n i"
[PROOF STATE]
proof (prove)
using this:
Suc (j + m) = n i

goal (1 subgoal):
 1. j + m < n i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j + m < n i

goal (1 subgoal):
 1. inf_concat n (k + Suc m) = (LEAST i'. i < i' \<and> 0 < n i', 0)
[PROOF STEP]
note res = inf_concat_add[OF res, OF this]
[PROOF STATE]
proof (state)
this:
inf_concat n (k + m) = (i, j + m)

goal (1 subgoal):
 1. inf_concat n (k + Suc m) = (LEAST i'. i < i' \<and> 0 < n i', 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_concat n (k + Suc m) = (LEAST i'. i < i' \<and> 0 < n i', 0)
[PROOF STEP]
by (simp add: res j)
[PROOF STATE]
proof (state)
this:
inf_concat n (k + Suc m) = (LEAST i'. i < i' \<and> 0 < n i', 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_surj_zero:
  assumes "0 < n i"
  shows "\<exists>k. inf_concat n k = (i, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
have "\<forall> j. j < l \<and> 0 < n j \<longrightarrow> (\<exists> k. inf_concat n k = (j,0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>j. j < 0 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
 2. \<And>l. \<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0)) \<Longrightarrow> \<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<forall>j. j < 0 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
 2. \<And>l. \<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0)) \<Longrightarrow> \<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. j < 0 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j. j < 0 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))

goal (1 subgoal):
 1. \<And>l. \<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0)) \<Longrightarrow> \<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. \<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0)) \<Longrightarrow> \<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))

goal (1 subgoal):
 1. \<And>l. \<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0)) \<Longrightarrow> \<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
proof (intro allI impI, elim conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < Suc l; 0 < n j\<rbrakk> \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < Suc l; 0 < n j\<rbrakk> \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
assume j: "j < Suc l" and nj: "0 < n j"
[PROOF STATE]
proof (state)
this:
j < Suc l
0 < n j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < Suc l; 0 < n j\<rbrakk> \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
show "\<exists> k. inf_concat n k = (j, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
proof (cases "j < l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
 2. \<not> j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j < l

goal (2 subgoals):
 1. j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
 2. \<not> j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
from Suc[THEN spec[of _ j]] True nj
[PROOF STATE]
proof (chain)
picking this:
j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
j < l
0 < n j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
j < l
0 < n j

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (j, 0)

goal (1 subgoal):
 1. \<not> j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> j < l

goal (1 subgoal):
 1. \<not> j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
with j
[PROOF STATE]
proof (chain)
picking this:
j < Suc l
\<not> j < l
[PROOF STEP]
have j: "j = l"
[PROOF STATE]
proof (prove)
using this:
j < Suc l
\<not> j < l

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

goal (1 subgoal):
 1. \<not> j < l \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
proof (cases "\<exists> j'. j' < l \<and> 0 < n j'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
 2. \<not> (\<exists>j'<l. 0 < n j') \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>j'<l. 0 < n j')

goal (2 subgoals):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
 2. \<not> (\<exists>j'<l. 0 < n j') \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
have l: "(LEAST i. 0 < n i) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST i. 0 < n i) = l
[PROOF STEP]
proof (rule Least_equality, rule nj[unfolded j])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. 0 < n y \<Longrightarrow> l \<le> y
[PROOF STEP]
fix l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. 0 < n y \<Longrightarrow> l \<le> y
[PROOF STEP]
assume "0 < n l'"
[PROOF STATE]
proof (state)
this:
0 < n l'

goal (1 subgoal):
 1. \<And>y. 0 < n y \<Longrightarrow> l \<le> y
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>j'<l. 0 < n j')
0 < n l'
[PROOF STEP]
have "\<not> l' < l"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j'<l. 0 < n j')
0 < n l'

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

goal (1 subgoal):
 1. \<And>y. 0 < n y \<Longrightarrow> l \<le> y
[PROOF STEP]
thus "l \<le> l'"
[PROOF STATE]
proof (prove)
using this:
\<not> l' < l

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST i. 0 < n i) = l

goal (2 subgoals):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
 2. \<not> (\<exists>j'<l. 0 < n j') \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
by (rule exI[of _ 0], simp add: l j)
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (j, 0)

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>j'<l. 0 < n j'

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j'<l. 0 < n j'
[PROOF STEP]
obtain lll where lll: "lll < l" and nlll: "0 < n lll"
[PROOF STATE]
proof (prove)
using this:
\<exists>j'<l. 0 < n j'

goal (1 subgoal):
 1. (\<And>lll. \<lbrakk>lll < l; 0 < n lll\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lll < l
0 < n lll

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lll < l
0 < n lll
[PROOF STEP]
obtain ll where l: "l = Suc ll"
[PROOF STATE]
proof (prove)
using this:
lll < l
0 < n lll

goal (1 subgoal):
 1. (\<And>ll. l = Suc ll \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases l, auto)
[PROOF STATE]
proof (state)
this:
l = Suc ll

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
from lll l
[PROOF STATE]
proof (chain)
picking this:
lll < l
l = Suc ll
[PROOF STEP]
have lll: "lll = ll - (ll - lll)"
[PROOF STATE]
proof (prove)
using this:
lll < l
l = Suc ll

goal (1 subgoal):
 1. lll = ll - (ll - lll)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lll = ll - (ll - lll)

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
let ?l' = "LEAST d. 0 < n (ll - d)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
have nl': "0 < n (ll - ?l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n (ll - (LEAST d. 0 < n (ll - d)))
[PROOF STEP]
proof (rule LeastI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < n (ll - ?k)
[PROOF STEP]
show "0 < n (ll - (ll - lll))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n (ll - (ll - lll))
[PROOF STEP]
using lll nlll
[PROOF STATE]
proof (prove)
using this:
lll = ll - (ll - lll)
0 < n lll

goal (1 subgoal):
 1. 0 < n (ll - (ll - lll))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n (ll - (ll - lll))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < n (ll - (LEAST d. 0 < n (ll - d)))

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
with Suc[THEN spec[of _ "ll - ?l'"]]
[PROOF STATE]
proof (chain)
picking this:
ll - (LEAST d. 0 < n (ll - d)) < l \<and> 0 < n (ll - (LEAST d. 0 < n (ll - d))) \<longrightarrow> (\<exists>k. inf_concat n k = (ll - (LEAST d. 0 < n (ll - d)), 0))
0 < n (ll - (LEAST d. 0 < n (ll - d)))
[PROOF STEP]
obtain k where k:
              "inf_concat n k = (ll - ?l',0)"
[PROOF STATE]
proof (prove)
using this:
ll - (LEAST d. 0 < n (ll - d)) < l \<and> 0 < n (ll - (LEAST d. 0 < n (ll - d))) \<longrightarrow> (\<exists>k. inf_concat n k = (ll - (LEAST d. 0 < n (ll - d)), 0))
0 < n (ll - (LEAST d. 0 < n (ll - d)))

goal (1 subgoal):
 1. (\<And>k. inf_concat n k = (ll - (LEAST d. 0 < n (ll - d)), 0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
using this:
ll - (LEAST d. 0 < n (ll - d)) < Suc ll \<and> 0 < n (ll - (LEAST d. 0 < n (ll - d))) \<longrightarrow> (\<exists>k. inf_concat n k = (ll - (LEAST d. 0 < n (ll - d)), 0))
0 < n (ll - (LEAST d. 0 < n (ll - d)))

goal (1 subgoal):
 1. (\<And>k. inf_concat n k = (ll - (LEAST d. 0 < n (ll - d)), 0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat n k = (ll - (LEAST d. 0 < n (ll - d)), 0)

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
from nl'
[PROOF STATE]
proof (chain)
picking this:
0 < n (ll - (LEAST d. 0 < n (ll - d)))
[PROOF STEP]
obtain off where off: "Suc (0 + off) = n (ll - ?l')"
[PROOF STATE]
proof (prove)
using this:
0 < n (ll - (LEAST d. 0 < n (ll - d)))

goal (1 subgoal):
 1. (\<And>off. Suc (0 + off) = n (ll - (LEAST d. 0 < n (ll - d))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "n (ll - ?l')", auto)
[PROOF STATE]
proof (state)
this:
Suc (0 + off) = n (ll - (LEAST d. 0 < n (ll - d)))

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
from inf_concat_step[OF k, OF off]
[PROOF STATE]
proof (chain)
picking this:
inf_concat n (k + Suc off) = (LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i', 0)
[PROOF STEP]
have id: "inf_concat n (k + Suc off) = (LEAST i'. ll - ?l' < i' \<and> 0 < n i',0)" (is "_ = (?l,0)")
[PROOF STATE]
proof (prove)
using this:
inf_concat n (k + Suc off) = (LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i', 0)

goal (1 subgoal):
 1. inf_concat n (k + Suc off) = (LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i', 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
inf_concat n (k + Suc off) = (LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i', 0)

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
have ll: "?l = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i') = l
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i') = Suc ll
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ll - (LEAST d. 0 < n (ll - d)) < Suc ll \<and> 0 < n (Suc ll)
 2. \<And>y. ll - (LEAST d. 0 < n (ll - d)) < y \<and> 0 < n y \<Longrightarrow> Suc ll \<le> y
[PROOF STEP]
show "ll - ?l' < Suc ll \<and> 0 < n (Suc ll)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ll - (LEAST d. 0 < n (ll - d)) < Suc ll \<and> 0 < n (Suc ll)
[PROOF STEP]
using nj[unfolded j l]
[PROOF STATE]
proof (prove)
using this:
0 < n (Suc ll)

goal (1 subgoal):
 1. ll - (LEAST d. 0 < n (ll - d)) < Suc ll \<and> 0 < n (Suc ll)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ll - (LEAST d. 0 < n (ll - d)) < Suc ll \<and> 0 < n (Suc ll)

goal (1 subgoal):
 1. \<And>y. ll - (LEAST d. 0 < n (ll - d)) < y \<and> 0 < n y \<Longrightarrow> Suc ll \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. ll - (LEAST d. 0 < n (ll - d)) < y \<and> 0 < n y \<Longrightarrow> Suc ll \<le> y
[PROOF STEP]
fix l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. ll - (LEAST d. 0 < n (ll - d)) < y \<and> 0 < n y \<Longrightarrow> Suc ll \<le> y
[PROOF STEP]
assume ass: "ll - ?l' < l' \<and> 0 < n l'"
[PROOF STATE]
proof (state)
this:
ll - (LEAST d. 0 < n (ll - d)) < l' \<and> 0 < n l'

goal (1 subgoal):
 1. \<And>y. ll - (LEAST d. 0 < n (ll - d)) < y \<and> 0 < n y \<Longrightarrow> Suc ll \<le> y
[PROOF STEP]
show "Suc ll \<le> l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ll \<le> l'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
assume not: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> Suc ll \<le> l'

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
hence "l' \<le> ll"
[PROOF STATE]
proof (prove)
using this:
\<not> Suc ll \<le> l'

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

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
hence "ll = l' + (ll - l')"
[PROOF STATE]
proof (prove)
using this:
l' \<le> ll

goal (1 subgoal):
 1. ll = l' + (ll - l')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ll = l' + (ll - l')

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ll = l' + (ll - l')
[PROOF STEP]
obtain k where ll: "ll = l' + k"
[PROOF STATE]
proof (prove)
using this:
ll = l' + (ll - l')

goal (1 subgoal):
 1. (\<And>k. ll = l' + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ll = l' + k

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
from ass
[PROOF STATE]
proof (chain)
picking this:
ll - (LEAST d. 0 < n (ll - d)) < l' \<and> 0 < n l'
[PROOF STEP]
have "l' + k - ?l' < l'"
[PROOF STATE]
proof (prove)
using this:
ll - (LEAST d. 0 < n (ll - d)) < l' \<and> 0 < n l'

goal (1 subgoal):
 1. l' + k - (LEAST d. 0 < n (ll - d)) < l'
[PROOF STEP]
unfolding ll
[PROOF STATE]
proof (prove)
using this:
l' + k - (LEAST d. 0 < n (l' + k - d)) < l' \<and> 0 < n l'

goal (1 subgoal):
 1. l' + k - (LEAST d. 0 < n (l' + k - d)) < l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' + k - (LEAST d. 0 < n (ll - d)) < l'

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
hence kl': "k < ?l'"
[PROOF STATE]
proof (prove)
using this:
l' + k - (LEAST d. 0 < n (ll - d)) < l'

goal (1 subgoal):
 1. k < (LEAST d. 0 < n (ll - d))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < (LEAST d. 0 < n (ll - d))

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
have "0 < n (ll - k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n (ll - k)
[PROOF STEP]
using ass
[PROOF STATE]
proof (prove)
using this:
ll - (LEAST d. 0 < n (ll - d)) < l' \<and> 0 < n l'

goal (1 subgoal):
 1. 0 < n (ll - k)
[PROOF STEP]
unfolding ll
[PROOF STATE]
proof (prove)
using this:
l' + k - (LEAST d. 0 < n (l' + k - d)) < l' \<and> 0 < n l'

goal (1 subgoal):
 1. 0 < n (l' + k - k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < n (ll - k)

goal (1 subgoal):
 1. \<not> Suc ll \<le> l' \<Longrightarrow> False
[PROOF STEP]
from Least_le[of "\<lambda> k. 0 < n (ll - k)", OF this] kl'
[PROOF STATE]
proof (chain)
picking this:
(LEAST x. 0 < n (ll - x)) \<le> k
k < (LEAST d. 0 < n (ll - d))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(LEAST x. 0 < n (ll - x)) \<le> k
k < (LEAST d. 0 < n (ll - d))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc ll \<le> l'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST i'. ll - (LEAST d. 0 < n (ll - d)) < i' \<and> 0 < n i') = l

goal (1 subgoal):
 1. \<exists>j'<l. 0 < n j' \<Longrightarrow> \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (j, 0)
[PROOF STEP]
unfolding j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (l, 0)
[PROOF STEP]
by (rule exI[of _ "k + Suc off"], unfold id ll, simp)
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (j, 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (j, 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (j, 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j. j < Suc l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j. j < l \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>j. j < ?l2 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < n i
\<forall>j. j < ?l2 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < n i
\<forall>j. j < ?l2 \<and> 0 < n j \<longrightarrow> (\<exists>k. inf_concat n k = (j, 0))

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (i, 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_surj:
  assumes j: "j < n i"
  shows "\<exists>k. inf_concat n k = (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, j)
[PROOF STEP]
from j
[PROOF STATE]
proof (chain)
picking this:
j < n i
[PROOF STEP]
have "0 < n i"
[PROOF STATE]
proof (prove)
using this:
j < n i

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

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, j)
[PROOF STEP]
from inf_concat_surj_zero[of n, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. inf_concat n k = (i, 0)
[PROOF STEP]
obtain k where "inf_concat n k = (i,0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. inf_concat n k = (i, 0)

goal (1 subgoal):
 1. (\<And>k. inf_concat n k = (i, 0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inf_concat n k = (i, 0)

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, j)
[PROOF STEP]
from inf_concat_add[OF this, of j] j
[PROOF STATE]
proof (chain)
picking this:
0 + j < n i \<Longrightarrow> inf_concat n (k + j) = (i, 0 + j)
j < n i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 + j < n i \<Longrightarrow> inf_concat n (k + j) = (i, 0 + j)
j < n i

goal (1 subgoal):
 1. \<exists>k. inf_concat n k = (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. inf_concat n k = (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_mono:
  assumes inf: "INFM i. n i > 0"
    and resk: "inf_concat n k = (i, j)"
    and reskp: "inf_concat n k' = (i', j')"
    and lt: "i < i'"
  shows "k < k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k < k'
[PROOF STEP]
note bounds = inf_concat_bounds[OF inf]
[PROOF STATE]
proof (state)
this:
inf_concat n ?k = (?i, ?j) \<Longrightarrow> ?j < n ?i

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inf_concat n ?k = (?i, ?j) \<Longrightarrow> ?j < n ?i

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
assume "k' \<le> k"
[PROOF STATE]
proof (state)
this:
k' \<le> k

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
hence "k = k' + (k - k')"
[PROOF STATE]
proof (prove)
using this:
k' \<le> k

goal (1 subgoal):
 1. k = k' + (k - k')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = k' + (k - k')

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = k' + (k - k')
[PROOF STEP]
obtain l where k: "k = k' + l"
[PROOF STATE]
proof (prove)
using this:
k = k' + (k - k')

goal (1 subgoal):
 1. (\<And>l. k = k' + l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = k' + l

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
have "i' \<le> fst (inf_concat n (k' + l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> fst (inf_concat n (k' + l))
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i' \<le> fst (inf_concat n (k' + 0))
 2. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. i' \<le> fst (inf_concat n (k' + 0))
 2. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
with reskp
[PROOF STATE]
proof (chain)
picking this:
inf_concat n k' = (i', j')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inf_concat n k' = (i', j')

goal (1 subgoal):
 1. i' \<le> fst (inf_concat n (k' + 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' \<le> fst (inf_concat n (k' + 0))

goal (1 subgoal):
 1. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
i' \<le> fst (inf_concat n (k' + l))

goal (1 subgoal):
 1. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
obtain i'' j'' where l: "inf_concat n (k' + l) = (i'',j'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'' j''. inf_concat n (k' + l) = (i'', j'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inf_concat n (k' + l) = (i'', j'')

goal (1 subgoal):
 1. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
i' \<le> fst (inf_concat n (k' + l))
inf_concat n (k' + l) = (i'', j'')
[PROOF STEP]
have one: "i' \<le> i''"
[PROOF STATE]
proof (prove)
using this:
i' \<le> fst (inf_concat n (k' + l))
inf_concat n (k' + l) = (i'', j'')

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

goal (1 subgoal):
 1. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
from bounds[OF l]
[PROOF STATE]
proof (chain)
picking this:
j'' < n i''
[PROOF STEP]
have j'': "j'' < n i''"
[PROOF STATE]
proof (prove)
using this:
j'' < n i''

goal (1 subgoal):
 1. j'' < n i''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j'' < n i''

goal (1 subgoal):
 1. \<And>l. i' \<le> fst (inf_concat n (k' + l)) \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
proof (cases "Suc j'' < n i''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
 2. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc j'' < n i''

goal (2 subgoals):
 1. Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
 2. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
by (simp add: l True one)
[PROOF STATE]
proof (state)
this:
i' \<le> fst (inf_concat n (k' + Suc l))

goal (1 subgoal):
 1. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Suc j'' < n i''

goal (1 subgoal):
 1. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
let ?i = "LEAST i'. i'' < i' \<and> 0 < n i'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
from inf[unfolded INFM_nat]
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. \<exists>na>m. 0 < n na
[PROOF STEP]
obtain k where "i'' < k \<and> 0 < n k"
[PROOF STATE]
proof (prove)
using this:
\<forall>m. \<exists>na>m. 0 < n na

goal (1 subgoal):
 1. (\<And>k. i'' < k \<and> 0 < n k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i'' < k \<and> 0 < n k

goal (1 subgoal):
 1. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
from LeastI[of "\<lambda> k. i'' < k \<and> 0 < n k", OF this]
[PROOF STATE]
proof (chain)
picking this:
i'' < (LEAST x. i'' < x \<and> 0 < n x) \<and> 0 < n (LEAST x. i'' < x \<and> 0 < n x)
[PROOF STEP]
have "i'' < ?i"
[PROOF STATE]
proof (prove)
using this:
i'' < (LEAST x. i'' < x \<and> 0 < n x) \<and> 0 < n (LEAST x. i'' < x \<and> 0 < n x)

goal (1 subgoal):
 1. i'' < (LEAST i'. i'' < i' \<and> 0 < n i')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i'' < (LEAST i'. i'' < i' \<and> 0 < n i')

goal (1 subgoal):
 1. \<not> Suc j'' < n i'' \<Longrightarrow> i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
with one
[PROOF STATE]
proof (chain)
picking this:
i' \<le> i''
i'' < (LEAST i'. i'' < i' \<and> 0 < n i')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i' \<le> i''
i'' < (LEAST i'. i'' < i' \<and> 0 < n i')

goal (1 subgoal):
 1. i' \<le> fst (inf_concat n (k' + Suc l))
[PROOF STEP]
by (simp add: l False)
[PROOF STATE]
proof (state)
this:
i' \<le> fst (inf_concat n (k' + Suc l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i' \<le> fst (inf_concat n (k' + Suc l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i' \<le> fst (inf_concat n (k' + l))

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
with resk k lt
[PROOF STATE]
proof (chain)
picking this:
inf_concat n k = (i, j)
k = k' + l
i < i'
i' \<le> fst (inf_concat n (k' + l))
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
inf_concat n k = (i, j)
k = k' + l
i < i'
i' \<le> fst (inf_concat n (k' + l))

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

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
k' \<le> k \<Longrightarrow> False

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k' \<le> k \<Longrightarrow> False

goal (1 subgoal):
 1. k < k'
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
k < k'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_concat_Suc:
  assumes inf: "INFM i. n i > 0"
    and f: "\<And> i. f i (n i) = f (Suc i) 0"
    and resk: "inf_concat n k = (i, j)"
    and ressk: "inf_concat n (Suc k) = (i', j')"
  shows "f i' j' = f i (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
note bounds = inf_concat_bounds[OF inf]
[PROOF STATE]
proof (state)
this:
inf_concat n ?k = (?i, ?j) \<Longrightarrow> ?j < n ?i

goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
from bounds[OF resk]
[PROOF STATE]
proof (chain)
picking this:
j < n i
[PROOF STEP]
have j: "j < n i"
[PROOF STATE]
proof (prove)
using this:
j < n i

goal (1 subgoal):
 1. j < n i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
j < n i

goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
proof (cases "Suc j < n i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
 2. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc j < n i

goal (2 subgoals):
 1. Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
 2. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
with ressk resk
[PROOF STATE]
proof (chain)
picking this:
inf_concat n (Suc k) = (i', j')
inf_concat n k = (i, j)
Suc j < n i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inf_concat n (Suc k) = (i', j')
inf_concat n k = (i, j)
Suc j < n i

goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f i' j' = f i (Suc j)

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Suc j < n i

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
let ?p = "\<lambda> i'. i < i' \<and> 0 < n i'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
let ?i' = "LEAST i'. ?p i'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
from False j
[PROOF STATE]
proof (chain)
picking this:
\<not> Suc j < n i
j < n i
[PROOF STEP]
have id: "Suc (j + 0) = n i"
[PROOF STATE]
proof (prove)
using this:
\<not> Suc j < n i
j < n i

goal (1 subgoal):
 1. Suc (j + 0) = n i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (j + 0) = n i

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
from inf_concat_step[OF resk, OF id] ressk
[PROOF STATE]
proof (chain)
picking this:
inf_concat n (k + Suc 0) = (LEAST i'. i < i' \<and> 0 < n i', 0)
inf_concat n (Suc k) = (i', j')
[PROOF STEP]
have i': "i' = ?i'" and j': "j' = 0"
[PROOF STATE]
proof (prove)
using this:
inf_concat n (k + Suc 0) = (LEAST i'. i < i' \<and> 0 < n i', 0)
inf_concat n (Suc k) = (i', j')

goal (1 subgoal):
 1. i' = (LEAST i'. i < i' \<and> 0 < n i') &&& j' = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' = (LEAST i'. i < i' \<and> 0 < n i')
j' = 0

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
from id
[PROOF STATE]
proof (chain)
picking this:
Suc (j + 0) = n i
[PROOF STEP]
have j: "Suc j = n i"
[PROOF STATE]
proof (prove)
using this:
Suc (j + 0) = n i

goal (1 subgoal):
 1. Suc j = n i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc j = n i

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
from inf[unfolded INFM_nat]
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. \<exists>na>m. 0 < n na
[PROOF STEP]
obtain k where "?p k"
[PROOF STATE]
proof (prove)
using this:
\<forall>m. \<exists>na>m. 0 < n na

goal (1 subgoal):
 1. (\<And>k. i < k \<and> 0 < n k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < k \<and> 0 < n k

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
from LeastI[of ?p, OF this]
[PROOF STATE]
proof (chain)
picking this:
i < (LEAST x. i < x \<and> 0 < n x) \<and> 0 < n (LEAST x. i < x \<and> 0 < n x)
[PROOF STEP]
have "?p ?i'"
[PROOF STATE]
proof (prove)
using this:
i < (LEAST x. i < x \<and> 0 < n x) \<and> 0 < n (LEAST x. i < x \<and> 0 < n x)

goal (1 subgoal):
 1. i < (LEAST i'. i < i' \<and> 0 < n i') \<and> 0 < n (LEAST i'. i < i' \<and> 0 < n i')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i < (LEAST i'. i < i' \<and> 0 < n i') \<and> 0 < n (LEAST i'. i < i' \<and> 0 < n i')

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
hence "?i' = Suc i + (?i' - Suc i)"
[PROOF STATE]
proof (prove)
using this:
i < (LEAST i'. i < i' \<and> 0 < n i') \<and> 0 < n (LEAST i'. i < i' \<and> 0 < n i')

goal (1 subgoal):
 1. (LEAST i'. i < i' \<and> 0 < n i') = Suc i + ((LEAST i'. i < i' \<and> 0 < n i') - Suc i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST i'. i < i' \<and> 0 < n i') = Suc i + ((LEAST i'. i < i' \<and> 0 < n i') - Suc i)

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LEAST i'. i < i' \<and> 0 < n i') = Suc i + ((LEAST i'. i < i' \<and> 0 < n i') - Suc i)
[PROOF STEP]
obtain d where ii': "?i' = Suc i + d"
[PROOF STATE]
proof (prove)
using this:
(LEAST i'. i < i' \<and> 0 < n i') = Suc i + ((LEAST i'. i < i' \<and> 0 < n i') - Suc i)

goal (1 subgoal):
 1. (\<And>d. (LEAST i'. i < i' \<and> 0 < n i') = Suc i + d \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST i'. i < i' \<and> 0 < n i') = Suc i + d

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
from not_less_Least[of _ ?p, unfolded ii']
[PROOF STATE]
proof (chain)
picking this:
?k < Suc i + d \<Longrightarrow> \<not> (i < ?k \<and> 0 < n ?k)
[PROOF STEP]
have d': "\<And> d'. d' < d \<Longrightarrow> n (Suc i + d') = 0"
[PROOF STATE]
proof (prove)
using this:
?k < Suc i + d \<Longrightarrow> \<not> (i < ?k \<and> 0 < n ?k)

goal (1 subgoal):
 1. \<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?d' < d \<Longrightarrow> n (Suc i + ?d') = 0

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
have "f (Suc i) 0 = f ?i' 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) 0 = f (LEAST i'. i < i' \<and> 0 < n i') 0
[PROOF STEP]
unfolding ii'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) 0 = f (Suc i + d) 0
[PROOF STEP]
using d'
[PROOF STATE]
proof (prove)
using this:
?d' < d \<Longrightarrow> n (Suc i + ?d') = 0

goal (1 subgoal):
 1. f (Suc i) 0 = f (Suc i + d) 0
[PROOF STEP]
proof (induct d)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>d'. d' < 0 \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + 0) 0
 2. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
?d' < 0 \<Longrightarrow> n (Suc i + ?d') = 0

goal (2 subgoals):
 1. (\<And>d'. d' < 0 \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + 0) 0
 2. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) 0 = f (Suc i + 0) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc i) 0 = f (Suc i + 0) 0

goal (1 subgoal):
 1. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
case (Suc d)
[PROOF STATE]
proof (state)
this:
(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0
?d' < Suc d \<Longrightarrow> n (Suc i + ?d') = 0

goal (1 subgoal):
 1. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
hence "f (Suc i) 0 = f (Suc i + d) 0"
[PROOF STATE]
proof (prove)
using this:
(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0
?d' < Suc d \<Longrightarrow> n (Suc i + ?d') = 0

goal (1 subgoal):
 1. f (Suc i) 0 = f (Suc i + d) 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc i) 0 = f (Suc i + d) 0

goal (1 subgoal):
 1. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (Suc i) 0 = f (Suc i + d) 0

goal (1 subgoal):
 1. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
have "... = f (Suc (Suc i + d)) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i + d) 0 = f (Suc (Suc i + d)) 0
[PROOF STEP]
unfolding f[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i + d) 0 = f (Suc i + d) (n (Suc i + d))
[PROOF STEP]
using Suc(2)[of d]
[PROOF STATE]
proof (prove)
using this:
d < Suc d \<Longrightarrow> n (Suc i + d) = 0

goal (1 subgoal):
 1. f (Suc i + d) 0 = f (Suc i + d) (n (Suc i + d))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc i + d) 0 = f (Suc (Suc i + d)) 0

goal (1 subgoal):
 1. \<And>d. \<lbrakk>(\<And>d'. d' < d \<Longrightarrow> n (Suc i + d') = 0) \<Longrightarrow> f (Suc i) 0 = f (Suc i + d) 0; \<And>d'. d' < Suc d \<Longrightarrow> n (Suc i + d') = 0\<rbrakk> \<Longrightarrow> f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (Suc i) 0 = f (Suc (Suc i + d)) 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f (Suc i) 0 = f (Suc (Suc i + d)) 0

goal (1 subgoal):
 1. f (Suc i) 0 = f (Suc i + Suc d) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc i) 0 = f (Suc i + Suc d) 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (Suc i) 0 = f (LEAST i'. i < i' \<and> 0 < n i') 0

goal (1 subgoal):
 1. \<not> Suc j < n i \<Longrightarrow> f i' j' = f i (Suc j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f (Suc i) 0 = f (LEAST i'. i < i' \<and> 0 < n i') 0

goal (1 subgoal):
 1. f i' j' = f i (Suc j)
[PROOF STEP]
unfolding i' j' j f
[PROOF STATE]
proof (prove)
using this:
f (Suc i) 0 = f (LEAST i'. i < i' \<and> 0 < n i') 0

goal (1 subgoal):
 1. f (LEAST i'. i < i' \<and> 0 < n i') 0 = f (Suc i) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f i' j' = f i (Suc j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f i' j' = f i (Suc j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_ascending_chain:
  "ascending_chain f \<Longrightarrow> descending_chain (\<lambda>n . -f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ascending_chain f \<Longrightarrow> descending_chain (\<lambda>n. a (f n))
[PROOF STEP]
by (simp add: a_antitone ascending_chain_def descending_chain_def)


[STATEMENT]
lemma a_descending_chain:
  "descending_chain f \<Longrightarrow> ascending_chain (\<lambda>n . -f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. descending_chain f \<Longrightarrow> ascending_chain (\<lambda>n. a (f n))
[PROOF STEP]
by (simp add: a_antitone ord.ascending_chain_def ord.descending_chain_def)


[STATEMENT]
lemma d_dist_Sum:
  "ascending_chain f \<Longrightarrow> d(Sum f) = Sum (\<lambda>n . d(f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ascending_chain f \<Longrightarrow> d (complete_tests_class.Sum f) = complete_tests_class.Sum (\<lambda>n. d (f n))
[PROOF STEP]
by (simp add: d_def a_ascending_chain a_dist_Prod a_dist_Sum)


[STATEMENT]
lemma d_dist_Prod:
  "descending_chain f \<Longrightarrow> d(Prod f) = Prod (\<lambda>n . d(f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. descending_chain f \<Longrightarrow> d (complete_tests_class.Prod f) = complete_tests_class.Prod (\<lambda>n. d (f n))
[PROOF STEP]
by (simp add: d_def a_dist_Sum a_dist_Prod a_descending_chain)


[STATEMENT]
lemma proper_it_fold:
    "proper_it it it' \<Longrightarrow> foldli (it (\<lambda>_. True) (\<lambda>x l. l@[x]) []) = it'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it it it' \<Longrightarrow> foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) = it'
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. it = foldli l \<and> it' = foldli l \<Longrightarrow> foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) = it'
[PROOF STEP]
by auto


[STATEMENT]
lemma proper_it_unfold:
    "proper_it it it' \<Longrightarrow> it' = foldli (it (\<lambda>_. True) (\<lambda>x l. l@[x]) [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it it it' \<Longrightarrow> it' = foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) [])
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. it = foldli l \<and> it' = foldli l \<Longrightarrow> it' = foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) [])
[PROOF STEP]
by auto


[STATEMENT]
lemma pi_it_to_it[icf_proper_iteratorI]: "proper_it (it_to_it I) (it_to_it I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (it_to_it I) (it_to_it I)
[PROOF STEP]
unfolding it_to_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (foldli (I (\<lambda>_. True) (\<lambda>x l. l @ [x]) [])) (foldli (I (\<lambda>_. True) (\<lambda>x l. l @ [x]) []))
[PROOF STEP]
by (rule pi_foldli)


[STATEMENT]
lemma it_to_it_fold: "proper_it it (it'::('x,'\<sigma>) set_iterator)
    \<Longrightarrow> it_to_it it = it'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it it it' \<Longrightarrow> it_to_it it = it'
[PROOF STEP]
unfolding it_to_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it it it' \<Longrightarrow> foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) = it'
[PROOF STEP]
by (simp add: proper_it_fold)


[STATEMENT]
lemma it_to_it_map_fold:
    assumes P: "proper_it it it'"
    shows "it_to_it (\<lambda>c f. it c (f \<circ> f')) = (\<lambda>c f. it' c (f o f'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_it (\<lambda>c f. it c (f \<circ> f')) = (\<lambda>c f. it' c (f \<circ> f'))
[PROOF STEP]
apply (rule proper_itE[OF P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> it_to_it (\<lambda>c f. it c (f \<circ> f')) = (\<lambda>c f. it' c (f \<circ> f'))
[PROOF STEP]
unfolding it_to_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> foldli (it (\<lambda>_. True) ((\<lambda>x l. l @ [x]) \<circ> f') []) = (\<lambda>c f. it' c (f \<circ> f'))
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l c f x. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> foldli (it (\<lambda>_. True) ((\<lambda>x l. l @ [x]) \<circ> f') []) c f x = it' c (f \<circ> f') x
[PROOF STEP]
apply (simp add: foldli_foldl map_by_foldl foldli_map)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma it_to_it_fold': "proper_it' it (it'::'s \<Rightarrow> ('x,'\<sigma>) set_iterator)
    \<Longrightarrow> it_to_it (it s) = (it' s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' it it' \<Longrightarrow> it_to_it (it s) = it' s
[PROOF STEP]
by (drule proper_it'D) (rule it_to_it_fold)


[STATEMENT]
lemma it_to_it_map_fold':
    assumes P: "proper_it' it it'"
    shows "it_to_it (\<lambda>c f. it s c (f \<circ> f')) = (\<lambda>c f. it' s c (f o f'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_it (\<lambda>c f. it s c (f \<circ> f')) = (\<lambda>c f. it' s c (f \<circ> f'))
[PROOF STEP]
using P[THEN proper_it'D]
[PROOF STATE]
proof (prove)
using this:
proper_it (it ?s) (it' ?s)

goal (1 subgoal):
 1. it_to_it (\<lambda>c f. it s c (f \<circ> f')) = (\<lambda>c f. it' s c (f \<circ> f'))
[PROOF STEP]
by (rule it_to_it_map_fold)


[STATEMENT]
lemma proper: "proper_it (it s) (it' s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (it s) (it' s)
[PROOF STEP]
using proper'
[PROOF STATE]
proof (prove)
using this:
proper_it' it it'

goal (1 subgoal):
 1. proper_it (it s) (it' s)
[PROOF STEP]
by (rule proper_it'D)


[STATEMENT]
lemma it_to_it_genord_correct:
    assumes "set_iterator_genord (it::('x,'x list) set_iterator) S R"
    shows "set_iterator_genord ((it_to_it it)::('x,'\<sigma>) set_iterator) S R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S R
[PROOF STEP]
interpret set_iterator_genord it S R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord it S R
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S R
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l0. distinct l0 \<and> S = set l0 \<and> sorted_wrt R l0 \<and> it_to_it it = foldli l0
[PROOF STEP]
unfolding it_to_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l0. distinct l0 \<and> S = set l0 \<and> sorted_wrt R l0 \<and> foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) = foldli l0
[PROOF STEP]
using foldli_transform
[PROOF STATE]
proof (prove)
using this:
\<exists>l0. distinct l0 \<and> S = set l0 \<and> sorted_wrt R l0 \<and> it = foldli l0

goal (1 subgoal):
 1. \<exists>l0. distinct l0 \<and> S = set l0 \<and> sorted_wrt R l0 \<and> foldli (it (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) = foldli l0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_iterator_genord (it_to_it it) S R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma it_to_it_linord_correct:
    assumes "set_iterator_linord (it::('x::linorder,'x list) set_iterator) S"
    shows "set_iterator_linord ((it_to_it it)::('x,'\<sigma>) set_iterator) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_linord (it_to_it it) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set_iterator_linord it S

goal (1 subgoal):
 1. set_iterator_linord (it_to_it it) S
[PROOF STEP]
unfolding set_iterator_linord_def
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord it S (\<le>)

goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S (\<le>)
[PROOF STEP]
by (rule it_to_it_genord_correct)


[STATEMENT]
lemma it_to_it_rev_linord_correct:
    assumes "set_iterator_rev_linord (it::('x::linorder,'x list) set_iterator) S"
    shows "set_iterator_rev_linord ((it_to_it it)::('x,'\<sigma>) set_iterator) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_rev_linord (it_to_it it) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set_iterator_rev_linord it S

goal (1 subgoal):
 1. set_iterator_rev_linord (it_to_it it) S
[PROOF STEP]
unfolding set_iterator_rev_linord_def
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord it S (\<lambda>x y. y \<le> x)

goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S (\<lambda>x y. y \<le> x)
[PROOF STEP]
by (rule it_to_it_genord_correct)


[STATEMENT]
lemma it_to_it_correct:
    assumes "set_iterator (it::('x,'x list) set_iterator) S"
    shows "set_iterator ((it_to_it it)::('x,'\<sigma>) set_iterator) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator (it_to_it it) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set_iterator it S

goal (1 subgoal):
 1. set_iterator (it_to_it it) S
[PROOF STEP]
unfolding set_iterator_def
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord it S (\<lambda>_ _. True)

goal (1 subgoal):
 1. set_iterator_genord (it_to_it it) S (\<lambda>_ _. True)
[PROOF STEP]
by (rule it_to_it_genord_correct)


[STATEMENT]
lemma it_to_it_map_genord_correct:
    assumes "map_iterator_genord (it::('u,'v,('u\<times>'v) list) map_iterator) S R"
    shows "map_iterator_genord ((it_to_it it)::('u,'v,'\<sigma>) map_iterator) S R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_genord (it_to_it it) S R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_iterator_genord it S R

goal (1 subgoal):
 1. map_iterator_genord (it_to_it it) S R
[PROOF STEP]
by (rule it_to_it_genord_correct)


[STATEMENT]
lemma it_to_it_map_linord_correct:
    assumes "map_iterator_linord (it::('u::linorder,'v,('u\<times>'v) list) map_iterator) S"
    shows "map_iterator_linord ((it_to_it it)::('u,'v,'\<sigma>) map_iterator) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_linord (it_to_it it) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_iterator_linord it S

goal (1 subgoal):
 1. map_iterator_linord (it_to_it it) S
[PROOF STEP]
unfolding set_iterator_map_linord_def
[PROOF STATE]
proof (prove)
using this:
map_iterator_genord it S (\<lambda>(k, uu_) (k', uu_). k \<le> k')

goal (1 subgoal):
 1. map_iterator_genord (it_to_it it) S (\<lambda>(k, uu_) (k', uu_). k \<le> k')
[PROOF STEP]
by (rule it_to_it_genord_correct)


[STATEMENT]
lemma it_to_it_map_rev_linord_correct:
    assumes
      "map_iterator_rev_linord (it::('u::linorder,'v,('u\<times>'v) list) map_iterator) S"
    shows "map_iterator_rev_linord ((it_to_it it)::('u,'v,'\<sigma>) map_iterator) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator_rev_linord (it_to_it it) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_iterator_rev_linord it S

goal (1 subgoal):
 1. map_iterator_rev_linord (it_to_it it) S
[PROOF STEP]
unfolding set_iterator_map_rev_linord_def
[PROOF STATE]
proof (prove)
using this:
map_iterator_genord it S (\<lambda>(k, uu_) (k', uu_). k' \<le> k)

goal (1 subgoal):
 1. map_iterator_genord (it_to_it it) S (\<lambda>(k, uu_) (k', uu_). k' \<le> k)
[PROOF STEP]
by (rule it_to_it_genord_correct)


[STATEMENT]
lemma it_to_it_map_correct:
    assumes "map_iterator (it::('u,'v,('u\<times>'v) list) map_iterator) S"
    shows "map_iterator ((it_to_it it)::('u,'v,'\<sigma>) map_iterator) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator (it_to_it it) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map_iterator it S

goal (1 subgoal):
 1. map_iterator (it_to_it it) S
[PROOF STEP]
by (rule it_to_it_correct)


[STATEMENT]
lemma seqp_broadcastTE [elim]:
  "\<lbrakk>((\<xi>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>;
    \<lbrakk>a = broadcast (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<lbrakk>a = broadcast (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma seqp_groupcastTE [elim]:
  "\<lbrakk>((\<xi>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>;
    \<lbrakk>a = groupcast (s\<^sub>i\<^sub>p\<^sub>s \<xi>) (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<lbrakk>a = groupcast (s\<^sub>i\<^sub>p\<^sub>s \<xi>) (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma seqp_unicastTE [elim]:
  "\<lbrakk>((\<xi>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g). p \<triangleright> q), a, (\<xi>', r)) \<in> seqp_sos \<Gamma>;
    \<lbrakk>a = unicast (s\<^sub>i\<^sub>p \<xi>) (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; r = p\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>a = \<not>unicast (s\<^sub>i\<^sub>p \<xi>); \<xi>' = \<xi>; r = q\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> q), a, \<xi>', r) \<in> seqp_sos \<Gamma>; \<lbrakk>a = unicast (s\<^sub>i\<^sub>p \<xi>) (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; r = p\<rbrakk> \<Longrightarrow> P; \<lbrakk>a = \<not>unicast (s\<^sub>i\<^sub>p \<xi>); \<xi>' = \<xi>; r = q\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g). p \<triangleright> q), a, (\<xi>', r)) \<in> seqp_sos \<Gamma>") simp_all


[STATEMENT]
lemma seqp_sendTE [elim]:
  "\<lbrakk>((\<xi>, {l}send(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>;
    \<lbrakk>a = send (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<lbrakk>a = send (s\<^sub>m\<^sub>s\<^sub>g \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}send(s\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma seqp_deliverTE [elim]:
  "\<lbrakk>((\<xi>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>;
    \<lbrakk>a = deliver (s\<^sub>d\<^sub>a\<^sub>t\<^sub>a \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<lbrakk>a = deliver (s\<^sub>d\<^sub>a\<^sub>t\<^sub>a \<xi>); \<xi>' = \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma seqp_receiveTE [elim]:
  "\<lbrakk>((\<xi>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>;
    \<And>msg. \<lbrakk>a = receive msg; \<xi>' = u\<^sub>m\<^sub>s\<^sub>g msg \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<And>msg. \<lbrakk>a = receive msg; \<xi>' = u\<^sub>m\<^sub>s\<^sub>g msg \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g). p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma seqp_assignTE [elim]:
  "\<lbrakk>((\<xi>, {l}\<lbrakk>u\<rbrakk> p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>; \<lbrakk>a = \<tau>; \<xi>' = u \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}\<lbrakk>u\<rbrakk>
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<lbrakk>a = \<tau>; \<xi>' = u \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}\<lbrakk>u\<rbrakk> p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma seqp_guardTE [elim]:
  "\<lbrakk>((\<xi>, {l}\<langle>g\<rangle> p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>; \<lbrakk>a = \<tau>; \<xi>' \<in> g \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<xi>, {l}\<langle>g\<rangle>
p), a, \<xi>', q) \<in> seqp_sos \<Gamma>; \<lbrakk>a = \<tau>; \<xi>' \<in> g \<xi>; q = p\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((\<xi>, {l}\<langle>g\<rangle> p), a, (\<xi>', q)) \<in> seqp_sos \<Gamma>") simp


[STATEMENT]
lemma par_broadcastTE [elim]:
  "\<lbrakk>((s, t), broadcast m, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(s, broadcast m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, broadcast m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), broadcast m, s', t') \<in> parp_sos S T; \<lbrakk>(s, broadcast m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, broadcast m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), broadcast m, (s', t')) \<in> parp_sos S T") simp_all


[STATEMENT]
lemma par_groupcastTE [elim]:
  "\<lbrakk>((s, t), groupcast ips m, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(s, groupcast ips m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, groupcast ips m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), groupcast ips m, s', t') \<in> parp_sos S T; \<lbrakk>(s, groupcast ips m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, groupcast ips m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), groupcast ips m, (s', t')) \<in> parp_sos S T") simp_all


[STATEMENT]
lemma par_unicastTE [elim]:
  "\<lbrakk>((s, t), unicast i m, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(s, unicast i m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, unicast i m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), unicast i m, s', t') \<in> parp_sos S T; \<lbrakk>(s, unicast i m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, unicast i m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), unicast i m, (s', t')) \<in> parp_sos S T") simp_all


[STATEMENT]
lemma par_notunicastTE [elim]:
  "\<lbrakk>((s, t), notunicast i, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(s, notunicast i, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, notunicast i, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), \<not>unicast i, s', t') \<in> parp_sos S T; \<lbrakk>(s, \<not>unicast i, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, \<not>unicast i, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), notunicast i, (s', t')) \<in> parp_sos S T") simp_all


[STATEMENT]
lemma par_sendTE [elim]:
  "\<lbrakk>((s, t), send m, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(s, send m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), send m, s', t') \<in> parp_sos S T; \<lbrakk>(s, send m, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), send m, (s', t')) \<in> parp_sos S T") auto


[STATEMENT]
lemma par_deliverTE [elim]:
  "\<lbrakk>((s, t), deliver d, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(s, deliver d, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P;
    \<lbrakk>(t, deliver d, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), deliver d, s', t') \<in> parp_sos S T; \<lbrakk>(s, deliver d, s') \<in> S; t' = t\<rbrakk> \<Longrightarrow> P; \<lbrakk>(t, deliver d, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), deliver d, (s', t')) \<in> parp_sos S T") simp_all


[STATEMENT]
lemma par_receiveTE [elim]:
  "\<lbrakk>((s, t), receive m, (s', t')) \<in> parp_sos S T;
    \<lbrakk>(t, receive m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((s, t), receive m, s', t') \<in> parp_sos S T; \<lbrakk>(t, receive m, t') \<in> T; s' = s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (ind_cases "((s, t), receive m, (s', t')) \<in> parp_sos S T") auto


[STATEMENT]
lemma trans_par_comp [simp]:
  "trans (s \<langle>\<langle> t) = parp_sos (trans s) (trans t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (s \<langle>\<langle> t) = parp_sos (automaton.trans s) (automaton.trans t)
[PROOF STEP]
unfolding par_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans \<lparr>init = init s \<times> init t, trans = parp_sos (automaton.trans s) (automaton.trans t)\<rparr> = parp_sos (automaton.trans s) (automaton.trans t)
[PROOF STEP]
by simp