[STATEMENT]
lemma srev_induct[case_names bottom snil ssnoc]:
  assumes "P \<bottom>"
  assumes "P [::]"
  assumes "\<And>x xs. \<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>; P xs\<rbrakk> \<Longrightarrow> P (xs :@ [:x:])"
  shows "P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
have "P (srev\<cdot>(srev\<cdot>xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (srev\<cdot>(srev\<cdot>xs))
[PROOF STEP]
by (rule slist.induct[where x="srev\<cdot>xs"]; simp add: assms)
[PROOF STATE]
proof (state)
this:
P (srev\<cdot>(srev\<cdot>xs))

goal (1 subgoal):
 1. P xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P (srev\<cdot>(srev\<cdot>xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P (srev\<cdot>(srev\<cdot>xs))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sfoldr_conv_sfoldl:
  assumes "\<And>x. f\<cdot>x\<cdot>\<bottom> = \<bottom>" \<comment>\<open>\<open>f\<close> must be strict in the accumulator.\<close>
  shows "sfoldr\<cdot>f\<cdot>z\<cdot>xs = sfoldl\<cdot>(\<Lambda> acc x. f\<cdot>x\<cdot>acc)\<cdot>z\<cdot>(srev\<cdot>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfoldr\<cdot>f\<cdot>z\<cdot>xs = sfoldl\<cdot>(\<Lambda> acc x. f\<cdot>x\<cdot>acc)\<cdot>z\<cdot>(srev\<cdot>xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f\<cdot>?x\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. sfoldr\<cdot>f\<cdot>z\<cdot>xs = sfoldl\<cdot>(\<Lambda> acc x. f\<cdot>x\<cdot>acc)\<cdot>z\<cdot>(srev\<cdot>xs)
[PROOF STEP]
by (induct xs arbitrary: z) simp_all


[STATEMENT]
lemma stake_strict[simp]:
  "stake\<cdot>\<bottom> = \<bottom>"
  "stake\<cdot>i\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake\<cdot>\<bottom> = \<bottom> &&& stake\<cdot>i\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp+


[STATEMENT]
lemma stake_bottom_iff[simp]: "(stake\<cdot>i\<cdot>xs = \<bottom>) \<longleftrightarrow> (i = \<bottom> \<or> xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stake\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)
[PROOF STEP]
by (induct xs arbitrary: i; clarsimp; case_tac i; clarsimp)


[STATEMENT]
lemma stake_0[simp]:
  "xs \<noteq> \<bottom> \<Longrightarrow> stake\<cdot>0\<cdot>xs = [::]"
  "xs \<noteq> \<bottom> \<Longrightarrow> stake\<cdot>(MkI\<cdot>0)\<cdot>xs = [::]"
  "stake\<cdot>0\<cdot>xs \<sqsubseteq> [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<noteq> \<bottom> \<Longrightarrow> stake\<cdot>0\<cdot>xs = [::]) &&& (xs \<noteq> \<bottom> \<Longrightarrow> stake\<cdot>(MkI\<cdot>0)\<cdot>xs = [::]) &&& stake\<cdot>0\<cdot>xs \<sqsubseteq> [::]
[PROOF STEP]
by (cases xs; simp add: zero_Integer_def)+


[STATEMENT]
lemma stake_scons[simp]: "le\<cdot>1\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>(x :# xs) = x :# stake\<cdot>(i - 1)\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le\<cdot>1\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>(x :# xs) = x :# stake\<cdot>(i - 1)\<cdot>xs
[PROOF STEP]
by (cases i; cases "x = \<bottom>"; cases "xs = \<bottom>";
    simp add: zero_Integer_def one_Integer_def split: if_splits)


[STATEMENT]
lemma take_MkI_scons[simp]:
  "0 < n \<Longrightarrow> stake\<cdot>(MkI\<cdot>n)\<cdot>(x :# xs) = x :# stake\<cdot>(MkI\<cdot>(n - 1))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> stake\<cdot>(MkI\<cdot>n)\<cdot>(x :# xs) = x :# stake\<cdot>(MkI\<cdot>(n - 1))\<cdot>xs
[PROOF STEP]
by (cases "x = \<bottom>"; cases "xs = \<bottom>"; simp add: zero_Integer_def one_Integer_def)


[STATEMENT]
lemma stake_numeral_scons[simp]:
  "xs \<noteq> \<bottom> \<Longrightarrow> stake\<cdot>1\<cdot>(x :# xs) = [:x:]"
  "stake\<cdot>(numeral (Num.Bit0 k))\<cdot>(x :# xs) = x :# stake\<cdot>(numeral (Num.BitM k))\<cdot>xs"
  "stake\<cdot>(numeral (Num.Bit1 k))\<cdot>(x :# xs) = x :# stake\<cdot>(numeral (Num.Bit0 k))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<noteq> \<bottom> \<Longrightarrow> stake\<cdot>1\<cdot>(x :# xs) = [:x:]) &&& stake\<cdot>(numeral (num.Bit0 k))\<cdot>(x :# xs) = x :# stake\<cdot>(numeral (Num.BitM k))\<cdot>xs &&& stake\<cdot>(numeral (num.Bit1 k))\<cdot>(x :# xs) = x :# stake\<cdot>(numeral (num.Bit0 k))\<cdot>xs
[PROOF STEP]
by (cases "x = \<bottom>"; cases xs; simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+


[STATEMENT]
lemma stake_all:
  assumes "le\<cdot>(slength\<cdot>xs)\<cdot>i = TT"
  shows "stake\<cdot>i\<cdot>xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake\<cdot>i\<cdot>xs = xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
le\<cdot>(slength\<cdot>xs)\<cdot>i = TT

goal (1 subgoal):
 1. stake\<cdot>i\<cdot>xs = xs
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>\<bottom> = \<bottom>
 2. \<And>i. le\<cdot>(slength\<cdot>[::])\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>[::] = [::]
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. le\<cdot>(slength\<cdot>xs)\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>xs = xs; le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i = TT\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>(a :# xs) = a :# xs
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
le\<cdot>(slength\<cdot>xs)\<cdot>?i = TT \<Longrightarrow> stake\<cdot>?i\<cdot>xs = xs
le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i = TT

goal (3 subgoals):
 1. \<And>i. le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>\<bottom> = \<bottom>
 2. \<And>i. le\<cdot>(slength\<cdot>[::])\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>[::] = [::]
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. le\<cdot>(slength\<cdot>xs)\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>xs = xs; le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i = TT\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>(a :# xs) = a :# xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
le\<cdot>(slength\<cdot>xs)\<cdot>?i = TT \<Longrightarrow> stake\<cdot>?i\<cdot>xs = xs
le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i = TT
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
le\<cdot>(slength\<cdot>xs)\<cdot>?i = TT \<Longrightarrow> stake\<cdot>?i\<cdot>xs = xs
le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i = TT

goal (1 subgoal):
 1. stake\<cdot>i\<cdot>(x :# xs) = x :# xs
[PROOF STEP]
by (cases i; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits if_splits elim!: slengthE)
[PROOF STATE]
proof (state)
this:
stake\<cdot>i\<cdot>(x :# xs) = x :# xs

goal (2 subgoals):
 1. \<And>i. le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>\<bottom> = \<bottom>
 2. \<And>i. le\<cdot>(slength\<cdot>[::])\<cdot>i = TT \<Longrightarrow> stake\<cdot>i\<cdot>[::] = [::]
[PROOF STEP]
qed (simp_all add: le_defined)


[STATEMENT]
lemma stake_all_triv[simp]: "stake\<cdot>(slength\<cdot>xs)\<cdot>xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake\<cdot>(slength\<cdot>xs)\<cdot>xs = xs
[PROOF STEP]
by (cases "xs = \<bottom>") (auto simp: stake_all)


[STATEMENT]
lemma stake_append[simp]: "stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. stake\<cdot>i\<cdot>(\<bottom> :@ ys) = stake\<cdot>i\<cdot>\<bottom> :@ stake\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>i. stake\<cdot>i\<cdot>([::] :@ ys) = stake\<cdot>i\<cdot>[::] :@ stake\<cdot>(i - slength\<cdot>[::])\<cdot>ys
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>((a :# xs) :@ ys) = stake\<cdot>i\<cdot>(a :# xs) :@ stake\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
case (snil i)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>i. stake\<cdot>i\<cdot>(\<bottom> :@ ys) = stake\<cdot>i\<cdot>\<bottom> :@ stake\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>i. stake\<cdot>i\<cdot>([::] :@ ys) = stake\<cdot>i\<cdot>[::] :@ stake\<cdot>(i - slength\<cdot>[::])\<cdot>ys
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>((a :# xs) :@ ys) = stake\<cdot>i\<cdot>(a :# xs) :@ stake\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake\<cdot>i\<cdot>([::] :@ ys) = stake\<cdot>i\<cdot>[::] :@ stake\<cdot>(i - slength\<cdot>[::])\<cdot>ys
[PROOF STEP]
by (cases i; simp add: zero_Integer_def)
[PROOF STATE]
proof (state)
this:
stake\<cdot>i\<cdot>([::] :@ ys) = stake\<cdot>i\<cdot>[::] :@ stake\<cdot>(i - slength\<cdot>[::])\<cdot>ys

goal (2 subgoals):
 1. \<And>i. stake\<cdot>i\<cdot>(\<bottom> :@ ys) = stake\<cdot>i\<cdot>\<bottom> :@ stake\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>((a :# xs) :@ ys) = stake\<cdot>i\<cdot>(a :# xs) :@ stake\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. stake\<cdot>i\<cdot>(\<bottom> :@ ys) = stake\<cdot>i\<cdot>\<bottom> :@ stake\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>((a :# xs) :@ ys) = stake\<cdot>i\<cdot>(a :# xs) :@ stake\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
stake\<cdot>?i\<cdot>(xs :@ ys) = stake\<cdot>?i\<cdot>xs :@ stake\<cdot>(?i - slength\<cdot>xs)\<cdot>ys

goal (2 subgoals):
 1. \<And>i. stake\<cdot>i\<cdot>(\<bottom> :@ ys) = stake\<cdot>i\<cdot>\<bottom> :@ stake\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. stake\<cdot>i\<cdot>(xs :@ ys) = stake\<cdot>i\<cdot>xs :@ stake\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> stake\<cdot>i\<cdot>((a :# xs) :@ ys) = stake\<cdot>i\<cdot>(a :# xs) :@ stake\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
stake\<cdot>?i\<cdot>(xs :@ ys) = stake\<cdot>?i\<cdot>xs :@ stake\<cdot>(?i - slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
stake\<cdot>?i\<cdot>(xs :@ ys) = stake\<cdot>?i\<cdot>xs :@ stake\<cdot>(?i - slength\<cdot>xs)\<cdot>ys

goal (1 subgoal):
 1. stake\<cdot>i\<cdot>((x :# xs) :@ ys) = stake\<cdot>i\<cdot>(x :# xs) :@ stake\<cdot>(i - slength\<cdot>(x :# xs))\<cdot>ys
[PROOF STEP]
by (cases i; cases ys; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits  elim!: slengthE)
[PROOF STATE]
proof (state)
this:
stake\<cdot>i\<cdot>((x :# xs) :@ ys) = stake\<cdot>i\<cdot>(x :# xs) :@ stake\<cdot>(i - slength\<cdot>(x :# xs))\<cdot>ys

goal (1 subgoal):
 1. \<And>i. stake\<cdot>i\<cdot>(\<bottom> :@ ys) = stake\<cdot>i\<cdot>\<bottom> :@ stake\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sdrop_strict[simp]:
  "sdrop\<cdot>\<bottom> = \<bottom>"
  "sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>\<bottom> = \<bottom> &&& sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp+


[STATEMENT]
lemma sdrop_bottom_iff[simp]: "(sdrop\<cdot>i\<cdot>xs = \<bottom>) \<longleftrightarrow> (i = \<bottom> \<or> xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sdrop\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. (sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>) = (i = \<bottom> \<or> \<bottom> = \<bottom>)
 2. \<And>i. (sdrop\<cdot>i\<cdot>[::] = \<bottom>) = (i = \<bottom> \<or> [::] = \<bottom>)
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. (sdrop\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)\<rbrakk> \<Longrightarrow> (sdrop\<cdot>i\<cdot>(a :# xs) = \<bottom>) = (i = \<bottom> \<or> a :# xs = \<bottom>)
[PROOF STEP]
case (snil i)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>i. (sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>) = (i = \<bottom> \<or> \<bottom> = \<bottom>)
 2. \<And>i. (sdrop\<cdot>i\<cdot>[::] = \<bottom>) = (i = \<bottom> \<or> [::] = \<bottom>)
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. (sdrop\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)\<rbrakk> \<Longrightarrow> (sdrop\<cdot>i\<cdot>(a :# xs) = \<bottom>) = (i = \<bottom> \<or> a :# xs = \<bottom>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sdrop\<cdot>i\<cdot>[::] = \<bottom>) = (i = \<bottom> \<or> [::] = \<bottom>)
[PROOF STEP]
by (subst sdrop.unfold) (cases i; simp)
[PROOF STATE]
proof (state)
this:
(sdrop\<cdot>i\<cdot>[::] = \<bottom>) = (i = \<bottom> \<or> [::] = \<bottom>)

goal (2 subgoals):
 1. \<And>i. (sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>) = (i = \<bottom> \<or> \<bottom> = \<bottom>)
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. (sdrop\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)\<rbrakk> \<Longrightarrow> (sdrop\<cdot>i\<cdot>(a :# xs) = \<bottom>) = (i = \<bottom> \<or> a :# xs = \<bottom>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. (sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>) = (i = \<bottom> \<or> \<bottom> = \<bottom>)
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. (sdrop\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)\<rbrakk> \<Longrightarrow> (sdrop\<cdot>i\<cdot>(a :# xs) = \<bottom>) = (i = \<bottom> \<or> a :# xs = \<bottom>)
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
(sdrop\<cdot>?i\<cdot>xs = \<bottom>) = (?i = \<bottom> \<or> xs = \<bottom>)

goal (2 subgoals):
 1. \<And>i. (sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>) = (i = \<bottom> \<or> \<bottom> = \<bottom>)
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. (sdrop\<cdot>i\<cdot>xs = \<bottom>) = (i = \<bottom> \<or> xs = \<bottom>)\<rbrakk> \<Longrightarrow> (sdrop\<cdot>i\<cdot>(a :# xs) = \<bottom>) = (i = \<bottom> \<or> a :# xs = \<bottom>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
(sdrop\<cdot>?i\<cdot>xs = \<bottom>) = (?i = \<bottom> \<or> xs = \<bottom>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
(sdrop\<cdot>?i\<cdot>xs = \<bottom>) = (?i = \<bottom> \<or> xs = \<bottom>)

goal (1 subgoal):
 1. (sdrop\<cdot>i\<cdot>(x :# xs) = \<bottom>) = (i = \<bottom> \<or> x :# xs = \<bottom>)
[PROOF STEP]
by (subst sdrop.unfold) fastforce
[PROOF STATE]
proof (state)
this:
(sdrop\<cdot>i\<cdot>(x :# xs) = \<bottom>) = (i = \<bottom> \<or> x :# xs = \<bottom>)

goal (1 subgoal):
 1. \<And>i. (sdrop\<cdot>i\<cdot>\<bottom> = \<bottom>) = (i = \<bottom> \<or> \<bottom> = \<bottom>)
[PROOF STEP]
qed simp


[STATEMENT]
lemma sdrop_snil[simp]:
  assumes "i \<noteq> \<bottom>"
  shows "sdrop\<cdot>i\<cdot>[::] = [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>[::] = [::]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<noteq> \<bottom>

goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>[::] = [::]
[PROOF STEP]
by (subst sdrop.unfold; fastforce)


[STATEMENT]
lemma sdrop_snil_conv[simp]: "(sdrop\<cdot>i\<cdot>[::] = [::]) \<longleftrightarrow> (i \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sdrop\<cdot>i\<cdot>[::] = [::]) = (i \<noteq> \<bottom>)
[PROOF STEP]
by (subst sdrop.unfold; fastforce)


[STATEMENT]
lemma sdrop_0[simp]:
  "sdrop\<cdot>0\<cdot>xs = xs"
  "sdrop\<cdot>(MkI\<cdot>0)\<cdot>xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>0\<cdot>xs = xs &&& sdrop\<cdot>(MkI\<cdot>0)\<cdot>xs = xs
[PROOF STEP]
by (subst sdrop.simps, simp add: zero_Integer_def)+


[STATEMENT]
lemma sdrop_pos:
  "le\<cdot>i\<cdot>0 = FF \<Longrightarrow> sdrop\<cdot>i\<cdot>xs = (case xs of [::] \<Rightarrow> [::] | y :# ys \<Rightarrow> sdrop\<cdot>(i - 1)\<cdot>ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le\<cdot>i\<cdot>0 = FF \<Longrightarrow> sdrop\<cdot>i\<cdot>xs = (case xs of [::] \<Rightarrow> [::] | y :# ys \<Rightarrow> sdrop\<cdot>(i - 1)\<cdot>ys)
[PROOF STEP]
by (subst sdrop.simps, simp)


[STATEMENT]
lemma sdrop_neg:
  "le\<cdot>i\<cdot>0 = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le\<cdot>i\<cdot>0 = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>xs = xs
[PROOF STEP]
by (subst sdrop.simps, simp)


[STATEMENT]
lemma sdrop_numeral_scons[simp]:
  "x \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>1\<cdot>(x :# xs) = xs"
  "x \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(numeral (Num.Bit0 k))\<cdot>(x :# xs) = sdrop\<cdot>(numeral (Num.BitM k))\<cdot>xs"
  "x \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(numeral (Num.Bit1 k))\<cdot>(x :# xs) = sdrop\<cdot>(numeral (Num.Bit0 k))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>1\<cdot>(x :# xs) = xs) &&& (x \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(numeral (num.Bit0 k))\<cdot>(x :# xs) = sdrop\<cdot>(numeral (Num.BitM k))\<cdot>xs) &&& (x \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(numeral (num.Bit1 k))\<cdot>(x :# xs) = sdrop\<cdot>(numeral (num.Bit0 k))\<cdot>xs)
[PROOF STEP]
by (subst sdrop.simps,
    simp add: zero_Integer_def one_Integer_def numeral_Integer_eq; cases xs; simp)+


[STATEMENT]
lemma sdrop_sappend[simp]:
  "sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. sdrop\<cdot>i\<cdot>(\<bottom> :@ ys) = sdrop\<cdot>i\<cdot>\<bottom> :@ sdrop\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>i. sdrop\<cdot>i\<cdot>([::] :@ ys) = sdrop\<cdot>i\<cdot>[::] :@ sdrop\<cdot>(i - slength\<cdot>[::])\<cdot>ys
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>((a :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(a :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
case (snil i)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>i. sdrop\<cdot>i\<cdot>(\<bottom> :@ ys) = sdrop\<cdot>i\<cdot>\<bottom> :@ sdrop\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>i. sdrop\<cdot>i\<cdot>([::] :@ ys) = sdrop\<cdot>i\<cdot>[::] :@ sdrop\<cdot>(i - slength\<cdot>[::])\<cdot>ys
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>((a :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(a :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>([::] :@ ys) = sdrop\<cdot>i\<cdot>[::] :@ sdrop\<cdot>(i - slength\<cdot>[::])\<cdot>ys
[PROOF STEP]
by (cases i; simp add: zero_Integer_def)
[PROOF STATE]
proof (state)
this:
sdrop\<cdot>i\<cdot>([::] :@ ys) = sdrop\<cdot>i\<cdot>[::] :@ sdrop\<cdot>(i - slength\<cdot>[::])\<cdot>ys

goal (2 subgoals):
 1. \<And>i. sdrop\<cdot>i\<cdot>(\<bottom> :@ ys) = sdrop\<cdot>i\<cdot>\<bottom> :@ sdrop\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>((a :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(a :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. sdrop\<cdot>i\<cdot>(\<bottom> :@ ys) = sdrop\<cdot>i\<cdot>\<bottom> :@ sdrop\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>((a :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(a :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sdrop\<cdot>?i\<cdot>(xs :@ ys) = sdrop\<cdot>?i\<cdot>xs :@ sdrop\<cdot>(?i - slength\<cdot>xs)\<cdot>ys

goal (2 subgoals):
 1. \<And>i. sdrop\<cdot>i\<cdot>(\<bottom> :@ ys) = sdrop\<cdot>i\<cdot>\<bottom> :@ sdrop\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. sdrop\<cdot>i\<cdot>(xs :@ ys) = sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - slength\<cdot>xs)\<cdot>ys\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>((a :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(a :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(a :# xs))\<cdot>ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sdrop\<cdot>?i\<cdot>(xs :@ ys) = sdrop\<cdot>?i\<cdot>xs :@ sdrop\<cdot>(?i - slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sdrop\<cdot>?i\<cdot>(xs :@ ys) = sdrop\<cdot>?i\<cdot>xs :@ sdrop\<cdot>(?i - slength\<cdot>xs)\<cdot>ys

goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>((x :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(x :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(x :# xs))\<cdot>ys
[PROOF STEP]
by (cases "ys = \<bottom>"; cases "le\<cdot>i\<cdot>0"; cases i;
        clarsimp simp: zero_Integer_def one_Integer_def sdrop_neg sdrop_pos add.commute diff_diff_add
                split: if_splits elim!: slengthE)
[PROOF STATE]
proof (state)
this:
sdrop\<cdot>i\<cdot>((x :# xs) :@ ys) = sdrop\<cdot>i\<cdot>(x :# xs) :@ sdrop\<cdot>(i - slength\<cdot>(x :# xs))\<cdot>ys

goal (1 subgoal):
 1. \<And>i. sdrop\<cdot>i\<cdot>(\<bottom> :@ ys) = sdrop\<cdot>i\<cdot>\<bottom> :@ sdrop\<cdot>(i - slength\<cdot>\<bottom>)\<cdot>ys
[PROOF STEP]
qed simp


[STATEMENT]
lemma sdrop_all:
  assumes "le\<cdot>(slength\<cdot>xs)\<cdot>i = TT"
  shows "sdrop\<cdot>i\<cdot>xs = [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>xs = [::]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
le\<cdot>(slength\<cdot>xs)\<cdot>i = TT

goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>xs = [::]
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>\<bottom> = [::]
 2. \<And>i. le\<cdot>(slength\<cdot>[::])\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>[::] = [::]
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. le\<cdot>(slength\<cdot>xs)\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>xs = [::]; le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i = TT\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>(a :# xs) = [::]
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
le\<cdot>(slength\<cdot>xs)\<cdot>?i = TT \<Longrightarrow> sdrop\<cdot>?i\<cdot>xs = [::]
le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i = TT

goal (3 subgoals):
 1. \<And>i. le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>\<bottom> = [::]
 2. \<And>i. le\<cdot>(slength\<cdot>[::])\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>[::] = [::]
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. le\<cdot>(slength\<cdot>xs)\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>xs = [::]; le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i = TT\<rbrakk> \<Longrightarrow> sdrop\<cdot>i\<cdot>(a :# xs) = [::]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
le\<cdot>(slength\<cdot>xs)\<cdot>?i = TT \<Longrightarrow> sdrop\<cdot>?i\<cdot>xs = [::]
le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i = TT
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
le\<cdot>(slength\<cdot>xs)\<cdot>?i = TT \<Longrightarrow> sdrop\<cdot>?i\<cdot>xs = [::]
le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i = TT

goal (1 subgoal):
 1. sdrop\<cdot>i\<cdot>(x :# xs) = [::]
[PROOF STEP]
by (subst sdrop.unfold; cases i;
        clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits if_splits elim!: slengthE)
[PROOF STATE]
proof (state)
this:
sdrop\<cdot>i\<cdot>(x :# xs) = [::]

goal (2 subgoals):
 1. \<And>i. le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>\<bottom> = [::]
 2. \<And>i. le\<cdot>(slength\<cdot>[::])\<cdot>i = TT \<Longrightarrow> sdrop\<cdot>i\<cdot>[::] = [::]
[PROOF STEP]
qed (simp_all add: le_defined)


[STATEMENT]
lemma slength_sdrop[simp]:
  "slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>\<bottom>) = If le\<cdot>i\<cdot>0 then slength\<cdot>\<bottom> else If le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i then 0 else slength\<cdot>\<bottom> - i
 2. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>[::]) = If le\<cdot>i\<cdot>0 then slength\<cdot>[::] else If le\<cdot>(slength\<cdot>[::])\<cdot>i then 0 else slength\<cdot>[::] - i
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i\<rbrakk> \<Longrightarrow> slength\<cdot>(sdrop\<cdot>i\<cdot>(a :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(a :# xs) else If le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i then 0 else slength\<cdot>(a :# xs) - i
[PROOF STEP]
case (snil i)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>\<bottom>) = If le\<cdot>i\<cdot>0 then slength\<cdot>\<bottom> else If le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i then 0 else slength\<cdot>\<bottom> - i
 2. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>[::]) = If le\<cdot>i\<cdot>0 then slength\<cdot>[::] else If le\<cdot>(slength\<cdot>[::])\<cdot>i then 0 else slength\<cdot>[::] - i
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i\<rbrakk> \<Longrightarrow> slength\<cdot>(sdrop\<cdot>i\<cdot>(a :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(a :# xs) else If le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i then 0 else slength\<cdot>(a :# xs) - i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(sdrop\<cdot>i\<cdot>[::]) = If le\<cdot>i\<cdot>0 then slength\<cdot>[::] else If le\<cdot>(slength\<cdot>[::])\<cdot>i then 0 else slength\<cdot>[::] - i
[PROOF STEP]
by (cases i; simp add: zero_Integer_def)
[PROOF STATE]
proof (state)
this:
slength\<cdot>(sdrop\<cdot>i\<cdot>[::]) = If le\<cdot>i\<cdot>0 then slength\<cdot>[::] else If le\<cdot>(slength\<cdot>[::])\<cdot>i then 0 else slength\<cdot>[::] - i

goal (2 subgoals):
 1. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>\<bottom>) = If le\<cdot>i\<cdot>0 then slength\<cdot>\<bottom> else If le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i then 0 else slength\<cdot>\<bottom> - i
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i\<rbrakk> \<Longrightarrow> slength\<cdot>(sdrop\<cdot>i\<cdot>(a :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(a :# xs) else If le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i then 0 else slength\<cdot>(a :# xs) - i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>\<bottom>) = If le\<cdot>i\<cdot>0 then slength\<cdot>\<bottom> else If le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i then 0 else slength\<cdot>\<bottom> - i
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i\<rbrakk> \<Longrightarrow> slength\<cdot>(sdrop\<cdot>i\<cdot>(a :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(a :# xs) else If le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i then 0 else slength\<cdot>(a :# xs) - i
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
slength\<cdot>(sdrop\<cdot>?i\<cdot>xs) = If le\<cdot>?i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>?i then 0 else slength\<cdot>xs - ?i

goal (2 subgoals):
 1. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>\<bottom>) = If le\<cdot>i\<cdot>0 then slength\<cdot>\<bottom> else If le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i then 0 else slength\<cdot>\<bottom> - i
 2. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>xs) = If le\<cdot>i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>i then 0 else slength\<cdot>xs - i\<rbrakk> \<Longrightarrow> slength\<cdot>(sdrop\<cdot>i\<cdot>(a :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(a :# xs) else If le\<cdot>(slength\<cdot>(a :# xs))\<cdot>i then 0 else slength\<cdot>(a :# xs) - i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
slength\<cdot>(sdrop\<cdot>?i\<cdot>xs) = If le\<cdot>?i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>?i then 0 else slength\<cdot>xs - ?i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
slength\<cdot>(sdrop\<cdot>?i\<cdot>xs) = If le\<cdot>?i\<cdot>0 then slength\<cdot>xs else If le\<cdot>(slength\<cdot>xs)\<cdot>?i then 0 else slength\<cdot>xs - ?i

goal (1 subgoal):
 1. slength\<cdot>(sdrop\<cdot>i\<cdot>(x :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(x :# xs) else If le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i then 0 else slength\<cdot>(x :# xs) - i
[PROOF STEP]
by (subst sdrop.unfold; cases i; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE)
[PROOF STATE]
proof (state)
this:
slength\<cdot>(sdrop\<cdot>i\<cdot>(x :# xs)) = If le\<cdot>i\<cdot>0 then slength\<cdot>(x :# xs) else If le\<cdot>(slength\<cdot>(x :# xs))\<cdot>i then 0 else slength\<cdot>(x :# xs) - i

goal (1 subgoal):
 1. \<And>i. slength\<cdot>(sdrop\<cdot>i\<cdot>\<bottom>) = If le\<cdot>i\<cdot>0 then slength\<cdot>\<bottom> else If le\<cdot>(slength\<cdot>\<bottom>)\<cdot>i then 0 else slength\<cdot>\<bottom> - i
[PROOF STEP]
qed simp


[STATEMENT]
lemma sdrop_not_snilD:
  assumes "sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<noteq> [::]"
  assumes "xs \<noteq> \<bottom>"
  shows "lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<noteq> [::]
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]
[PROOF STEP]
proof(induct xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>\<bottom> \<noteq> [::]; \<bottom> \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>\<bottom>) = TT \<and> \<bottom> \<noteq> [::]
 2. \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>[::] \<noteq> [::]; [::] \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>[::]) = TT \<and> [::] \<noteq> [::]
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<noteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]; sdrop\<cdot>(MkI\<cdot>i)\<cdot>(a :# xs) \<noteq> [::]; a :# xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>(a :# xs)) = TT \<and> a :# xs \<noteq> [::]
[PROOF STEP]
case (scons x xs i)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
\<lbrakk>sdrop\<cdot>(MkI\<cdot>?i)\<cdot>xs \<noteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>?i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]
sdrop\<cdot>(MkI\<cdot>i)\<cdot>(x :# xs) \<noteq> [::]
x :# xs \<noteq> \<bottom>

goal (3 subgoals):
 1. \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>\<bottom> \<noteq> [::]; \<bottom> \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>\<bottom>) = TT \<and> \<bottom> \<noteq> [::]
 2. \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>[::] \<noteq> [::]; [::] \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>[::]) = TT \<and> [::] \<noteq> [::]
 3. \<And>a xs i. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<noteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]; sdrop\<cdot>(MkI\<cdot>i)\<cdot>(a :# xs) \<noteq> [::]; a :# xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>(a :# xs)) = TT \<and> a :# xs \<noteq> [::]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
\<lbrakk>sdrop\<cdot>(MkI\<cdot>?i)\<cdot>xs \<noteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>?i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]
sdrop\<cdot>(MkI\<cdot>i)\<cdot>(x :# xs) \<noteq> [::]
x :# xs \<noteq> \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
\<lbrakk>sdrop\<cdot>(MkI\<cdot>?i)\<cdot>xs \<noteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>?i)\<cdot>(slength\<cdot>xs) = TT \<and> xs \<noteq> [::]
sdrop\<cdot>(MkI\<cdot>i)\<cdot>(x :# xs) \<noteq> [::]
x :# xs \<noteq> \<bottom>

goal (1 subgoal):
 1. lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>(x :# xs)) = TT \<and> x :# xs \<noteq> [::]
[PROOF STEP]
by (subst (asm) (2) sdrop.unfold, clarsimp simp: zero_Integer_def one_Integer_def not_le sdrop_all elim!: slengthE)
[PROOF STATE]
proof (state)
this:
lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>(x :# xs)) = TT \<and> x :# xs \<noteq> [::]

goal (2 subgoals):
 1. \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>\<bottom> \<noteq> [::]; \<bottom> \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>\<bottom>) = TT \<and> \<bottom> \<noteq> [::]
 2. \<And>i. \<lbrakk>sdrop\<cdot>(MkI\<cdot>i)\<cdot>[::] \<noteq> [::]; [::] \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> lt\<cdot>(MkI\<cdot>i)\<cdot>(slength\<cdot>[::]) = TT \<and> [::] \<noteq> [::]
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sdrop_sappend_same:
  assumes "xs \<noteq> \<bottom>"
  shows "sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ys) = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ys) = ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ys) = ys
[PROOF STEP]
proof(induct xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ys. \<bottom> \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>\<bottom>)\<cdot>(\<bottom> :@ ys) = ys
 2. \<And>ys. [::] \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>[::])\<cdot>([::] :@ ys) = ys
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. xs \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ys) = ys; a :# xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>(a :# xs))\<cdot>((a :# xs) :@ ys) = ys
[PROOF STEP]
case (scons x xs ys)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
xs \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ?ys) = ?ys
x :# xs \<noteq> \<bottom>

goal (3 subgoals):
 1. \<And>ys. \<bottom> \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>\<bottom>)\<cdot>(\<bottom> :@ ys) = ys
 2. \<And>ys. [::] \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>[::])\<cdot>([::] :@ ys) = ys
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. xs \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ys) = ys; a :# xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>(a :# xs))\<cdot>((a :# xs) :@ ys) = ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
xs \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ?ys) = ?ys
x :# xs \<noteq> \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
xs \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>xs)\<cdot>(xs :@ ?ys) = ?ys
x :# xs \<noteq> \<bottom>

goal (1 subgoal):
 1. sdrop\<cdot>(slength\<cdot>(x :# xs))\<cdot>((x :# xs) :@ ys) = ys
[PROOF STEP]
by (cases "ys = \<bottom>"; subst sdrop.unfold; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE)
[PROOF STATE]
proof (state)
this:
sdrop\<cdot>(slength\<cdot>(x :# xs))\<cdot>((x :# xs) :@ ys) = ys

goal (2 subgoals):
 1. \<And>ys. \<bottom> \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>\<bottom>)\<cdot>(\<bottom> :@ ys) = ys
 2. \<And>ys. [::] \<noteq> \<bottom> \<Longrightarrow> sdrop\<cdot>(slength\<cdot>[::])\<cdot>([::] :@ ys) = ys
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sscanl_strict[simp]:
  "sscanl\<cdot>f\<cdot>\<bottom>\<cdot>xs = \<bottom>"
  "sscanl\<cdot>f\<cdot>z\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>\<bottom>\<cdot>xs = \<bottom> &&& sscanl\<cdot>f\<cdot>z\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (cases xs) fixrec_simp+


[STATEMENT]
lemma sscanl_cong:
  assumes "xs = xs'"
  assumes "z = z'"
  assumes "\<And>x z. x \<in> sset xs \<Longrightarrow> f\<cdot>z\<cdot>x = f'\<cdot>z\<cdot>x"
  shows "sscanl\<cdot>f\<cdot>z\<cdot>xs = sscanl\<cdot>f'\<cdot>z'\<cdot>xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>z\<cdot>xs = sscanl\<cdot>f'\<cdot>z'\<cdot>xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = xs'
z = z'
?x \<in> sset xs \<Longrightarrow> f\<cdot>?z\<cdot>?x = f'\<cdot>?z\<cdot>?x

goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>z\<cdot>xs = sscanl\<cdot>f'\<cdot>z'\<cdot>xs'
[PROOF STEP]
by (induct xs arbitrary: xs' z z') auto


[STATEMENT]
lemma sscanl_lfp_fusion':
  assumes "g\<cdot>\<bottom> = \<bottom>"
  assumes *: "\<And>acc x. x \<noteq> \<bottom> \<Longrightarrow> g\<cdot>(f\<cdot>acc\<cdot>x) = f'\<cdot>(g\<cdot>acc)\<cdot>x"
  shows "smap\<cdot>g\<cdot>(sscanl\<cdot>f\<cdot>z\<cdot>xs) = sscanl\<cdot>f'\<cdot>(g\<cdot>z)\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>g\<cdot>(sscanl\<cdot>f\<cdot>z\<cdot>xs) = sscanl\<cdot>f'\<cdot>(g\<cdot>z)\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g\<cdot>\<bottom> = \<bottom>
?x \<noteq> \<bottom> \<Longrightarrow> g\<cdot>(f\<cdot>?acc\<cdot>?x) = f'\<cdot>(g\<cdot>?acc)\<cdot>?x

goal (1 subgoal):
 1. smap\<cdot>g\<cdot>(sscanl\<cdot>f\<cdot>z\<cdot>xs) = sscanl\<cdot>f'\<cdot>(g\<cdot>z)\<cdot>xs
[PROOF STEP]
by (induct xs arbitrary: z) simp_all


[STATEMENT]
lemma sscanl_lfp_fusion:
  assumes "g\<cdot>\<bottom> = \<bottom>"
  assumes *: "\<And>acc x. x \<noteq> \<bottom> \<Longrightarrow> g\<cdot>(f\<cdot>acc\<cdot>x) = f'\<cdot>(g\<cdot>acc)\<cdot>x"
  shows "smap\<cdot>g oo sscanl\<cdot>f\<cdot>z = sscanl\<cdot>f'\<cdot>(g\<cdot>z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>g oo sscanl\<cdot>f\<cdot>z = sscanl\<cdot>f'\<cdot>(g\<cdot>z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g\<cdot>\<bottom> = \<bottom>
?x \<noteq> \<bottom> \<Longrightarrow> g\<cdot>(f\<cdot>?acc\<cdot>?x) = f'\<cdot>(g\<cdot>?acc)\<cdot>?x

goal (1 subgoal):
 1. smap\<cdot>g oo sscanl\<cdot>f\<cdot>z = sscanl\<cdot>f'\<cdot>(g\<cdot>z)
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff sscanl_lfp_fusion')


[STATEMENT]
lemma sscanl_ww_fusion': \<comment>\<open> Worker/wrapper @{cite [cite_macro=citep] "GillHutton:2009" and "Gammie:2011"} specialised to @{const \<open>sscanl\<close>} \<close>
  fixes wrap :: "'b \<rightarrow> 'a"
  fixes unwrap :: "'a \<rightarrow> 'b"
  fixes z :: "'a"
  fixes f :: "'a \<rightarrow> 'c \<rightarrow> 'a"
  fixes f' :: "'b \<rightarrow> 'c \<rightarrow> 'b"
  assumes ww: "wrap oo unwrap = ID"
  assumes wb: "\<And>z x. x \<noteq> \<bottom> \<Longrightarrow> unwrap\<cdot>(f\<cdot>(wrap\<cdot>z)\<cdot>x) = f'\<cdot>(unwrap\<cdot>(wrap\<cdot>z))\<cdot>x"
  shows "sscanl\<cdot>f\<cdot>z\<cdot>xs = smap\<cdot>wrap\<cdot>(sscanl\<cdot>f'\<cdot>(unwrap\<cdot>z)\<cdot>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>z\<cdot>xs = smap\<cdot>wrap\<cdot>(sscanl\<cdot>f'\<cdot>(unwrap\<cdot>z)\<cdot>xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wrap oo unwrap = ID
?x \<noteq> \<bottom> \<Longrightarrow> unwrap\<cdot>(f\<cdot>(wrap\<cdot>?z)\<cdot>?x) = f'\<cdot>(unwrap\<cdot>(wrap\<cdot>?z))\<cdot>?x

goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>z\<cdot>xs = smap\<cdot>wrap\<cdot>(sscanl\<cdot>f'\<cdot>(unwrap\<cdot>z)\<cdot>xs)
[PROOF STEP]
by (induct xs arbitrary: z) (simp add: cfun_eq_iff retraction_cfcomp_strict | metis)+


[STATEMENT]
lemma sscanl_ww_fusion: \<comment>\<open> Worker/wrapper @{cite [cite_macro=citep] "GillHutton:2009" and "Gammie:2011"} specialised to @{const \<open>sscanl\<close>} \<close>
  fixes wrap :: "'b \<rightarrow> 'a"
  fixes unwrap :: "'a \<rightarrow> 'b"
  fixes z :: "'a"
  fixes f :: "'a \<rightarrow> 'c \<rightarrow> 'a"
  fixes f' :: "'b \<rightarrow> 'c \<rightarrow> 'b"
  assumes ww: "wrap oo unwrap = ID"
  assumes wb: "\<And>z x. x \<noteq> \<bottom> \<Longrightarrow> unwrap\<cdot>(f\<cdot>(wrap\<cdot>z)\<cdot>x) = f'\<cdot>(unwrap\<cdot>(wrap\<cdot>z))\<cdot>x"
  shows "sscanl\<cdot>f\<cdot>z = smap\<cdot>wrap oo sscanl\<cdot>f'\<cdot>(unwrap\<cdot>z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>z = smap\<cdot>wrap oo sscanl\<cdot>f'\<cdot>(unwrap\<cdot>z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wrap oo unwrap = ID
?x \<noteq> \<bottom> \<Longrightarrow> unwrap\<cdot>(f\<cdot>(wrap\<cdot>?z)\<cdot>?x) = f'\<cdot>(unwrap\<cdot>(wrap\<cdot>?z))\<cdot>?x

goal (1 subgoal):
 1. sscanl\<cdot>f\<cdot>z = smap\<cdot>wrap oo sscanl\<cdot>f'\<cdot>(unwrap\<cdot>z)
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff sscanl_ww_fusion')


[STATEMENT]
lemma sinits_strict[simp]: "sinits\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinits\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma sinits_bottom_iff[simp]: "(sinits\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinits\<cdot>xs = \<bottom>) = (xs = \<bottom>)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sinits_not_snil[iff]: "sinits\<cdot>xs \<noteq> [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinits\<cdot>xs \<noteq> [::]
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma sinits_empty_bottom[simp]: "(sset (sinits\<cdot>xs) = {}) \<longleftrightarrow> (xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sset (sinits\<cdot>xs) = {}) = (xs = \<bottom>)
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma sinits_scons[simp]: "sinits\<cdot>(x :# xs) = [::] :# smap\<cdot>(x :#)\<cdot>(sinits\<cdot>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinits\<cdot>(x :# xs) = [::] :# smap\<cdot>(x:#)\<cdot>(sinits\<cdot>xs)
[PROOF STEP]
by (cases "x = \<bottom>", force) (induct xs; force)


[STATEMENT]
lemma sinits_length[simp]: "slength\<cdot>(sinits\<cdot>xs) = slength\<cdot>xs + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(sinits\<cdot>xs) = slength\<cdot>xs + 1
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sinits_snoc[simp]: "sinits\<cdot>(xs :@ [:x:]) = sinits\<cdot>xs :@ [:xs :@ [:x:]:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinits\<cdot>(xs :@ [:x:]) = sinits\<cdot>xs :@ [:xs :@ [:x:]:]
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sinits_foldr': \<comment>\<open> @{cite [cite_macro=citet] \<open>p30\<close> "Bird:1987"} \<close>
  shows "sinits\<cdot>xs = sfoldr\<cdot>(\<Lambda> x xs. [:[::]:] :@ smap\<cdot>(x :#)\<cdot>xs)\<cdot>[:[::]:]\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinits\<cdot>xs = sfoldr\<cdot>(\<Lambda> x xs. [:[::]:] :@ smap\<cdot>(x:#)\<cdot>xs)\<cdot>[:[::]:]\<cdot>xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sinits_sscanl':
  shows "smap\<cdot>(sfoldl\<cdot>f\<cdot>z)\<cdot>(sinits\<cdot>xs) = sscanl\<cdot>f\<cdot>z\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>(sfoldl\<cdot>f\<cdot>z)\<cdot>(sinits\<cdot>xs) = sscanl\<cdot>f\<cdot>z\<cdot>xs
[PROOF STEP]
by (induct xs arbitrary: z) (simp_all cong: smap_cong add: oo_def eta_cfun)


[STATEMENT]
lemma sinits_sscanl: \<comment>\<open> @{cite [cite_macro=citet] \<open>Lemma~5\<close> "Bird:1987"}, @{cite [cite_macro=citet] \<open>p118 ``the scan lemma''\<close> "Bird:PearlsofFAD:2010"} \<close>
  shows "smap\<cdot>(sfoldl\<cdot>f\<cdot>z) oo sinits = sscanl\<cdot>f\<cdot>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>(sfoldl\<cdot>f\<cdot>z) oo sinits = sscanl\<cdot>f\<cdot>z
[PROOF STEP]
by (simp add: sinits_sscanl' cfun_eq_iff)


[STATEMENT]
lemma sinits_all[simp]: "(xs \<in> sset (sinits\<cdot>xs)) \<longleftrightarrow> (xs \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<in> sset (sinits\<cdot>xs)) = (xs \<noteq> \<bottom>)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma stails_strict[simp]: "stails\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma stails_bottom_iff[simp]: "(stails\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stails\<cdot>xs = \<bottom>) = (xs = \<bottom>)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma stails_not_snil[iff]: "stails\<cdot>xs \<noteq> [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails\<cdot>xs \<noteq> [::]
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma stails_scons[simp]: "stails\<cdot>(x :# xs) = (x :# xs) :# stails\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails\<cdot>(x :# xs) = (x :# xs) :# stails\<cdot>xs
[PROOF STEP]
by (induct xs) (cases "x = \<bottom>"; simp)+


[STATEMENT]
lemma stails_slength[simp]: "slength\<cdot>(stails\<cdot>xs) = slength\<cdot>xs + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(stails\<cdot>xs) = slength\<cdot>xs + 1
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma stails_snoc[simp]:
  shows "stails\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> ys. ys :@ [:x:])\<cdot>(stails\<cdot>xs) :@ [:[::]:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> ys. ys :@ [:x:])\<cdot>(stails\<cdot>xs) :@ [:[::]:]
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma stails_sfoldl':
  shows "stails\<cdot>xs = sfoldl\<cdot>(\<Lambda> xs x. smap\<cdot>(\<Lambda> ys. ys :@ [:x:])\<cdot>xs :@ [:[::]:])\<cdot>[:[::]:]\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails\<cdot>xs = sfoldl\<cdot>(\<Lambda> xs x. smap\<cdot>(\<Lambda> ys. ys :@ [:x:])\<cdot>xs :@ [:[::]:])\<cdot>[:[::]:]\<cdot>xs
[PROOF STEP]
by (induct xs rule: srev_induct) simp_all


[STATEMENT]
lemma stails_sfoldl:
  shows "stails = sfoldl\<cdot>(\<Lambda> xs x. smap\<cdot>(\<Lambda> ys. ys :@ [:x:])\<cdot>xs :@ [:[::]:])\<cdot>[:[::]:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails = sfoldl\<cdot>(\<Lambda> xs x. smap\<cdot>(\<Lambda> ys. ys :@ [:x:])\<cdot>xs :@ [:[::]:])\<cdot>[:[::]:]
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff stails_sfoldl')


[STATEMENT]
lemma selem_strict[simp]: "selem\<cdot>x\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selem\<cdot>x\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma selem_bottom_iff[simp]: "(selem\<cdot>x\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> (xs \<noteq> [::] \<and> x = \<bottom>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (selem\<cdot>x\<cdot>xs = \<bottom>) = (xs = \<bottom> \<or> xs \<noteq> [::] \<and> x = \<bottom>)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma selem_sappend[simp]:
  assumes "ys \<noteq> \<bottom>"
  shows "selem\<cdot>x\<cdot>(xs :@ ys) = (selem\<cdot>x\<cdot>xs orelse selem\<cdot>x\<cdot>ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selem\<cdot>x\<cdot>(xs :@ ys) = (selem\<cdot>x\<cdot>xs orelse selem\<cdot>x\<cdot>ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> \<bottom>

goal (1 subgoal):
 1. selem\<cdot>x\<cdot>(xs :@ ys) = (selem\<cdot>x\<cdot>xs orelse selem\<cdot>x\<cdot>ys)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma elem_TT[simp]: "(selem\<cdot>x\<cdot>xs = TT) \<longleftrightarrow> (x \<in> sset xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (selem\<cdot>x\<cdot>xs = TT) = (x \<in> sset xs)
[PROOF STEP]
by (induct xs; auto) (metis sset_defined)+


[STATEMENT]
lemma elem_FF[simp]: "(selem\<cdot>x\<cdot>xs = FF) \<longleftrightarrow> (xs = [::] \<or> (x \<noteq> \<bottom> \<and> xs \<noteq> \<bottom> \<and> x \<notin> sset xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (selem\<cdot>x\<cdot>xs = FF) = (xs = [::] \<or> x \<noteq> \<bottom> \<and> xs \<noteq> \<bottom> \<and> x \<notin> sset xs)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma selem_snil_stails[iff]:
  assumes "xs \<noteq> \<bottom>"
  shows "selem\<cdot>[::]\<cdot>(stails\<cdot>xs) = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. selem\<cdot>[::]\<cdot>(stails\<cdot>xs) = TT
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. selem\<cdot>[::]\<cdot>(stails\<cdot>xs) = TT
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sconcatMap_strict[simp]: "sconcatMap\<cdot>f\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcatMap\<cdot>f\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma sconcatMap_snil[simp]: "sconcatMap\<cdot>f\<cdot>[::] = [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcatMap\<cdot>f\<cdot>[::] = [::]
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma sconcatMap_scons[simp]: "x \<noteq> \<bottom> \<Longrightarrow> sconcatMap\<cdot>f\<cdot>(x :# xs) = f\<cdot>x :@ sconcatMap\<cdot>f\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> \<bottom> \<Longrightarrow> sconcatMap\<cdot>f\<cdot>(x :# xs) = f\<cdot>x :@ sconcatMap\<cdot>f\<cdot>xs
[PROOF STEP]
by (cases "xs = \<bottom>"; simp add: sconcatMap.unfold)


[STATEMENT]
lemma sconcatMap_bottom_iff[simp]: "(sconcatMap\<cdot>f\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> (\<exists>x\<in>sset xs. f\<cdot>x = \<bottom>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sconcatMap\<cdot>f\<cdot>xs = \<bottom>) = (xs = \<bottom> \<or> (\<exists>x\<in>sset xs. f\<cdot>x = \<bottom>))
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sconcatMap_sappend[simp]: "sconcatMap\<cdot>f\<cdot>(xs :@ ys) = sconcatMap\<cdot>f\<cdot>xs :@ sconcatMap\<cdot>f\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcatMap\<cdot>f\<cdot>(xs :@ ys) = sconcatMap\<cdot>f\<cdot>xs :@ sconcatMap\<cdot>f\<cdot>ys
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sconcatMap_monad_laws:
  "sconcatMap\<cdot>(\<Lambda> x. [:x:])\<cdot>xs = xs"
  "sconcatMap\<cdot>g\<cdot>(sconcatMap\<cdot>f\<cdot>xs) = sconcatMap\<cdot>(\<Lambda> x. sconcatMap\<cdot>g\<cdot>(f\<cdot>x))\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcatMap\<cdot>(:#[::])\<cdot>xs = xs &&& sconcatMap\<cdot>g\<cdot>(sconcatMap\<cdot>f\<cdot>xs) = sconcatMap\<cdot>(\<Lambda> x. sconcatMap\<cdot>g\<cdot>(f\<cdot>x))\<cdot>xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma upto_strict[simp]:
  "supto\<cdot>\<bottom> = \<bottom>"
  "supto\<cdot>m\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supto\<cdot>\<bottom> = \<bottom> &&& supto\<cdot>m\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp+


[STATEMENT]
lemma supto_is_snil_conv[simp]:
  "(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = [::]) \<longleftrightarrow> (j < i)"
  "([::] = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) \<longleftrightarrow> (j < i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = [::]) = (j < i) &&& ([::] = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = (j < i)
[PROOF STEP]
by (subst supto.unfold; simp)+


[STATEMENT]
lemma supto_simp[simp]:
  "j < i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = [::]"
  "i \<le> j \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>i+1)\<cdot>(MkI\<cdot>j)"
  "supto\<cdot>0\<cdot>0 = [:0:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (j < i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = [::]) &&& (i \<le> j \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>i + 1)\<cdot>(MkI\<cdot>j)) &&& supto\<cdot>0\<cdot>0 = [:0:]
[PROOF STEP]
by (subst supto.simps, simp)+


[STATEMENT]
lemma supto_defined[simp]: "supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>" (is "?P i j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
proof (cases "j - i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
assume "j - i = int d"
[PROOF STATE]
proof (state)
this:
j - i = int d

goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j - i = int d
[PROOF STEP]
show "?P i j"
[PROOF STATE]
proof (prove)
using this:
j - i = int d

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
proof (induct d arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>; j - i = int (Suc d)\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
case (Suc d i j)
[PROOF STATE]
proof (state)
this:
?j - ?i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) \<noteq> \<bottom>
j - i = int (Suc d)

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>; j - i = int (Suc d)\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j - ?i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) \<noteq> \<bottom>
j - i = int (Suc d)
[PROOF STEP]
have "j - (i + 1) = int d" and le: "i \<le> j"
[PROOF STATE]
proof (prove)
using this:
?j - ?i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) \<noteq> \<bottom>
j - i = int (Suc d)

goal (1 subgoal):
 1. j - (i + 1) = int d &&& i \<le> j
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
j - (i + 1) = int d
i \<le> j

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>; j - i = int (Suc d)\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
from Suc(1)[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
have IH: "?P (i+1) j"
[PROOF STATE]
proof (prove)
using this:
supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>; j - i = int (Suc d)\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
i \<le> j

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
qed (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
assume "j - i = - int d"
[PROOF STATE]
proof (state)
this:
j - i = - int d

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j - i = - int d
[PROOF STEP]
have "j \<le> i"
[PROOF STATE]
proof (prove)
using this:
j - i = - int d

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

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
assume "j = i"
[PROOF STATE]
proof (state)
this:
j = i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j = i
[PROOF STEP]
have "?P i j"
[PROOF STATE]
proof (prove)
using this:
j = i

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
assume "j < i"
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < i
[PROOF STEP]
have "?P i j"
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
j = i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
j < i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<le> i
j = i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
j < i \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) \<noteq> \<bottom>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supto_bottom_iff[simp]:
  "(supto\<cdot>i\<cdot>j = \<bottom>) \<longleftrightarrow> (i = \<bottom> \<or> j = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (supto\<cdot>i\<cdot>j = \<bottom>) = (i = \<bottom> \<or> j = \<bottom>)
[PROOF STEP]
by (cases i; simp; cases j; simp)


[STATEMENT]
lemma supto_snoc[simp]:
  "i \<le> j \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j-1) :@ [:MkI\<cdot>j:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
proof(induct "nat(j - i)" arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>0 = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
 2. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]; Suc x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = nat (j - i)
i \<le> j

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>0 = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
 2. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]; Suc x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = nat (j - i)
i \<le> j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 = nat (j - i)
i \<le> j

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]

goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]; Suc x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]; Suc x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
case (Suc k i j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k = nat (?j - ?i); ?i \<le> ?j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j - 1) :@ [:MkI\<cdot>?j:]
Suc k = nat (j - i)
i \<le> j

goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]; Suc x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>k = nat (?j - ?i); ?i \<le> ?j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j - 1) :@ [:MkI\<cdot>?j:]
Suc k = nat (j - i)
i \<le> j
[PROOF STEP]
have "k = nat (j - (i + 1))" "i < j"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k = nat (?j - ?i); ?i \<le> ?j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j - 1) :@ [:MkI\<cdot>?j:]
Suc k = nat (j - i)
i \<le> j

goal (1 subgoal):
 1. k = nat (j - (i + 1)) &&& i < j
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
k = nat (j - (i + 1))
i < j

goal (1 subgoal):
 1. \<And>x i j. \<lbrakk>\<And>i j. \<lbrakk>x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]; Suc x = nat (j - i); i \<le> j\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3)
[PROOF STATE]
proof (chain)
picking this:
i < j
i + 1 \<le> j \<Longrightarrow> supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
Suc k = nat (j - i)
i \<le> j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < j
i + 1 \<le> j \<Longrightarrow> supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
Suc k = nat (j - i)
i \<le> j

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j - 1) :@ [:MkI\<cdot>j:]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma slength_supto[simp]: "slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)" (is "?P i j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
proof (cases "j - i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
assume "j - i = int d"
[PROOF STATE]
proof (state)
this:
j - i = int d

goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j - i = int d
[PROOF STEP]
show "?P i j"
[PROOF STATE]
proof (prove)
using this:
j - i = int d

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
proof (induct d arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1); j - i = int (Suc d)\<rbrakk> \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
case (Suc d i j)
[PROOF STATE]
proof (state)
this:
?j - ?i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j)) = MkI\<cdot>(if ?j < ?i then 0 else ?j - ?i + 1)
j - i = int (Suc d)

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1); j - i = int (Suc d)\<rbrakk> \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j - ?i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j)) = MkI\<cdot>(if ?j < ?i then 0 else ?j - ?i + 1)
j - i = int (Suc d)
[PROOF STEP]
have "j - (i + 1) = int d" and le: "i \<le> j"
[PROOF STATE]
proof (prove)
using this:
?j - ?i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j)) = MkI\<cdot>(if ?j < ?i then 0 else ?j - ?i + 1)
j - i = int (Suc d)

goal (1 subgoal):
 1. j - (i + 1) = int d &&& i \<le> j
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
j - (i + 1) = int d
i \<le> j

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1); j - i = int (Suc d)\<rbrakk> \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
from Suc(1)[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)
[PROOF STEP]
have IH: "?P (i+1) j"
[PROOF STATE]
proof (prove)
using this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
 2. \<And>d i j. \<lbrakk>\<And>i j. j - i = int d \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1); j - i = int (Suc d)\<rbrakk> \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i + 1 then 0 else j - (i + 1) + 1)
i \<le> j

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
qed (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
assume "j - i = - int d"
[PROOF STATE]
proof (state)
this:
j - i = - int d

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j - i = - int d
[PROOF STEP]
have "j \<le> i"
[PROOF STATE]
proof (prove)
using this:
j - i = - int d

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

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
assume "j = i"
[PROOF STATE]
proof (state)
this:
j = i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j = i
[PROOF STEP]
have "?P i j"
[PROOF STATE]
proof (prove)
using this:
j = i

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j = i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
assume "j < i"
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < i
[PROOF STEP]
have "?P i j"
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
j = i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
j < i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<le> i
j = i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
j < i \<Longrightarrow> slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal (1 subgoal):
 1. slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
slength\<cdot>(supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = MkI\<cdot>(if j < i then 0 else j - i + 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sset_supto[simp]:
  "sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}" (is "sset (?u i j) = ?R i j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
proof (cases "j - i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
case (nonneg k)
[PROOF STATE]
proof (state)
this:
j - i = int k

goal (2 subgoals):
 1. \<And>n. j - i = int n \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>n. j - i = - int (Suc n) \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j - i = int k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j - i = int k

goal (1 subgoal):
 1. sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
proof (induct k arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?j - ?i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j)) = {MkI\<cdot>k |k. ?i \<le> k \<and> k \<le> ?j}
j - i = int (Suc k)

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?j - ?i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j)) = {MkI\<cdot>k |k. ?i \<le> k \<and> k \<le> ?j}
j - i = int (Suc k)
[PROOF STEP]
have *: "j - (i + 1) = int k"
[PROOF STATE]
proof (prove)
using this:
?j - ?i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j)) = {MkI\<cdot>k |k. ?i \<le> k \<and> k \<le> ?j}
j - i = int (Suc k)

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

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
from Suc(1)[OF *]
[PROOF STATE]
proof (chain)
picking this:
sset (supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}
[PROOF STEP]
have IH: "sset (?u (i+1) j) = ?R (i+1) j"
[PROOF STATE]
proof (prove)
using this:
sset (supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}

goal (1 subgoal):
 1. sset (supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sset (supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
j - (i + 1) = int k
[PROOF STEP]
have "i \<le> j"
[PROOF STATE]
proof (prove)
using this:
j - (i + 1) = int k

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

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
have "sset (?u i j) = sset (MkI\<cdot>i :# ?u (i+1) j)"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = sset (MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j))
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = sset (MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j))

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = sset (MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j))

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
have "\<dots> = insert (MkI\<cdot>i) (?R (i+1) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = insert (MkI\<cdot>i) {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}
[PROOF STEP]
by (simp add: IH)
[PROOF STATE]
proof (state)
this:
sset (MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = insert (MkI\<cdot>i) {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sset (MkI\<cdot>i :# supto\<cdot>(MkI\<cdot>(i + 1))\<cdot>(MkI\<cdot>j)) = insert (MkI\<cdot>i) {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j}

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
have "\<dots> = ?R i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (MkI\<cdot>i) {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j} = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
using \<open>i \<le> j\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. insert (MkI\<cdot>i) {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j} = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (MkI\<cdot>i) {MkI\<cdot>k |k. i + 1 \<le> k \<and> k \<le> j} = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}

goal (2 subgoals):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
 2. \<And>k i j. \<lbrakk>\<And>i j. j - i = int k \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}; j - i = int (Suc k)\<rbrakk> \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}

goal (1 subgoal):
 1. sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}

goal (1 subgoal):
 1. \<And>i j. j - i = int 0 \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
qed (force simp: one_Integer_def)
[PROOF STATE]
proof (state)
this:
sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}

goal (1 subgoal):
 1. \<And>n. j - i = - int (Suc n) \<Longrightarrow> sset (supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j)) = {MkI\<cdot>k |k. i \<le> k \<and> k \<le> j}
[PROOF STEP]
qed simp