# Theory FSSublist

```(*
* cf. planning/hol/sublistScript
*)
theory FSSublist
imports Main "HOL-Library.Sublist" ListUtils
begin

text ‹ This file is a port of the original HOL4 source file sublistScript.sml. ›

section "Factored System Sublist"
subsection "Sublist Characterization"

text ‹ We take a look at the characterization of sublists. As a precursor, we are replacing the
original definition of `sublist` in HOL4 (sublistScript.sml:10) with the semantically equivalent
`subseq` of Isabelle/HOL's to be able to use the associated theorems and automation.

In HOL4 `sublist` is defined as

(sublist [] l1 = T) /\
(sublist (h::t) [] = F) /\
(sublist (x::l1) (y::l2) = (x = y) /\ sublist l1 l2 \/ sublist (x::l1) l2)

[Abdulaziz et al., HOL4 Definition 10, p.19]. Whereas `subseq` (Sublist.tyh:927) is defined as an
abbrevation of `list\_emb` with the predicate @{term "λ x y. x = y"}, i.e.

@{term "subseq xs ys ≡ list_emb (=) xs ys"}

`list\_emb` itself is defined as an inductive predicate. However, an equivalent function definition
is provided in `list\_emb\_code` (Sublist.thy:784) which is very close to `sublist` in HOL4.

The correctness of the equivalence claim is shown below by the technical lemma
`sublist\_HOL4\_equiv\_subseq` (where the HOL4 definition of `sublist` is renamed to `sublist\_HOL4`).
›

fun sublist_HOL4 where
"sublist_HOL4 [] l1 = True"
| "(sublist_HOL4 (h # t) [] = False)"
| "(sublist_HOL4 (x # l1) (y # l2) = ((x = y) ∧ sublist_HOL4 l1 l2 ∨ sublist_HOL4 (x # l1) l2))"

lemma sublist_HOL4_equiv_subseq:
fixes l1 l2
shows "sublist_HOL4 l1 l2 ⟷ subseq l1 l2"
proof -
have "subseq l1 l2 = list_emb (λx y. x = y) l1 l2"
by blast
moreover {
have "sublist_HOL4 l1 l2 ⟷ list_emb (λx y. x = y) l1 l2"
proof (induction rule: sublist_HOL4.induct)
case (3 x l1 y l2)
then show "sublist_HOL4 (x # l1) (y # l2) ⟷ list_emb (λx y. x = y) (x # l1) (y # l2)"
proof (cases "x = y")
case True
then show ?thesis
using "3.IH"(1, 2)
by (metis sublist_HOL4.simps(3) subseq_Cons' subseq_Cons2_iff)
next
case False
then show ?thesis
using "3.IH"(2)
by force
qed
qed simp+
}
ultimately show ?thesis
by blast
qed

text ‹ Likewise as with `sublist` and `subseq`, the HOL4 definition of `list\_frag`
(list\_utilsScript.sml:207) has a an Isabelle/HOL counterpart in `sublist` (Sublist.thy:1124).

The equivalence claim is proven in the technical lemma `list\_frag\_HOL4\_equiv\_sublist`. Note that
`sublist` reverses the argument order of `list\_frag`. Other than that, both definitions are
syntactically identical. ›
definition list_frag_HOL4 where
"list_frag_HOL4 l frag ≡ ∃pfx sfx. pfx @ frag @ sfx = l"

lemma list_frag_HOL4_equiv_sublist:
shows "list_frag_HOL4 l l' ⟷ sublist l' l"
unfolding list_frag_HOL4_def sublist_def
by blast

text ‹ Given these equivalences, occurences of `sublist` and `list\_frag` in the original HOL4
source are now always translated directly to `subseq` and `sublist` respectively.

The remainer of this subsection is concerned with characterizations of `sublist`/ `subseq`. ›

lemma sublist_EQNS:
"subseq [] l = True"
"subseq (h # t) [] = False"
by auto

lemma sublist_refl: "subseq l l"
by auto

lemma sublist_cons:
assumes "subseq l1 l2"
shows "subseq l1 (h # l2)"
using assms
by blast

lemma sublist_NIL: "subseq l1 [] = (l1 = [])"
by fastforce

lemma sublist_trans:
fixes l1 l2
assumes "subseq l1 l2" "subseq l2 l3"
shows "subseq l1 l3"
using assms
by force

― ‹NOTE can be solved directly with 'list\_emb\_length'.›
lemma sublist_length:
fixes l l'
assumes "subseq l l'"
shows "length l ≤ length l'"
using assms list_emb_length
by blast

― ‹NOTE can be solved directly with subseq\_Cons'.›
lemma sublist_CONS1_E:
fixes l1 l2
assumes "subseq (h # l1) l2"
shows "subseq l1 l2"
using assms subseq_Cons'
by metis

lemma sublist_equal_lengths:
fixes l1 l2
assumes "subseq l1 l2" "(length l1 = length l2)"
shows "(l1 = l2)"
using assms subseq_same_length
by blast

― ‹NOTE can be solved directly with 'subseq\_order.antisym'.›
lemma sublist_antisym:
assumes "subseq l1 l2" "subseq l2 l1"
shows "(l1 = l2)"
using assms subseq_order.antisym
by blast

lemma sublist_append_back:
fixes l1 l2
shows "subseq l1 (l2 @ l1)"
by blast

― ‹NOTE can be solved directly with 'subseq\_rev\_drop\_many'.›
lemma sublist_snoc:
fixes l1 l2
assumes "subseq l1 l2"
shows "subseq l1 (l2 @ [h])"
using assms subseq_rev_drop_many
by blast

lemma sublist_append_front:
fixes l1 l2
shows "subseq l1 (l1 @ l2)"
by fast

lemma append_sublist_1:
assumes "subseq (l1 @ l2) l"
shows "subseq l1 l ∧ subseq l2 l"
using assms sublist_append_back sublist_append_front sublist_trans
by blast

― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).›
lemma sublist_prefix:
shows "subseq (h # l1) l2 ⟹ ∃l2a l2b. l2 = l2a @ [h] @ l2b ∧ ¬ListMem h l2a"
proof (induction l2 arbitrary: h l1)
― ‹NOTE l2 cannot be empty when @{term "(h # l1)"} isn't.›
case Nil
have "¬(subseq (h # l1) [])"
by simp
then show ?case
using Nil.prems
by blast
next
case (Cons a l2)
then show ?case proof (cases "a = h")
― ‹NOTE If a = h then a trivial solution exists in l2a = [] and l2b = l2.›
case True
then show "∃ l2a l2b. (Cons a l2) = l2a @ [h] @ l2b ∧ ¬ListMem h l2a"
using ListMem_iff
by force
next
case False
have "subseq (h # l1) l2"
using Cons.prems False subseq_Cons2_neq
by force
then obtain l2a l2b where "l2 = l2a @ [h] @ l2b" "¬ListMem h l2a"
using Cons.IH Cons.prems
by meson
moreover have "a # l2 = (a # l2a) @ [h] @ l2b"
using calculation(1)
by simp
moreover have "¬(ListMem h (a # l2a))"
using False calculation(2) ListMem.simps
by fastforce
ultimately show ?thesis
by blast
qed
qed

― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).›
lemma sublist_skip:
fixes l1 l2 h l1'
assumes "l1 = (h # l1')" "l2 = l2a @ [h] @ l2b" "subseq l1 l2" "¬(ListMem h l2a)"
shows "subseq l1 (h # l2b)"
using assms
proof (induction l2a arbitrary: l1 l2 h l1')
case Nil
then have "l2 = h # l2b"
by fastforce
then show ?case using Nil.prems(3)
by blast
next
case (Cons a l2a)
have "a ≠ h"
using Cons.prems(4) ListMem.simps
by fast
then have "subseq l1 (l2a @ [h] @ l2b)"
using Cons.prems(1, 2, 3) subseq_Cons2_neq
by force
moreover have "¬ListMem h l2a"
using Cons.prems(4) insert
by metis
ultimately have "subseq l1 (h # l2b)"
using Cons.IH Cons.prems
by meson
then show ?case
by simp
qed

― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).›
lemma sublist_split_trans:
fixes l1 l2 h l1'
assumes "l1 = (h # l1')" "l2 = l2a @ [h] @ l2b" "subseq l1 l2" "¬(ListMem h l2a)"
shows "subseq l1' l2b"
proof -
have "subseq (h # l1') (h # l2b)"
using assms sublist_skip
by metis
then show ?thesis
using subseq_Cons2'
by metis
qed

lemma sublist_cons_exists:
shows "
subseq (h # l1) l2
⟷ (∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b)
"
proof -
― ‹NOTE show both directions of the equivalence in pure proof blocks.›
{
have
"subseq (h # l1) l2 ⟹ (∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b)"
proof (induction l2 arbitrary: h l1)
case (Cons a l2)
show ?case
proof (cases "a = h")
case True
― ‹NOTE This case has a trivial solution in '?l2a = []', '?l2b = l2'.›
let ?l2a="[]"
have "(a # l2) = ?l2a @ [h] @ l2"
using True
by auto
moreover have "¬(ListMem h ?l2a)"
using ListMem_iff
by force
moreover have "subseq l1 l2"
using Cons.prems True
by simp
ultimately show ?thesis
by blast
next
case False
have 1: "subseq (h # l1) l2"
using Cons.prems False subseq_Cons2_neq
by metis
then obtain l2a l2b where "l2 = l2a @ [h] @ l2b" "¬ListMem h l2a"
using Cons.IH Cons.prems
by meson
moreover have "a # l2 = (a # l2a) @ [h] @ l2b"
using calculation(1)
by simp
moreover have "¬(ListMem h (a # l2a))"
using False calculation(2) ListMem.simps
by fastforce
ultimately show ?thesis
using 1 sublist_split_trans
by metis
qed
qed simp
}
moreover
{
assume "∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b"
then have  "subseq (h # l1) l2"
by auto
}
ultimately show ?thesis
by argo
qed

lemma sublist_append_exists:
fixes l1 l2
shows "subseq (l1 @ l2) l3 ⟹ ∃l3a l3b. (l3 = l3a @ l3b) ∧ subseq l1 l3a ∧ subseq l2 l3b"
using list_emb_appendD
by fast

― ‹NOTE can be solved directly with 'list\_emb\_append\_mono'.›
lemma sublist_append_both_I:
assumes "subseq a b" "subseq c d"
shows "subseq (a @ c) (b @ d)"
using assms list_emb_append_mono
by blast

lemma sublist_append:
assumes "subseq l1 l1'" "subseq l2 l2'"
shows "subseq (l1 @ l2) (l1' @ l2')"
using assms sublist_append_both_I
by blast

lemma sublist_append2:
assumes "subseq l1 l2"
shows "subseq l1 (l2 @ l3)"
using assms sublist_append[of "l1" "l2" "[]" "l3"]
by fast

lemma append_sublist:
shows "subseq (l1 @ l2 @ l3) l ⟹ subseq (l1 @ l3) l"
proof (induction l)
case Nil
then show ?case
using sublist_NIL
by fastforce
next
case (Cons a l)
then show ?case
proof (cases l1)
case Nil
then show ?thesis
using Cons.prems append_sublist_1
by auto
next
case (Cons a list)
then show ?thesis
using Cons.prems subseq_append' subseq_order.dual_order.trans
by blast
qed
qed

lemma sublist_subset:
assumes "subseq l1 l2"
shows "set l1 ⊆ set l2"
using assms set_nths_subset subseq_conv_nths
by metis

lemma sublist_filter:
fixes P l
shows "subseq (filter P l) l"
using subseq_filter_left
by blast

lemma sublist_cons_2:
fixes l1 l2 h
shows "(subseq (h # l1) (h # l2) ⟷ (subseq l1 l2))"
by fastforce

lemma sublist_every:
fixes l1 l2 P
assumes "(subseq l1 l2 ∧ list_all P l2)"
shows "list_all P l1"
by (metis (full_types) Ball_set assms list_emb_set)

lemma sublist_SING_MEM: "subseq [h] l ⟷ ListMem h l"
using ListMem_iff subseq_singleton_left
by metis

― ‹NOTE renamed due to previous declaration of `sublist\_append\_exists\_2.›
lemma sublist_append_exists_2:
fixes l1 l2 l3
assumes "subseq (h # l1) l2"
shows "(∃l3 l4. (l2 = l3 @ [h] @ l4) ∧ (subseq l1 l4))"
using assms sublist_cons_exists
by metis

lemma sublist_append_4:
fixes l l1 l2 h
assumes "(subseq (h # l) (l1 @ [h] @ l2))" "(list_all (λx. ¬(h = x)) l1)"
shows "subseq l l2"
using assms
proof (induction l1)
qed auto

lemma sublist_append_5:
fixes l l1 l2 h
assumes "(subseq (h # l) (l1 @ l2))" "(list_all (λx. ¬(h = x)) l1)"
shows "subseq (h # l) l2"
using assms
proof (induction l1)
qed auto

lemma sublist_append_6:
fixes l l1 l2 h
assumes "(subseq (h # l) (l1 @ l2))" "(¬(ListMem h l1))"
shows "subseq (h # l) l2"
using assms
proof (induction l1)
case (Cons a l1)
then show ?case
qed simp

lemma sublist_MEM:
fixes h l1 l2
shows "subseq (h # l1) l2 ⟹ ListMem h l2"
proof (induction l2)
next
case (Cons a l2)
then show ?case
using elem insert subseq_Cons2_neq
by metis
qed simp

lemma sublist_cons_4:
fixes l h l'
shows "subseq l l' ⟹ subseq l (h # l')"
using sublist_cons
by blast

subsection "Main Theorems"

theorem sublist_imp_len_filter_le:
fixes P l l'
assumes "subseq l' l"
shows "length (filter P l') ≤ length (filter P l)"
using assms

― ‹TODO showcase (non-trivial proof translation/ obscurity).›
theorem list_with_three_types_shorten_type2:
fixes P1 P2 P3 k1 f PProbs PProbl s l
assumes "(PProbs s)" "(PProbl l)"
"(∀l s.
(PProbs s)
∧ (PProbl l)
∧ (list_all P1 l)
⟶ (∃l'.
(f s l' = f s l)
∧ (length (filter P2 l') ≤ k1)
∧ (length (filter P3 l') ≤ length (filter P3 l))
∧ (list_all P1 l')
∧ (subseq l' l)
)
)"
"(∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2))"
"(∀s l. (PProbs s) ∧ (PProbl l) ⟶ (PProbs (f s l)))"
"(∀l1 l2. (subseq l1 l2) ∧ (PProbl l2) ⟶ (PProbl l1))"
"(∀l1 l2. PProbl (l1 @ l2) ⟷ (PProbl l1 ∧ PProbl l2))"
shows "(∃l'.
(f s l' = f s l)
∧ (length (filter P3 l') ≤ length (filter P3 l))
∧ (∀l''.
(sublist l'' l') ∧ (list_all P1 l'')
⟶ (length (filter P2 l'') ≤ k1)
)
∧ (subseq l' l)
)"
using assms
proof (induction "filter (λx. ¬P1 x) l" arbitrary: P1 P2 P3 k1 f PProbs PProbl s l)
case Nil
then have "list_all (λx. P1 x) l"
using Nil(1) filter_empty_every_not[of "λx. ¬P1 x" l]
by presburger
then obtain l' where 1:
"(f s l' = f s l)" "length (filter P2 l') ≤ k1" "length (filter P3 l') ≤ length (filter P3 l)"
"list_all P1 l'" "subseq l' l"
using Nil.prems(1, 2, 3)
by blast
moreover {
fix l''
assume "sublist l'' l'" "list_all P1 l''"
then have "subseq l'' l'"
by blast
― ‹NOTE original proof uses `frag\_len\_filter\_le` which however requires the fact
`sublist l' ?l`. Unfortunately, this could not be derived in Isabelle/HOL.›
then have "length (filter P2 l'') ≤ length (filter P2 l')"
using sublist_imp_len_filter_le
by blast
then have "length (filter P2 l'') ≤ k1"
using 1
by linarith
}
ultimately show ?case
by blast
next
case (Cons a x)
― ‹NOTE The proof of the induction step basically consists of construction a list
`?l'=l'' @ [a] @ l'''` where `l''` and `l'''` are lists obtained from certain specifications
of the induction hypothesis.›
then obtain l1 l2 where 2:
"l = l1 @ a # l2" "(∀u∈set l1. P1 u)" "¬ P1 a ∧ x = [x←l2 . ¬ P1 x]"
using Cons(2) filter_eq_Cons_iff[of "λx. ¬P1 x"]
by metis
then have 3: "PProbl l2"
using Cons.prems(2, 6) 2(1) sublist_append_back
by blast
― ‹NOTE Use the induction hypothesis to obtain a specific  `l'''`.›
{
have "x = filter (λx. ¬P1 x) l2"
using 2(3)
by blast
moreover have "PProbs (f (f s l1) [a])"
using Cons.prems(1, 2, 5, 6, 7) 2(1) elem sublist_SING_MEM
by metis
moreover have "∀l s. PProbs s ∧ PProbl l ∧ list_all P1 l ⟶ (∃l'.
f s l' = f s l ∧ length (filter P2 l') ≤ k1 ∧ length (filter P3 l') ≤ length (filter P3 l)
∧ list_all P1 l' ∧ subseq l' l)"
using Cons.prems(3)
by blast
moreover have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)"
"∀s l. PProbs s ∧ PProbl l ⟶ PProbs (f s l)"
"∀l1 l2. subseq l1 l2 ∧ PProbl l2 ⟶ PProbl l1"
"∀l1 l2. PProbl (l1 @ l2) = (PProbl l1 ∧ PProbl l2)"
using Cons.prems(4, 5, 6, 7)
by blast+
ultimately have "∃l'.
f (f (f s l1) [a]) l' = f (f (f s l1) [a]) l2 ∧ length (filter P3 l') ≤ length (filter P3 l2)
∧ (∀l''. sublist l'' l' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l' l2"
using 3 Cons(1)[of P1 l2, where s="(f (f s l1) [a])"]
by blast
}
then obtain l''' where 4:
"f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2"
"length (filter P3 l''') ≤ length (filter P3 l2)"
"(∀l''. sublist l'' l''' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l''' l2"
by blast
then have "f s (l1 @ [a] @ l''') = f s (l1 @ [a] @ l2)"
using Cons.prems(4)
by auto
then have "subseq l''' l2"
using 4(3)
by blast
― ‹NOTE Use the induction hypothesis to obtain a specific  `l''`.›
{
have "∀l s.
PProbs s ∧ PProbl l1 ∧ list_all P1 l1
⟶ (∃l''.
f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1)
∧ list_all P1 l'' ∧ subseq l'' l1)"
using Cons.prems(3)
by blast
then have "∃l''.
f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1)
∧ list_all P1 l'' ∧ subseq l'' l1"
using Cons.prems(1, 2, 7) 2(1, 2)
by (metis Ball_set)
}

then obtain l'' where 5:
"f s l'' = f s l1" "length (filter P2 l'') ≤ k1"
"length (filter P3 l'') ≤ length (filter P3 l1)" "list_all P1 l'' ∧ subseq l'' l1"
by blast
text ‹ Proof the proposition by providing the witness @{term "l'=(l'' @ [a] @ l''')"}. ›
let ?l'="(l'' @ [a] @ l''') "
{
have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)"
text ‹ Rewrite and show the goal.›
have "f s ?l' = f s (l1 @ [a] @ l2) ⟷ f s (l'' @ (a # l''')) = f s (l1 @ (a # l2))"
by simp
also have "… ⟷ f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2"
by (metis Cons.prems(4) ‹f s l'' = f s l1› calculation)
finally have "f s ?l' = f s (l1 @ [a] @ l2)"
using 4(1)
by blast
}
moreover
{
have "
length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))
⟷
(length (filter P3 l'') + 1 + length (filter P3 l''')
≤ length (filter P3 l1) + 1 + length (filter P3 l2))"
by force
then have "
length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))
⟷
length (filter P3 l'') + length (filter P3 l''')
≤ length (filter P3 l1) + length (filter P3 l2)"
by linarith
then have "length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))"
using 4(2) ‹length (filter P3 l'') ≤ length (filter P3 l1)›
by blast
}
moreover
{
fix l''''
assume P: "sublist l'''' ?l'" "list_all P1 l''''"
have "list_all P1 l1"
using 2(2) Ball_set
by blast
consider (i) "sublist l'''' l''" | (ii) "sublist l'''' l'''"
using P(1, 2) 2(3)  LIST_FRAG_DICHOTOMY_2
by metis
then have "length (filter P2 l'''') ≤ k1"
proof (cases)
case i
then have "length (filter P2 l'''') ≤ length (filter P2 l'')"
using frag_len_filter_le
by blast
then show ?thesis
using 5(2) order_trans
by blast
next
case ii
then show ?thesis
using 4(3) P(2)
by blast
qed
}
― ‹NOTE the following two steps seem to be necessary to convince Isabelle that the split
@{term "l = l1 @ a # l2"} matches the split `(l1 @ [a] @ l2` and the previous proof steps therefore is
prove the goal.›
moreover {
have "subseq ?l' (l1 @ [a] @ l2)"
by (simp add: FSSublist.sublist_append ‹list_all P1 l'' ∧ subseq l'' l1› ‹subseq l''' l2›)
}
moreover have "l = l1 @ [a] @ l2"
using 2
by force
ultimately show ?case
by blast
qed

lemma isPREFIX_sublist:
fixes x y
assumes "prefix x y"
shows "subseq x y"
using assms prefix_order.dual_order.antisym
by blast

end```