theory ListUtils imports Main "HOL-Library.Sublist" begin ― ‹TODO assure translations * 'sublist' --> 'subseq' * list\_frag l l' --> sublist l' l (switch operands!)› lemma len_ge_0: fixes l shows "length l ≥ 0" by simp lemma len_gt_pref_is_pref: fixes l l1 l2 assumes "(length l2 > length l1)" "(prefix l1 l)" "(prefix l2 l)" shows "(prefix l1 l2)" using assms proof (induction l2 arbitrary: l1 l) case Nil then have "¬(length [] > length l1)" by simp then show ?case using Nil by blast next case (Cons a l2) then show ?case proof(induction l1 arbitrary: l) case Nil then show ?case using Nil_prefix by blast next case (Cons b l1) then show ?case proof(cases l) case Nil then have "¬(prefix (a # l2) l)" by simp then show ?thesis using Cons.prems(4) by simp next case (Cons c l) then have 1: "length l2 > length l1" using Cons.prems(2) by fastforce then show ?thesis using Cons proof(cases l) case Nil then have "l1 = [c]" "l2 = [c]" using Cons.prems(3, 4) local.Cons 1 by fastforce+ then show ?thesis using 1 by auto next case (Cons d l') { thm len_ge_0 have "length l1 ≥ 0" by simp then have "length l2 > 0" using 1 by force then have "l2 ≠ []" using 1 by blast } then have "length (a # l1) ≤ length (b # l2)" using 1 le_eq_less_or_eq by simp then show ?thesis using Cons.prems(3, 4) prefix_length_prefix by fastforce qed qed qed qed lemma nempty_list_append_length_add: fixes l1 l2 l3 assumes "l2 ≠ []" shows "length (l1 @ l3) < length (l1 @ l2 @l3)" using assms by (induction l2) auto lemma append_filter: fixes f1 :: "'a ⇒ bool" and f2 as1 as2 and p :: "'a list" assumes "(as1 @ as2 = filter f1 (map f2 p))" shows "(∃p_1 p_2. (p_1 @ p_2 = p) ∧ (as1 = filter f1 (map f2 p_1)) ∧ (as2 = filter f1 (map f2 p_2)) )" using assms proof (induction p arbitrary: f1 f2 as1 as2) case Nil from Nil have 1: "as1 @ as2 = []" by force then have 2: "as1 = []" "as2 = []" by blast+ let ?p1="[]" let ?p2="[]" from 1 2 have "?p1 @ ?p2 = []" "as1 = (filter f1 (map f2 ?p1))" "as2 = (filter f1 (map f2 ?p2))" subgoal by blast subgoal using 2(1) by simp subgoal using 2(2) by simp done then show ?case by fast next case cons: (Cons a p) then show ?case proof (cases "as1") case Nil from cons.prems Nil have 1: "as2 = filter f1 (map f2 (a # p))" by simp let ?p1="[]" let ?p2="a # p" have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)" subgoal by simp subgoal using Nil by simp subgoal using 1 by auto done then show ?thesis by blast next case (Cons a' p') then show ?thesis proof (cases "¬f1 (f2 a)") case True hence "filter f1 (map f2 (a # p)) = filter f1 (map f2 p)" by fastforce hence "as1 @ as2 = filter f1 (map f2 p)" using cons.prems by argo then obtain p1 p2 where a: "p1 @ p2 = p" "as1 = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)" using cons.IH by meson let ?p1="a # p1" let ?p2="p2" have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)" subgoal using a(1) by fastforce subgoal using True a(2) by auto subgoal using a(3) by blast done then show ?thesis by blast next case False hence "filter f1 (map f2 (a # p)) = f2 a # filter f1 (map f2 p)" by fastforce then have 1: "a' = f2 a" "p' @ as2 = filter f1 (map f2 p)" "as1 = a' # p'" using cons.prems Cons by fastforce+ then obtain p1 p2 where 2: "p1 @ p2 = p" "p' = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)" using cons.IH by meson let ?p1="a # p1" let ?p2="p2" have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)" subgoal using 2(1) by simp subgoal using False 1(1, 3) 2(2) by force subgoal using 2(3) by blast done then show ?thesis by blast qed qed qed ― ‹NOTE types of `f1` and `p` had to be fixed for `append\_eq\_as\_proj\_1`.› lemma append_eq_as_proj_1: fixes f1 :: "'a ⇒ bool" and f2 as1 as2 as3 and p :: "'a list" assumes "(as1 @ as2 @ as3 = filter f1 (map f2 p))" shows "(∃p_1 p_2 p_3. (p_1 @ p_2 @ p_3 = p) ∧ (as1 = filter f1 (map f2 p_1)) ∧ (as2 = filter f1 (map f2 p_2)) ∧ (as3 = filter f1 (map f2 p_3)) )" proof - from assms obtain p_1 p_2 where 1: "(p_1 @ p_2 = p)" "(as1 = filter f1 (map f2 p_1))" "(as2 @ as3 = filter f1 (map f2 p_2))" using append_filter[of as1 "(as2 @ as3)"] by meson moreover from 1 obtain p_a p_b where "(p_a @ p_b = p_2)" "(as2 = filter f1 (map f2 p_a))" "(as3 = filter f1 (map f2 p_b))" using append_filter[where p=p_2] by meson ultimately show ?thesis by blast qed lemma filter_empty_every_not: "⋀P l. (filter (λx. P x) l = []) = list_all (λx. ¬P x) l" proof - fix P l show "(filter (λx. P x) l = []) = list_all (λx. ¬P x) l" apply(induction l) apply(auto) done qed ― ‹NOTE added lemma (listScript.sml:810).› lemma MEM_SPLIT: fixes x l assumes "¬ListMem x l" shows "∀l1 l2. l ≠ l1 @ [x] @ l2" proof - { assume C: "¬(∀l1 l2. l ≠ l1 @ [x] @ l2)" then have "∃l1 l2. l = l1 @ [x] @ l2" by blast then obtain l1 l2 where 1: "l = l1 @ [x] @ l2" by blast from assms have 2: "(∀xs. l ≠ x # xs) ∧ (∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)" using ListMem_iff by fastforce then have False proof (cases l1) case Nil let ?xs="l2" from 1 Nil have "l = [x] @ ?xs" by blast then show ?thesis using 2 by simp next case (Cons a list) { let ?y="a" let ?xs="list @ [x] @ l2" from 1 Cons have "l = ?y # ?xs" by simp moreover have "ListMem x ?xs" by (simp add: ListMem_iff) ultimately have "∃xs. ∃y. l = y # xs ∧ ListMem x xs" by blast then have "¬(∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)" by presburger } then show ?thesis using 2 by auto qed } then show ?thesis by blast qed ― ‹NOTE added lemma (listScript.sml:2784)› lemma APPEND_EQ_APPEND_MID: fixes l1 l2 m1 m2 e shows "(l1 @ [e] @ l2 = m1 @ m2) ⟷ (∃l. (m1 = l1 @ [e] @ l) ∧ (l2 = l @ m2)) ∨ (∃l. (l1 = m1 @ l) ∧ (m2 = l @ [e] @ l2))" proof (induction "l1" arbitrary: m1) case Nil then show ?case by (simp; metis Cons_eq_append_conv)+ next case (Cons a l1) then show ?case by (cases m1; simp; blast) qed ― ‹NOTE variable `P` was removed (redundant).› lemma LIST_FRAG_DICHOTOMY: fixes l la x lb assumes "sublist l (la @ [x] @ lb)" "¬ListMem x l" shows "sublist l la ∨ sublist l lb" proof - { from assms(1) obtain pfx sfx where 1: "pfx @ l @ sfx = la @ [x] @ lb" unfolding sublist_def by force from assms(2) have 2: "∀l1 l2. l ≠ l1 @ [x] @ l2" using MEM_SPLIT[OF assms(2)] by blast from 1 consider (a) "(∃lc. pfx = la @ [x] @ lc ∧ lb = lc @ l @ sfx)" | (b) "(∃lc. la = pfx @ lc ∧ l @ sfx = lc @ [x] @ lb)" using APPEND_EQ_APPEND_MID[of la x lb pfx "l @ sfx"] by presburger then have "∃pfx' sfx. (pfx' @ l @ sfx = la) ∨ (pfx'@ l @ sfx = lb)" proof (cases) case a ― ‹NOTE `lc` is `l'` in original proof.› then obtain lc where a: "pfx = la @ [x] @ lc" "lb = lc @ l @ sfx" by blast then show ?thesis by blast next case b then obtain lc where i: "la = pfx @ lc" "l @ sfx = lc @ [x] @ lb" by blast then show ?thesis using 2 by (metis APPEND_EQ_APPEND_MID) qed } then show ?thesis unfolding sublist_def by blast qed lemma LIST_FRAG_DICHOTOMY_2: fixes l la x lb P assumes "sublist l (la @ [x] @ lb) " "¬P x" "list_all P l" shows "sublist l la ∨ sublist l lb" proof - { assume "¬P x" "list_all P l" then have "¬ListMem x l" proof (induction l arbitrary: x P) case Nil then show ?case using ListMem_iff by force next case (Cons a l) { have "list_all P l" using Cons.prems(2) by simp then have "¬ListMem x l" using Cons.prems(1) Cons.IH by blast } moreover { have "P a" using Cons.prems(2) by simp then have "a ≠ x" using Cons.prems(1) by meson } ultimately show ?case using Cons.prems(1, 2) ListMem_iff list.pred_set by metis qed } then have "¬ListMem x l" using assms(2, 3) by fast then show ?thesis using assms(1) LIST_FRAG_DICHOTOMY by metis qed lemma frag_len_filter_le: fixes P l' l assumes "sublist l' l" shows "length (filter P l') ≤ length (filter P l)" proof - obtain ps ss where "l = ps @ l' @ ss" using assms sublist_def by blast then have 1: "length (filter P l) = length (filter P ps) + length (filter P l') + length (filter P ss)" by force then have "length (filter P ps) ≥ 0" "length (filter P ss) ≥ 0" by blast+ then show ?thesis using 1 by linarith qed end