[STATEMENT]
lemma strict_borderE[elim]:
  fixes xs ys :: "'a list"
  assumes "strict_border xs ys"
  obtains "border xs ys" and "length xs < length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>border xs ys; length xs < length ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
strict_border xs ys

goal (1 subgoal):
 1. (\<lbrakk>border xs ys; length xs < length ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding strict_border_def
[PROOF STATE]
proof (prove)
using this:
border xs ys \<and> length xs < length ys

goal (1 subgoal):
 1. (\<lbrakk>border xs ys; length xs < length ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma strict_border_simps[simp]:
  "strict_border xs [] \<longleftrightarrow> False"
  "strict_border [] (x # xs) \<longleftrightarrow> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_border xs [] = False &&& strict_border [] (x # xs) = True
[PROOF STEP]
by (simp_all add: strict_border_def)


[STATEMENT]
lemma strict_border_prefix: "strict_border xs ys \<Longrightarrow> strict_prefix xs ys"
  and strict_border_suffix: "strict_border xs ys \<Longrightarrow> strict_suffix xs ys"
  and strict_border_imp_nonempty: "strict_border xs ys \<Longrightarrow> ys \<noteq> []"
  and strict_border_prefix_suffix: "strict_border xs ys \<longleftrightarrow> strict_prefix xs ys \<and> strict_suffix xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((strict_border xs ys \<Longrightarrow> strict_prefix xs ys) &&& (strict_border xs ys \<Longrightarrow> strict_suffix xs ys)) &&& (strict_border xs ys \<Longrightarrow> ys \<noteq> []) &&& strict_border xs ys = (strict_prefix xs ys \<and> strict_suffix xs ys)
[PROOF STEP]
by (auto simp: border_order.order.strict_iff_order border_def)


[STATEMENT]
lemma border_length_le: "border xs ys \<Longrightarrow> length xs \<le> length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. border xs ys \<Longrightarrow> length xs \<le> length ys
[PROOF STEP]
unfolding border_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix xs ys \<and> suffix xs ys \<Longrightarrow> length xs \<le> length ys
[PROOF STEP]
by (simp add: prefix_length_le)


[STATEMENT]
lemma border_length_r_less (*rm*): "\<forall>xs. strict_border xs ys \<longrightarrow> length xs < length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. strict_border xs ys \<longrightarrow> length xs < length ys
[PROOF STEP]
using strict_borderE
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>strict_border ?xs ?ys; \<lbrakk>border ?xs ?ys; length ?xs < length ?ys\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<forall>xs. strict_border xs ys \<longrightarrow> length xs < length ys
[PROOF STEP]
by auto


[STATEMENT]
lemma all_positions_drop_length_take: "\<lbrakk>i \<le> length w; i \<le> length x;
  \<forall>j<i. x ! j = w ! (length w + j - i)\<rbrakk>
    \<Longrightarrow> drop (length w - i) w = take i x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> length w; i \<le> length x; \<forall>j<i. x ! j = w ! (length w + j - i)\<rbrakk> \<Longrightarrow> drop (length w - i) w = take i x
[PROOF STEP]
by (cases "i = length x") (auto intro: nth_equalityI)


[STATEMENT]
lemma all_positions_suffix_take: "\<lbrakk>i \<le> length w; i \<le> length x;
  \<forall>j<i. x ! j = w ! (length w + j - i)\<rbrakk>
    \<Longrightarrow> suffix (take i x) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> length w; i \<le> length x; \<forall>j<i. x ! j = w ! (length w + j - i)\<rbrakk> \<Longrightarrow> suffix (take i x) w
[PROOF STEP]
by (metis all_positions_drop_length_take suffix_drop)


[STATEMENT]
lemma suffix_butlast: "suffix xs ys \<Longrightarrow> suffix (butlast xs) (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix xs ys \<Longrightarrow> suffix (butlast xs) (butlast ys)
[PROOF STEP]
unfolding suffix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>zs. ys = zs @ xs \<Longrightarrow> \<exists>zs. butlast ys = zs @ butlast xs
[PROOF STEP]
by (metis append_Nil2 butlast.simps(1) butlast_append)


[STATEMENT]
lemma positions_border: "\<forall>j<l. w!j = w!(length w - l + j) \<Longrightarrow> border (take l w) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<l. w ! j = w ! (length w - l + j) \<Longrightarrow> border (take l w) w
[PROOF STEP]
by (cases "l < length w") (simp_all add: border_def all_positions_suffix_take take_is_prefix)


[STATEMENT]
lemma positions_strict_border: "l < length w \<Longrightarrow> \<forall>j<l. w!j = w!(length w - l + j) \<Longrightarrow> strict_border (take l w) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l < length w; \<forall>j<l. w ! j = w ! (length w - l + j)\<rbrakk> \<Longrightarrow> strict_border (take l w) w
[PROOF STEP]
by (simp add: positions_border strict_border_def)


[STATEMENT]
lemma nonempty_is_arg_max_ib: "ys \<noteq> [] \<Longrightarrow> is_arg_max length (\<lambda>xs. strict_border xs ys) (intrinsic_border ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> is_arg_max length (\<lambda>xs. strict_border xs ys) (intrinsic_border ys)
[PROOF STEP]
by (simp add: intrinsic_borderI' intrinsic_border_max is_arg_max_linorder)


[STATEMENT]
lemma intrinsic_border_less: "w \<noteq> [] \<Longrightarrow> length (intrinsic_border w) < length w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<noteq> [] \<Longrightarrow> length (intrinsic_border w) < length w
[PROOF STEP]
using intrinsic_borderI[of w] border_length_r_less intrinsic_borderI'
[PROOF STATE]
proof (prove)
using this:
strict_border w ?ys \<Longrightarrow> strict_border (intrinsic_border ?ys) ?ys
\<forall>xs. strict_border xs ?ys \<longrightarrow> length xs < length ?ys
?ys \<noteq> [] \<Longrightarrow> strict_border (intrinsic_border ?ys) ?ys

goal (1 subgoal):
 1. w \<noteq> [] \<Longrightarrow> length (intrinsic_border w) < length w
[PROOF STEP]
by blast


[STATEMENT]
lemma intrinsic_border_take_less: "j > 0 \<Longrightarrow> w \<noteq> [] \<Longrightarrow> length (intrinsic_border (take j w)) < length w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < j; w \<noteq> []\<rbrakk> \<Longrightarrow> length (intrinsic_border (take j w)) < length w
[PROOF STEP]
by (metis intrinsic_border_less length_take less_not_refl2 min_less_iff_conj take_eq_Nil)


[STATEMENT]
lemma border_example: "{b. border b ''aabaabaa''} = {'''', ''a'', ''aa'', ''aabaa'', ''aabaabaa''}"
  (is "{b. border b ?l} = {?take0, ?take1, ?take2, ?take5, ?l}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {b. border b ''aabaabaa''} = {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
 2. {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''} \<subseteq> {b. border b ''aabaabaa''}
[PROOF STEP]
show "{?take0, ?take1, ?take2, ?take5, ?l} \<subseteq> {b. border b ?l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''} \<subseteq> {b. border b ''aabaabaa''}
[PROOF STEP]
by simp eval
[PROOF STATE]
proof (state)
this:
{[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''} \<subseteq> {b. border b ''aabaabaa''}

goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
[PROOF STEP]
have "\<not>border ''aab'' ?l" "\<not>border ''aaba'' ?l" "\<not>border ''aabaab'' ?l" "\<not>border ''aabaaba'' ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> border ''aab'' ''aabaabaa'' &&& \<not> border ''aaba'' ''aabaabaa'') &&& \<not> border ''aabaab'' ''aabaabaa'' &&& \<not> border ''aabaaba'' ''aabaabaa''
[PROOF STEP]
by eval+
[PROOF STATE]
proof (state)
this:
\<not> border ''aab'' ''aabaabaa''
\<not> border ''aaba'' ''aabaabaa''
\<not> border ''aabaab'' ''aabaabaa''
\<not> border ''aabaaba'' ''aabaabaa''

goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> border ''aab'' ''aabaabaa''
\<not> border ''aaba'' ''aabaabaa''
\<not> border ''aabaab'' ''aabaabaa''
\<not> border ''aabaaba'' ''aabaabaa''

goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
[PROOF STEP]
have "{b. border b ?l} \<subseteq> set (prefixes ?l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> set (prefixes ''aabaabaa'')
[PROOF STEP]
using border_def in_set_prefixes
[PROOF STATE]
proof (prove)
using this:
border ?xs ?ys = (prefix ?xs ?ys \<and> suffix ?xs ?ys)
(?xs \<in> set (prefixes ?ys)) = prefix ?xs ?ys

goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> set (prefixes ''aabaabaa'')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{b. border b ''aabaabaa''} \<subseteq> set (prefixes ''aabaabaa'')

goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> border ''aab'' ''aabaabaa''
\<not> border ''aaba'' ''aabaabaa''
\<not> border ''aabaab'' ''aabaabaa''
\<not> border ''aabaaba'' ''aabaabaa''
{b. border b ''aabaabaa''} \<subseteq> set (prefixes ''aabaabaa'')
[PROOF STEP]
show "{b. border b ?l} \<subseteq> {?take0, ?take1, ?take2, ?take5, ?l}"
[PROOF STATE]
proof (prove)
using this:
\<not> border ''aab'' ''aabaabaa''
\<not> border ''aaba'' ''aabaabaa''
\<not> border ''aabaab'' ''aabaabaa''
\<not> border ''aabaaba'' ''aabaabaa''
{b. border b ''aabaabaa''} \<subseteq> set (prefixes ''aabaabaa'')

goal (1 subgoal):
 1. {b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{b. border b ''aabaabaa''} \<subseteq> {[], ''a'', ''aa'', ''aabaa'', ''aabaabaa''}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<ff>_eq_0_iff_j_eq_0[simp]: "\<ff> s j = 0 \<longleftrightarrow> j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<ff> s j = 0) = (j = 0)
[PROOF STEP]
by (cases j) simp_all


[STATEMENT]
lemma j_le_\<ff>_le: "j \<le> length s \<Longrightarrow> \<ff> s j \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> length s \<Longrightarrow> \<ff> s j \<le> j
[PROOF STEP]
apply (cases j)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>j \<le> length s; j = 0\<rbrakk> \<Longrightarrow> \<ff> s j \<le> j
 2. \<And>nat. \<lbrakk>j \<le> length s; j = Suc nat\<rbrakk> \<Longrightarrow> \<ff> s j \<le> j
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> length s; j = Suc nat\<rbrakk> \<Longrightarrow> length (intrinsic_border (take (Suc nat) s)) \<le> nat
[PROOF STEP]
by (metis Suc_leI intrinsic_border_less length_take list.size(3) min.absorb2 nat.simps(3) not_less)


[STATEMENT]
lemma j_le_\<ff>_le': "0 < j \<Longrightarrow> j \<le> length s \<Longrightarrow> \<ff> s j - 1 < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < j; j \<le> length s\<rbrakk> \<Longrightarrow> \<ff> s j - 1 < j
[PROOF STEP]
by (metis diff_less j_le_\<ff>_le le_eq_less_or_eq less_imp_diff_less less_one)


[STATEMENT]
lemma \<ff>_le: "s \<noteq> [] \<Longrightarrow> \<ff> s j - 1 < length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> \<ff> s j - 1 < length s
[PROOF STEP]
by (cases j) (simp_all add: intrinsic_border_take_less)


[STATEMENT]
lemma reuse_matches:
  assumes j_le: "j \<le> length s"
  and old_matches: "\<forall>jj<j. t ! (i + jj) = s ! jj"
  shows "\<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj"
    (is "\<forall>jj<?j'. t ! (?i' + jj) = s ! jj")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
proof (cases "j>0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
assume "j>0"
[PROOF STATE]
proof (state)
this:
0 < j

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
have \<ff>_le: "\<ff> s j \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ff> s j \<le> j
[PROOF STEP]
by (simp add: j_le j_le_\<ff>_le)
[PROOF STATE]
proof (state)
this:
\<ff> s j \<le> j

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
with old_matches
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<j. t ! (i + jj) = s ! jj
\<ff> s j \<le> j
[PROOF STEP]
have 1: "\<forall>jj<?j'. t ! (?i' + jj) = s ! (j - \<ff> s j + 1 + jj)"
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<j. t ! (i + jj) = s ! jj
\<ff> s j \<le> j

goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! (j - \<ff> s j + 1 + jj)
[PROOF STEP]
by (metis ab_semigroup_add_class.add.commute add.assoc diff_diff_cancel less_diff_conv)
[PROOF STATE]
proof (state)
this:
\<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! (j - \<ff> s j + 1 + jj)

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
have [simp]: "length (take j s) = j" "length (intrinsic_border (take j s)) = ?j'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (take j s) = j &&& length (intrinsic_border (take j s)) = \<ff> s j - 1
[PROOF STEP]
by (simp add: j_le) (metis \<open>0 < j\<close> diff_add_inverse2 \<ff>.elims nat_neq_iff)
[PROOF STATE]
proof (state)
this:
length (take j s) = j
length (intrinsic_border (take j s)) = \<ff> s j - 1

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (take j s) = j
length (intrinsic_border (take j s)) = \<ff> s j - 1
[PROOF STEP]
have "\<forall>jj<?j'. take j s ! jj = take j s ! (j - (\<ff> s j - 1) + jj)"
[PROOF STATE]
proof (prove)
using this:
length (take j s) = j
length (intrinsic_border (take j s)) = \<ff> s j - 1

goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - (\<ff> s j - 1) + jj)
[PROOF STEP]
by (metis intrinsic_borderI' \<open>0 < j\<close> border_positions length_greater_0_conv strict_border_def)
[PROOF STATE]
proof (state)
this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - (\<ff> s j - 1) + jj)

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - (\<ff> s j - 1) + jj)
[PROOF STEP]
have "\<forall>jj<?j'. take j s ! jj = take j s ! (j - \<ff> s j + 1 + jj)"
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - (\<ff> s j - 1) + jj)

goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - \<ff> s j + 1 + jj)
[PROOF STEP]
by (simp add: \<ff>_le)
[PROOF STATE]
proof (state)
this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - \<ff> s j + 1 + jj)

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - \<ff> s j + 1 + jj)
[PROOF STEP]
have 2: "\<forall>jj<?j'. s ! (j - \<ff> s j + 1 + jj) = s ! jj"
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - \<ff> s j + 1 + jj)

goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. s ! (j - \<ff> s j + 1 + jj) = s ! jj
[PROOF STEP]
using \<ff>_le
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<\<ff> s j - 1. take j s ! jj = take j s ! (j - \<ff> s j + 1 + jj)
\<ff> s j \<le> j

goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. s ! (j - \<ff> s j + 1 + jj) = s ! jj
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>jj<\<ff> s j - 1. s ! (j - \<ff> s j + 1 + jj) = s ! jj

goal (2 subgoals):
 1. 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
 2. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! (j - \<ff> s j + 1 + jj)
\<forall>jj<\<ff> s j - 1. s ! (j - \<ff> s j + 1 + jj) = s ! jj
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! (j - \<ff> s j + 1 + jj)
\<forall>jj<\<ff> s j - 1. s ! (j - \<ff> s j + 1 + jj) = s ! jj

goal (1 subgoal):
 1. \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj

goal (1 subgoal):
 1. \<not> 0 < j \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
[PROOF STEP]
qed simp


[STATEMENT]
theorem shift_safe:
  assumes
    "\<forall>ii<i. \<not>sublist_at s t ii"
    "t!(i+j) \<noteq> s!j" and
    [simp]: "j < length s" and
    matches: "\<forall>jj<j. t!(i+jj) = s!jj"
  defines
    assignment: "i' \<equiv> i + (j - \<ff> s j + 1)"
  shows
    "\<forall>ii<i'. \<not>sublist_at s t ii"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ii<i'. \<not> sublist_at s t ii
[PROOF STEP]
proof (standard, standard)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ii. ii < i' \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
fix ii
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ii. ii < i' \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
assume "ii < i'"
[PROOF STATE]
proof (state)
this:
ii < i'

goal (1 subgoal):
 1. \<And>ii. ii < i' \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ii < i'
[PROOF STEP]
consider \<comment> \<open>The position falls into one of three categories:\<close>
    (old) "ii < i" |
    (current) "ii = i" |
    (skipped) "ii > i"
[PROOF STATE]
proof (prove)
using this:
ii < i'

goal (1 subgoal):
 1. \<lbrakk>ii < i \<Longrightarrow> thesis; ii = i \<Longrightarrow> thesis; i < ii \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>ii < i \<Longrightarrow> ?thesis; ii = i \<Longrightarrow> ?thesis; i < ii \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>ii. ii < i' \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>ii < i \<Longrightarrow> ?thesis; ii = i \<Longrightarrow> ?thesis; i < ii \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "\<not>sublist_at s t ii"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ii < i \<Longrightarrow> ?thesis; ii = i \<Longrightarrow> ?thesis; i < ii \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<not> sublist_at s t ii
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ii < i \<Longrightarrow> \<not> sublist_at s t ii
 2. ii = i \<Longrightarrow> \<not> sublist_at s t ii
 3. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
case old \<comment> \<open>Old position, use invariant.\<close>
[PROOF STATE]
proof (state)
this:
ii < i

goal (3 subgoals):
 1. ii < i \<Longrightarrow> \<not> sublist_at s t ii
 2. ii = i \<Longrightarrow> \<not> sublist_at s t ii
 3. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
with \<open>\<forall>ii<i. \<not>sublist_at s t ii\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ii<i. \<not> sublist_at s t ii
ii < i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>ii<i. \<not> sublist_at s t ii
ii < i

goal (1 subgoal):
 1. \<not> sublist_at s t ii
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> sublist_at s t ii

goal (2 subgoals):
 1. ii = i \<Longrightarrow> \<not> sublist_at s t ii
 2. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ii = i \<Longrightarrow> \<not> sublist_at s t ii
 2. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
case current \<comment> \<open>The mismatch occurred while testing this alignment.\<close>
[PROOF STATE]
proof (state)
this:
ii = i

goal (2 subgoals):
 1. ii = i \<Longrightarrow> \<not> sublist_at s t ii
 2. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
with \<open>t!(i+j) \<noteq> s!j\<close>
[PROOF STATE]
proof (chain)
picking this:
t ! (i + j) \<noteq> s ! j
ii = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t ! (i + j) \<noteq> s ! j
ii = i

goal (1 subgoal):
 1. \<not> sublist_at s t ii
[PROOF STEP]
using sublist_all_positions[of s t i]
[PROOF STATE]
proof (prove)
using this:
t ! (i + j) \<noteq> s ! j
ii = i
sublist_at s t i \<Longrightarrow> \<forall>jj<length s. t ! (i + jj) = s ! jj

goal (1 subgoal):
 1. \<not> sublist_at s t ii
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> sublist_at s t ii

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
case skipped \<comment> \<open>The skipped positions.\<close>
[PROOF STATE]
proof (state)
this:
i < ii

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < ii
[PROOF STEP]
have "0<j"
[PROOF STATE]
proof (prove)
using this:
i < ii

goal (1 subgoal):
 1. 0 < j
[PROOF STEP]
using \<open>ii < i'\<close> assignment
[PROOF STATE]
proof (prove)
using this:
i < ii
ii < i'
i' \<equiv> i + (j - \<ff> s j + 1)

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

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < j
[PROOF STEP]
have less_j[simp]: "j + i - ii < j" and le_s: "j + i - ii \<le> length s"
[PROOF STATE]
proof (prove)
using this:
0 < j

goal (1 subgoal):
 1. j + i - ii < j &&& j + i - ii \<le> length s
[PROOF STEP]
using \<open>ii < i'\<close> assms(3) skipped
[PROOF STATE]
proof (prove)
using this:
0 < j
ii < i'
j < length s
i < ii

goal (1 subgoal):
 1. j + i - ii < j &&& j + i - ii \<le> length s
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
j + i - ii < j
j + i - ii \<le> length s

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
note \<ff>_le[simp] = j_le_\<ff>_le[OF assms(3)[THEN less_imp_le]]
[PROOF STATE]
proof (state)
this:
\<ff> s j \<le> j

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
have "0 < \<ff> s j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<ff> s j
[PROOF STEP]
using \<open>0 < j\<close> \<ff>_eq_0_iff_j_eq_0 neq0_conv
[PROOF STATE]
proof (prove)
using this:
0 < j
(\<ff> ?s ?j = 0) = (?j = 0)
(?n \<noteq> 0) = (0 < ?n)

goal (1 subgoal):
 1. 0 < \<ff> s j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < \<ff> s j

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < \<ff> s j
[PROOF STEP]
have "j + i - ii > \<ff> s j - 1"
[PROOF STATE]
proof (prove)
using this:
0 < \<ff> s j

goal (1 subgoal):
 1. \<ff> s j - 1 < j + i - ii
[PROOF STEP]
using \<open>ii < i'\<close> assignment \<ff>_le
[PROOF STATE]
proof (prove)
using this:
0 < \<ff> s j
ii < i'
i' \<equiv> i + (j - \<ff> s j + 1)
\<ff> s j \<le> j

goal (1 subgoal):
 1. \<ff> s j - 1 < j + i - ii
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<ff> s j - 1 < j + i - ii

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<ff> s j - 1 < j + i - ii
[PROOF STEP]
have contradiction_goal: "j + i - ii > length (intrinsic_border (take j s))"
[PROOF STATE]
proof (prove)
using this:
\<ff> s j - 1 < j + i - ii

goal (1 subgoal):
 1. length (intrinsic_border (take j s)) < j + i - ii
[PROOF STEP]
by (metis \<ff>.elims \<open>0 < j\<close> add_diff_cancel_right' not_gr_zero)
[PROOF STATE]
proof (state)
this:
length (intrinsic_border (take j s)) < j + i - ii

goal (1 subgoal):
 1. i < ii \<Longrightarrow> \<not> sublist_at s t ii
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> sublist_at s t ii
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
assume "sublist_at s t ii"
[PROOF STATE]
proof (state)
this:
sublist_at s t ii

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
note sublist_all_positions[OF this]
[PROOF STATE]
proof (state)
this:
\<forall>jj<length s. t ! (ii + jj) = s ! jj

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
with le_s
[PROOF STATE]
proof (chain)
picking this:
j + i - ii \<le> length s
\<forall>jj<length s. t ! (ii + jj) = s ! jj
[PROOF STEP]
have a: "\<forall>jj < j+i-ii. t!(ii+jj) = s!jj"
[PROOF STATE]
proof (prove)
using this:
j + i - ii \<le> length s
\<forall>jj<length s. t ! (ii + jj) = s ! jj

goal (1 subgoal):
 1. \<forall>jj<j + i - ii. t ! (ii + jj) = s ! jj
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>jj<j + i - ii. t ! (ii + jj) = s ! jj

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
have ff1: "\<not> ii < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ii < i
[PROOF STEP]
by (metis not_less_iff_gr_or_eq skipped)
[PROOF STATE]
proof (state)
this:
\<not> ii < i

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> ii < i
[PROOF STEP]
have "i + (ii - i + jj) = ii + jj" for jj
[PROOF STATE]
proof (prove)
using this:
\<not> ii < i

goal (1 subgoal):
 1. i + (ii - i + jj) = ii + jj
[PROOF STEP]
by (metis add.assoc add_diff_inverse_nat)
[PROOF STATE]
proof (state)
this:
i + (ii - i + ?jj) = ii + ?jj

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i + (ii - i + ?jj) = ii + ?jj
[PROOF STEP]
have "\<not> jj < j + i - ii \<or> t ! (ii + jj) = s ! (ii - i + jj)" if "ii - i + jj < j" for jj
[PROOF STATE]
proof (prove)
using this:
i + (ii - i + ?jj) = ii + ?jj

goal (1 subgoal):
 1. \<not> jj < j + i - ii \<or> t ! (ii + jj) = s ! (ii - i + jj)
[PROOF STEP]
using that ff1
[PROOF STATE]
proof (prove)
using this:
i + (ii - i + ?jj) = ii + ?jj
ii - i + jj < j
\<not> ii < i

goal (1 subgoal):
 1. \<not> jj < j + i - ii \<or> t ! (ii + jj) = s ! (ii - i + jj)
[PROOF STEP]
by (metis matches)
[PROOF STATE]
proof (state)
this:
ii - i + ?jj < j \<Longrightarrow> \<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ii - i + ?jj < j \<Longrightarrow> \<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)
[PROOF STEP]
have "\<not> jj < j + i - ii \<or> t ! (ii + jj) = s ! (ii - i + jj)" for jj
[PROOF STATE]
proof (prove)
using this:
ii - i + ?jj < j \<Longrightarrow> \<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)

goal (1 subgoal):
 1. \<not> jj < j + i - ii \<or> t ! (ii + jj) = s ! (ii - i + jj)
[PROOF STEP]
using ff1
[PROOF STATE]
proof (prove)
using this:
ii - i + ?jj < j \<Longrightarrow> \<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)
\<not> ii < i

goal (1 subgoal):
 1. \<not> jj < j + i - ii \<or> t ! (ii + jj) = s ! (ii - i + jj)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
with matches
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<j. t ! (i + jj) = s ! jj
\<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)
[PROOF STEP]
have "\<forall>jj < j+i-ii. t!(ii+jj) = s!(ii-i+jj)"
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<j. t ! (i + jj) = s ! jj
\<not> ?jj < j + i - ii \<or> t ! (ii + ?jj) = s ! (ii - i + ?jj)

goal (1 subgoal):
 1. \<forall>jj<j + i - ii. t ! (ii + jj) = s ! (ii - i + jj)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>jj<j + i - ii. t ! (ii + jj) = s ! (ii - i + jj)

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<j + i - ii. t ! (ii + jj) = s ! (ii - i + jj)
[PROOF STEP]
have "\<forall>jj < j+i-ii. s!jj = s!(ii-i+jj)"
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<j + i - ii. t ! (ii + jj) = s ! (ii - i + jj)

goal (1 subgoal):
 1. \<forall>jj<j + i - ii. s ! jj = s ! (ii - i + jj)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<j + i - ii. t ! (ii + jj) = s ! (ii - i + jj)
\<forall>jj<j + i - ii. t ! (ii + jj) = s ! jj

goal (1 subgoal):
 1. \<forall>jj<j + i - ii. s ! jj = s ! (ii - i + jj)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>jj<j + i - ii. s ! jj = s ! (ii - i + jj)

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>jj<j + i - ii. s ! jj = s ! (ii - i + jj)
[PROOF STEP]
have "\<forall>jj < j+i-ii. (take j s)!jj = (take j s)!(ii-i+jj)"
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<j + i - ii. s ! jj = s ! (ii - i + jj)

goal (1 subgoal):
 1. \<forall>jj<j + i - ii. take j s ! jj = take j s ! (ii - i + jj)
[PROOF STEP]
using \<open>i<ii\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>jj<j + i - ii. s ! jj = s ! (ii - i + jj)
i < ii

goal (1 subgoal):
 1. \<forall>jj<j + i - ii. take j s ! jj = take j s ! (ii - i + jj)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>jj<j + i - ii. take j s ! jj = take j s ! (ii - i + jj)

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
with positions_strict_border[of "j+i-ii" "take j s", simplified]
[PROOF STATE]
proof (chain)
picking this:
\<forall>ja<j + i - ii. take j s ! ja = take j s ! (ii - i + ja) \<Longrightarrow> strict_border (take (j + i - ii) s) (take j s)
\<forall>jj<j + i - ii. take j s ! jj = take j s ! (ii - i + jj)
[PROOF STEP]
have "strict_border (take (j+i-ii) s) (take j s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ja<j + i - ii. take j s ! ja = take j s ! (ii - i + ja) \<Longrightarrow> strict_border (take (j + i - ii) s) (take j s)
\<forall>jj<j + i - ii. take j s ! jj = take j s ! (ii - i + jj)

goal (1 subgoal):
 1. strict_border (take (j + i - ii) s) (take j s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
strict_border (take (j + i - ii) s) (take j s)

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
note intrinsic_border_max[OF this]
[PROOF STATE]
proof (state)
this:
length (take (j + i - ii) s) \<le> length (intrinsic_border (take j s))

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (take (j + i - ii) s) \<le> length (intrinsic_border (take j s))

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
note contradiction_goal
[PROOF STATE]
proof (state)
this:
length (intrinsic_border (take j s)) < j + i - ii

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (intrinsic_border (take j s)) < j + i - ii

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
have "j+i-ii \<le> length s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j + i - ii \<le> length s
[PROOF STEP]
by (fact le_s)
[PROOF STATE]
proof (state)
this:
j + i - ii \<le> length s

goal (1 subgoal):
 1. sublist_at s t ii \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (take (j + i - ii) s) < j + i - ii
j + i - ii \<le> length s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
length (take (j + i - ii) s) < j + i - ii
j + i - ii \<le> length s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> sublist_at s t ii

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> sublist_at s t ii

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kmp_correct: "s \<noteq> []
  \<Longrightarrow> kmp s t \<le> kmp_SPEC s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> kmp s t \<le> kmp_SPEC s t
[PROOF STEP]
unfolding kmp_def kmp_SPEC_def I_outer_def I_in_na_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> ASSERT (s \<noteq> []) \<bind> (\<lambda>_. let i = 0; j = 0; pos = None in WHILE\<^sub>T\<^bsup>\<lambda>(i, j, pos). (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i)\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>\<lambda>(j, pos). case pos of None \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (i + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). let j = j + 1 in if j = length s then RETURN (j, Some i) else RETURN (j, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length s) \<bind> (\<lambda>_. let i = i + (j - \<ff> s j + 1); j = max 0 (\<ff> s j - 1) in RETURN (i, j, None)) else RETURN (i, j, Some i)))) (i, j, pos) \<bind> (\<lambda>(uu_, uu_, pos). RETURN pos)) \<le> SPEC (case_option (\<not> Ex (sublist_at s t)) (\<lambda>i. sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)))
[PROOF STEP]
apply (refine_vcg
    WHILEIT_rule[where R="measure (\<lambda>(i,_,pos). length t - i + (if pos = None then 1 else 0))"]
    WHILEIT_rule[where R="measure (\<lambda>(j,_::nat option). length s - j)"]
    )
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<lbrakk>s \<noteq> []; s \<noteq> []\<rbrakk> \<Longrightarrow> wf (measure (\<lambda>(i, uu_, pos). length t - i + (if pos = None then 1 else 0)))
 2. \<And>x1 x2 x1a x2a ii. \<lbrakk>s \<noteq> []; s \<noteq> []; x2 = (x1a, x2a); (0, 0, None) = (x1, x2); ii < x1\<rbrakk> \<Longrightarrow> \<not> sublist_at s t ii
 3. \<And>x1 x2 x1a x2a. \<lbrakk>s \<noteq> []; s \<noteq> []; x2 = (x1a, x2a); (0, 0, None) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2a of None \<Rightarrow> (\<forall>jj<x1a. t ! (x1 + jj) = s ! jj) \<and> x1a < length s | Some p \<Rightarrow> p = x1 \<and> sublist_at s t x1
 4. \<And>sa a b aa ba. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba)\<rbrakk> \<Longrightarrow> a + length s \<le> length t
 5. \<And>sa a b aa ba. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); a + length s \<le> length t\<rbrakk> \<Longrightarrow> wf (measure (\<lambda>(j, uu_). length s - j))
 6. \<And>sa a b aa ba x1 x2. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); a + length s \<le> length t; (aa, ba) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2 of None \<Rightarrow> x1 < length s \<and> (\<forall>jj<x1. t ! (a + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t a
 7. \<And>sa a b aa ba saa ab bb x1 x2. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); a + length s \<le> length t; case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 = length s; (ab + 1, Some a) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2 of None \<Rightarrow> x1 < length s \<and> (\<forall>jj<x1. t ! (a + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t a
 8. \<And>sa a b aa ba saa ab bb. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); a + length s \<le> length t; case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 = length s\<rbrakk> \<Longrightarrow> ((ab + 1, Some a), saa) \<in> measure (\<lambda>(j, uu_). length s - j)
 9. \<And>sa a b aa ba saa ab bb x1 x2. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); a + length s \<le> length t; case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 \<noteq> length s; (ab + 1, None) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2 of None \<Rightarrow> x1 < length s \<and> (\<forall>jj<x1. t ! (a + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t a
 10. \<And>sa a b aa ba saa ab bb. \<lbrakk>s \<noteq> []; s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> (\<forall>jj<j. t ! (i + jj) = s ! jj) \<and> j < length s | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); a + length s \<le> length t; case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 \<noteq> length s\<rbrakk> \<Longrightarrow> ((ab + 1, None), saa) \<in> measure (\<lambda>(j, uu_). length s - j)
A total of 18 subgoals...
[PROOF STEP]
apply (vc_solve solve: asm_rl)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ab aaa aba. \<lbrakk>s \<noteq> []; Suc (ab + aba) \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) = s ! aba; length s = Suc aba; \<forall>ii<ab. \<not> sublist_at s t ii; aaa < Suc aba\<rbrakk> \<Longrightarrow> sublist_at s t ab
 2. \<And>ab aaa aba jj. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; t ! (ab + aba) = s ! aba; Suc aba \<noteq> length s; \<forall>ii<ab. \<not> sublist_at s t ii; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s; jj < Suc aba\<rbrakk> \<Longrightarrow> t ! (ab + jj) = s ! jj
 3. \<And>ab aaa aba ii. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; ii < Suc (ab + (aba - \<ff> s aba)); \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s; sublist_at s t ii\<rbrakk> \<Longrightarrow> False
 4. \<And>ab aaa aba. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s\<rbrakk> \<Longrightarrow> (\<forall>jj<\<ff> s aba - Suc 0. t ! Suc (ab + (aba - \<ff> s aba) + jj) = s ! jj) \<and> \<ff> s aba - Suc 0 < length s
 5. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> (\<forall>jj<aaa. t ! (ab + jj) = s ! jj) \<and> aaa < length s | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; Suc (ab_ + aba_) \<le> length t; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; t ! (ab_ + aba_) = s ! aba_; length s = Suc aba_; \<forall>ii<ab_. \<not> sublist_at s t ii; aaa_ < Suc aba_\<rbrakk> \<Longrightarrow> sublist_at s t ab_
[PROOF STEP]
by (metis add_Suc_right all_positions_sublist less_antisym)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ab aaa aba jj. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; t ! (ab + aba) = s ! aba; Suc aba \<noteq> length s; \<forall>ii<ab. \<not> sublist_at s t ii; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s; jj < Suc aba\<rbrakk> \<Longrightarrow> t ! (ab + jj) = s ! jj
 2. \<And>ab aaa aba ii. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; ii < Suc (ab + (aba - \<ff> s aba)); \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s; sublist_at s t ii\<rbrakk> \<Longrightarrow> False
 3. \<And>ab aaa aba. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s\<rbrakk> \<Longrightarrow> (\<forall>jj<\<ff> s aba - Suc 0. t ! Suc (ab + (aba - \<ff> s aba) + jj) = s ! jj) \<and> \<ff> s aba - Suc 0 < length s
 4. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> (\<forall>jj<aaa. t ! (ab + jj) = s ! jj) \<and> aaa < length s | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; ab_ + length s \<le> length t; t ! (ab_ + aba_) = s ! aba_; Suc aba_ \<noteq> length s; \<forall>ii<ab_. \<not> sublist_at s t ii; aba_ < length s; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; \<forall>jj<aaa_. t ! (ab_ + jj) = s ! jj; aaa_ < length s; jj_ < Suc aba_\<rbrakk> \<Longrightarrow> t ! (ab_ + jj_) = s ! jj_
[PROOF STEP]
using less_antisym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> ?n < ?m; ?n < Suc ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; ab_ + length s \<le> length t; t ! (ab_ + aba_) = s ! aba_; Suc aba_ \<noteq> length s; \<forall>ii<ab_. \<not> sublist_at s t ii; aba_ < length s; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; \<forall>jj<aaa_. t ! (ab_ + jj) = s ! jj; aaa_ < length s; jj_ < Suc aba_\<rbrakk> \<Longrightarrow> t ! (ab_ + jj_) = s ! jj_
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ab aaa aba ii. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; ii < Suc (ab + (aba - \<ff> s aba)); \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s; sublist_at s t ii\<rbrakk> \<Longrightarrow> False
 2. \<And>ab aaa aba. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s\<rbrakk> \<Longrightarrow> (\<forall>jj<\<ff> s aba - Suc 0. t ! Suc (ab + (aba - \<ff> s aba) + jj) = s ! jj) \<and> \<ff> s aba - Suc 0 < length s
 3. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> (\<forall>jj<aaa. t ! (ab + jj) = s ! jj) \<and> aaa < length s | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal for i jout j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; i + length s \<le> length t; \<forall>jj<j. t ! (i + jj) = s ! jj; t ! (i + j) \<noteq> s ! j; j < length s; ii_ < Suc (i + (j - \<ff> s j)); \<forall>ii<i. \<not> sublist_at s t ii; \<forall>jj<jout. t ! (i + jj) = s ! jj; jout < length s; sublist_at s t ii_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using shift_safe[of i s t j]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>ii<i. \<not> sublist_at s t ii; t ! (i + j) \<noteq> s ! j; j < length s; \<forall>jj<j. t ! (i + jj) = s ! jj\<rbrakk> \<Longrightarrow> \<forall>ii<i + (j - \<ff> s j + 1). \<not> sublist_at s t ii

goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; i + length s \<le> length t; \<forall>jj<j. t ! (i + jj) = s ! jj; t ! (i + j) \<noteq> s ! j; j < length s; ii_ < Suc (i + (j - \<ff> s j)); \<forall>ii<i. \<not> sublist_at s t ii; \<forall>jj<jout. t ! (i + jj) = s ! jj; jout < length s; sublist_at s t ii_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ab aaa aba. \<lbrakk>s \<noteq> []; ab + length s \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) \<noteq> s ! aba; aba < length s; \<forall>ii<ab. \<not> sublist_at s t ii; \<forall>jj<aaa. t ! (ab + jj) = s ! jj; aaa < length s\<rbrakk> \<Longrightarrow> (\<forall>jj<\<ff> s aba - Suc 0. t ! Suc (ab + (aba - \<ff> s aba) + jj) = s ! jj) \<and> \<ff> s aba - Suc 0 < length s
 2. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> (\<forall>jj<aaa. t ! (ab + jj) = s ! jj) \<and> aaa < length s | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal for i jout j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; i + length s \<le> length t; \<forall>jj<j. t ! (i + jj) = s ! jj; t ! (i + j) \<noteq> s ! j; j < length s; \<forall>ii<i. \<not> sublist_at s t ii; \<forall>jj<jout. t ! (i + jj) = s ! jj; jout < length s\<rbrakk> \<Longrightarrow> (\<forall>jj<\<ff> s j - Suc 0. t ! Suc (i + (j - \<ff> s j) + jj) = s ! jj) \<and> \<ff> s j - Suc 0 < length s
[PROOF STEP]
using reuse_matches[of j s t i] \<ff>_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>j \<le> length s; \<forall>jj<j. t ! (i + jj) = s ! jj\<rbrakk> \<Longrightarrow> \<forall>jj<\<ff> s j - 1. t ! (i + (j - \<ff> s j + 1) + jj) = s ! jj
?s \<noteq> [] \<Longrightarrow> \<ff> ?s ?j - 1 < length ?s

goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; i + length s \<le> length t; \<forall>jj<j. t ! (i + jj) = s ! jj; t ! (i + j) \<noteq> s ! j; j < length s; \<forall>ii<i. \<not> sublist_at s t ii; \<forall>jj<jout. t ! (i + jj) = s ! jj; jout < length s\<rbrakk> \<Longrightarrow> (\<forall>jj<\<ff> s j - Suc 0. t ! Suc (i + (j - \<ff> s j) + jj) = s ! jj) \<and> \<ff> s j - Suc 0 < length s
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> (\<forall>jj<aaa. t ! (ab + jj) = s ! jj) \<and> aaa < length s | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; ab_ + length s \<le> length t \<longrightarrow> (\<exists>y. baa_ = Some y); \<forall>ii<ab_. \<not> sublist_at s t ii; case baa_ of None \<Rightarrow> (\<forall>jj<aaa_. t ! (ab_ + jj) = s ! jj) \<and> aaa_ < length s | Some p \<Rightarrow> p = ab_ \<and> sublist_at s t ab_\<rbrakk> \<Longrightarrow> case baa_ of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
by (auto split: option.splits) (metis sublist_lengths add_less_cancel_right leI le_less_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<ff>_butlast[simp]: "j < length s \<Longrightarrow> \<ff> (butlast s) j = \<ff> s j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length s \<Longrightarrow> \<ff> (butlast s) j = \<ff> s j
[PROOF STEP]
by (cases j) (simp_all add: take_butlast)


[STATEMENT]
lemma kmp1_refine: "kmp1 s t \<le> kmp s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp1 s t \<le> kmp s t
[PROOF STEP]
apply (rule refine_IdD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp1 s t \<le> \<Down> Id (kmp s t)
[PROOF STEP]
unfolding kmp1_def kmp_def Let_def compute_\<ff>s_SPEC_def nres_monad_laws
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (s \<noteq> []) \<bind> (\<lambda>_. SPEC (\<lambda>\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)) \<bind> (\<lambda>\<ff>s. WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff>s ! j + 1), max 0 (\<ff>s ! j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y))) \<le> \<Down> Id (ASSERT (s \<noteq> []) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff> s j + 1), max 0 (\<ff> s j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y)))
[PROOF STEP]
apply (intro ASSERT_refine_right ASSERT_refine_left)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. s \<noteq> [] \<Longrightarrow> s \<noteq> []
 2. \<lbrakk>s \<noteq> []; s \<noteq> []\<rbrakk> \<Longrightarrow> SPEC (\<lambda>\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)) \<bind> (\<lambda>\<ff>s. WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff>s ! j + 1), max 0 (\<ff>s ! j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y)) \<le> \<Down> Id (WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff> s j + 1), max 0 (\<ff> s j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; s \<noteq> []\<rbrakk> \<Longrightarrow> SPEC (\<lambda>\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)) \<bind> (\<lambda>\<ff>s. WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff>s ! j + 1), max 0 (\<ff>s ! j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y)) \<le> \<Down> Id (WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff> s j + 1), max 0 (\<ff> s j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y))
[PROOF STEP]
apply (rule Refine_Basic.intro_spec_refine)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<ff>s. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}\<rbrakk> \<Longrightarrow> WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length \<ff>s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff>s ! j + 1), max 0 (\<ff>s ! j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y) \<le> \<Down> Id (WHILE\<^sub>T\<^bsup>I_outer s t\<^esup> (\<lambda>(i, j, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). ASSERT (i + length s \<le> length t) \<bind> (\<lambda>_. WHILE\<^sub>T\<^bsup>I_in_na s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, pos). if j + 1 = length s then RETURN (j + 1, Some i) else RETURN (j + 1, None)) (j, pos) \<bind> (\<lambda>(j, pos). if pos = None then ASSERT (j < length s) \<bind> (\<lambda>_. RETURN (i + (j - \<ff> s j + 1), max 0 (\<ff> s j - 1), None)) else RETURN (i, j, Some i)))) (0, 0, None) \<bind> (\<lambda>(_, uu_, y). RETURN y))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>\<ff>s. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; I_outer s t (0, 0, None)\<rbrakk> \<Longrightarrow> ((0, 0, None), 0, 0, None) \<in> ?R'6 \<ff>s
 2. \<And>\<ff>s x x'. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; I_outer s t x'\<rbrakk> \<Longrightarrow> I_outer s t x
 3. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x1 + length s \<le> length t \<and> x2a = None) = (x1b + length s \<le> length t \<and> x2c = None)
 4. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t\<rbrakk> \<Longrightarrow> x1b + length s \<le> length t
 5. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; I_in_na s t x1 (x1a, x2a)\<rbrakk> \<Longrightarrow> ((x1c, x2c), x1a, x2a) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c
 6. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c; I_in_na s t x1 x'a\<rbrakk> \<Longrightarrow> I_in_na s t x1b xa
 7. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c; I_in_na s t x1b xa; I_in_na s t x1 x'a; xa = (x1d, x2d); x'a = (x1e, x2e)\<rbrakk> \<Longrightarrow> (t ! (x1b + x1d) = s ! x1d \<and> x2d = None) = (t ! (x1 + x1e) = s ! x1e \<and> x2e = None)
 8. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e)\<rbrakk> \<Longrightarrow> (x1e + 1 = length s) = (x1d + 1 = length s)
 9. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e); x1e + 1 = length s; x1d + 1 = length s\<rbrakk> \<Longrightarrow> ((x1e + 1, Some x1b), x1d + 1, Some x1) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c
 10. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> ?R'6 \<ff>s; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e); x1e + 1 \<noteq> length s; x1d + 1 \<noteq> length s\<rbrakk> \<Longrightarrow> ((x1e + 1, None), x1d + 1, None) \<in> ?R'114 \<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c
A total of 15 subgoals...
[PROOF STEP]
apply refine_dref_type
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>\<ff>s. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; I_outer s t (0, 0, None)\<rbrakk> \<Longrightarrow> ((0, 0, None), 0, 0, None) \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel
 2. \<And>\<ff>s x x'. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_outer s t x'\<rbrakk> \<Longrightarrow> I_outer s t x
 3. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x = (x1, x2); x2b = (x1c, x2c); x' = (x1b, x2b)\<rbrakk> \<Longrightarrow> (x1 + length s \<le> length t \<and> x2a = None) = (x1b + length s \<le> length t \<and> x2c = None)
 4. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t\<rbrakk> \<Longrightarrow> x1b + length s \<le> length t
 5. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; I_in_na s t x1 (x1a, x2a)\<rbrakk> \<Longrightarrow> ((x1c, x2c), x1a, x2a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel
 6. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_in_na s t x1 x'a\<rbrakk> \<Longrightarrow> I_in_na s t x1b xa
 7. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; I_in_na s t x1b xa; I_in_na s t x1 x'a; xa = (x1d, x2d); x'a = (x1e, x2e)\<rbrakk> \<Longrightarrow> (t ! (x1b + x1d) = s ! x1d \<and> x2d = None) = (t ! (x1 + x1e) = s ! x1e \<and> x2e = None)
 8. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e)\<rbrakk> \<Longrightarrow> (x1e + 1 = length s) = (x1d + 1 = length s)
 9. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e); x1e + 1 = length s; x1d + 1 = length s\<rbrakk> \<Longrightarrow> ((x1e + 1, Some x1b), x1d + 1, Some x1) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel
 10. \<And>\<ff>s x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e. \<lbrakk>s \<noteq> []; s \<noteq> []; \<ff>s \<in> {\<ff>s. length \<ff>s = length (butlast s) + 1 \<and> (\<forall>j\<le>length (butlast s). \<ff>s ! j = \<ff> (butlast s) j)}; (x, x') \<in> nat_rel \<times>\<^sub>r nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case x of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; case x' of (i, j, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; I_outer s t x; I_outer s t x'; x2 = (x1a, x2a); x' = (x1, x2); x2b = (x1c, x2c); x = (x1b, x2b); x1 + length s \<le> length t; x1b + length s \<le> length t; (xa, x'a) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel; case xa of (j, pos) \<Rightarrow> t ! (x1b + j) = s ! j \<and> pos = None; case x'a of (j, pos) \<Rightarrow> t ! (x1 + j) = s ! j \<and> pos = None; I_in_na s t x1b xa; I_in_na s t x1 x'a; x'a = (x1d, x2d); xa = (x1e, x2e); x1e + 1 \<noteq> length s; x1d + 1 \<noteq> length s\<rbrakk> \<Longrightarrow> ((x1e + 1, None), x1d + 1, None) \<in> nat_rel \<times>\<^sub>r \<langle>nat_rel\<rangle>option_rel
A total of 15 subgoals...
[PROOF STEP]
apply vc_solve
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma take_length_ib[simp]:
  assumes "0 < j" "j \<le> length s"
    shows "take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < j
j \<le> length s
[PROOF STEP]
have "prefix (intrinsic_border (take j s)) (take j s)"
[PROOF STATE]
proof (prove)
using this:
0 < j
j \<le> length s

goal (1 subgoal):
 1. prefix (intrinsic_border (take j s)) (take j s)
[PROOF STEP]
by (metis intrinsic_borderI' border_def list.size(3) neq0_conv not_less strict_border_def take_eq_Nil)
[PROOF STATE]
proof (state)
this:
prefix (intrinsic_border (take j s)) (take j s)

goal (1 subgoal):
 1. take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prefix (intrinsic_border (take j s)) (take j s)

goal (1 subgoal):
 1. take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)
[PROOF STEP]
have "prefix (take j s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (take j s) s
[PROOF STEP]
by (simp add: \<open>j \<le> length s\<close> take_is_prefix)
[PROOF STATE]
proof (state)
this:
prefix (take j s) s

goal (1 subgoal):
 1. take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prefix (intrinsic_border (take j s)) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prefix (intrinsic_border (take j s)) s

goal (1 subgoal):
 1. take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)
[PROOF STEP]
by (metis append_eq_conv_conj prefixE)
[PROOF STATE]
proof (state)
this:
take (length (intrinsic_border (take j s))) s = intrinsic_border (take j s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ib_singleton[simp]: "intrinsic_border [z] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intrinsic_border [z] = []
[PROOF STEP]
by (metis intrinsic_border_less length_Cons length_greater_0_conv less_Suc0 list.size(3))


[STATEMENT]
lemma border_butlast: "border xs ys \<Longrightarrow> border (butlast xs) (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. border xs ys \<Longrightarrow> border (butlast xs) (butlast ys)
[PROOF STEP]
apply (auto simp: border_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prefix xs ys; suffix xs ys\<rbrakk> \<Longrightarrow> prefix (butlast xs) (butlast ys)
 2. \<lbrakk>prefix xs ys; suffix xs ys\<rbrakk> \<Longrightarrow> suffix (butlast xs) (butlast ys)
[PROOF STEP]
apply (metis butlast_append prefixE prefix_order.eq_refl prefix_prefix prefixeq_butlast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix xs ys; suffix xs ys\<rbrakk> \<Longrightarrow> suffix (butlast xs) (butlast ys)
[PROOF STEP]
apply (metis Sublist.suffix_def append.right_neutral butlast.simps(1) butlast_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma border_take_lengths: "i \<le> length s \<Longrightarrow> border (take i s) (take j s) \<Longrightarrow> i \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> length s; border (take i s) (take j s)\<rbrakk> \<Longrightarrow> i \<le> j
[PROOF STEP]
using border_length_le
[PROOF STATE]
proof (prove)
using this:
border ?xs ?ys \<Longrightarrow> length ?xs \<le> length ?ys

goal (1 subgoal):
 1. \<lbrakk>i \<le> length s; border (take i s) (take j s)\<rbrakk> \<Longrightarrow> i \<le> j
[PROOF STEP]
by fastforce


[STATEMENT]
lemma border_step: "border xs ys \<longleftrightarrow> border (xs@[ys!length xs]) (ys@[ys!length xs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. border xs ys = border (xs @ [ys ! length xs]) (ys @ [ys ! length xs])
[PROOF STEP]
apply (auto simp: border_def suffix_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs. \<lbrakk>prefix xs (zs @ xs); ys = zs @ xs; \<not> prefix (xs @ [(zs @ xs) ! length xs]) (zs @ xs)\<rbrakk> \<Longrightarrow> zs = []
 2. \<And>zs. \<lbrakk>ys = zs @ xs; prefix (xs @ [(zs @ xs) ! length xs]) (zs @ xs)\<rbrakk> \<Longrightarrow> prefix xs (zs @ xs)
[PROOF STEP]
using append_one_prefix prefixE
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prefix ?xs ?ys; length ?xs < length ?ys\<rbrakk> \<Longrightarrow> prefix (?xs @ [?ys ! length ?xs]) ?ys
\<lbrakk>prefix ?xs ?ys; \<And>zs. ?ys = ?xs @ zs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<And>zs. \<lbrakk>prefix xs (zs @ xs); ys = zs @ xs; \<not> prefix (xs @ [(zs @ xs) ! length xs]) (zs @ xs)\<rbrakk> \<Longrightarrow> zs = []
 2. \<And>zs. \<lbrakk>ys = zs @ xs; prefix (xs @ [(zs @ xs) ! length xs]) (zs @ xs)\<rbrakk> \<Longrightarrow> prefix xs (zs @ xs)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs. \<lbrakk>ys = zs @ xs; prefix (xs @ [(zs @ xs) ! length xs]) (zs @ xs)\<rbrakk> \<Longrightarrow> prefix xs (zs @ xs)
[PROOF STEP]
using append_prefixD
[PROOF STATE]
proof (prove)
using this:
prefix (?xs @ ?ys) ?zs \<Longrightarrow> prefix ?xs ?zs

goal (1 subgoal):
 1. \<And>zs. \<lbrakk>ys = zs @ xs; prefix (xs @ [(zs @ xs) ! length xs]) (zs @ xs)\<rbrakk> \<Longrightarrow> prefix xs (zs @ xs)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ib_butlast: "length w \<ge> 2 \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
assume "length w \<ge> 2"
[PROOF STATE]
proof (state)
this:
2 \<le> length w

goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> length w
[PROOF STEP]
have "w \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
2 \<le> length w

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

goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> []
[PROOF STEP]
have "strict_border (intrinsic_border w) w"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> []

goal (1 subgoal):
 1. strict_border (intrinsic_border w) w
[PROOF STEP]
by (fact intrinsic_borderI')
[PROOF STATE]
proof (state)
this:
strict_border (intrinsic_border w) w

goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
with \<open>2 \<le> length w\<close>
[PROOF STATE]
proof (chain)
picking this:
2 \<le> length w
strict_border (intrinsic_border w) w
[PROOF STEP]
have "strict_border (butlast (intrinsic_border w)) (butlast w)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> length w
strict_border (intrinsic_border w) w

goal (1 subgoal):
 1. strict_border (butlast (intrinsic_border w)) (butlast w)
[PROOF STEP]
by (metis One_nat_def border_bot.bot.not_eq_extremum butlast.simps(1) len_greater_imp_nonempty length_butlast lessI less_le_trans numerals(2) strict_border_butlast zero_less_diff)
[PROOF STATE]
proof (state)
this:
strict_border (butlast (intrinsic_border w)) (butlast w)

goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_border (butlast (intrinsic_border w)) (butlast w)
[PROOF STEP]
have "length (butlast (intrinsic_border w)) \<le> length (intrinsic_border (butlast w))"
[PROOF STATE]
proof (prove)
using this:
strict_border (butlast (intrinsic_border w)) (butlast w)

goal (1 subgoal):
 1. length (butlast (intrinsic_border w)) \<le> length (intrinsic_border (butlast w))
[PROOF STEP]
using intrinsic_border_max
[PROOF STATE]
proof (prove)
using this:
strict_border (butlast (intrinsic_border w)) (butlast w)
strict_border ?x ?ys \<Longrightarrow> length ?x \<le> length (intrinsic_border ?ys)

goal (1 subgoal):
 1. length (butlast (intrinsic_border w)) \<le> length (intrinsic_border (butlast w))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (butlast (intrinsic_border w)) \<le> length (intrinsic_border (butlast w))

goal (1 subgoal):
 1. 2 \<le> length w \<Longrightarrow> length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (butlast (intrinsic_border w)) \<le> length (intrinsic_border (butlast w))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (butlast (intrinsic_border w)) \<le> length (intrinsic_border (butlast w))

goal (1 subgoal):
 1. length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (intrinsic_border w) \<le> length (intrinsic_border (butlast w)) + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<ff>_step_bound(*rm*):
  assumes "j \<le> length w"
  shows "\<ff> w j \<le> \<ff> w (j-1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<ff> w j \<le> \<ff> w (j - 1) + 1
[PROOF STEP]
using assms[THEN j_le_\<ff>_le] \<ff>_Suc assms
[PROOF STATE]
proof (prove)
using this:
\<ff> w j \<le> j
Suc ?i \<le> length ?w \<Longrightarrow> \<ff> ?w (Suc ?i) \<le> \<ff> ?w ?i + 1
j \<le> length w

goal (1 subgoal):
 1. \<ff> w j \<le> \<ff> w (j - 1) + 1
[PROOF STEP]
by (metis One_nat_def Suc_pred le_SucI not_gr_zero trans_le_add2)


[STATEMENT]
lemma border_take_\<ff>: "border (take (\<ff> s i - 1) s ) (take i s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. border (take (\<ff> s i - 1) s) (take i s)
[PROOF STEP]
apply (cases i, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> border (take (length (intrinsic_border (take (Suc nat) s))) s) (take (Suc nat) s)
[PROOF STEP]
by (metis intrinsic_borderI' border_order.order.eq_iff border_order.less_imp_le border_positions nat.simps(3) nat_le_linear positions_border take_all take_eq_Nil take_length_ib zero_less_Suc)


[STATEMENT]
lemma \<ff>_is_max: "j \<le> length s \<Longrightarrow> strict_border b (take j s) \<Longrightarrow> \<ff> s j \<ge> length b + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> length s; strict_border b (take j s)\<rbrakk> \<Longrightarrow> length b + 1 \<le> \<ff> s j
[PROOF STEP]
by (metis \<ff>.elims add_le_cancel_right add_less_same_cancel2 border_length_r_less intrinsic_border_max length_take min_absorb2 not_add_less2)