Theory patternMatches

⊢ ∀is xs.
    APPLY_REDUNDANT_ROWS_INFO is xs =
    MAP SND (FILTER (λx. ¬FST x) (ZIP (is,xs)))

⊢ ∀v rows c infos.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇔
    (LENGTH rows = LENGTH infos) ∧
    (∀i. i < LENGTH rows ⇒ infos❲i❳ ⇒ PMATCH_ROW_REDUNDANT v rows i) ∧
    (EVERY (λr. r v = NONE) rows ⇒ c)

⊢ ∀v rows1 rows2.
    PMATCH_EQUIV_ROWS v rows1 rows2 ⇔
    (PMATCH v rows1 = PMATCH v rows2) ∧
    ((∃r. MEM r rows1 ∧ IS_SOME (r v)) ⇔ ∃r. MEM r rows2 ∧ IS_SOME (r v))

⊢ (∀P v rows_before.
     PMATCH_EXPAND_PRED P v rows_before [] ⇔
     ¬PMATCH_IS_EXHAUSTIVE v (REVERSE rows_before) ⇒ P ARB) ∧
  ∀P v rows_before r rows_after.
    PMATCH_EXPAND_PRED P v rows_before (r::rows_after) ⇔
    (r v ≠ NONE ⇒
     EVERY (λr'. r' v ≠ NONE ⇒ (r' v = r v)) rows_before ⇒
     P (THE (r v))) ∧ PMATCH_EXPAND_PRED P v (r::rows_before) rows_after

⊢ ∀p g row v.
    PMATCH_FLATTEN_FUN p g row v =
    case some x. PMATCH_ROW_COND p g v x of
      NONE => NONE
    | SOME x => row x x

⊢ PMATCH_INCOMPLETE = ARB

⊢ ∀v rs. PMATCH_IS_EXHAUSTIVE v rs ⇔ EXISTS (λr. IS_SOME (r v)) rs

⊢ ∀i p g. PMATCH_ROW_COND_EX i p g ⇔ ∃x. PMATCH_ROW_COND p g i x

⊢ ∀i r rows.
    PMATCH_ROW_COND_NOT_EX_OR_EQ i r rows ⇔
    ¬(r i ≠ NONE) ∨
    EXISTS (λrow. row i ≠ NONE) rows ∧ (THE (r i) = PMATCH i rows)

⊢ ∀pat guard inp v.
    PMATCH_ROW_COND pat guard inp v ⇔ (pat v = inp) ∧ guard v

⊢ ∀f r. PMATCH_ROW_LIFT f r = (λx. OPTION_MAP f (r x))

⊢ ∀v rs i.
    PMATCH_ROW_REDUNDANT v rs i ⇔
    i < LENGTH rs ∧
    (IS_SOME (fEL rs i v) ⇒ ∃j. j < i ∧ IS_SOME (fEL rs j v))

⊢ ∀pat guard rhs i.
    PMATCH_ROW pat guard rhs i =
    OPTION_MAP rhs (some v. PMATCH_ROW_COND pat guard i v)

⊢ (∀v. PMATCH v [] = PMATCH_INCOMPLETE) ∧
  ∀v r rs. PMATCH v (r::rs) = option_CASE (r v) (PMATCH v rs) I

⊢ ∀ip1 ip2.
    REDUNDANT_ROWS_INFOS_CONJ ip1 ip2 = MAP2 (λi1 i2. i1 ∧ i2) ip1 ip2

⊢ ∀ip1 ip2.
    REDUNDANT_ROWS_INFOS_DISJ ip1 ip2 = MAP2 (λi1 i2. i1 ∨ i2) ip1 ip2

⊢ (∀v p infos. STRONGEST_REDUNDANT_ROWS_INFO_AUX v [] p infos = (p,infos)) ∧
  ∀v r rows p infos.
    STRONGEST_REDUNDANT_ROWS_INFO_AUX v (r::rows) p infos =
    STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows (p ∧ (r v = NONE))
      (SNOC (p ⇒ (r v = NONE)) infos)

⊢ ∀v rows.
    STRONGEST_REDUNDANT_ROWS_INFO v rows =
    SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows T [])

⊢ (APPLY_REDUNDANT_ROWS_INFO [] [] = []) ∧
  (∀is x xs.
     APPLY_REDUNDANT_ROWS_INFO (T::is) (x::xs) =
     APPLY_REDUNDANT_ROWS_INFO is xs) ∧
  ∀is x xs.
    APPLY_REDUNDANT_ROWS_INFO (F::is) (x::xs) =
    x::APPLY_REDUNDANT_ROWS_INFO is xs

⊢ ∀v rows p infos i.
    i < LENGTH infos ⇒
    ((SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos))❲i❳ ⇔ infos❲i❳)

⊢ ∀v rows p infos i.
    i ≥ LENGTH infos ∧ i < LENGTH rows + LENGTH infos ⇒
    ((SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos))❲i❳ ⇔
     p ∧ EVERY (λr. r v = NONE) (TAKE (i − LENGTH infos) rows) ⇒
     (fEL rows (i − LENGTH infos) v = NONE))

⊢ ∀v rows i.
    i < LENGTH rows ⇒
    ((STRONGEST_REDUNDANT_ROWS_INFO v rows)❲i❳ ⇔
     EVERY (λr. r v = NONE) (TAKE i rows) ⇒ (fEL rows i v = NONE))

⊢ ∀v rows p infos.
    FST (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos) ⇔
    p ∧ EVERY (λr. r v = NONE) rows

⊢ ∀v rs1 rs2 p g r.
    (∀x1 x2. (p x1 = p x2) ⇒ (x1 = x2)) ⇒
    (PMATCH v (rs1 ⧺ PMATCH_ROW p g r::rs2) =
     PMATCH v
       (rs1 ⧺
        PMATCH_ROW p (λx. T) (λx. if g x then r x else PMATCH (p x) rs2)::
          rs2))

⊢ IS_REDUNDANT_ROWS_INFO v (row::rows) c (i::infos') ⇔
  (LENGTH rows = LENGTH infos') ∧ (i ⇒ (row v = NONE)) ∧
  ((row v = NONE) ⇒ IS_REDUNDANT_ROWS_INFO v rows c infos')

⊢ ∀v rows c infos.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    ¬c ⇒
    PMATCH_IS_EXHAUSTIVE v rows

⊢ ∀v. IS_REDUNDANT_ROWS_INFO v [] T []

⊢ ∀v rows c infos r i c'.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    ((r v = NONE) ⇒ c ⇒ c') ⇒
    (c ⇒ i ⇒ (r v = NONE)) ⇒
    IS_REDUNDANT_ROWS_INFO v (SNOC r rows) c' (SNOC i infos)

⊢ ∀v rows c infos p g r c'.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    (¬PMATCH_ROW_COND_EX v p g ⇒ (c ⇔ c')) ⇒
    IS_REDUNDANT_ROWS_INFO v (SNOC (PMATCH_ROW p g r) rows) c'
      (SNOC (c ⇒ ¬PMATCH_ROW_COND_EX v p g) infos)

⊢ LENGTH (STRONGEST_REDUNDANT_ROWS_INFO v rows) = LENGTH rows

⊢ ∀v rows p infos.
    LENGTH (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) =
    LENGTH rows + LENGTH infos

⊢ ∀v rows1 rows2.
    PMATCH v (rows1 ⧺ rows2) =
    if ∃r. MEM r rows1 ∧ IS_SOME (r v) then PMATCH v rows1
    else PMATCH v rows2

⊢ ∀p g i.
    (∀x1 x2. g x1 ∧ g x2 ∧ (p x1 = p x2) ⇒ (x1 = x2)) ⇒
    ∀x. PMATCH_ROW_COND p g i x ⇒ ((@y. PMATCH_ROW_COND p g i y) = x)

⊢ ∀v v' rows rows' r r'.
    (v = v') ∧ (r v' = r' v') ∧ (PMATCH v' rows = PMATCH v' rows') ⇒
    (PMATCH v (r::rows) = PMATCH v' (r'::rows'))

⊢ ∀v rows1a rows1b rows2a rows2b.
    PMATCH_EQUIV_ROWS v rows1a rows1b ⇒
    PMATCH_EQUIV_ROWS v rows2a rows2b ⇒
    PMATCH_EQUIV_ROWS v (rows1a ⧺ rows2a) (rows1b ⧺ rows2b)

⊢ (row v = NONE) ⇒
  (PMATCH_EQUIV_ROWS v (row::rows) = PMATCH_EQUIV_ROWS v rows)

⊢ PMATCH_EQUIV_ROWS v rows1 rows2 ⇔
  (PMATCH_EQUIV_ROWS v rows1 = PMATCH_EQUIV_ROWS v rows2)

⊢ PMATCH_EQUIV_ROWS v rows1 rows2 ⇒ (PMATCH v rows1 = PMATCH v rows2)

⊢ ∀v rows. PMATCH_EQUIV_ROWS v rows rows

⊢ ∀v rows1 rows2.
    PMATCH_EQUIV_ROWS v rows1 rows2 ⇔ PMATCH_EQUIV_ROWS v rows2 rows1

⊢ ∀v rows1 rows2 rows3.
    PMATCH_EQUIV_ROWS v rows1 rows2 ⇒
    PMATCH_EQUIV_ROWS v rows2 rows3 ⇒
    PMATCH_EQUIV_ROWS v rows1 rows3

⊢ (PMATCH v [] = PMATCH_INCOMPLETE) ∧
  (PMATCH v (PMATCH_ROW p g r::rs) =
   if ∃x. PMATCH_ROW_COND p g v x then r (@x. PMATCH_ROW_COND p g v x)
   else PMATCH v rs)

⊢ PMATCH_ROW p g r v ≠ NONE ⇒
  (PMATCH v (PMATCH_ROW p g r::rs) = r (@x. PMATCH_ROW_COND p g v x))

⊢ ∀P v rows. P (PMATCH v rows) ⇔ PMATCH_EXPAND_PRED P v [] rows

⊢ ∀P v rows_before rows_after.
    PMATCH_EXPAND_PRED P v rows_before rows_after ⇔
    EVERY (λr. PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows_after) rows_before ⇒
    P (PMATCH v rows_after)

⊢ ∀v_old v_new. PMATCH v_old [] = PMATCH v_new []

⊢ ∀v_old v_new rows_old rows_new r_old r_new.
    (r_old v_old = r_new v_new) ⇒
    (PMATCH v_old rows_old = PMATCH v_new rows_new) ⇒
    (PMATCH v_old (r_old::rows_old) = PMATCH v_new (r_new::rows_new))

⊢ ∀v rows_old rows_new r.
    (PMATCH v rows_old = PMATCH v rows_new) ⇒
    (PMATCH v (r::rows_old) = PMATCH v (r::rows_new))

⊢ ∀v_old v_new rows_old rows_new r_old.
    (r_old v_old = NONE) ⇒
    (PMATCH v_old rows_old = PMATCH v_new rows_new) ⇒
    (PMATCH v_old (r_old::rows_old) = PMATCH v_new rows_new)

⊢ ∀p. (∀x1 x2. (p x1 = p x2) ⇒ (x1 = x2)) ⇒
      ∀g p' g' r'.
        PMATCH_FLATTEN_FUN p g (λx. PMATCH_ROW p' (g' x) (r' x)) =
        PMATCH_ROW (λx. p (p' x)) (λx. g (p' x) ∧ g' (p' x) x)
          (λx. r' (p' x) x)

⊢ ∀v p g rows1 rows2 rows.
    (∀x. PMATCH_IS_EXHAUSTIVE x (MAP (λr. r x) rows)) ⇒
    (PMATCH v
       (rows1 ⧺ PMATCH_ROW p g (λx. PMATCH x (MAP (λr. r x) rows))::rows2) =
     PMATCH v (rows1 ⧺ MAP (λr. PMATCH_FLATTEN_FUN p g r) rows ⧺ rows2))

⊢ ∀v p g rows.
    (∀x. PMATCH_IS_EXHAUSTIVE x (MAP (λr. r x) rows)) ⇒
    PMATCH_EQUIV_ROWS v
      [PMATCH_ROW p g (λx. PMATCH x (MAP (λr. r x) rows))]
      (MAP (λr. PMATCH_FLATTEN_FUN p g r) rows)

⊢ PMATCH v rows =
  PMATCH v (SNOC (PMATCH_ROW (λ_0. _0) (λ_0. T) (λ_0. ARB)) rows)

⊢ ∀v rs. (EVERY (λr. r v = NONE) rs ⇒ F) ⇒ PMATCH_IS_EXHAUSTIVE v rs

⊢ ∀f v rows.
    PMATCH_IS_EXHAUSTIVE v rows ⇒
    PMATCH_IS_EXHAUSTIVE v (MAP (PMATCH_ROW_LIFT f) rows)

⊢ (∀v. PMATCH_IS_EXHAUSTIVE v [] ⇔ F) ∧
  ∀v r rs.
    PMATCH_IS_EXHAUSTIVE v (r::rs) ⇔ r v ≠ NONE ∨ PMATCH_IS_EXHAUSTIVE v rs

⊢ ∀f v rows.
    PMATCH_IS_EXHAUSTIVE v rows ⇒
    (f (PMATCH v rows) = PMATCH v (MAP (PMATCH_ROW_LIFT f) rows))

⊢ ∀P v r rows.
    P (PMATCH v (r::rows)) ⇔
    (r v ≠ NONE ⇒ P (THE (r v))) ∧
    (PMATCH_ROW_COND_NOT_EX_OR_EQ v r rows ⇒ P (PMATCH v rows))

⊢ ∀P v. P (PMATCH v []) = P ARB

⊢ ∀p g r v rows.
    (∀x. r x = ARB) ⇒
    (PMATCH v (SNOC (PMATCH_ROW p g r) rows) = PMATCH v rows)

⊢ ∀v p g r rows1 rows2.
    (∀x. r x = ARB) ∧
    (∀x. (v = p x) ∧ g x ⇒ EVERY (λrow. row (p x) = NONE) rows2) ⇒
    (PMATCH v (rows1 ⧺ PMATCH_ROW p g r::rows2) = PMATCH v (rows1 ⧺ rows2))

⊢ ∀r1 r2 rows1 rows2 rows3 v.
    (IS_SOME (r2 v) ⇒ IS_SOME (r1 v)) ⇒
    (PMATCH v (rows1 ⧺ r1::rows2 ⧺ r2::rows3) =
     PMATCH v (rows1 ⧺ r1::rows2 ⧺ rows3))

⊢ ∀p g r p' g' r' rows1 rows2 rows3 v.
    (∀x'. (v = p' x') ∧ g' x' ⇒ ∃x. (p' x' = p x) ∧ g x) ⇒
    (PMATCH v
       (rows1 ⧺ PMATCH_ROW p g r::rows2 ⧺ PMATCH_ROW p' g' r'::rows3) =
     PMATCH v (rows1 ⧺ PMATCH_ROW p g r::rows2 ⧺ rows3))

⊢ ∀v c rows infos.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    PMATCH_EQUIV_ROWS v rows (APPLY_REDUNDANT_ROWS_INFO infos rows)

⊢ ∀v rows n.
    n < LENGTH rows ∧ IS_SOME (fEL rows n v) ⇒
    (PMATCH v rows = PMATCH v (TAKE (SUC n) rows))

⊢ ∀v rows n.
    n < LENGTH rows ∧ IS_SOME (fEL rows n v) ⇒
    PMATCH_EQUIV_ROWS v rows (TAKE (SUC n) rows)

⊢ ∀r1 r2 rows1 rows2 rows3 v.
    (∀x. (r1 v = SOME x) ⇒ (r2 v = SOME x)) ∧
    (IS_SOME (r1 v) ⇒ EVERY (λrow. row v = NONE) rows2) ⇒
    (PMATCH v (rows1 ⧺ r1::(rows2 ⧺ r2::rows3)) =
     PMATCH v (rows1 ⧺ rows2 ⧺ r2::rows3))

⊢ ∀p g r p' g' r' rows1 rows2 rows3 v.
    (∀x. (v = p x) ∧ g x ⇒ ∃x'. (p x = p' x') ∧ g' x') ∧
    (∀x x'. (v = p x) ∧ (p x = p' x') ∧ g x ∧ g' x' ⇒ (r x = r' x')) ∧
    (∀x. (v = p x) ∧ g x ⇒ EVERY (λrow. row (p x) = NONE) rows2) ⇒
    (PMATCH v
       (rows1 ⧺ PMATCH_ROW p g r::(rows2 ⧺ PMATCH_ROW p' g' r'::rows3)) =
     PMATCH v (rows1 ⧺ rows2 ⧺ PMATCH_ROW p' g' r'::rows3))

⊢ PMATCH_ROW_COND pat guard inp v ⇔ (inp = pat v) ∧ guard v

⊢ ∀v p g. (∀x. ¬g x) ⇒ (PMATCH_ROW_COND_EX v p g ⇔ F)

⊢ PMATCH_ROW_COND_EX i p g ⇔ ∃x. (i = p x) ∧ g x

⊢ ∀v p g p' g' RES.
    PMATCH_ROW_COND_EX v p g ⇒
    (∀x. g x ⇒ ((∃x'. (p' x' = p x) ∧ g' x') ⇔ RES)) ⇒
    (PMATCH_ROW_COND_EX v p' g' ⇔ RES)

⊢ ∀f v p g p' g'.
    ¬PMATCH_ROW_COND_EX v p g ⇒
    (∀x. p' x = p (f x)) ⇒
    (PMATCH_ROW_COND_EX v p' g' ⇔
     PMATCH_ROW_COND_EX v p' (λx. g' x ∧ ¬g (f x)))

⊢ ∀i r r' rows.
    r' i ≠ NONE ⇒
    (PMATCH_ROW_COND_NOT_EX_OR_EQ i r (r'::rows) ⇔
     r i ≠ NONE ⇒ (r i = r' i))

⊢ PMATCH_ROW_COND_NOT_EX_OR_EQ i r [] ⇔ r i ≠ NONE ⇒ F

⊢ PMATCH_ROW_COND_NOT_EX_OR_EQ i r' rows ⇒
  (PMATCH_ROW_COND_NOT_EX_OR_EQ i r (r'::rows) ⇔
   PMATCH_ROW_COND_NOT_EX_OR_EQ i r rows)

⊢ ∀p p' g g' r r' v v'.
    (p = p') ∧ (v = v') ∧ (∀x. (v = p x) ⇒ (g x ⇔ g' x)) ∧
    (∀x. (v = p x) ∧ g x ⇒ (r x = r' x)) ⇒
    (PMATCH_ROW p g r v = PMATCH_ROW p' g' r' v')

⊢ (∀i. (∃x. PMATCH_ROW_COND p g i x) ⇔ ∃x'. PMATCH_ROW_COND p' g' i x') ∧
  (∀x x'. (p x = p' x') ∧ g x ∧ g' x' ⇒ (r x = r' x')) ⇒
  (PMATCH_ROW p g r = PMATCH_ROW p' g' r')

⊢ (PMATCH_ROW p g r i = NONE) ⇔ ∀x. ¬PMATCH_ROW_COND p g i x

⊢ (PMATCH_ROW p g r i = SOME y) ⇒ ∃x. PMATCH_ROW_COND p g i x ∧ (y = r x)

⊢ PMATCH_ROW_COND_EX i p g ⇒
  (PMATCH_ROW p g r i = SOME (r (@x. PMATCH_ROW_COND p g i x)))

⊢ ∀v v' f' f p g r p'.
    (∀x'. (v' = p' x') ⇒ (p (f x') = v)) ∧
    (∀x. (v = p x) ⇒ ∃x'. p' x' = v') ∧ (∀x y. (p x = p y) ⇒ (x = y)) ⇒
    (PMATCH_ROW p (g (f' v')) (r (f' v')) v =
     PMATCH_ROW p' (λx. g (f' (p' x)) (f x)) (λx. r (f' (p' x)) (f x)) v')

⊢ ∀f p g r.
    PMATCH_ROW_LIFT f (PMATCH_ROW p g r) = PMATCH_ROW p g (λx. f (r x))

⊢ PMATCH_ROW p g r i ≠ NONE ⇔ PMATCH_ROW_COND_EX i p g

⊢ PMATCH_ROW_REDUNDANT v (r::rs) 0 ⇔ (r v = NONE)

⊢ ∀v rs1 rs2 i.
    ¬(i < LENGTH rs1) ⇒
    (PMATCH_ROW_REDUNDANT v (rs1 ⧺ rs2) i ⇔
     ¬EVERY (λr. r v = NONE) rs1 ∧ i < LENGTH rs1 + LENGTH rs2 ∨
     PMATCH_ROW_REDUNDANT v rs2 (i − LENGTH rs1))

⊢ ∀v rs1 rs2 i.
    i < LENGTH rs1 ⇒
    (PMATCH_ROW_REDUNDANT v (rs1 ⧺ rs2) i ⇔ PMATCH_ROW_REDUNDANT v rs1 i)

⊢ PMATCH_ROW_REDUNDANT v [] i ⇔ F

⊢ ∀v r rs i.
    PMATCH_ROW_REDUNDANT v (r::rs) (SUC i) ⇔
    r v ≠ NONE ∧ i < LENGTH rs ∨ PMATCH_ROW_REDUNDANT v rs i

⊢ ∀g p1 g1 r1 p2 g2 r2.
    (∀x y. (p1 x = p1 y) ⇒ (x = y)) ∧ (∀x. p2 (g x) = p1 x) ∧
    (∀x'. g2 x' ⇔ ∃x. (x' = g x) ∧ g1 x) ∧ (∀x. r2 (g x) = r1 x) ⇒
    (PMATCH_ROW p1 g1 r1 = PMATCH_ROW p2 g2 r2)

⊢ ∀ff v p g r.
    (∀x y. (ff x = ff y) ⇒ (x = y)) ⇒
    (PMATCH_ROW (λx. ff (p x)) g r (ff v) = PMATCH_ROW (λx. p x) g r v)

⊢ ∀v v' f p g r p'.
    (∀x'. (v' = p' x') ⇔ (p (f x') = v)) ∧
    (∀x. (v = p x) ⇒ ∃x'. f x' = x) ∧ (∀x y. (p x = p y) ⇒ (x = y)) ⇒
    (PMATCH_ROW p g r v = PMATCH_ROW p' (λx. g (f x)) (λx. r (f x)) v')

⊢ (REDUNDANT_ROWS_INFOS_CONJ [] [] = []) ∧
  (REDUNDANT_ROWS_INFOS_CONJ (i1::is1) (i2::is2) =
   (i1 ∧ i2)::REDUNDANT_ROWS_INFOS_CONJ is1 is2)

⊢ ∀v rows c infos c' infos'.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    (LENGTH infos' = LENGTH infos) ⇒
    IS_REDUNDANT_ROWS_INFO v rows (c ∨ c')
      (REDUNDANT_ROWS_INFOS_CONJ infos infos')

⊢ ∀v rows c infos c' infos'.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    IS_REDUNDANT_ROWS_INFO v rows c' infos' ⇒
    IS_REDUNDANT_ROWS_INFO v rows (c ∧ c')
      (REDUNDANT_ROWS_INFOS_DISJ infos infos')

⊢ ∀v c rows infos.
    IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
    (PMATCH v rows = PMATCH v (APPLY_REDUNDANT_ROWS_INFO infos rows))

⊢ IS_REDUNDANT_ROWS_INFO v rows (EVERY (λr. r v = NONE) rows)
    (STRONGEST_REDUNDANT_ROWS_INFO v rows)

⊢ (some x. ¬x) = SOME F

⊢ (some x. x) = SOME T