Theory ListInterleaving
section "List interleaving"
theory ListInterleaving
imports Main
begin
text ‹
\null
Among the various mathematical tools introduced in his outstanding work on Communicating Sequential
Processes \<^cite>‹"R2"›, Hoare has defined \emph{interleaves} as the predicate satisfied by any three
lists \emph{s}, \emph{t}, emph{u} such that \emph{s} may be split into sublists alternately
extracted from \emph{t} and \emph{u}, whatever is the criterion for extracting an item from either
\emph{t} or \emph{u} in each step.
This paper enriches Hoare's definition by identifying such criterion with the truth value of a
predicate taking as inputs the head and the tail of \emph{s}. This enhanced \emph{interleaves}
predicate turns out to permit the proof of equalities between lists without the need of an
induction. Some rules that allow to infer \emph{interleaves} statements without induction,
particularly applying to the addition of a prefix to the input lists, are also proven. Finally, a
stronger version of the predicate, named \emph{Interleaves}, is shown to fulfil further rules
applying to the addition of a suffix to the input lists.
Throughout this paper, the salient points of definitions and proofs are commented; for additional
information, cf. Isabelle documentation, particularly \<^cite>‹"R3"›, \<^cite>‹"R4"›, \<^cite>‹"R5"›, and
\<^cite>‹"R6"›. For a sample nontrivial application of the mathematical machinery developed in this
paper, cf. \<^cite>‹"R1"›.
›
subsection "A first version of interleaving"
text ‹
Here below is the definition of predicate ‹interleaves›, as well as of a convenient symbolic
notation for it. As in the definition of predicate \emph{interleaves} formulated in \<^cite>‹"R2"›, the
recursive decomposition of the input lists is performed by item prepending. In the case of a list
‹ws› constructed recursively by item appending rather than prepending, the statement that it
satisfies predicate ‹interleaves› with two further lists can nevertheless be proven by
induction using as input @{term "rev ws"}, rather than ‹ws› itself.
With respect to Hoare's homonymous predicate, ‹interleaves› takes as an additional input a
predicate ‹P›, which is a function of a single item and a list. Then, for statement
@{term "interleaves P (x # xs) (y # ys) (z # zs)"} to hold, the item picked for being ‹x› must
be ‹y› if ‹P x xs›, ‹z› otherwise. On the contrary, in case either the second or
the third list is empty, the truth value of ‹P x xs› does not matter and list
@{term "x # xs"} just has to match the other nonempty one, if any.
\null
›
fun interleaves ::
"('a ⇒ 'a list ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ bool" where
"interleaves P (x # xs) (y # ys) (z # zs) = (if P x xs
then x = y ∧ interleaves P xs ys (z # zs)
else x = z ∧ interleaves P xs (y # ys) zs)" |
"interleaves P (x # xs) (y # ys) [] =
(x = y ∧ interleaves P xs ys [])" |
"interleaves P (x # xs) [] (z # zs) =
(x = z ∧ interleaves P xs [] zs)" |
"interleaves _ (_ # _) [] [] = False" |
"interleaves _ [] (_ # _) _ = False" |
"interleaves _ [] _ (_ # _) = False" |
"interleaves _ [] [] [] = True"
abbreviation interleaves_syntax ::
"'a list ⇒ 'a list ⇒ 'a list ⇒ ('a ⇒ 'a list ⇒ bool) ⇒ bool"
("(_ ≃ {_, _, _})" [60, 60, 60] 51)
where "xs ≃ {ys, zs, P} ≡ interleaves P xs ys zs"
text ‹
\null
The advantage provided by this enhanced \emph{interleaves} predicate is that in case
@{term "xs ≃ {ys, zs, P}"}, fixing the values of ‹xs› and either ‹ys› or ‹zs› has
the effect of fixing the value of the remaining list, too. Namely, if @{term "xs ≃ {ys', zs, P}"}
also holds, then @{term "ys = ys'"}, and likewise, if @{term "xs ≃ {ys, zs', P}"} also holds, then
@{term "zs = zs'"}. Therefore, once two \emph{interleaves} statements @{term "xs ≃ {ys, zs, P}"},
@{term "xs' ≃ {ys', zs', P'}"} have been proven along with equalities @{term "xs = xs'"},
@{term "P = P'"}, and either @{term "zs = zs'"} or @{term "ys = ys'"}, possibly by induction, the
remaining equality, i.e. respectively @{term "ys = ys'"} and @{term "zs = zs'"}, can be inferred
without the need of a further induction.
Here below is the proof of this property as well as of other ones. Particularly, it is also proven
that in case @{term "xs ≃ {ys, zs, P}"}, lists ‹ys› and ‹zs› can be swapped by
replacing predicate ‹P› with its negation.
It is worth noting that fixing the values of ‹ys› and ‹zs› does not fix the value of
‹xs› instead. A counterexample is @{term "ys = [y]"}, @{term "zs = [z]"} with @{term "y ≠ z"},
@{term "P y [z] = True"}, @{term "P z [y] = False"}, in which case both of the \emph{interleaves}
statements @{term "[y, z] ≃ {ys, zs, P}"} and @{term "[z, y] ≃ {ys, zs, P}"} hold.
\null
›
lemma interleaves_length [rule_format]:
"xs ≃ {ys, zs, P} ⟶ length xs = length ys + length zs"
proof (induction P xs ys zs rule: interleaves.induct, simp_all)
qed (rule conjI, (rule_tac [!] impI)+, simp_all)
lemma interleaves_nil:
"[] ≃ {ys, zs, P} ⟹ ys = [] ∧ zs = []"
by (rule interleaves.cases [of "(P, [], ys, zs)"], simp_all)
lemma interleaves_swap:
"xs ≃ {ys, zs, P} = xs ≃ {zs, ys, λw ws. ¬ P w ws}"
proof (induction P xs ys zs rule: interleaves.induct, simp_all)
fix y' :: 'a and ys' zs' P'
show "¬ [] ≃ {zs', y' # ys', λw ws. ¬ P' w ws}" by (cases zs', simp_all)
qed
lemma interleaves_equal_fst [rule_format]:
"xs ≃ {ys, zs, P} ⟶ xs ≃ {ys', zs, P} ⟶ ys = ys'"
proof (induction xs arbitrary: ys ys' zs, (rule_tac [!] impI)+)
fix ys ys' zs
assume "[] ≃ {ys, zs, P}"
hence "ys = [] ∧ zs = []" by (rule interleaves_nil)
moreover assume "[] ≃ {ys', zs, P}"
hence "ys' = [] ∧ zs = []" by (rule interleaves_nil)
ultimately show "ys = ys'" by simp
next
fix x xs ys ys' zs
assume
A: "⋀ys ys' zs. xs ≃ {ys, zs, P} ⟶ xs ≃ {ys', zs, P} ⟶ ys = ys'" and
B: "x # xs ≃ {ys, zs, P}" and
B': "x # xs ≃ {ys', zs, P}"
show "ys = ys'"
proof (cases zs, case_tac [2] ys, case_tac [2-3] ys', simp_all)
assume C: "zs = []"
hence "∃w ws. ys = w # ws" using B by (cases ys, simp_all)
then obtain w ws where Y: "ys = w # ws" by blast
hence D: "w = x" using B and C by simp
have "xs ≃ {ws, [], P}" using B and C and Y by simp
moreover have "∃w' ws'. ys' = w' # ws'"
using B' and C by (cases ys', simp_all)
then obtain w' ws' where Y': "ys' = w' # ws'" by blast
hence D': "w' = x" using B' and C by simp
have "xs ≃ {ws', [], P}" using B' and C and Y' by simp
moreover have "xs ≃ {ws, [], P} ⟶ xs ≃ {ws', [], P} ⟶ ws = ws'"
using A .
ultimately have "ws = ws'" by simp
with Y and Y' and D and D' show ?thesis by simp
next
fix v vs w' ws'
assume C: "zs = v # vs" and "ys = []"
hence D: "xs ≃ {[], vs, P}" using B by simp
assume E: "ys' = w' # ws'"
have "P x xs ∨ ¬ P x xs" by simp
moreover {
assume "P x xs"
hence "xs ≃ {ws', v # vs, P}" using B' and C and E by simp
hence "length xs = Suc (length vs) + length ws'"
by (simp add: interleaves_length)
moreover have "length xs = length vs"
using D by (simp add: interleaves_length)
ultimately have False by simp
}
moreover {
assume "¬ P x xs"
hence "xs ≃ {w' # ws', vs, P}" using B' and C and E by simp
moreover have "xs ≃ {[], vs, P} ⟶ xs ≃ {w' # ws', vs, P} ⟶
[] = w' # ws'"
using A .
ultimately have "[] = w' # ws'" using D by simp
hence False by simp
}
ultimately show False ..
next
fix v vs w ws
assume C: "zs = v # vs" and "ys' = []"
hence D: "xs ≃ {[], vs, P}" using B' by simp
assume E: "ys = w # ws"
have "P x xs ∨ ¬ P x xs" by simp
moreover {
assume "P x xs"
hence "xs ≃ {ws, v # vs, P}" using B and C and E by simp
hence "length xs = Suc (length vs) + length ws"
by (simp add: interleaves_length)
moreover have "length xs = length vs"
using D by (simp add: interleaves_length)
ultimately have False by simp
}
moreover {
assume "¬ P x xs"
hence "xs ≃ {w # ws, vs, P}" using B and C and E by simp
moreover have "xs ≃ {[], vs, P} ⟶ xs ≃ {w # ws, vs, P} ⟶ [] = w # ws"
using A .
ultimately have "[] = w # ws" using D by simp
hence False by simp
}
ultimately show False ..
next
fix v vs w ws w' ws'
assume C: "zs = v # vs" and D: "ys = w # ws" and D': "ys' = w' # ws'"
have "P x xs ∨ ¬ P x xs" by simp
moreover {
assume E: "P x xs"
hence F: "w = x" using B and C and D by simp
have "xs ≃ {ws, v # vs, P}" using B and C and D and E by simp
moreover have F': "w' = x" using B' and C and D' and E by simp
have "xs ≃ {ws', v # vs, P}" using B' and C and D' and E by simp
moreover have "xs ≃ {ws, v # vs, P} ⟶ xs ≃ {ws', v # vs, P} ⟶
ws = ws'"
using A .
ultimately have "ws = ws'" by simp
hence "w = w' ∧ ws = ws'" using F and F' by simp
}
moreover {
assume E: "¬ P x xs"
hence "xs ≃ {w # ws, vs, P}" using B and C and D by simp
moreover have "xs ≃ {w' # ws', vs, P}"
using B' and C and D' and E by simp
moreover have "xs ≃ {w # ws, vs, P} ⟶ xs ≃ {w' # ws', vs, P} ⟶
w # ws = w' # ws'"
using A .
ultimately have "w # ws = w' # ws'" by simp
hence "w = w' ∧ ws = ws'" by simp
}
ultimately show "w = w' ∧ ws = ws'" ..
qed
qed
lemma interleaves_equal_snd:
"xs ≃ {ys, zs, P} ⟹ xs ≃ {ys, zs', P} ⟹ zs = zs'"
by (subst (asm) (1 2) interleaves_swap, rule interleaves_equal_fst)
text ‹
\null
Since \emph{interleaves} statements permit to prove equalities between lists without the need of an
induction, it is useful to search for rules that allow to infer such statements themselves without
induction, which is precisely what is done here below. Particularly, it is proven that under proper
assumptions, predicate @{term interleaves} keeps being satisfied by applying a filter, a mapping, or
the addition or removal of a prefix to the input lists.
\null
›
lemma interleaves_all_nil:
"xs ≃ {xs, [], P}"
by (induction xs, simp_all)
lemma interleaves_nil_all:
"xs ≃ {[], xs, P}"
by (induction xs, simp_all)
lemma interleaves_equal_all_nil:
"xs ≃ {ys, [], P} ⟹ xs = ys"
by (insert interleaves_all_nil, rule interleaves_equal_fst)
lemma interleaves_equal_nil_all:
"xs ≃ {[], zs, P} ⟹ xs = zs"
by (insert interleaves_nil_all, rule interleaves_equal_snd)
lemma interleaves_filter [rule_format]:
assumes A: "∀x xs. P x (filter Q xs) = P x xs"
shows "xs ≃ {ys, zs, P} ⟶ filter Q xs ≃ {filter Q ys, filter Q zs, P}"
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp)
fix ys zs
assume "[] ≃ {ys, zs, P}"
hence "ys = [] ∧ zs = []" by (rule interleaves_nil)
thus "[] ≃ {filter Q ys, filter Q zs, P}" by simp
next
fix x xs ys zs
assume
B: "⋀ys' zs'. xs ≃ {ys', zs', P} ⟶
filter Q xs ≃ {filter Q ys', filter Q zs', P}" and
C: "x # xs ≃ {ys, zs, P}"
show "filter Q (x # xs) ≃ {filter Q ys, filter Q zs, P}"
proof (cases ys, case_tac [!] zs, simp_all del: filter.simps, rule ccontr)
assume "ys = []" and "zs = []"
thus False using C by simp
next
fix z zs'
assume "ys = []" and "zs = z # zs'"
hence D: "x = z ∧ xs ≃ {[], zs', P}" using C by simp
moreover have "xs ≃ {[], zs', P} ⟶
filter Q xs ≃ {filter Q [], filter Q zs', P}"
using B .
ultimately have "filter Q xs ≃ {[], filter Q zs', P}" by simp
thus "filter Q (x # xs) ≃ {[], filter Q (z # zs'), P}" using D by simp
next
fix y ys'
assume "ys = y # ys'" and "zs = []"
hence D: "x = y ∧ xs ≃ {ys', [], P}" using C by simp
moreover have "xs ≃ {ys', [], P} ⟶
filter Q xs ≃ {filter Q ys', filter Q [], P}"
using B .
ultimately have "filter Q xs ≃ {filter Q ys', [], P}" by simp
thus "filter Q (x # xs) ≃ {filter Q (y # ys'), [], P}" using D by simp
next
fix y ys' z zs'
assume "ys = y # ys'" and "zs = z # zs'"
hence D: "x # xs ≃ {y # ys', z # zs', P}" using C by simp
show "filter Q (x # xs) ≃ {filter Q (y # ys'), filter Q (z # zs'), P}"
proof (cases "P x xs")
case True
hence E: "P x (filter Q xs)" using A by simp
have F: "x = y ∧ xs ≃ {ys', z # zs', P}" using D and True by simp
moreover have "xs ≃ {ys', z # zs', P} ⟶
filter Q xs ≃ {filter Q ys', filter Q (z # zs'), P}"
using B .
ultimately have G: "filter Q xs ≃ {filter Q ys', filter Q (z # zs'), P}"
by simp
show ?thesis
proof (cases "Q x")
assume "Q x"
hence "filter Q (x # xs) = x # filter Q xs" by simp
moreover have "filter Q (y # ys') = x # filter Q ys'"
using ‹Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (z # zs')", simp_all)
next
assume "¬ Q x"
hence "filter Q (x # xs) = filter Q xs" by simp
moreover have "filter Q (y # ys') = filter Q ys'"
using ‹¬ Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (z # zs')", simp_all)
qed
next
case False
hence E: "¬ P x (filter Q xs)" using A by simp
have F: "x = z ∧ xs ≃ {y # ys', zs', P}" using D and False by simp
moreover have "xs ≃ {y # ys', zs', P} ⟶
filter Q xs ≃ {filter Q (y # ys'), filter Q zs', P}"
using B .
ultimately have G: "filter Q xs ≃ {filter Q (y # ys'), filter Q zs', P}"
by simp
show ?thesis
proof (cases "Q x")
assume "Q x"
hence "filter Q (x # xs) = x # filter Q xs" by simp
moreover have "filter Q (z # zs') = x # filter Q zs'"
using ‹Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (y # ys')", simp_all)
next
assume "¬ Q x"
hence "filter Q (x # xs) = filter Q xs" by simp
moreover have "filter Q (z # zs') = filter Q zs'"
using ‹¬ Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (z # zs')", simp_all)
qed
qed
qed
qed
lemma interleaves_map [rule_format]:
assumes A: "inj f"
shows "xs ≃ {ys, zs, P} ⟶
map f xs ≃ {map f ys, map f zs, λw ws. P (inv f w) (map (inv f) ws)}"
(is "_ ⟶ _ ≃ {_, _, ?P'}")
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp_all)
fix ys zs
assume "[] ≃ {ys, zs, P}"
hence "ys = [] ∧ zs = []" by (rule interleaves_nil)
thus "[] ≃ {map f ys, map f zs, ?P'}" by simp
next
fix x xs ys zs
assume
B: "⋀ys zs. xs ≃ {ys, zs, P} ⟶ map f xs ≃ {map f ys, map f zs, ?P'}" and
C: "x # xs ≃ {ys, zs, P}"
show "f x # map f xs ≃ {map f ys, map f zs, ?P'}"
proof (cases ys, case_tac [!] zs, simp_all del: interleaves.simps(1))
assume "ys = []" and "zs = []"
thus False using C by simp
next
fix z zs'
assume "ys = []" and "zs = z # zs'"
hence "x = z ∧ xs ≃ {[], zs', P}" using C by simp
moreover have "xs ≃ {[], zs', P} ⟶ map f xs ≃ {map f [], map f zs', ?P'}"
using B .
ultimately show "f x = f z ∧ map f xs ≃ {[], map f zs', ?P'}" by simp
next
fix y ys'
assume "ys = y # ys'" and "zs = []"
hence "x = y ∧ xs ≃ {ys', [], P}" using C by simp
moreover have "xs ≃ {ys', [], P} ⟶ map f xs ≃ {map f ys', map f [], ?P'}"
using B .
ultimately show "f x = f y ∧ map f xs ≃ {map f ys', [], ?P'}" by simp
next
fix y ys' z zs'
assume "ys = y # ys'" and "zs = z # zs'"
hence D: "x # xs ≃ {y # ys', z # zs', P}" using C by simp
show "f x # map f xs ≃ {f y # map f ys', f z # map f zs', ?P'}"
proof (cases "P x xs")
case True
hence E: "?P' (f x) (map f xs)" using A by simp
have "x = y ∧ xs ≃ {ys', z # zs', P}" using D and True by simp
moreover have "xs ≃ {ys', z # zs', P} ⟶
map f xs ≃ {map f ys', map f (z # zs'), ?P'}"
using B .
ultimately have "f x = f y ∧ map f xs ≃ {map f ys', map f (z # zs'), ?P'}"
by simp
thus ?thesis using E by simp
next
case False
hence E: "¬ ?P' (f x) (map f xs)" using A by simp
have "x = z ∧ xs ≃ {y # ys', zs', P}" using D and False by simp
moreover have "xs ≃ {y # ys', zs', P} ⟶
map f xs ≃ {map f (y # ys'), map f zs', ?P'}"
using B .
ultimately have "f x = f z ∧ map f xs ≃ {map f (y # ys'), map f zs', ?P'}"
by simp
thus ?thesis using E by simp
qed
qed
qed
lemma interleaves_prefix_fst_1 [rule_format]:
assumes A: "xs ≃ {ys, zs, P}"
shows "(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
ws @ xs ≃ {ws @ ys, zs, P}"
proof (induction ws, simp_all add: A, rule impI)
fix w ws
assume B: "∀n < Suc (length ws). P ((w # ws) ! n) (drop n ws @ xs)"
assume "(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
ws @ xs ≃ {ws @ ys, zs, P}"
moreover have "∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)"
proof (rule allI, rule impI)
fix n
assume "n < length ws"
moreover have "Suc n < Suc (length ws) ⟶
P ((w # ws) ! (Suc n)) (drop (Suc n) ws @ xs)"
using B ..
ultimately show "P (ws ! n) (drop (Suc n) ws @ xs)" by simp
qed
ultimately have "ws @ xs ≃ {ws @ ys, zs, P}" ..
moreover have "0 < Suc (length ws) ⟶ P ((w # ws) ! 0) (drop 0 ws @ xs)"
using B ..
hence "P w (ws @ xs)" by simp
ultimately show "w # ws @ xs ≃ {w # ws @ ys, zs, P}" by (cases zs, simp_all)
qed
lemma interleaves_prefix_fst_2 [rule_format]:
"ws @ xs ≃ {ws @ ys, zs, P} ⟶
(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
xs ≃ {ys, zs, P}"
proof (induction ws, simp_all, (rule impI)+)
fix w ws
assume A: "∀n < Suc (length ws). P ((w # ws) ! n) (drop n ws @ xs)"
hence "0 < Suc (length ws) ⟶ P ((w # ws) ! 0) (drop 0 ws @ xs)" ..
hence "P w (ws @ xs)" by simp
moreover assume "w # ws @ xs ≃ {w # ws @ ys, zs, P}"
ultimately have "ws @ xs ≃ {ws @ ys, zs, P}" by (cases zs, simp_all)
moreover assume "ws @ xs ≃ {ws @ ys, zs, P} ⟶
(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
xs ≃ {ys, zs, P}"
ultimately have "(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
xs ≃ {ys, zs, P}"
by simp
moreover have "∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)"
proof (rule allI, rule impI)
fix n
assume "n < length ws"
moreover have "Suc n < Suc (length ws) ⟶
P ((w # ws) ! (Suc n)) (drop (Suc n) ws @ xs)"
using A ..
ultimately show "P (ws ! n) (drop (Suc n) ws @ xs)" by simp
qed
ultimately show "xs ≃ {ys, zs, P}" ..
qed
lemma interleaves_prefix_fst [rule_format]:
"∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs) ⟹
xs ≃ {ys, zs, P} = ws @ xs ≃ {ws @ ys, zs, P}"
proof (rule iffI, erule interleaves_prefix_fst_1, simp)
qed (erule interleaves_prefix_fst_2, simp)
lemma interleaves_prefix_snd [rule_format]:
"∀n < length ws. ¬ P (ws ! n) (drop (Suc n) ws @ xs) ⟹
xs ≃ {ys, zs, P} = ws @ xs ≃ {ys, ws @ zs, P}"
proof (subst (1 2) interleaves_swap)
qed (rule interleaves_prefix_fst, simp)
subsection "A second, stronger version of interleaving"
text ‹
Simple counterexamples show that unlike prefixes, the addition or removal of suffixes to the input
lists does not generally preserve the validity of predicate @{term interleaves}. In fact, if
@{term "P y [x] = True"} with @{term "x ≠ y"}, then @{term "[y, x] ≃ {[x], [y], P}"} does not hold
although @{term "[y] ≃ {[], [y], λw ws. P w (ws @ [x])}"} does, by virtue of lemma
@{thm interleaves_nil_all}. Similarly, @{term "[x, y] ≃ {[], [y, x], λw ws. P w (ws @ [x])}"} does
not hold for @{term "x ≠ y"} even though @{term "[x, y, x] ≃ {[x], [y, x], P}"} does.
Both counterexamples would not work any longer if the truth value of the input predicate were
significant even if either the second or the third list is empty. In fact, in the former case,
condition @{term "P y [x] = True"} would entail the falseness of statement
@{term "[y] ≃ {[], [y], λw ws. P w (ws @ [x])}"}, so that the validity of rule
@{term "[y] ≃ {[], [y], λw ws. P w (ws @ [x])} ⟹ [y, x] ≃ {[x], [y], P}"} would be preserved. In
the latter case, statement @{term "[x, y, x] ≃ {[x], [y, x], P}"} may only hold provided the last
item ‹x› of the first list is extracted from the third one, which would require that
@{term "¬ P x []"}; thus, subordinating rule
@{term "[x, y, x] ≃ {[x], [y, x], P} ⟹ [x, y] ≃ {[], [y, x], λw ws. P w (ws @ [x])}"} to
condition @{term "P x []"} would preserve its validity.
This argument suggests that in order to obtain an \emph{interleaves} predicate whose validity is
also preserved upon the addition or removal of a suffix to the input lists, the truth value of the
input predicate must matter until both the second and the third list are empty. In what follows,
such a stronger version of the predicate, named ‹Interleaves›, is defined along with a
convenient symbolic notation for it.
\null
›
fun Interleaves ::
"('a ⇒ 'a list ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ bool" where
"Interleaves P (x # xs) (y # ys) (z # zs) = (if P x xs
then x = y ∧ Interleaves P xs ys (z # zs)
else x = z ∧ Interleaves P xs (y # ys) zs)" |
"Interleaves P (x # xs) (y # ys) [] =
(P x xs ∧ x = y ∧ Interleaves P xs ys [])" |
"Interleaves P (x # xs) [] (z # zs) =
(¬ P x xs ∧ x = z ∧ Interleaves P xs [] zs)" |
"Interleaves _ (_ # _) [] [] = False" |
"Interleaves _ [] (_ # _) _ = False" |
"Interleaves _ [] _ (_ # _) = False" |
"Interleaves _ [] [] [] = True"
abbreviation Interleaves_syntax ::
"'a list ⇒ 'a list ⇒ 'a list ⇒ ('a ⇒ 'a list ⇒ bool) ⇒ bool"
("(_ ≅ {_, _, _})" [60, 60, 60] 51)
where "xs ≅ {ys, zs, P} ≡ Interleaves P xs ys zs"
text ‹
\null
In what follows, it is proven that predicate @{term Interleaves} is actually not weaker than, viz.
is a sufficient condition for, predicate @{term interleaves}. Moreover, the former predicate is
shown to fulfil the same rules as the latter, although sometimes under more stringent assumptions
(cf. lemmas ‹Interleaves_all_nil›, ‹Interleaves_nil_all› with lemmas
@{thm interleaves_all_nil}, @{thm interleaves_nil_all}), and to have the further property that under
proper assumptions, its validity is preserved upon the addition or removal of a suffix to the input
lists.
\null
›
lemma Interleaves_interleaves [rule_format]:
"xs ≅ {ys, zs, P} ⟶ xs ≃ {ys, zs, P}"
proof (induction P xs ys zs rule: interleaves.induct, simp_all)
qed (rule conjI, (rule_tac [!] impI)+, simp_all)
lemma Interleaves_length:
"xs ≅ {ys, zs, P} ⟹ length xs = length ys + length zs"
by (drule Interleaves_interleaves, rule interleaves_length)
lemma Interleaves_nil:
"[] ≅ {ys, zs, P} ⟹ ys = [] ∧ zs = []"
by (drule Interleaves_interleaves, rule interleaves_nil)
lemma Interleaves_swap:
"xs ≅ {ys, zs, P} = xs ≅ {zs, ys, λw ws. ¬ P w ws}"
proof (induction P xs ys zs rule: Interleaves.induct, simp_all)
fix y' :: 'a and ys' zs' P'
show "¬ [] ≅ {zs', y' # ys', λw ws. ¬ P' w ws}" by (cases zs', simp_all)
qed
lemma Interleaves_equal_fst:
"xs ≅ {ys, zs, P} ⟹ xs ≅ {ys', zs, P} ⟹ ys = ys'"
by ((drule Interleaves_interleaves)+, rule interleaves_equal_fst)
lemma Interleaves_equal_snd:
"xs ≅ {ys, zs, P} ⟹ xs ≅ {ys, zs', P} ⟹ zs = zs'"
by ((drule Interleaves_interleaves)+, rule interleaves_equal_snd)
lemma Interleaves_equal_all_nil:
"xs ≅ {ys, [], P} ⟹ xs = ys"
by (drule Interleaves_interleaves, rule interleaves_equal_all_nil)
lemma Interleaves_equal_nil_all:
"xs ≅ {[], zs, P} ⟹ xs = zs"
by (drule Interleaves_interleaves, rule interleaves_equal_nil_all)
lemma Interleaves_filter [rule_format]:
assumes A: "∀x xs. P x (filter Q xs) = P x xs"
shows "xs ≅ {ys, zs, P} ⟶ filter Q xs ≅ {filter Q ys, filter Q zs, P}"
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp)
fix ys zs
assume "[] ≅ {ys, zs, P}"
hence "ys = [] ∧ zs = []" by (rule Interleaves_nil)
thus "[] ≅ {filter Q ys, filter Q zs, P}" by simp
next
fix x xs ys zs
assume
B: "⋀ys' zs'. xs ≅ {ys', zs', P} ⟶
filter Q xs ≅ {filter Q ys', filter Q zs', P}" and
C: "x # xs ≅ {ys, zs, P}"
show "filter Q (x # xs) ≅ {filter Q ys, filter Q zs, P}"
proof (cases ys, case_tac [!] zs, simp_all del: filter.simps, rule ccontr)
assume "ys = []" and "zs = []"
thus False using C by simp
next
fix z zs'
assume "ys = []" and "zs = z # zs'"
hence D: "¬ P x xs ∧ x = z ∧ xs ≅ {[], zs', P}" using C by simp+
moreover have "xs ≅ {[], zs', P} ⟶
filter Q xs ≅ {filter Q [], filter Q zs', P}"
using B .
ultimately have "filter Q xs ≅ {[], filter Q zs', P}" by simp
moreover have "¬ P x (filter Q xs)" using A and D by simp+
ultimately show "filter Q (x # xs) ≅ {[], filter Q (z # zs'), P}"
using D by simp
next
fix y ys'
assume "ys = y # ys'" and "zs = []"
hence D: "P x xs ∧ x = y ∧ xs ≅ {ys', [], P}" using C by simp+
moreover have "xs ≅ {ys', [], P} ⟶
filter Q xs ≅ {filter Q ys', filter Q [], P}"
using B .
ultimately have "filter Q xs ≅ {filter Q ys', [], P}" by simp
moreover have "P x (filter Q xs)" using A and D by simp+
ultimately show "filter Q (x # xs) ≅ {filter Q (y # ys'), [], P}"
using D by simp
next
fix y ys' z zs'
assume "ys = y # ys'" and "zs = z # zs'"
hence D: "x # xs ≅ {y # ys', z # zs', P}" using C by simp
show "filter Q (x # xs) ≅ {filter Q (y # ys'), filter Q (z # zs'), P}"
proof (cases "P x xs")
case True
hence E: "P x (filter Q xs)" using A by simp
have F: "x = y ∧ xs ≅ {ys', z # zs', P}" using D and True by simp
moreover have "xs ≅ {ys', z # zs', P} ⟶
filter Q xs ≅ {filter Q ys', filter Q (z # zs'), P}"
using B .
ultimately have G: "filter Q xs ≅ {filter Q ys', filter Q (z # zs'), P}"
by simp
show ?thesis
proof (cases "Q x")
assume "Q x"
hence "filter Q (x # xs) = x # filter Q xs" by simp
moreover have "filter Q (y # ys') = x # filter Q ys'"
using ‹Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (z # zs')", simp_all)
next
assume "¬ Q x"
hence "filter Q (x # xs) = filter Q xs" by simp
moreover have "filter Q (y # ys') = filter Q ys'"
using ‹¬ Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (z # zs')", simp_all)
qed
next
case False
hence E: "¬ P x (filter Q xs)" using A by simp
have F: "x = z ∧ xs ≅ {y # ys', zs', P}" using D and False by simp
moreover have "xs ≅ {y # ys', zs', P} ⟶
filter Q xs ≅ {filter Q (y # ys'), filter Q zs', P}"
using B .
ultimately have G: "filter Q xs ≅ {filter Q (y # ys'), filter Q zs', P}"
by simp
show ?thesis
proof (cases "Q x")
assume "Q x"
hence "filter Q (x # xs) = x # filter Q xs" by simp
moreover have "filter Q (z # zs') = x # filter Q zs'"
using ‹Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (y # ys')", simp_all)
next
assume "¬ Q x"
hence "filter Q (x # xs) = filter Q xs" by simp
moreover have "filter Q (z # zs') = filter Q zs'"
using ‹¬ Q x› and F by simp
ultimately show ?thesis using E and G
by (cases "filter Q (z # zs')", simp_all)
qed
qed
qed
qed
lemma Interleaves_map [rule_format]:
assumes A: "inj f"
shows "xs ≅ {ys, zs, P} ⟶
map f xs ≅ {map f ys, map f zs, λw ws. P (inv f w) (map (inv f) ws)}"
(is "_ ⟶ _ ≅ {_, _, ?P'}")
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp_all)
fix ys zs
assume "[] ≅ {ys, zs, P}"
hence "ys = [] ∧ zs = []" by (rule Interleaves_nil)
thus "[] ≅ {map f ys, map f zs, ?P'}" by simp
next
fix x xs ys zs
assume
B: "⋀ys zs. xs ≅ {ys, zs, P} ⟶ map f xs ≅ {map f ys, map f zs, ?P'}" and
C: "x # xs ≅ {ys, zs, P}"
show "f x # map f xs ≅ {map f ys, map f zs, ?P'}"
proof (cases ys, case_tac [!] zs, simp_all del: Interleaves.simps(1-3))
assume "ys = []" and "zs = []"
thus False using C by simp
next
fix z zs'
assume "ys = []" and "zs = z # zs'"
hence D: "¬ P x xs ∧ x = z ∧ xs ≅ {[], zs', P}" using C by simp+
moreover have "xs ≅ {[], zs', P} ⟶ map f xs ≅ {map f [], map f zs', ?P'}"
using B .
ultimately have "map f xs ≅ {[], map f zs', ?P'}" by simp
moreover have "¬ ?P' (f x) (map f xs)" using A and D by simp+
ultimately show "f x # map f xs ≅ {[], f z # map f zs', ?P'}"
using D by simp
next
fix y ys'
assume "ys = y # ys'" and "zs = []"
hence D: "P x xs ∧ x = y ∧ xs ≅ {ys', [], P}" using C by simp+
moreover have "xs ≅ {ys', [], P} ⟶ map f xs ≅ {map f ys', map f [], ?P'}"
using B .
ultimately have "map f xs ≅ {map f ys', [], ?P'}" by simp
moreover have "?P' (f x) (map f xs)" using A and D by simp+
ultimately show "f x # map f xs ≅ {f y # map f ys', [], ?P'}"
using D by simp
next
fix y ys' z zs'
assume "ys = y # ys'" and "zs = z # zs'"
hence D: "x # xs ≅ {y # ys', z # zs', P}" using C by simp
show "f x # map f xs ≅ {f y # map f ys', f z # map f zs', ?P'}"
proof (cases "P x xs")
case True
hence E: "?P' (f x) (map f xs)" using A by simp
have "x = y ∧ xs ≅ {ys', z # zs', P}" using D and True by simp
moreover have "xs ≅ {ys', z # zs', P} ⟶
map f xs ≅ {map f ys', map f (z # zs'), ?P'}"
using B .
ultimately have "f x = f y ∧ map f xs ≅ {map f ys', map f (z # zs'), ?P'}"
by simp
thus ?thesis using E by simp
next
case False
hence E: "¬ ?P' (f x) (map f xs)" using A by simp
have "x = z ∧ xs ≅ {y # ys', zs', P}" using D and False by simp
moreover have "xs ≅ {y # ys', zs', P} ⟶
map f xs ≅ {map f (y # ys'), map f zs', ?P'}"
using B .
ultimately have "f x = f z ∧ map f xs ≅ {map f (y # ys'), map f zs', ?P'}"
by simp
thus ?thesis using E by simp
qed
qed
qed
lemma Interleaves_prefix_fst_1 [rule_format]:
assumes A: "xs ≅ {ys, zs, P}"
shows "(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
ws @ xs ≅ {ws @ ys, zs, P}"
proof (induction ws, simp_all add: A, rule impI)
fix w ws
assume B: "∀n < Suc (length ws). P ((w # ws) ! n) (drop n ws @ xs)"
assume "(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
ws @ xs ≅ {ws @ ys, zs, P}"
moreover have "∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)"
proof (rule allI, rule impI)
fix n
assume "n < length ws"
moreover have "Suc n < Suc (length ws) ⟶
P ((w # ws) ! (Suc n)) (drop (Suc n) ws @ xs)"
using B ..
ultimately show "P (ws ! n) (drop (Suc n) ws @ xs)" by simp
qed
ultimately have "ws @ xs ≅ {ws @ ys, zs, P}" ..
moreover have "0 < Suc (length ws) ⟶ P ((w # ws) ! 0) (drop 0 ws @ xs)"
using B ..
hence "P w (ws @ xs)" by simp
ultimately show "w # ws @ xs ≅ {w # ws @ ys, zs, P}" by (cases zs, simp_all)
qed
lemma Interleaves_prefix_fst_2 [rule_format]:
"ws @ xs ≅ {ws @ ys, zs, P} ⟶
(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
xs ≅ {ys, zs, P}"
proof (induction ws, simp_all, (rule impI)+)
fix w ws
assume A: "∀n < Suc (length ws). P ((w # ws) ! n) (drop n ws @ xs)"
hence "0 < Suc (length ws) ⟶ P ((w # ws) ! 0) (drop 0 ws @ xs)" ..
hence "P w (ws @ xs)" by simp
moreover assume "w # ws @ xs ≅ {w # ws @ ys, zs, P}"
ultimately have "ws @ xs ≅ {ws @ ys, zs, P}" by (cases zs, simp_all)
moreover assume "ws @ xs ≅ {ws @ ys, zs, P} ⟶
(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
xs ≅ {ys, zs, P}"
ultimately have "(∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)) ⟶
xs ≅ {ys, zs, P}"
by simp
moreover have "∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs)"
proof (rule allI, rule impI)
fix n
assume "n < length ws"
moreover have "Suc n < Suc (length ws) ⟶
P ((w # ws) ! (Suc n)) (drop (Suc n) ws @ xs)"
using A ..
ultimately show "P (ws ! n) (drop (Suc n) ws @ xs)" by simp
qed
ultimately show "xs ≅ {ys, zs, P}" ..
qed
lemma Interleaves_prefix_fst [rule_format]:
"∀n < length ws. P (ws ! n) (drop (Suc n) ws @ xs) ⟹
xs ≅ {ys, zs, P} = ws @ xs ≅ {ws @ ys, zs, P}"
proof (rule iffI, erule Interleaves_prefix_fst_1, simp)
qed (erule Interleaves_prefix_fst_2, simp)
lemma Interleaves_prefix_snd [rule_format]:
"∀n < length ws. ¬ P (ws ! n) (drop (Suc n) ws @ xs) ⟹
xs ≅ {ys, zs, P} = ws @ xs ≅ {ys, ws @ zs, P}"
proof (subst (1 2) Interleaves_swap)
qed (rule Interleaves_prefix_fst, simp)
lemma Interleaves_all_nil_1 [rule_format]:
"xs ≅ {xs, [], P} ⟶ (∀n < length xs. P (xs ! n) (drop (Suc n) xs))"
proof (induction xs, simp_all, rule impI, erule conjE, rule allI, rule impI)
fix x xs n
assume
"xs ≅ {xs, [], P} ⟶ (∀n < length xs. P (xs ! n) (drop (Suc n) xs))" and
"xs ≅ {xs, [], P}"
hence A: "∀n < length xs. P (xs ! n) (drop (Suc n) xs)" ..
assume
B: "P x xs" and
C: "n < Suc (length xs)"
show "P ((x # xs) ! n) (drop n xs)"
proof (cases n, simp_all add: B)
case (Suc m)
have "m < length xs ⟶ P (xs ! m) (drop (Suc m) xs)" using A ..
moreover have "m < length xs" using C and Suc by simp
ultimately show "P (xs ! m) (drop (Suc m) xs)" ..
qed
qed
lemma Interleaves_all_nil_2 [rule_format]:
"∀n < length xs. P (xs ! n) (drop (Suc n) xs) ⟹ xs ≅ {xs, [], P}"
by (insert Interleaves_prefix_fst [of xs P "[]" "[]" "[]"], simp)
lemma Interleaves_all_nil:
"xs ≅ {xs, [], P} = (∀n < length xs. P (xs ! n) (drop (Suc n) xs))"
proof (rule iffI, rule allI, rule impI, rule Interleaves_all_nil_1, assumption+)
qed (rule Interleaves_all_nil_2, simp)
lemma Interleaves_nil_all:
"xs ≅ {[], xs, P} = (∀n < length xs. ¬ P (xs ! n) (drop (Suc n) xs))"
by (subst Interleaves_swap, simp add: Interleaves_all_nil)
lemma Interleaves_suffix_one_aux:
assumes A: "P x []"
shows "¬ xs @ [x] ≅ {[], zs, P}"
using [[simproc del: defined_all]]
proof (induction xs arbitrary: zs, simp_all, rule_tac [!] notI)
fix zs
assume "[x] ≅ {[], zs, P}"
thus False by (cases zs, simp_all add: A)
next
fix w xs zs
assume B: "⋀zs. ¬ xs @ [x] ≅ {[], zs, P}"
assume "w # xs @ [x] ≅ {[], zs, P}"
thus False proof (cases zs, simp_all, (erule_tac conjE)+)
fix zs'
assume "xs @ [x] ≅ {[], zs', P}"
moreover have "¬ xs @ [x] ≅ {[], zs', P}" using B .
ultimately show False by contradiction
qed
qed
lemma Interleaves_suffix_one_fst_2 [rule_format]:
assumes A: "P x []"
shows "xs @ [x] ≅ {ys @ [x], zs, P} ⟶ xs ≅ {ys, zs, λw ws. P w (ws @ [x])}"
(is "_ ⟶ _ ≅ {_, _, ?P'}")
using [[simproc del: defined_all]]
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp_all)
fix ys zs
assume "[x] ≅ {ys @ [x], zs, P}"
hence B: "length [x] = length (ys @ [x]) + length zs"
by (rule Interleaves_length)
have ys: "ys = []" by (cases ys, simp, insert B, simp)
then have "zs = []" by (cases zs, simp, insert B, simp)
with ys show "[] ≅ {ys, zs, ?P'}" by simp
next
fix w xs ys zs
assume B: "⋀ys zs. xs @ [x] ≅ {ys @ [x], zs, P} ⟶ xs ≅ {ys, zs, ?P'}"
assume "w # xs @ [x] ≅ {ys @ [x], zs, P}"
thus "w # xs ≅ {ys, zs, ?P'}"
proof (cases zs, case_tac [!] ys, simp_all del: Interleaves.simps(1,3),
(erule_tac [1-2] conjE)+)
assume "xs @ [x] ≅ {[], [], P}"
thus False by (cases xs, simp_all)
next
fix ys'
have "xs @ [x] ≅ {ys' @ [x], [], P} ⟶ xs ≅ {ys', [], ?P'}" using B .
moreover assume "xs @ [x] ≅ {ys' @ [x], [], P}"
ultimately show "xs ≅ {ys', [], ?P'}" ..
next
fix z' zs'
assume "w # xs @ [x] ≅ {[x], z' # zs', P}"
thus "w # xs ≅ {[], z' # zs', ?P'}"
proof (cases "P w (xs @ [x])", simp_all, erule_tac [!] conjE)
assume "xs @ [x] ≅ {[], z' # zs', P}"
moreover have "¬ xs @ [x] ≅ {[], z' # zs', P}"
using A by (rule Interleaves_suffix_one_aux)
ultimately show False by contradiction
next
have "xs @ [x] ≅ {[x], zs', P} ⟶ xs ≅ {[], zs', ?P'}" using B by simp
moreover assume "xs @ [x] ≅ {[x], zs', P}"
ultimately show "xs ≅ {[], zs', ?P'}" ..
qed
next
fix y' ys' z' zs'
assume "w # xs @ [x] ≅ {y' # ys' @ [x], z' # zs', P}"
thus "w # xs ≅ {y' # ys', z' # zs', ?P'}"
proof (cases "P w (xs @ [x])", simp_all, erule_tac [!] conjE)
have "xs @ [x] ≅ {ys' @ [x], z' # zs', P} ⟶ xs ≅ {ys', z' # zs', ?P'}"
using B .
moreover assume "xs @ [x] ≅ {ys' @ [x], z' # zs', P}"
ultimately show "xs ≅ {ys', z' # zs', ?P'}" ..
next
have "xs @ [x] ≅ {y' # ys' @ [x], zs', P} ⟶ xs ≅ {y' # ys', zs', ?P'}"
using B by simp
moreover assume "xs @ [x] ≅ {y' # ys' @ [x], zs', P}"
ultimately show "xs ≅ {y' # ys', zs', ?P'}" ..
qed
qed
qed
lemma Interleaves_suffix_fst_1 [rule_format]:
assumes A: "∀n < length ws. P (ws ! n) (drop (Suc n) ws)"
shows "xs ≅ {ys, zs, λv vs. P v (vs @ ws)} ⟶ xs @ ws ≅ {ys @ ws, zs, P}"
(is "_ ≅ {_, _, ?P'} ⟶ _")
using [[simproc del: defined_all]]
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp_all)
fix ys zs
assume "[] ≅ {ys, zs, ?P'}"
hence "ys = [] ∧ zs = []" by (rule Interleaves_nil)
thus "ws ≅ {ys @ ws, zs, P}" using A by (simp add: Interleaves_all_nil)
next
fix x xs ys zs
assume A: "⋀ys zs. xs ≅ {ys, zs, ?P'} ⟶ xs @ ws ≅ {ys @ ws, zs, P}"
assume "x # xs ≅ {ys, zs, ?P'}"
thus "x # xs @ ws ≅ {ys @ ws, zs, P}"
proof (rule_tac Interleaves.cases [of "(?P', x # xs, ys, zs)"],
simp_all del: Interleaves.simps(1),
(erule_tac conjE)+, (erule_tac [2] conjE)+, (erule_tac [3] conjE)+)
fix P' x' xs' y' ys' z' zs'
assume
B: "x' # xs' ≅ {y' # ys', z' # zs', P'}" and
C: "?P' = P'" and
D: "xs = xs'"
show "x' # xs' @ ws ≅ {y' # ys' @ ws, z' # zs', P}"
proof (cases "P' x' xs'")
have "xs ≅ {ys', z' # zs', ?P'} ⟶ xs @ ws ≅ {ys' @ ws, z' # zs', P}"
using A .
moreover case True
hence "xs ≅ {ys', z' # zs', ?P'}" using B and C and D by simp
ultimately have "xs @ ws ≅ {ys' @ ws, z' # zs', P}" ..
moreover have "P x' (xs' @ ws)" using C [symmetric] and True by simp
moreover have "x' = y'" using B and True by simp
ultimately show ?thesis using D by simp
next
have "xs ≅ {y' # ys', zs', ?P'} ⟶ xs @ ws ≅ {(y' # ys') @ ws, zs', P}"
using A .
moreover case False
hence "xs ≅ {y' # ys', zs', ?P'}" using B and C and D by simp
ultimately have "xs @ ws ≅ {(y' # ys') @ ws, zs', P}" ..
moreover have "¬ P x' (xs' @ ws)" using C [symmetric] and False by simp
moreover have "x' = z'" using B and False by simp
ultimately show ?thesis using D by simp
qed
next
fix P' x' xs' y' ys'
have "xs ≅ {ys', [], ?P'} ⟶ xs @ ws ≅ {ys' @ ws, [], P}" using A .
moreover assume
"xs' ≅ {ys', [], P'}" and
B: "?P' = P'" and
C: "xs = xs'"
hence "xs ≅ {ys', [], ?P'}" by simp
ultimately have "xs' @ ws ≅ {ys' @ ws, [], P}" using C by simp
moreover assume
"P' x' xs'" and
"x' = y'"
hence "P y' (xs' @ ws)" using B [symmetric] by simp
ultimately show "P y' (xs' @ ws) ∧ xs' @ ws ≅ {ys' @ ws, [], P}" by simp
next
fix P' x' xs' z' zs'
have "xs ≅ {[], zs', ?P'} ⟶ xs @ ws ≅ {[] @ ws, zs', P}" using A .
moreover assume
"xs' ≅ {[], zs', P'}" and
B: "?P' = P'" and
C: "xs = xs'"
hence "xs ≅ {[], zs', ?P'}" by simp
ultimately have "xs' @ ws ≅ {ws, zs', P}" using C by simp
moreover assume
"¬ P' x' xs'" and
"x' = z'"
hence "¬ P z' (xs' @ ws)" using B [symmetric] by simp
ultimately show "z' # xs' @ ws ≅ {ws, z' # zs', P}" by (cases ws, simp_all)
qed
qed
lemma Interleaves_suffix_one_fst_1 [rule_format]:
"P x [] ⟹
xs ≅ {ys, zs, λw ws. P w (ws @ [x])} ⟹ xs @ [x] ≅ {ys @ [x], zs, P}"
by (rule Interleaves_suffix_fst_1, simp)
lemma Interleaves_suffix_one_fst:
"P x [] ⟹
xs ≅ {ys, zs, λw ws. P w (ws @ [x])} = xs @ [x] ≅ {ys @ [x], zs, P}"
proof (rule iffI, rule Interleaves_suffix_one_fst_1, assumption+)
qed (rule Interleaves_suffix_one_fst_2)
lemma Interleaves_suffix_one_snd:
"¬ P x [] ⟹
xs ≅ {ys, zs, λw ws. P w (ws @ [x])} = xs @ [x] ≅ {ys, zs @ [x], P}"
by (subst (1 2) Interleaves_swap, rule Interleaves_suffix_one_fst)
lemma Interleaves_suffix_aux [rule_format]:
"(∀n < length ws. P (ws ! n) (drop (Suc n) ws)) ⟶
x # xs @ ws ≅ {ws, zs, P} ⟶
¬ P x (xs @ ws)"
proof (induction ws arbitrary: P rule: rev_induct, simp_all,
rule impI, (rule_tac [2] impI)+)
fix P
assume "x # xs ≅ {[], zs, P}"
thus "¬ P x xs" by (cases zs, simp_all)
next
fix w ws P
assume
A: "⋀P'. (∀n < length ws. P' (ws ! n) (drop (Suc n) ws)) ⟶
x # xs @ ws ≅ {ws, zs, P'} ⟶ ¬ P' x (xs @ ws)" and
B: "∀n < Suc (length ws). P ((ws @ [w]) ! n)
(drop (Suc n) ws @ drop (Suc n - length ws) [w])"
assume "x # xs @ ws @ [w] ≅ {ws @ [w], zs, P}"
hence C: "(x # xs @ ws) @ [w] ≅ {ws @ [w], zs, P}" by simp
let ?P' = "λv vs. P v (vs @ [w])"
have "(∀n < length ws. ?P' (ws ! n) (drop (Suc n) ws)) ⟶
x # xs @ ws ≅ {ws, zs, ?P'} ⟶ ¬ ?P' x (xs @ ws)"
using A .
moreover have "∀n < length ws. ?P' (ws ! n) (drop (Suc n) ws)"
proof (rule allI, rule impI)
fix n
assume D: "n < length ws"
moreover have "n < Suc (length ws) ⟶ P ((ws @ [w]) ! n)
(drop (Suc n) ws @ drop (Suc n - length ws) [w])"
using B ..
ultimately have "P ((ws @ [w]) ! n) (drop (Suc n) ws @ [w])" by simp
moreover have "n < length (butlast (ws @ [w]))" using D by simp
hence "butlast (ws @ [w]) ! n = (ws @ [w]) ! n" by (rule nth_butlast)
ultimately show "P (ws ! n) (drop (Suc n) ws @ [w])" by simp
qed
ultimately have "x # xs @ ws ≅ {ws, zs, ?P'} ⟶ ¬ ?P' x (xs @ ws)" ..
moreover have "length ws < Suc (length ws) ⟶ P ((ws @ [w]) ! length ws)
(drop (Suc (length ws)) ws @ drop (Suc (length ws) - length ws) [w])"
using B ..
hence "P w []" by simp
hence "x # xs @ ws ≅ {ws, zs, ?P'}"
using C by (rule Interleaves_suffix_one_fst_2)
ultimately have "¬ ?P' x (xs @ ws)" ..
thus "¬ P x (xs @ ws @ [w])" by simp
qed
lemma Interleaves_suffix_fst_2 [rule_format]:
assumes A: "∀n < length ws. P (ws ! n) (drop (Suc n) ws)"
shows "xs @ ws ≅ {ys @ ws, zs, P} ⟶ xs ≅ {ys, zs, λv vs. P v (vs @ ws)}"
(is "_ ⟶ _ ≅ {_, _, ?P'}")
using [[simproc del: defined_all]]
proof (induction xs arbitrary: ys zs, rule_tac [!] impI, simp_all)
fix ys zs
assume "ws ≅ {ys @ ws, zs, P}"
hence B: "length ws = length (ys @ ws) + length zs"
by (rule Interleaves_length)
have ys: "ys = []" by (cases ys, simp, insert B, simp)
then have "zs = []" by (cases zs, simp, insert B, simp)
with ys show "[] ≅ {ys, zs, ?P'}" by simp
next
fix x xs ys zs
assume B: "⋀ys zs. xs @ ws ≅ {ys @ ws, zs, P} ⟶ xs ≅ {ys, zs, ?P'}"
assume "x # xs @ ws ≅ {ys @ ws, zs, P}"
thus "x # xs ≅ {ys, zs, ?P'}"
proof (cases zs, case_tac [!] ys, simp_all del: Interleaves.simps(1,3),
(erule_tac [2] conjE)+)
assume C: "x # xs @ ws ≅ {ws, [], P}"
have "length (x # xs @ ws) = length ws + length []"
by (insert Interleaves_length [OF C], simp)
thus False by simp
next
fix ys'
have "xs @ ws ≅ {ys' @ ws, [], P} ⟶ xs ≅ {ys', [], ?P'}" using B .
moreover assume "xs @ ws ≅ {ys' @ ws, [], P}"
ultimately show "xs ≅ {ys', [], ?P'}" ..
next
fix z' zs'
assume "x # xs @ ws ≅ {ws, z' # zs', P}"
thus "x # xs ≅ {[], z' # zs', ?P'}"
proof (cases "P x (xs @ ws)", simp_all)
case True
moreover assume "x # xs @ ws ≅ {ws, z' # zs', P}"
with A [rule_format] have "¬ P x (xs @ ws)"
by (rule Interleaves_suffix_aux)
ultimately show False by contradiction
next
case False
moreover assume "x # xs @ ws ≅ {ws, z' # zs', P}"
ultimately have "x = z' ∧ xs @ ws ≅ {ws, zs', P}" by (cases ws, simp_all)
moreover have "xs @ ws ≅ {[] @ ws, zs', P} ⟶ xs ≅ {[], zs', ?P'}"
using B .
ultimately show "x = z' ∧ xs ≅ {[], zs', ?P'}" by simp
qed
next
fix y' ys' z' zs'
assume "x # xs @ ws ≅ {y' # ys' @ ws, z' # zs', P}"
thus "x # xs ≅ {y' # ys', z' # zs', ?P'}"
proof (cases "P x (xs @ ws)", simp_all, erule_tac [!] conjE)
have "xs @ ws ≅ {ys' @ ws, z' # zs', P} ⟶ xs ≅ {ys', z' # zs', ?P'}"
using B .
moreover assume "xs @ ws ≅ {ys' @ ws, z' # zs', P}"
ultimately show "xs ≅ {ys', z' # zs', ?P'}" ..
next
have "xs @ ws ≅ {y' # ys' @ ws, zs', P} ⟶ xs ≅ {y' # ys', zs', ?P'}"
using B by simp
moreover assume "xs @ ws ≅ {y' # ys' @ ws, zs', P}"
ultimately show "xs ≅ {y' # ys', zs', ?P'}" ..
qed
qed
qed
lemma Interleaves_suffix_fst [rule_format]:
"∀n < length ws. P (ws ! n) (drop (Suc n) ws) ⟹
xs ≅ {ys, zs, λv vs. P v (vs @ ws)} = xs @ ws ≅ {ys @ ws, zs, P}"
proof (rule iffI, rule Interleaves_suffix_fst_1, simp_all)
qed (rule Interleaves_suffix_fst_2, simp)
lemma Interleaves_suffix_snd [rule_format]:
"∀n < length ws. ¬ P (ws ! n) (drop (Suc n) ws) ⟹
xs ≅ {ys, zs, λv vs. P v (vs @ ws)} = xs @ ws ≅ {ys, zs @ ws, P}"
by (subst (1 2) Interleaves_swap, rule Interleaves_suffix_fst, simp)
end