Theory "list_utils"

Parents     indexedLists   patternMatches

Signature

Constant Type
list_frag :α list # α list -> bool
list_frag_rec :α list # α list # α list -> bool

Definitions

list_frag_def
|- ∀l frag. list_frag (l,frag) ⇔ ∃pfx sfx. pfx ⧺ frag ⧺ sfx = l
list_frag_rec_primitive_def
|- list_frag_rec =
   WFREC
     (@R.
        WF R ∧
        (∀l' l_original l h_orig h' h.
           h ≠ h' ∧ h ≠ h_orig ⇒
           R (l,h_orig::l_original,h_orig::l_original)
             (h::l,h'::l',h_orig::l_original)) ∧
        (∀l' l_original l h_orig h' h.
           h ≠ h' ∧ (h = h_orig) ⇒
           R (l,l_original,h_orig::l_original)
             (h::l,h'::l',h_orig::l_original)) ∧
        ∀l_original h_orig l' l h' h.
          (h = h') ⇒
          R (l,l',h_orig::l_original) (h::l,h'::l',h_orig::l_original))
     (λlist_frag_rec a.
        case a of
          (l'',[],l''') => I T
        | ([],h'::l',l''') => I F
        | (h::l,h'::l',[]) => I T
        | (h::l,h'::l',h_orig::l_original) =>
            I
              (if h = h' then list_frag_rec (l,l',h_orig::l_original)
               else if h = h_orig then
                 list_frag_rec (l,l_original,h_orig::l_original)
               else list_frag_rec (l,h_orig::l_original,h_orig::l_original)))


Theorems

LENGTH_0
|- (LENGTH l = 0) ⇔ (l = [])
IS_SUFFIX_MEM
|- IS_SUFFIX s (h::t) ⇒ MEM h s
IS_PREFIX_MEM
|- ∀y. x ≼ y ⇒ ∀e. MEM e x ⇒ MEM e y
MEM_LAST'
|- seq ≠ [] ⇒ MEM (LAST seq) seq
lemma_2_1_1_2
|- ∀l1 l2. LENGTH l1 > LENGTH l2 ⇒ l1 ≠ l2
LENGTH_INJ_PREFIXES
|- ∀x1 x2. x1 ≼ y ∧ x2 ≼ y ⇒ ((LENGTH x1 = LENGTH x2) ⇔ (x1 = x2))
lemma_2_3_1_4
|- ∀l. l ≠ [] ⇒ FRONT l ≼ l
non_empty_list
|- ∀l. l ≠ [] ⇒ ∃h t. l = h::t
lemma_2_3_2_1
|- ∀l. LENGTH l ≥ 0
lemma_2_3_2
|- ∀l l1 l2. LENGTH l2 > LENGTH l1 ∧ l1 ≼ l ∧ l2 ≼ l ⇒ l1 ≼ l2
lemma_3_1
|- ∀l1 l2 l3. l2 ≠ [] ⇒ LENGTH (l1 ⧺ l3) < LENGTH (l1 ⧺ l2 ⧺ l3)
graph_plan_lemma_19
|- ∀as s. set as ⊆ s ⇒ ∀a. MEM a as ⇒ a ∈ s
twosorted_list_length
|- ∀P1 P2 l k1 k2.
     (∀x. MEM x l ⇒ (¬P1 x ⇔ P2 x)) ∧ LENGTH (FILTER P1 l) < k1 ∧
     (∀l'.
        (∃pfx sfx. pfx ⧺ l' ⧺ sfx = l) ∧ (∀x. MEM x l' ⇒ P2 x) ⇒
        LENGTH l' < k2) ⇒
     LENGTH l < k1 * k2
graph_plan_lemma_6_2
|- ∀P l s. set l ⊆ s ⇒ set (FILTER P l) ⊆ s
graph_plan_lemma_8_1_1
|- ∀f1 f2 as1 as2 p.
     (as1 ⧺ as2 = FILTER f1 (MAP f2 p)) ⇒
     ∃p_1 p_2.
       (p_1 ⧺ p_2 = p) ∧ (as1 = FILTER f1 (MAP f2 p_1)) ∧
       (as2 = FILTER f1 (MAP f2 p_2))
graph_plan_lemma_8_1
|- ∀f1 f2 as1 as2 as3 p.
     (as1 ⧺ as2 ⧺ as3 = FILTER f1 (MAP f2 p)) ⇒
     ∃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))
graph_plan_lemma_8_1_1_light
|- ∀f1 f2 as1 as2 p.
     (as1 ⧺ as2 = MAP f2 p) ⇒
     ∃p_1 p_2. (p_1 ⧺ p_2 = p) ∧ (as1 = MAP f2 p_1) ∧ (as2 = MAP f2 p_2)
graph_plan_lemma_8_1_light
|- ∀f1 f2 as1 as2 as3 p.
     (as1 ⧺ as2 ⧺ as3 = MAP f2 p) ⇒
     ∃p_1 p_2 p_3.
       (p_1 ⧺ p_2 ⧺ p_3 = p) ∧ (as1 = MAP f2 p_1) ∧ (as2 = MAP f2 p_2) ∧
       (as3 = MAP f2 p_3)
graph_plan_lemma_14
|- ∀l f1 f2 x.
     MEM x (MAP f1 l) ∧ f2 x ∧ (∀g. SND (f1 g) = SND g) ∧
     (∀g h. (SND g = SND h) ⇒ (f2 g ⇔ f2 h)) ⇒
     ∃y. MEM y l ∧ f2 y
graph_plan_lemma_15_1
|- ∀l1 l2 l3 P.
     LENGTH (FILTER P l3) < LENGTH (FILTER P l2) ⇒
     LENGTH (FILTER P (l1 ⧺ l3)) < LENGTH (FILTER P (l1 ⧺ l2))
graph_plan_lemma_15_2
|- ∀l1 l2 l3 P.
     LENGTH (FILTER P l3) < LENGTH (FILTER P l2) ⇒
     LENGTH (FILTER P (l3 ⧺ l1)) < LENGTH (FILTER P (l2 ⧺ l1))
graph_plan_lemma_15
|- ∀l1 l2 l3 l4 P.
     LENGTH (FILTER P l2) < LENGTH (FILTER P l3) ⇒
     LENGTH (FILTER P (l1 ⧺ l2 ⧺ l4)) < LENGTH (FILTER P (l1 ⧺ l3 ⧺ l4))
graph_plan_lemma_20
|- ∀l P. EVERY P l ⇒ (LENGTH (FILTER P l) = LENGTH l)
graph_plan_lemma_21
|- ∀P1 P2 l. EVERY P1 l ∧ EVERY P2 l ⇔ EVERY (λa. P1 a ∧ P2 a) l
two_children_parent_bound_main_lemma_3_1_3
|- ∀P l. LENGTH (FILTER (λa. P a) l) + LENGTH (FILTER (λa. ¬P a) l) = LENGTH l
child_parent_lemma_2_1_1_1_2
|- ∀P l. (∃x. MEM x l ∧ P x) ⇒ LENGTH (FILTER (λx. ¬P x) l) < LENGTH l
FILTER_P_NOT_P_EMPTY
|- ∀P l. FILTER (λa. P a) (FILTER (λa. ¬P a) l) = []
child_parent_lemma_2_1_1_1_3_1_1
|- ∀P l. LENGTH (FILTER (λa. P a) (FILTER (λa. ¬P a) l)) = 0
child_parent_lemma_2_1_1_1_3_1
|- ∀P P2 l.
     (∃a. MEM a l ∧ P a) ⇒
     LENGTH (FILTER (λa. P a) (FILTER (λa. ¬P a ∧ P2 a) l)) <
     LENGTH (FILTER (λa. P a) l)
child_parent_lemma_2_1_2_2_2
|- ∀P l. (FILTER (λx. P x) l = []) ⇔ EVERY (λx. ¬P x) l
list_frag_rec_ind
|- ∀P.
     (∀h l h' l' h_orig l_original.
        (h ≠ h' ∧ h ≠ h_orig ⇒ P (l,h_orig::l_original,h_orig::l_original)) ∧
        (h ≠ h' ∧ (h = h_orig) ⇒ P (l,l_original,h_orig::l_original)) ∧
        ((h = h') ⇒ P (l,l',h_orig::l_original)) ⇒
        P (h::l,h'::l',h_orig::l_original)) ∧ (∀l l'. P (l,[],l')) ∧
     (∀h l l'. P ([],h::l,l')) ∧ (∀v8 v9 v4 v5. P (v8::v9,v4::v5,[])) ⇒
     ∀v v1 v2. P (v,v1,v2)
list_frag_rec_def
|- (∀l_original l' l h_orig h' h.
      list_frag_rec (h::l,h'::l',h_orig::l_original) ⇔
      if h = h' then list_frag_rec (l,l',h_orig::l_original)
      else if h = h_orig then list_frag_rec (l,l_original,h_orig::l_original)
      else list_frag_rec (l,h_orig::l_original,h_orig::l_original)) ∧
   (∀l' l. list_frag_rec (l,[],l') ⇔ T) ∧
   (∀l' l h. list_frag_rec ([],h::l,l') ⇔ F) ∧
   ∀v9 v8 v5 v4. list_frag_rec (v8::v9,v4::v5,[]) ⇔ T
child_parent_lemma_2_1_3_1_1_1_1
|- ∀l la x lb P.
     list_frag (la ⧺ [x] ⧺ lb,l) ∧ ¬MEM x l ⇒
     list_frag (la,l) ∨ list_frag (lb,l)
child_parent_lemma_2_1_3_1_1_1
|- ∀l la x lb P.
     list_frag (la ⧺ [x] ⧺ lb,l) ∧ ¬P x ∧ EVERY P l ⇒
     list_frag (la,l) ∨ list_frag (lb,l)
child_parent_lemma_2_1_3_1_1_2
|- ∀l' l. list_frag (l,l') ⇒ LENGTH l' ≤ LENGTH l
child_parent_lemma_2_1_3_1_1
|- ∀Ch k1 Par f s l PProbs PProbl.
     PProbs s ∧ PProbl l ∧
     (∀l s.
        PProbs s ∧ PProbl l ∧ EVERY Par l ⇒
        ∃l'.
          (f (s,l') = f (s,l)) ∧ LENGTH l' ≤ k1 ∧ EVERY Par l' ∧ PProbl l') ∧
     (∀a l. PProbl l ∧ MEM a l ⇒ (Ch a ⇔ ¬Par a)) ∧
     (∀s l1 l2. f (f (s,l1),l2) = f (s,l1 ⧺ l2)) ∧
     (∀l1 l2. PProbl (l1 ⧺ l2) ⇔ PProbl l1 ∧ PProbl l2) ∧
     (∀s l. PProbs s ∧ PProbl l ⇒ PProbs (f (s,l))) ⇒
     ∃l'.
       (f (s,l') = f (s,l)) ∧ (LENGTH (FILTER Ch l') = LENGTH (FILTER Ch l)) ∧
       (∀l''. list_frag (l',l'') ∧ EVERY Par l'' ⇒ LENGTH l'' ≤ k1) ∧
       PProbl l'
child_parent_lemma_2_1_3_1
|- ∀k1 k2 s Par Ch f l PProbs PProbl.
     PProbs s ∧ PProbl l ∧
     (∀l s.
        PProbs s ∧ PProbl l ∧ EVERY Par l ⇒
        ∃l'.
          (f (s,l') = f (s,l)) ∧ LENGTH l' ≤ k1 ∧ EVERY Par l' ∧ PProbl l') ∧
     (∀l s.
        PProbs s ∧ PProbl l ⇒
        ∃l'. (f (s,l') = f (s,l)) ∧ LENGTH (FILTER Ch l') ≤ k2 ∧ PProbl l') ∧
     (∀a l. PProbl l ∧ MEM a l ⇒ (Ch a ⇔ ¬Par a)) ∧
     (∀s l1 l2. f (f (s,l1),l2) = f (s,l1 ⧺ l2)) ∧
     (∀l1 l2. PProbl (l1 ⧺ l2) ⇔ PProbl l1 ∧ PProbl l2) ∧
     (∀s l. PProbs s ∧ PProbl l ⇒ PProbs (f (s,l))) ⇒
     ∃l'.
       (f (s,l') = f (s,l)) ∧ LENGTH (FILTER Ch l') ≤ k2 ∧
       (∀l''. list_frag (l',l'') ∧ EVERY Par l'' ⇒ LENGTH l'' ≤ k1) ∧
       PProbl l'
EVERY_ABSORB
|- ∀P1 P2 l. EVERY P2 l ⇒ (FILTER (λx. P1 x ∧ P2 x) l = FILTER (λx. P1 x) l)
parent_children_lemma_1_1_1_11_5_1
|- ∀P1 P2.
     (∀x. P1 x ⇒ P2 x) ⇒
     ∀l. LENGTH (FILTER (λa. P1 a) (FILTER (λa. ¬P2 a) l)) = 0
parent_children_lemma_1_1_1_11_5_2
|- ∀P1 P2 P3.
     (∀x. P1 x ∧ P2 x ⇒ P3 x) ⇒
     ∀l. EVERY P2 l ⇒ (LENGTH (FILTER (λa. P1 a) (FILTER (λa. ¬P3 a) l)) = 0)
parent_children_lemma_1_1_1_11_8
|- ∀l s. set l ⊆ s ⇒ EVERY (λx. x ∈ s) l
parent_children_lemma_1_1_2_1
|- ∀P l' l. list_frag (l,l') ⇒ LENGTH (FILTER P l') ≤ LENGTH (FILTER P l)
threesorted_list_length_1
|- ∀l. list_frag (l,l)
threesorted_list_length_2
|- ∀l l'. list_frag (l ⧺ l',l)
threesorted_list_length_3
|- ∀l l' l''. list_frag (l',l) ⇒ list_frag (l'' ⧺ l',l)
threesorted_list_length
|- ∀P1 P2 l k1 k2.
     LENGTH (FILTER P1 l) ≤ k1 ∧ (∀x. MEM x l ⇒ P1 x ⇒ ¬P2 x) ∧
     (∀l'.
        list_frag (l,l') ∧ EVERY (λx. ¬P1 x) l' ⇒
        LENGTH (FILTER P2 l') ≤ k2) ⇒
     LENGTH (FILTER P2 l) ≤ (k1 + 1) * k2
parent_children_main_lemma_1_1_2_1
|- ∀x l. MEM x l ⇔ MEM x l
parent_children_main_lemma_1_1_5_1_1
|- ∀P acc l. FOLDL (λx y. x ∧ P y) acc l ⇒ acc
parent_children_main_lemma_1_1_5_1_2
|- ∀P acc acc' l.
     (acc ⇒ acc') ∧ FOLDL (λx y. x ∧ P y) acc l ⇒ FOLDL (λx y. x ∧ P y) acc' l
parent_children_main_lemma_1_1_5_1_3
|- ∀P acc l. FOLDL (λx y. x ∧ P y) T l ∧ acc ⇒ FOLDL (λx y. x ∧ P y) acc l
parent_children_main_lemma_1_1_5_1
|- ∀P P' l.
     (∀x. P x ⇒ P' x) ∧ FOLDL (λx y. x ∧ P y) T l ⇒ FOLDL (λx y. x ∧ P' y) T l
parent_children_main_lemma_1_1_8_6
|- ∀x x' l.
     MEM x l ∧ MEM x' l ∧ x ≠ x' ⇒
     (∃pfx mid sfx. l = pfx ⧺ [x] ⧺ mid ⧺ [x'] ⧺ sfx) ∨
     ∃pfx mid sfx. l = pfx ⧺ [x'] ⧺ mid ⧺ [x] ⧺ sfx
parent_children_main_lemma_1_1_9
|- ∀P P' lvs.
     (∀vs. MEM vs lvs ∧ P vs ⇒ P' vs) ∧ EVERY (λvs'. P vs') lvs ⇒
     EVERY (λvs'. P' vs') lvs
parent_children_main_lemma_1_1_16_2
|- ∀f1 f2 P l.
     EVERY (λx. ¬P x) l ⇒
     (MAP (λx. if P x then f1 x else f2 x) l = MAP (λx. f2 x) l)
parent_children_main_lemma_1_3
|- ∀l. FILTER (λx. T) l = l
nondistinct_repeated_segment
|- ∀l. ¬ALL_DISTINCT l ⇒ ∃e l1 l2 l3. l = l1 ⧺ e::l2 ⧺ e::l3
TAKE_isPREFIX
|- ∀m n l. m ≤ n ∧ n ≤ LENGTH l ⇒ TAKE m l ≼ TAKE n l
N_gen_valid_thm_2
|- ∀f1 f2 l. (∀x. f1 x ≤ f2 x) ⇒ SUM (MAP f1 l) ≤ SUM (MAP f2 l)
N_super_gen_valid_thm_2
|- ∀f1 f2 l. (∀x. MEM x l ⇒ f1 x ≤ f2 x) ⇒ SUM (MAP f1 l) ≤ SUM (MAP f2 l)
MAP_LAMBDA_ABSTRACTION_thm
|- MAP f l = MAP (λx. f x) l
FOLDL_TRUE_eq_EVERY_TRUE
|- FOLDL (λx y. x ∧ P y) T l ⇔ EVERY (λy. P y) l