(* Title: Reasoning about Lists via List Interleaving Author: Pasquale Noce Security Certification Specialist at Arjo Systems - Gep S.p.A. pasquale dot noce dot lavoro at gmail dot com pasquale dot noce at arjowiggins-it dot com *) 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 #