(* * 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`). › ― ‹NOTE added definition› 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))" ― ‹NOTE added lemma› 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 by (simp add: ListMem_iff) 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 by (simp add: sublist_length) ― ‹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)" by (simp add: Cons.prems(4)) 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)› add_mono_thms_linordered_semiring(1) 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