[STATEMENT]
lemma subseq_of_length_Suc_upt:
  "subseq_of_length (Suc n) [0..<m] xs \<longleftrightarrow>
   (if n = 0 then length xs = Suc 0 \<and> hd xs < m
    else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
proof(cases "n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
 2. \<And>nat. n = Suc nat \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
 2. \<And>nat. n = Suc nat \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
proof(intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
assume l: "?l"
[PROOF STATE]
proof (state)
this:
subseq_of_length (Suc n) [0..<m] xs

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with 0
[PROOF STATE]
proof (chain)
picking this:
n = 0
subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
have 1: "length xs = Suc 0"
[PROOF STATE]
proof (prove)
using this:
n = 0
subseq_of_length (Suc n) [0..<m] xs

goal (1 subgoal):
 1. length xs = Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs = Suc 0

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = Suc 0
[PROOF STEP]
have xs: "xs = [hd xs]"
[PROOF STATE]
proof (prove)
using this:
length xs = Suc 0

goal (1 subgoal):
 1. xs = [hd xs]
[PROOF STEP]
by (metis length_0_conv length_Suc_conv list.sel(1))
[PROOF STATE]
proof (state)
this:
xs = [hd xs]

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with l
[PROOF STATE]
proof (chain)
picking this:
subseq_of_length (Suc n) [0..<m] xs
xs = [hd xs]
[PROOF STEP]
have "[hd xs] \<in> set (subseqs [0..<m])"
[PROOF STATE]
proof (prove)
using this:
subseq_of_length (Suc n) [0..<m] xs
xs = [hd xs]

goal (1 subgoal):
 1. [hd xs] \<in> set (subseqs [0..<m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[hd xs] \<in> set (subseqs [0..<m])

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
length xs = Suc 0
[hd xs] \<in> set (subseqs [0..<m])
[PROOF STEP]
show "?r"
[PROOF STATE]
proof (prove)
using this:
length xs = Suc 0
[hd xs] \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
[PROOF STEP]
by (unfold 0, auto)
[PROOF STATE]
proof (state)
this:
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
assume ?r
[PROOF STATE]
proof (state)
this:
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with 0
[PROOF STATE]
proof (chain)
picking this:
n = 0
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
[PROOF STEP]
have 1: "length xs = Suc 0" and 2: "hd xs < m"
[PROOF STATE]
proof (prove)
using this:
n = 0
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)

goal (1 subgoal):
 1. length xs = Suc 0 &&& hd xs < m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs = Suc 0
hd xs < m

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = Suc 0
hd xs < m
[PROOF STEP]
have xs: "xs = [hd xs]"
[PROOF STATE]
proof (prove)
using this:
length xs = Suc 0
hd xs < m

goal (1 subgoal):
 1. xs = [hd xs]
[PROOF STEP]
by (metis length_0_conv length_Suc_conv list.sel(1))
[PROOF STATE]
proof (state)
this:
xs = [hd xs]

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
hd xs < m
[PROOF STEP]
show "?l"
[PROOF STATE]
proof (prove)
using this:
hd xs < m

goal (1 subgoal):
 1. subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
by (subst xs, auto simp: 0)
[PROOF STATE]
proof (state)
this:
subseq_of_length (Suc n) [0..<m] xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
case n: (Suc n')
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
assume "?l"
[PROOF STATE]
proof (state)
this:
subseq_of_length (Suc n) [0..<m] xs

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
have 1: "length xs = Suc (Suc n')" and 2: "xs \<in> set (subseqs [0..<m])"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'
subseq_of_length (Suc n) [0..<m] xs

goal (1 subgoal):
 1. length xs = Suc (Suc n') &&& xs \<in> set (subseqs [0..<m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs = Suc (Suc n')
xs \<in> set (subseqs [0..<m])

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from 1[unfolded length_Suc_conv]
[PROOF STATE]
proof (chain)
picking this:
\<exists>y ys. xs = y # ys \<and> (\<exists>y ysa. ys = y # ysa \<and> length ysa = n')
[PROOF STEP]
obtain x y ys where xs: "xs = x#y#ys" and n': "length ys = n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>y ys. xs = y # ys \<and> (\<exists>y ysa. ys = y # ysa \<and> length ysa = n')

goal (1 subgoal):
 1. (\<And>x y ys. \<lbrakk>xs = x # y # ys; length ys = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs = x # y # ys
length ys = n'

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
have "sorted xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted xs
[PROOF STEP]
by(rule sorted_subseqs_sorted[OF _ 2], auto)
[PROOF STATE]
proof (state)
this:
sorted xs

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from this[unfolded xs]
[PROOF STATE]
proof (chain)
picking this:
sorted (x # y # ys)
[PROOF STEP]
have "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
sorted (x # y # ys)

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

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
xs \<in> set (subseqs [0..<m])
[PROOF STEP]
have "distinct xs"
[PROOF STATE]
proof (prove)
using this:
xs \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
by (rule subseqs_distinctD, auto)
[PROOF STATE]
proof (state)
this:
distinct xs

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from this[unfolded xs]
[PROOF STATE]
proof (chain)
picking this:
distinct (x # y # ys)
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
distinct (x # y # ys)

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

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<le> y
x \<noteq> y
[PROOF STEP]
have "x < y"
[PROOF STATE]
proof (prove)
using this:
x \<le> y
x \<noteq> y

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

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x < y

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
xs \<in> set (subseqs [0..<m])
[PROOF STEP]
have "y#ys \<in> set (subseqs [0..<m])"
[PROOF STATE]
proof (prove)
using this:
xs \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. y # ys \<in> set (subseqs [0..<m])
[PROOF STEP]
by (unfold xs, auto dest: Cons_in_subseqsD)
[PROOF STATE]
proof (state)
this:
y # ys \<in> set (subseqs [0..<m])

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with n n'
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
length ys = n'
y # ys \<in> set (subseqs [0..<m])
[PROOF STEP]
have "subseq_of_length n [0..<m] (y#ys)"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'
length ys = n'
y # ys \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. subseq_of_length n [0..<m] (y # ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subseq_of_length n [0..<m] (y # ys)

goal (2 subgoals):
 1. subseq_of_length (Suc n) [0..<m] xs \<Longrightarrow> if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
 2. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x < y
subseq_of_length n [0..<m] (y # ys)
[PROOF STEP]
show ?r
[PROOF STATE]
proof (prove)
using this:
x < y
subseq_of_length n [0..<m] (y # ys)

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
[PROOF STEP]
by (auto simp: xs)
[PROOF STATE]
proof (state)
this:
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
assume r: "?r"
[PROOF STATE]
proof (state)
this:
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)
[PROOF STEP]
have len: "length xs = Suc (Suc n')"
     and *: "hd xs < hd (tl xs)" "tl xs \<in> set (subseqs [0..<m])"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'
if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs)

goal (1 subgoal):
 1. length xs = Suc (Suc n') &&& hd xs < hd (tl xs) &&& tl xs \<in> set (subseqs [0..<m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs = Suc (Suc n')
hd xs < hd (tl xs)
tl xs \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from len[unfolded length_Suc_conv]
[PROOF STATE]
proof (chain)
picking this:
\<exists>y ys. xs = y # ys \<and> (\<exists>y ysa. ys = y # ysa \<and> length ysa = n')
[PROOF STEP]
obtain x y ys
    where xs: "xs = x#y#ys" and n': "length ys = n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>y ys. xs = y # ys \<and> (\<exists>y ysa. ys = y # ysa \<and> length ysa = n')

goal (1 subgoal):
 1. (\<And>x y ys. \<lbrakk>xs = x # y # ys; length ys = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs = x # y # ys
length ys = n'

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
hd xs < hd (tl xs)
tl xs \<in> set (subseqs [0..<m])
xs = x # y # ys
length ys = n'
[PROOF STEP]
have xy: "x < y" and yys: "y#ys \<in> set (subseqs [0..<m])"
[PROOF STATE]
proof (prove)
using this:
hd xs < hd (tl xs)
tl xs \<in> set (subseqs [0..<m])
xs = x # y # ys
length ys = n'

goal (1 subgoal):
 1. x < y &&& y # ys \<in> set (subseqs [0..<m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y
y # ys \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from Cons_mem_set_subseqs_sorted[OF _ yys]
[PROOF STATE]
proof (chain)
picking this:
sorted [0..<m] \<Longrightarrow> y # ys \<in> set (subseqs (filter ((\<le>) y) [0..<m]))
[PROOF STEP]
have "y#ys \<in> set (subseqs (filter ((\<le>) y) [0..<m]))"
[PROOF STATE]
proof (prove)
using this:
sorted [0..<m] \<Longrightarrow> y # ys \<in> set (subseqs (filter ((\<le>) y) [0..<m]))

goal (1 subgoal):
 1. y # ys \<in> set (subseqs (filter ((\<le>) y) [0..<m]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y # ys \<in> set (subseqs (filter ((\<le>) y) [0..<m]))

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y # ys \<in> set (subseqs (filter ((\<le>) y) [0..<m]))

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from Cons_mem_set_subseqsD[OF yys]
[PROOF STATE]
proof (chain)
picking this:
y \<in> set [0..<m]
[PROOF STEP]
have ym: "y < m"
[PROOF STATE]
proof (prove)
using this:
y \<in> set [0..<m]

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

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y < m
[PROOF STEP]
have "filter ((\<le>) y) [0..<m] = [y..<m]"
[PROOF STATE]
proof (prove)
using this:
y < m

goal (1 subgoal):
 1. filter ((\<le>) y) [0..<m] = [y..<m]
[PROOF STEP]
by (auto intro: filter_upt)
[PROOF STATE]
proof (state)
this:
filter ((\<le>) y) [0..<m] = [y..<m]

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y # ys \<in> set (subseqs [y..<m])
[PROOF STEP]
have "y#ys \<in> set (subseqs [y..<m])"
[PROOF STATE]
proof (prove)
using this:
y # ys \<in> set (subseqs [y..<m])

goal (1 subgoal):
 1. y # ys \<in> set (subseqs [y..<m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y # ys \<in> set (subseqs [y..<m])

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with xy
[PROOF STATE]
proof (chain)
picking this:
x < y
y # ys \<in> set (subseqs [y..<m])
[PROOF STEP]
have "x#y#ys \<in> set (subseqs (x#[y..<m]))"
[PROOF STATE]
proof (prove)
using this:
x < y
y # ys \<in> set (subseqs [y..<m])

goal (1 subgoal):
 1. x # y # ys \<in> set (subseqs (x # [y..<m]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # y # ys \<in> set (subseqs (x # [y..<m]))

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x # y # ys \<in> set (subseqs (x # [y..<m]))

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
x < y
[PROOF STEP]
have "... \<subseteq> set (subseqs ([0..<y] @ [y..<m]))"
[PROOF STATE]
proof (prove)
using this:
x < y

goal (1 subgoal):
 1. set (subseqs (x # [y..<m])) \<subseteq> set (subseqs ([0..<y] @ [y..<m]))
[PROOF STEP]
by (intro subseqs_of_subseq Cons_mem_set_subseqs_append, auto intro: subseqs_refl)
[PROOF STATE]
proof (state)
this:
set (subseqs (x # [y..<m])) \<subseteq> set (subseqs ([0..<y] @ [y..<m]))

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (subseqs (x # [y..<m])) \<subseteq> set (subseqs ([0..<y] @ [y..<m]))

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
from xy ym
[PROOF STATE]
proof (chain)
picking this:
x < y
y < m
[PROOF STEP]
have "[0..<y] @ [y..<m] = [0..<m]"
[PROOF STATE]
proof (prove)
using this:
x < y
y < m

goal (1 subgoal):
 1. [0..<y] @ [y..<m] = [0..<m]
[PROOF STEP]
by (auto intro: upt_append)
[PROOF STATE]
proof (state)
this:
[0..<y] @ [y..<m] = [0..<m]

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x # y # ys \<in> set (subseqs [0..<m])
[PROOF STEP]
have "xs \<in> set (subseqs [0..<m])"
[PROOF STATE]
proof (prove)
using this:
x # y # ys \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. xs \<in> set (subseqs [0..<m])
[PROOF STEP]
by (unfold xs)
[PROOF STATE]
proof (state)
this:
xs \<in> set (subseqs [0..<m])

goal (1 subgoal):
 1. if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs) \<Longrightarrow> subseq_of_length (Suc n) [0..<m] xs
[PROOF STEP]
with len[folded n]
[PROOF STATE]
proof (chain)
picking this:
length xs = Suc n
xs \<in> set (subseqs [0..<m])
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
using this:
length xs = Suc n
xs \<in> set (subseqs [0..<m])

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subseq_of_length (Suc n) [0..<m] xs = (if n = 0 then length xs = Suc 0 \<and> hd xs < m else hd xs < hd (tl xs) \<and> subseq_of_length n [0..<m] (tl xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subseqs_of_length_of_indices:
  "{ ys. subseq_of_length n xs ys } = { map (nth xs) is | is. subseq_of_length n [0..<length xs] is }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ys. subseq_of_length n xs ys} = {map ((!) xs) is |is. subseq_of_length n [0..<length xs] is}
[PROOF STEP]
by(unfold subseq_of_length_def, subst subseqs_of_indices[symmetric], auto)


[STATEMENT]
lemma subseqs_of_length_Suc_Cons:
  "{ ys. subseq_of_length (Suc n) (x#xs) ys } =
   Cons x ` { ys. subseq_of_length n xs ys } \<union> { ys. subseq_of_length (Suc n) xs ys }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ys. subseq_of_length (Suc n) (x # xs) ys} = (#) x ` {ys. subseq_of_length n xs ys} \<union> {ys. subseq_of_length (Suc n) xs ys}
[PROOF STEP]
by (unfold subseq_of_length_def, auto)


[STATEMENT]
lemma subseqs_length: assumes f_ac: "\<And> x y z. f x (f y z) = f y (f x z)"
  shows "set (subseqs_length f a n xs) =
  { (foldr f ys a, ys) | ys. ys \<in> set (subseqs xs) \<and> length ys = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
proof (cases "length xs < n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. \<not> length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs < n

goal (2 subgoals):
 1. length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. \<not> length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs < n

goal (1 subgoal):
 1. set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
unfolding subseqs_length_def Let_def
[PROOF STATE]
proof (prove)
using this:
length xs < n

goal (1 subgoal):
 1. set (if length xs < n then [] else subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
using length_subseqs[of xs] subseqs_length_simple_False
[PROOF STATE]
proof (prove)
using this:
length xs < n
length (subseqs xs) = 2 ^ length xs
\<lbrakk>?b \<in> set (subseqs ?xs); length ?xs < length ?b\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. set (if length xs < n then [] else subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal (1 subgoal):
 1. \<not> length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs < n

goal (1 subgoal):
 1. \<not> length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
hence id: "(length xs < n) = False" and "n \<le> length xs"
[PROOF STATE]
proof (prove)
using this:
\<not> length xs < n

goal (1 subgoal):
 1. (length xs < n) = False &&& n \<le> length xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(length xs < n) = False
n \<le> length xs

goal (1 subgoal):
 1. \<not> length xs < n \<Longrightarrow> set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
n \<le> length xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> length xs

goal (1 subgoal):
 1. set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
unfolding subseqs_length_def Let_def id if_False
[PROOF STATE]
proof (prove)
using this:
n \<le> length xs

goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
proof (induct xs arbitrary: n a rule: length_induct[rule_format])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n a. \<lbrakk>\<And>ys n a. \<lbrakk>length ys < length xs; n \<le> length ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a ys n (length ys)) = {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = n}; n \<le> length xs\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case (1 xs n a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?ys < length xs; ?n \<le> length ?ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f ?a ?ys ?n (length ?ys)) = {(foldr f ys ?a, ys) |ys. ys \<in> set (subseqs ?ys) \<and> length ys = ?n}
n \<le> length xs

goal (1 subgoal):
 1. \<And>xs n a. \<lbrakk>\<And>ys n a. \<lbrakk>length ys < length xs; n \<le> length ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a ys n (length ys)) = {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = n}; n \<le> length xs\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
note n = 1(2)
[PROOF STATE]
proof (state)
this:
n \<le> length xs

goal (1 subgoal):
 1. \<And>xs n a. \<lbrakk>\<And>ys n a. \<lbrakk>length ys < length xs; n \<le> length ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a ys n (length ys)) = {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = n}; n \<le> length xs\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
note IH = 1(1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?ys < length xs; ?n \<le> length ?ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f ?a ?ys ?n (length ?ys)) = {(foldr f ys ?a, ys) |ys. ys \<in> set (subseqs ?ys) \<and> length ys = ?n}

goal (1 subgoal):
 1. \<And>xs n a. \<lbrakk>\<And>ys n a. \<lbrakk>length ys < length xs; n \<le> length ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a ys n (length ys)) = {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = n}; n \<le> length xs\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
note simp[simp] = subseqs_i_n_main.simps[of f _ xs n]
[PROOF STATE]
proof (state)
this:
subseqs_i_n_main f ?b xs n ?n = (if n = 0 then [(?b, [])] else if n = ?n then [(foldr f xs ?b, xs)] else case xs of y # ys \<Rightarrow> map (\<lambda>(c, zs). (c, y # zs)) (subseqs_i_n_main f (f y ?b) ys (n - 1) (?n - 1)) @ subseqs_i_n_main f ?b ys n (?n - 1))

goal (1 subgoal):
 1. \<And>xs n a. \<lbrakk>\<And>ys n a. \<lbrakk>length ys < length xs; n \<le> length ys\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a ys n (length ys)) = {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = n}; n \<le> length xs\<rbrakk> \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. n \<noteq> 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. n \<noteq> 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
unfolding simp
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. set (if n = 0 then [(a, [])] else if n = length xs then [(foldr f xs a, xs)] else case xs of y # ys \<Rightarrow> map (\<lambda>(c, zs). (c, y # zs)) (subseqs_i_n_main f (f y a) ys (n - 1) (length xs - 1)) @ subseqs_i_n_main f a ys n (length xs - 1)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
note 0 = this
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
proof (cases "n = length xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = length xs

goal (2 subgoals):
 1. n = length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
have "?thesis = ({(foldr f xs a, xs)} = (\<lambda> ys. (foldr f ys a, ys)) ` {ys. ys \<in> set (subseqs xs) \<and> length ys = length xs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}) = ({(foldr f xs a, xs)} = (\<lambda>ys. (foldr f ys a, ys)) ` {ys \<in> set (subseqs xs). length ys = length xs})
[PROOF STEP]
unfolding simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (if n = 0 then [(a, [])] else if n = length xs then [(foldr f xs a, xs)] else case xs of y # ys \<Rightarrow> map (\<lambda>(c, zs). (c, y # zs)) (subseqs_i_n_main f (f y a) ys (n - 1) (length xs - 1)) @ subseqs_i_n_main f a ys n (length xs - 1)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}) = ({(foldr f xs a, xs)} = (\<lambda>ys. (foldr f ys a, ys)) ` {ys \<in> set (subseqs xs). length ys = length xs})
[PROOF STEP]
using 0 True
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0
n = length xs

goal (1 subgoal):
 1. (set (if n = 0 then [(a, [])] else if n = length xs then [(foldr f xs a, xs)] else case xs of y # ys \<Rightarrow> map (\<lambda>(c, zs). (c, y # zs)) (subseqs_i_n_main f (f y a) ys (n - 1) (length xs - 1)) @ subseqs_i_n_main f a ys n (length xs - 1)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}) = ({(foldr f xs a, xs)} = (\<lambda>ys. (foldr f ys a, ys)) ` {ys \<in> set (subseqs xs). length ys = length xs})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}) = ({(foldr f xs a, xs)} = (\<lambda>ys. (foldr f ys a, ys)) ` {ys \<in> set (subseqs xs). length ys = length xs})

goal (2 subgoals):
 1. n = length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
 2. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
from this[unfolded full_list_subseqs]
[PROOF STATE]
proof (chain)
picking this:
(set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}) = ({(foldr f xs a, xs)} = (\<lambda>ys. (foldr f ys a, ys)) ` {xs})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}) = ({(foldr f xs a, xs)} = (\<lambda>ys. (foldr f ys a, ys)) ` {xs})

goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> length xs

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
n \<le> length xs
n \<noteq> length xs
[PROOF STEP]
have n: "n < length xs"
[PROOF STATE]
proof (prove)
using this:
n \<le> length xs
n \<noteq> length xs

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

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
from 0
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
obtain m where m: "n = Suc m"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

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

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
from n 0
[PROOF STATE]
proof (chain)
picking this:
n < length xs
n \<noteq> 0
[PROOF STEP]
obtain y ys where xs: "xs = y # ys"
[PROOF STATE]
proof (prove)
using this:
n < length xs
n \<noteq> 0

goal (1 subgoal):
 1. (\<And>y ys. xs = y # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases xs, auto)
[PROOF STATE]
proof (state)
this:
xs = y # ys

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
from n m xs
[PROOF STATE]
proof (chain)
picking this:
n < length xs
n = Suc m
xs = y # ys
[PROOF STEP]
have le: "m \<le> length ys" "n \<le> length ys"
[PROOF STATE]
proof (prove)
using this:
n < length xs
n = Suc m
xs = y # ys

goal (1 subgoal):
 1. m \<le> length ys &&& n \<le> length ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> length ys
n \<le> length ys

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
from xs
[PROOF STATE]
proof (chain)
picking this:
xs = y # ys
[PROOF STEP]
have lt: "length ys < length xs"
[PROOF STATE]
proof (prove)
using this:
xs = y # ys

goal (1 subgoal):
 1. length ys < length xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ys < length xs

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
have sub: "set (subseqs_i_n_main f a xs n (length xs)) =
            (\<lambda>(c, zs). (c, y # zs)) ` set (subseqs_i_n_main f (f y a) ys m (length ys)) \<union>
            set (subseqs_i_n_main f a ys n (length ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = (\<lambda>(c, zs). (c, y # zs)) ` set (subseqs_i_n_main f (f y a) ys m (length ys)) \<union> set (subseqs_i_n_main f a ys n (length ys))
[PROOF STEP]
unfolding simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (if n = 0 then [(a, [])] else if n = length xs then [(foldr f xs a, xs)] else case xs of y # ys \<Rightarrow> map (\<lambda>(c, zs). (c, y # zs)) (subseqs_i_n_main f (f y a) ys (n - 1) (length xs - 1)) @ subseqs_i_n_main f a ys n (length xs - 1)) = (\<lambda>(c, zs). (c, y # zs)) ` set (subseqs_i_n_main f (f y a) ys m (length ys)) \<union> set (subseqs_i_n_main f a ys n (length ys))
[PROOF STEP]
using 0 False
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0
n \<noteq> length xs

goal (1 subgoal):
 1. set (if n = 0 then [(a, [])] else if n = length xs then [(foldr f xs a, xs)] else case xs of y # ys \<Rightarrow> map (\<lambda>(c, zs). (c, y # zs)) (subseqs_i_n_main f (f y a) ys (n - 1) (length xs - 1)) @ subseqs_i_n_main f a ys n (length xs - 1)) = (\<lambda>(c, zs). (c, y # zs)) ` set (subseqs_i_n_main f (f y a) ys m (length ys)) \<union> set (subseqs_i_n_main f a ys n (length ys))
[PROOF STEP]
by (simp add: xs m)
[PROOF STATE]
proof (state)
this:
set (subseqs_i_n_main f a xs n (length xs)) = (\<lambda>(c, zs). (c, y # zs)) ` set (subseqs_i_n_main f (f y a) ys m (length ys)) \<union> set (subseqs_i_n_main f a ys n (length ys))

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
have fold: "\<And> ys. foldr f ys (f y a) = f y (foldr f ys a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys. foldr f ys (f y a) = f y (foldr f ys a)
[PROOF STEP]
by (induct_tac ys, auto simp: f_ac)
[PROOF STATE]
proof (state)
this:
foldr f ?ys (f y a) = f y (foldr f ?ys a)

goal (1 subgoal):
 1. n \<noteq> length xs \<Longrightarrow> set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
unfolding sub IH[OF lt le(1)] IH[OF lt le(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(c, zs). (c, y # zs)) ` {(foldr f ysa (f y a), ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = m} \<union> {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = n} = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}
[PROOF STEP]
unfolding m xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(c, zs). (c, y # zs)) ` {(foldr f ysa (f y a), ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = m} \<union> {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs ys) \<and> length ysa = Suc m} = {(foldr f ysa a, ysa) |ysa. ysa \<in> set (subseqs (y # ys)) \<and> length ysa = Suc m}
[PROOF STEP]
by (auto simp: Let_def fold)
[PROOF STATE]
proof (state)
this:
set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (subseqs_i_n_main f a xs n (length xs)) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (subseqs_length f a n xs) = {(foldr f ys a, ys) |ys. ys \<in> set (subseqs xs) \<and> length ys = n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basic_subseqs_impl: assumes f_ac: "\<And> x y z. f x (f y z) = f y (f x z)"
  shows "correct_subseqs_impl f (basic_subseqs_impl f)
    (\<lambda> a xs n triple. (a,xs,n) = triple)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. correct_subseqs_impl f (basic_subseqs_impl f) (\<lambda>a xs n. (=) (a, xs, n))
[PROOF STEP]
by (unfold_locales; unfold subseqs_impl.S_def basic_subseqs_impl_def subseq_of_length_def,
      insert subseqs_length[of f, OF f_ac], auto)


[STATEMENT]
lemma next_subseqs2_Cons:
  "next_subseqs2_set v (j#js) = insert (j, f (tail!!j) v) (next_subseqs2_set v js)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_set v (j # js) = insert (j, f (tail !! j) v) (next_subseqs2_set v js)
[PROOF STEP]
by (auto simp: next_subseqs2_set_def)


[STATEMENT]
lemma out_subseqs2_Cons:
  "out_subseqs2_set v (j#js) = insert (f (tail!!j) v) (out_subseqs2_set v js)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out_subseqs2_set v (j # js) = insert (f (tail !! j) v) (out_subseqs2_set v js)
[PROOF STEP]
by (auto simp: out_subseqs2_set_def)


[STATEMENT]
lemma next_subseqs1_set_as_next_subseqs2_set:
  "next_subseqs1_set ((i,v) # prevs) = next_subseqs1_set prevs \<union> next_subseqs2_set v [0..<i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs1_set ((i, v) # prevs) = next_subseqs1_set prevs \<union> next_subseqs2_set v [0..<i]
[PROOF STEP]
by (auto simp: next_subseqs1_set_def)


[STATEMENT]
lemma out_subseqs1_set_as_out_subseqs2_set:
  "out_subseqs1_set ((i,v) # prevs) =
   { f head v } \<union> out_subseqs1_set prevs \<union> out_subseqs2_set v [0..<i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out_subseqs1_set ((i, v) # prevs) = {f head v} \<union> out_subseqs1_set prevs \<union> out_subseqs2_set v [0..<i]
[PROOF STEP]
by (auto simp: out_subseqs1_set_def)


[STATEMENT]
lemma next_subseqs1_spec:
  shows "\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)"
    and "\<And>out nexts. next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) &&& (\<And>out nexts. next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js))
[PROOF STEP]
proof(induct rule: next_subseqs1_next_subseqs2.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ret0 ret1 out nexts. next_subseqs1_spec out nexts [] (next_subseqs1 out nexts [])
 2. \<And>ret0 ret1 i v prevs out nexts. (\<And>out nexts. next_subseqs2_spec out nexts prevs v [0..<i] (next_subseqs2 out nexts prevs v [0..<i])) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
 3. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 4. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
case (1 ret0 ret1)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>ret0 ret1 out nexts. next_subseqs1_spec out nexts [] (next_subseqs1 out nexts [])
 2. \<And>ret0 ret1 i v prevs out nexts. (\<And>out nexts. next_subseqs2_spec out nexts prevs v [0..<i] (next_subseqs2 out nexts prevs v [0..<i])) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
 3. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 4. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs1_spec out nexts [] (next_subseqs1 out nexts [])
[PROOF STEP]
by (simp add: next_subseqs1_set_def out_subseqs1_set_def)
[PROOF STATE]
proof (state)
this:
next_subseqs1_spec out nexts [] (next_subseqs1 out nexts [])

goal (3 subgoals):
 1. \<And>ret0 ret1 i v prevs out nexts. (\<And>out nexts. next_subseqs2_spec out nexts prevs v [0..<i] (next_subseqs2 out nexts prevs v [0..<i])) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
 2. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 3. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ret0 ret1 i v prevs out nexts. (\<And>out nexts. next_subseqs2_spec out nexts prevs v [0..<i] (next_subseqs2 out nexts prevs v [0..<i])) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
 2. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 3. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
case (2 ret0 ret1 i v prevs)
[PROOF STATE]
proof (state)
this:
next_subseqs2_spec ?out10 ?nexts10 prevs v [0..<i] (next_subseqs2 ?out10 ?nexts10 prevs v [0..<i])

goal (3 subgoals):
 1. \<And>ret0 ret1 i v prevs out nexts. (\<And>out nexts. next_subseqs2_spec out nexts prevs v [0..<i] (next_subseqs2 out nexts prevs v [0..<i])) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
 2. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 3. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
[PROOF STEP]
proof(cases "next_subseqs1 out nexts ((i, v) # prevs)")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. next_subseqs1 out nexts ((i, v) # prevs) = (a, b, c, d) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
[PROOF STEP]
case split: (fields out' head' tail' nexts')
[PROOF STATE]
proof (state)
this:
next_subseqs1 out nexts ((i, v) # prevs) = (out', head', tail', nexts')

goal (1 subgoal):
 1. \<And>a b c d. next_subseqs1 out nexts ((i, v) # prevs) = (a, b, c, d) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
[PROOF STEP]
have "next_subseqs2_spec (f head v # out) nexts prevs v [0..<i] (out', (head',tail',nexts'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec (f head v # out) nexts prevs v [0..<i] (out', head', tail', nexts')
[PROOF STEP]
by (fold split, unfold next_subseqs1.simps, rule 2)
[PROOF STATE]
proof (state)
this:
next_subseqs2_spec (f head v # out) nexts prevs v [0..<i] (out', head', tail', nexts')

goal (1 subgoal):
 1. \<And>a b c d. next_subseqs1 out nexts ((i, v) # prevs) = (a, b, c, d) \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
next_subseqs2_spec (f head v # out) nexts prevs v [0..<i] (out', head', tail', nexts')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
next_subseqs2_spec (f head v # out) nexts prevs v [0..<i] (out', head', tail', nexts')

goal (1 subgoal):
 1. next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))
[PROOF STEP]
apply (unfold next_subseqs2_spec.simps split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set nexts' = set nexts \<union> next_subseqs1_set prevs \<union> next_subseqs2_set v [0..<i] \<and> set out' = set (f head v # out) \<union> out_subseqs1_set prevs \<union> out_subseqs2_set v [0..<i] \<Longrightarrow> next_subseqs1_spec out nexts ((i, v) # prevs) (out', head', tail', nexts')
[PROOF STEP]
by (auto simp: next_subseqs1_set_as_next_subseqs2_set out_subseqs1_set_as_out_subseqs2_set)
[PROOF STATE]
proof (state)
this:
next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
next_subseqs1_spec out nexts ((i, v) # prevs) (next_subseqs1 out nexts ((i, v) # prevs))

goal (2 subgoals):
 1. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 2. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 2. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
case (3 ret0 ret1 prevs v)
[PROOF STATE]
proof (state)
this:
next_subseqs1_spec ?out10 ?nexts10 prevs (next_subseqs1 ?out10 ?nexts10 prevs)

goal (2 subgoals):
 1. \<And>ret0 ret1 prevs v out nexts. (\<And>out nexts. next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
 2. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
[PROOF STEP]
proof (cases "next_subseqs1 out nexts prevs")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. next_subseqs1 out nexts prevs = (a, b, c, d) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
[PROOF STEP]
case split: (fields out' head' tail' nexts')
[PROOF STATE]
proof (state)
this:
next_subseqs1 out nexts prevs = (out', head', tail', nexts')

goal (1 subgoal):
 1. \<And>a b c d. next_subseqs1 out nexts prevs = (a, b, c, d) \<Longrightarrow> next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
[PROOF STEP]
from 3[of out nexts]
[PROOF STATE]
proof (chain)
picking this:
next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
next_subseqs1_spec out nexts prevs (next_subseqs1 out nexts prevs)

goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])
[PROOF STEP]
by(simp add: split next_subseqs2_set_def out_subseqs2_set_def)
[PROOF STATE]
proof (state)
this:
next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
next_subseqs2_spec out nexts prevs v [] (next_subseqs2 out nexts prevs v [])

goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
case (4 ret0 ret1 prevs v j js)
[PROOF STATE]
proof (state)
this:
?x10 = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec ?out10 ?nexts10 prevs v js (next_subseqs2 ?out10 ?nexts10 prevs v js)

goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
define tj where "tj = tail !! j"
[PROOF STATE]
proof (state)
this:
tj = tail !! j

goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
define nexts'' where "nexts'' = (j, f tj v) # nexts"
[PROOF STATE]
proof (state)
this:
nexts'' = (j, f tj v) # nexts

goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
define out'' where "out'' = (f tj v) # out"
[PROOF STATE]
proof (state)
this:
out'' = f tj v # out

goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
let ?n = "next_subseqs2 out'' nexts'' prevs v js"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ret0 ret1 prevs v j js out nexts. (\<And>x out nexts. x = f (tail !! j) v \<Longrightarrow> next_subseqs2_spec out nexts prevs v js (next_subseqs2 out nexts prevs v js)) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
proof (cases ?n)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. next_subseqs2 out'' nexts'' prevs v js = (a, b, c, d) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
case split: (fields out' head' tail' nexts')
[PROOF STATE]
proof (state)
this:
next_subseqs2 out'' nexts'' prevs v js = (out', head', tail', nexts')

goal (1 subgoal):
 1. \<And>a b c d. next_subseqs2 out'' nexts'' prevs v js = (a, b, c, d) \<Longrightarrow> next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))
[PROOF STEP]
apply (unfold next_subseqs2.simps Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 (f (tail !! j) v # out) ((j, f (tail !! j) v) # nexts) prevs v js)
[PROOF STEP]
apply (fold tj_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 (f tj v # out) ((j, f tj v) # nexts) prevs v js)
[PROOF STEP]
apply (fold out''_def nexts''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out'' nexts'' prevs v js)
[PROOF STEP]
apply (unfold split next_subseqs2_spec.simps next_subseqs2_Cons out_subseqs2_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set nexts' = set nexts \<union> next_subseqs1_set prevs \<union> insert (j, f (tail !! j) v) (next_subseqs2_set v js) \<and> set out' = set out \<union> out_subseqs1_set prevs \<union> insert (f (tail !! j) v) (out_subseqs2_set v js)
[PROOF STEP]
using 4[OF refl, of out'' nexts'', unfolded split]
[PROOF STATE]
proof (prove)
using this:
next_subseqs2_spec out'' nexts'' prevs v js (out', head', tail', nexts')

goal (1 subgoal):
 1. set nexts' = set nexts \<union> next_subseqs1_set prevs \<union> insert (j, f (tail !! j) v) (next_subseqs2_set v js) \<and> set out' = set out \<union> out_subseqs1_set prevs \<union> insert (f (tail !! j) v) (out_subseqs2_set v js)
[PROOF STEP]
apply (auto simp: tj_def nexts''_def out''_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
next_subseqs2_spec out nexts prevs v (j # js) (next_subseqs2 out nexts prevs v (j # js))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_set_prevs:
  "snd ` (set_prevs base tail n) = (\<lambda>as. foldr f as base) ` { as. subseq_of_length n tail as }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` set_prevs base tail n = (\<lambda>as. foldr f as base) ` {as. subseq_of_length n tail as}
[PROOF STEP]
by (subst subseqs_of_length_of_indices, auto simp: set_prevs_def image_Collect)


[STATEMENT]
lemma next_subseq_preserve:
  assumes "next_subseqs (head,tail,prevs) = (out, (head',tail',prevs'))"
  shows "head' = head" "tail' = tail"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head' = head &&& tail' = tail
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. head' = head
 2. tail' = tail
[PROOF STEP]
define P :: "'b list \<times> _ \<times> _ \<times> (nat \<times> 'b) list \<Rightarrow> bool"
  where "P \<equiv> \<lambda> (out, (head',tail',prevs')). head' = head \<and> tail' = tail"
[PROOF STATE]
proof (state)
this:
P \<equiv> \<lambda>(out, head', tail', prevs'). head' = head \<and> tail' = tail

goal (2 subgoals):
 1. head' = head
 2. tail' = tail
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P \<equiv> \<lambda>(out, head', tail', prevs'). head' = head \<and> tail' = tail

goal (2 subgoals):
 1. head' = head
 2. tail' = tail
[PROOF STEP]
fix ret0 ret1 v js
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. head' = head
 2. tail' = tail
[PROOF STEP]
have *: "P (next_subseqs1 head tail ret0 ret1 prevs)"
     and  "P (next_subseqs2 head tail ret0 ret1 prevs v js)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (next_subseqs1 head tail ret0 ret1 prevs) &&& P (next_subseqs2 head tail ret0 ret1 prevs v js)
[PROOF STEP]
by(induct rule: next_subseqs1_next_subseqs2.induct, simp add: P_def, auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
P (next_subseqs1 head tail ret0 ret1 prevs)
P (next_subseqs2 head tail ret0 ret1 prevs v js)

goal (2 subgoals):
 1. head' = head
 2. tail' = tail
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
P (next_subseqs1 head tail ?ret0.12 ?ret1.12 prevs)
P (next_subseqs2 head tail ?ret0.12 ?ret1.12 prevs ?v12 ?js12)

goal (2 subgoals):
 1. head' = head
 2. tail' = tail
[PROOF STEP]
from this(1)[unfolded P_def, of "[]" "[]", folded next_subseqs.simps] assms
[PROOF STATE]
proof (chain)
picking this:
case local.next_subseqs (head, tail, prevs) of (out, head', tail', prevs') \<Rightarrow> head' = head \<and> tail' = tail
local.next_subseqs (head, tail, prevs) = (out, head', tail', prevs')
[PROOF STEP]
show "head' = head" "tail' = tail"
[PROOF STATE]
proof (prove)
using this:
case local.next_subseqs (head, tail, prevs) of (out, head', tail', prevs') \<Rightarrow> head' = head \<and> tail' = tail
local.next_subseqs (head, tail, prevs) = (out, head', tail', prevs')

goal (1 subgoal):
 1. head' = head &&& tail' = tail
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
head' = head
tail' = tail

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_subseqs_spec:
  assumes nxt: "next_subseqs (head,tail,prevs) = (out, (head',tail',prevs'))"
  shows "set prevs' = { (j, f (tail !! j) v) | v i j. (i,v) \<in> set prevs \<and> j < i }" (is "?g1")
    and "set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'" (is "?g2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i} &&& set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
 2. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
note next_subseqs1_spec(1)[of head tail Nil Nil prevs]
[PROOF STATE]
proof (state)
this:
next_subseqs1_spec head tail [] [] prevs (next_subseqs1 head tail [] [] prevs)

goal (2 subgoals):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
 2. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
note this[unfolded nxt[simplified]]
[PROOF STATE]
proof (state)
this:
next_subseqs1_spec head tail [] [] prevs (out, head', tail', prevs')

goal (2 subgoals):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
 2. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
note this[unfolded next_subseqs1_spec.simps]
[PROOF STATE]
proof (state)
this:
set prevs' = set [] \<union> next_subseqs1_set tail prevs \<and> set out = set [] \<union> out_subseqs1_set head tail prevs

goal (2 subgoals):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
 2. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
note this[unfolded next_subseqs1_set_def out_subseqs1_set_def]
[PROOF STATE]
proof (state)
this:
set prevs' = set [] \<union> \<Union> {next_subseqs2_set tail v [0..<i] |v i. (i, v) \<in> set prevs} \<and> set out = set [] \<union> ((f head \<circ> snd) ` set prevs \<union> \<Union> {out_subseqs2_set tail v [0..<i] |v i. (i, v) \<in> set prevs})

goal (2 subgoals):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
 2. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
note * = this[unfolded next_subseqs2_set_def out_subseqs2_set_def]
[PROOF STATE]
proof (state)
this:
set prevs' = set [] \<union> \<Union> {{(j, f (tail !! j) v) |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs} \<and> set out = set [] \<union> ((f head \<circ> snd) ` set prevs \<union> \<Union> {{f (tail !! j) v |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs})

goal (2 subgoals):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
 2. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set prevs' = set [] \<union> \<Union> {{(j, f (tail !! j) v) |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs} \<and> set out = set [] \<union> ((f head \<circ> snd) ` set prevs \<union> \<Union> {{f (tail !! j) v |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs})
[PROOF STEP]
show g1: ?g1
[PROOF STATE]
proof (prove)
using this:
set prevs' = set [] \<union> \<Union> {{(j, f (tail !! j) v) |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs} \<and> set out = set [] \<union> ((f head \<circ> snd) ` set prevs \<union> \<Union> {{f (tail !! j) v |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs})

goal (1 subgoal):
 1. set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}

goal (1 subgoal):
 1. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}

goal (1 subgoal):
 1. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
have "snd ` ... =  (\<Union> {{(f (tail !! j) v) | j. j < i} | v i. (i, v) \<in> set prevs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i} = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}
[PROOF STEP]
by (unfold image_Collect, auto)
[PROOF STATE]
proof (state)
this:
snd ` {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i} = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}

goal (1 subgoal):
 1. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
snd ` set prevs' = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}
[PROOF STEP]
have **: "snd ` set prevs' = ..."
[PROOF STATE]
proof (prove)
using this:
snd ` set prevs' = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}

goal (1 subgoal):
 1. snd ` set prevs' = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd ` set prevs' = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}

goal (1 subgoal):
 1. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
with conjunct2[OF *]
[PROOF STATE]
proof (chain)
picking this:
set out = set [] \<union> ((f head \<circ> snd) ` set prevs \<union> \<Union> {{f (tail !! j) v |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs})
snd ` set prevs' = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}
[PROOF STEP]
show ?g2
[PROOF STATE]
proof (prove)
using this:
set out = set [] \<union> ((f head \<circ> snd) ` set prevs \<union> \<Union> {{f (tail !! j) v |j. j \<in> set [0..<i]} |v i. (i, v) \<in> set prevs})
snd ` set prevs' = \<Union> {{f (tail !! j) v |j. j < i} |v i. (i, v) \<in> set prevs}

goal (1 subgoal):
 1. set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma next_subseq_prevs:
  assumes nxt: "next_subseqs (head,tail,prevs) = (out, (head',tail',prevs'))"
      and inv_prevs: "set prevs = set_prevs base (IArray.list_of tail) n"
  shows "set prevs' = set_prevs base (IArray.list_of tail) (Suc n)" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set prevs' = set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
proof(intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
assume r: "t \<in> ?r"
[PROOF STATE]
proof (state)
this:
t \<in> set_prevs base (IArray.list_of tail) (Suc n)

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
from this[unfolded set_prevs_def]
[PROOF STATE]
proof (chain)
picking this:
t \<in> {(i, foldr f (map ((!) (IArray.list_of tail)) is) base) |i is. subseq_of_length (Suc n) [0..<length (IArray.list_of tail)] is \<and> i = (if Suc n = 0 then length (IArray.list_of tail) else hd is)}
[PROOF STEP]
obtain iis
  where t: "t = (hd iis, foldr f (map ((!!) tail) iis) base)"
    and sl: "subseq_of_length (Suc n) [0..<IArray.length tail] iis"
[PROOF STATE]
proof (prove)
using this:
t \<in> {(i, foldr f (map ((!) (IArray.list_of tail)) is) base) |i is. subseq_of_length (Suc n) [0..<length (IArray.list_of tail)] is \<and> i = (if Suc n = 0 then length (IArray.list_of tail) else hd is)}

goal (1 subgoal):
 1. (\<And>iis. \<lbrakk>t = (hd iis, foldr f (map ((!!) tail) iis) base); subseq_of_length (Suc n) [0..<IArray.length tail] iis\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = (hd iis, foldr f (map ((!!) tail) iis) base)
subseq_of_length (Suc n) [0..<IArray.length tail] iis

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
from sl
[PROOF STATE]
proof (chain)
picking this:
subseq_of_length (Suc n) [0..<IArray.length tail] iis
[PROOF STEP]
have "length iis > 0"
[PROOF STATE]
proof (prove)
using this:
subseq_of_length (Suc n) [0..<IArray.length tail] iis

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

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < length iis
[PROOF STEP]
obtain i "is" where iis: "iis = i#is"
[PROOF STATE]
proof (prove)
using this:
0 < length iis

goal (1 subgoal):
 1. (\<And>i is. iis = i # is \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson list.set_cases nth_mem)
[PROOF STATE]
proof (state)
this:
iis = i # is

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
define v where "v = foldr f (map ((!!) tail) is) base"
[PROOF STATE]
proof (state)
this:
v = foldr f (map ((!!) tail) is) base

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
note sl[unfolded subseq_of_length_Suc_upt]
[PROOF STATE]
proof (state)
this:
if n = 0 then length iis = Suc 0 \<and> hd iis < IArray.length tail else hd iis < hd (tl iis) \<and> subseq_of_length n [0..<IArray.length tail] (tl iis)

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
note nxt = next_subseqs_spec[OF nxt]
[PROOF STATE]
proof (state)
this:
set prevs' = {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
set out = (f head \<circ> snd) ` set prevs \<union> snd ` set prevs'

goal (2 subgoals):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
 2. \<And>x. x \<in> set_prevs base (IArray.list_of tail) (Suc n) \<Longrightarrow> x \<in> set prevs'
[PROOF STEP]
show "t \<in> ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> set prevs'
[PROOF STEP]
proof(cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> t \<in> set prevs'
 2. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> t \<in> set prevs'
 2. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
from sl[unfolded subseq_of_length_Suc_upt] t
[PROOF STATE]
proof (chain)
picking this:
if n = 0 then length iis = Suc 0 \<and> hd iis < IArray.length tail else hd iis < hd (tl iis) \<and> subseq_of_length n [0..<IArray.length tail] (tl iis)
t = (hd iis, foldr f (map ((!!) tail) iis) base)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
if n = 0 then length iis = Suc 0 \<and> hd iis < IArray.length tail else hd iis < hd (tl iis) \<and> subseq_of_length n [0..<IArray.length tail] (tl iis)
t = (hd iis, foldr f (map ((!!) tail) iis) base)

goal (1 subgoal):
 1. t \<in> set prevs'
[PROOF STEP]
by (unfold nxt[unfolded inv_prevs] True set_prevs_def length_Suc_conv, auto)
[PROOF STATE]
proof (state)
this:
t \<in> set prevs'

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
from sl[unfolded subseq_of_length_Suc_upt iis,simplified]
[PROOF STATE]
proof (chain)
picking this:
i < hd is \<and> subseq_of_length n [0..<length (IArray.list_of tail)] is
[PROOF STEP]
have i: "i < hd is" and "is": "subseq_of_length n [0..<IArray.length tail] is"
[PROOF STATE]
proof (prove)
using this:
i < hd is \<and> subseq_of_length n [0..<length (IArray.list_of tail)] is

goal (1 subgoal):
 1. i < hd is &&& subseq_of_length n [0..<IArray.length tail] is
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < hd is
subseq_of_length n [0..<IArray.length tail] is

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < hd is
subseq_of_length n [0..<IArray.length tail] is
[PROOF STEP]
have *: "(hd is, v) \<in> set_prevs base (IArray.list_of tail) n"
[PROOF STATE]
proof (prove)
using this:
i < hd is
subseq_of_length n [0..<IArray.length tail] is

goal (1 subgoal):
 1. (hd is, v) \<in> set_prevs base (IArray.list_of tail) n
[PROOF STEP]
by (unfold set_prevs_def, auto intro!: exI[of _ "is"] simp: v_def)
[PROOF STATE]
proof (state)
this:
(hd is, v) \<in> set_prevs base (IArray.list_of tail) n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i < hd is
(hd is, v) \<in> set_prevs base (IArray.list_of tail) n
[PROOF STEP]
have "(i, f (tail !! i) v) \<in> {(j, f (tail !! j) v) | j. j < hd is}"
[PROOF STATE]
proof (prove)
using this:
i < hd is
(hd is, v) \<in> set_prevs base (IArray.list_of tail) n

goal (1 subgoal):
 1. (i, f (tail !! i) v) \<in> {(j, f (tail !! j) v) |j. j < hd is}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, f (tail !! i) v) \<in> {(j, f (tail !! j) v) |j. j < hd is}

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
with t[unfolded iis]
[PROOF STATE]
proof (chain)
picking this:
t = (hd (i # is), foldr f (map ((!!) tail) (i # is)) base)
(i, f (tail !! i) v) \<in> {(j, f (tail !! j) v) |j. j < hd is}
[PROOF STEP]
have "t \<in> ..."
[PROOF STATE]
proof (prove)
using this:
t = (hd (i # is), foldr f (map ((!!) tail) (i # is)) base)
(i, f (tail !! i) v) \<in> {(j, f (tail !! j) v) |j. j < hd is}

goal (1 subgoal):
 1. t \<in> {(j, f (tail !! j) v) |j. j < hd is}
[PROOF STEP]
by (auto simp: v_def)
[PROOF STATE]
proof (state)
this:
t \<in> {(j, f (tail !! j) v) |j. j < hd is}

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> t \<in> set prevs'
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
(hd is, v) \<in> set_prevs base (IArray.list_of tail) n
t \<in> {(j, f (tail !! j) v) |j. j < hd is}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(hd is, v) \<in> set_prevs base (IArray.list_of tail) n
t \<in> {(j, f (tail !! j) v) |j. j < hd is}

goal (1 subgoal):
 1. t \<in> set prevs'
[PROOF STEP]
by (unfold nxt[unfolded inv_prevs], auto)
[PROOF STATE]
proof (state)
this:
t \<in> set prevs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> set prevs'

goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
assume l: "t \<in> ?l"
[PROOF STATE]
proof (state)
this:
t \<in> set prevs'

goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
from l[unfolded next_subseqs_spec(1)[OF nxt]]
[PROOF STATE]
proof (chain)
picking this:
t \<in> {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}
[PROOF STEP]
obtain j v i
  where t: "t = (j, f (tail!!j) v)"
    and j: "j < i"
    and iv: "(i,v) \<in> set prevs"
[PROOF STATE]
proof (prove)
using this:
t \<in> {uu_. \<exists>v i j. uu_ = (j, f (tail !! j) v) \<and> (i, v) \<in> set prevs \<and> j < i}

goal (1 subgoal):
 1. (\<And>j v i. \<lbrakk>t = (j, f (tail !! j) v); j < i; (i, v) \<in> set prevs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = (j, f (tail !! j) v)
j < i
(i, v) \<in> set prevs

goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
from iv[unfolded inv_prevs set_prevs_def, simplified]
[PROOF STATE]
proof (chain)
picking this:
\<exists>is. i = (if n = 0 then length (IArray.list_of tail) else hd is) \<and> v = foldr f (map ((!) (IArray.list_of tail)) is) base \<and> subseq_of_length n [0..<length (IArray.list_of tail)] is
[PROOF STEP]
obtain "is"
  where v: "v = foldr f (map ((!!) tail) is) base"
    and "is": "subseq_of_length n [0..<IArray.length tail] is"
    and i: "if n = 0 then i = IArray.length tail else i = hd is"
[PROOF STATE]
proof (prove)
using this:
\<exists>is. i = (if n = 0 then length (IArray.list_of tail) else hd is) \<and> v = foldr f (map ((!) (IArray.list_of tail)) is) base \<and> subseq_of_length n [0..<length (IArray.list_of tail)] is

goal (1 subgoal):
 1. (\<And>is. \<lbrakk>v = foldr f (map ((!!) tail) is) base; subseq_of_length n [0..<IArray.length tail] is; if n = 0 then i = IArray.length tail else i = hd is\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = foldr f (map ((!!) tail) is) base
subseq_of_length n [0..<IArray.length tail] is
if n = 0 then i = IArray.length tail else i = hd is

goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
from "is" j i
[PROOF STATE]
proof (chain)
picking this:
subseq_of_length n [0..<IArray.length tail] is
j < i
if n = 0 then i = IArray.length tail else i = hd is
[PROOF STEP]
have jis: "subseq_of_length (Suc n) [0..<IArray.length tail] (j#is)"
[PROOF STATE]
proof (prove)
using this:
subseq_of_length n [0..<IArray.length tail] is
j < i
if n = 0 then i = IArray.length tail else i = hd is

goal (1 subgoal):
 1. subseq_of_length (Suc n) [0..<IArray.length tail] (j # is)
[PROOF STEP]
by (unfold subseq_of_length_Suc_upt, auto)
[PROOF STATE]
proof (state)
this:
subseq_of_length (Suc n) [0..<IArray.length tail] (j # is)

goal (1 subgoal):
 1. \<And>x. x \<in> set prevs' \<Longrightarrow> x \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subseq_of_length (Suc n) [0..<IArray.length tail] (j # is)
[PROOF STEP]
show "t \<in> ?r"
[PROOF STATE]
proof (prove)
using this:
subseq_of_length (Suc n) [0..<IArray.length tail] (j # is)

goal (1 subgoal):
 1. t \<in> set_prevs base (IArray.list_of tail) (Suc n)
[PROOF STEP]
by (auto intro!: exI[of _ "j#is"] simp: set_prevs_def t v)
[PROOF STATE]
proof (state)
this:
t \<in> set_prevs base (IArray.list_of tail) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invariant_next_subseqs:
  assumes inv: "invariant base elements n state"
      and nxt: "next_subseqs state = (out, state')"
  shows "invariant base elements (Suc n) state'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant base elements (Suc n) state'
[PROOF STEP]
proof(cases "elements = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. elements = [] \<Longrightarrow> invariant base elements (Suc n) state'
 2. elements \<noteq> [] \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
elements = []

goal (2 subgoals):
 1. elements = [] \<Longrightarrow> invariant base elements (Suc n) state'
 2. elements \<noteq> [] \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
with inv nxt
[PROOF STATE]
proof (chain)
picking this:
invariant base elements n state
local.next_subseqs state = (out, state')
elements = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invariant base elements n state
local.next_subseqs state = (out, state')
elements = []

goal (1 subgoal):
 1. invariant base elements (Suc n) state'
[PROOF STEP]
by(cases state, auto)
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state'

goal (1 subgoal):
 1. elements \<noteq> [] \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elements \<noteq> [] \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
elements \<noteq> []

goal (1 subgoal):
 1. elements \<noteq> [] \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
with inv nxt
[PROOF STATE]
proof (chain)
picking this:
invariant base elements n state
local.next_subseqs state = (out, state')
elements \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invariant base elements n state
local.next_subseqs state = (out, state')
elements \<noteq> []

goal (1 subgoal):
 1. invariant base elements (Suc n) state'
[PROOF STEP]
proof (cases state)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>invariant base elements n state; local.next_subseqs state = (out, state'); elements \<noteq> []; state = (a, b, c)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
case state: (fields head tail prevs)
[PROOF STATE]
proof (state)
this:
state = (head, tail, prevs)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>invariant base elements n state; local.next_subseqs state = (out, state'); elements \<noteq> []; state = (a, b, c)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
note inv = inv[unfolded state]
[PROOF STATE]
proof (state)
this:
invariant base elements n (head, tail, prevs)

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>invariant base elements n state; local.next_subseqs state = (out, state'); elements \<noteq> []; state = (a, b, c)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant base elements (Suc n) state'
[PROOF STEP]
proof (cases state')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
case state': (fields head' tail' prevs')
[PROOF STATE]
proof (state)
this:
state' = (head', tail', prevs')

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
note nxt = nxt[unfolded state state']
[PROOF STATE]
proof (state)
this:
local.next_subseqs (head, tail, prevs) = (out, head', tail', prevs')

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
note [simp] = next_subseq_preserve[OF nxt]
[PROOF STATE]
proof (state)
this:
head' = head
tail' = tail

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
from False inv
[PROOF STATE]
proof (chain)
picking this:
elements \<noteq> []
invariant base elements n (head, tail, prevs)
[PROOF STEP]
have "set prevs = set_prevs base (IArray.list_of tail) n"
[PROOF STATE]
proof (prove)
using this:
elements \<noteq> []
invariant base elements n (head, tail, prevs)

goal (1 subgoal):
 1. set prevs = set_prevs base (IArray.list_of tail) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set prevs = set_prevs base (IArray.list_of tail) n

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> invariant base elements (Suc n) state'
[PROOF STEP]
from False next_subseq_prevs[OF nxt this] inv
[PROOF STATE]
proof (chain)
picking this:
elements \<noteq> []
set prevs' = set_prevs base (IArray.list_of tail) (Suc n)
invariant base elements n (head, tail, prevs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elements \<noteq> []
set prevs' = set_prevs base (IArray.list_of tail) (Suc n)
invariant base elements n (head, tail, prevs)

goal (1 subgoal):
 1. invariant base elements (Suc n) state'
[PROOF STEP]
by(auto simp: state')
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state'

goal:
No subgoals!
[PROOF STEP]
qed