Theory "patternMatches"

Signature

Definitions

APPLY_REDUNDANT_ROWS_INFO_def

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

IS_REDUNDANT_ROWS_INFO_def

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

PMATCH_EQUIV_ROWS_def

⊢ ∀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))

PMATCH_EXPAND_PRED_def

⊢ (∀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

PMATCH_FLATTEN_FUN_def

⊢ ∀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_def

⊢ PMATCH_INCOMPLETE = ARB

PMATCH_IS_EXHAUSTIVE_def

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

PMATCH_ROW_COND_EX_def

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

PMATCH_ROW_COND_NOT_EX_OR_EQ_def

⊢ ∀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)

PMATCH_ROW_COND_def

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

PMATCH_ROW_LIFT_def

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

PMATCH_ROW_REDUNDANT_def

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

PMATCH_ROW_def

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

PMATCH_def

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

REDUNDANT_ROWS_INFOS_CONJ_def

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

REDUNDANT_ROWS_INFOS_DISJ_def

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

STRONGEST_REDUNDANT_ROWS_INFO_AUX_def

⊢ (∀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)

STRONGEST_REDUNDANT_ROWS_INFO_def

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

Theorems

APPLY_REDUNDANT_ROWS_INFO_THMS

⊢ (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

EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX

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

EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX

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

EL_STRONGEST_REDUNDANT_ROWS_INFO

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

FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX

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

GUARDS_ELIM_THM

⊢ ∀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_CONS

⊢ 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')

IS_REDUNDANT_ROWS_INFO_EXTRACT_IS_EXHAUSTIVE

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

IS_REDUNDANT_ROWS_INFO_NIL

⊢ ∀v. IS_REDUNDANT_ROWS_INFO v [] T []

IS_REDUNDANT_ROWS_INFO_SNOC

⊢ ∀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)

IS_REDUNDANT_ROWS_INFO_SNOC_PMATCH_ROW

⊢ ∀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

⊢ LENGTH (STRONGEST_REDUNDANT_ROWS_INFO v rows) = LENGTH rows

LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX

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

PMATCH_APPEND_SEM

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

PMATCH_COND_SELECT_UNIQUE

⊢ ∀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)

PMATCH_CONG

⊢ ∀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'))

PMATCH_EQUIV_APPEND

⊢ ∀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)

PMATCH_EQUIV_ROWS_CONS_NONE

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

PMATCH_EQUIV_ROWS_EQUIV_EXPAND

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

PMATCH_EQUIV_ROWS_MATCH

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

PMATCH_EQUIV_ROWS_is_equiv_1

⊢ ∀v rows. PMATCH_EQUIV_ROWS v rows rows

PMATCH_EQUIV_ROWS_is_equiv_2

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

PMATCH_EQUIV_ROWS_is_equiv_3

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

PMATCH_EVAL

⊢ (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_EVAL_MATCH

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

PMATCH_EXPAND_PRED_THM

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

PMATCH_EXPAND_PRED_THM_GEN

⊢ ∀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)

PMATCH_EXTEND_BASE

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

PMATCH_EXTEND_BOTH

⊢ ∀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))

PMATCH_EXTEND_BOTH_ID

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

PMATCH_EXTEND_OLD

⊢ ∀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)

PMATCH_FLATTEN_FUN_PMATCH_ROW

⊢ ∀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)

PMATCH_FLATTEN_THM

⊢ ∀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))

PMATCH_FLATTEN_THM_SINGLE

⊢ ∀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_INTRO_CATCHALL

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

PMATCH_IS_EXHAUSTIVE_CONTRADICT

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

PMATCH_IS_EXHAUSTIVE_LIFT

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

PMATCH_IS_EXHAUSTIVE_REWRITES

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

PMATCH_LIFT_THM

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

PMATCH_PRED_UNROLL_CONS

⊢ ∀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))

PMATCH_PRED_UNROLL_NIL

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

PMATCH_REMOVE_ARB

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

PMATCH_REMOVE_ARB_NO_OVERLAP

⊢ ∀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))

PMATCH_ROWS_DROP_REDUNDANT

⊢ ∀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))

PMATCH_ROWS_DROP_REDUNDANT_PMATCH_ROWS

⊢ ∀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))

PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV

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

PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS

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

PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV

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

PMATCH_ROWS_DROP_SUBSUMED

⊢ ∀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))

PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS

⊢ ∀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_DEF_GSYM

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

PMATCH_ROW_COND_EX_FALSE

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

PMATCH_ROW_COND_EX_FULL_DEF

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

PMATCH_ROW_COND_EX_IMP_REWRITE

⊢ ∀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)

PMATCH_ROW_COND_EX_WEAKEN

⊢ ∀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)))

PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW

⊢ ∀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_NIL

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

PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW

⊢ 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)

PMATCH_ROW_CONG

⊢ ∀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')

PMATCH_ROW_EQ_AUX

⊢ (∀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_EQ_NONE

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

PMATCH_ROW_EQ_SOME

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

PMATCH_ROW_EVAL_COND_EX

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

PMATCH_ROW_EXTEND_INPUT

⊢ ∀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')

PMATCH_ROW_LIFT_THM

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

PMATCH_ROW_NEQ_NONE

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

PMATCH_ROW_REDUNDANT_0

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

PMATCH_ROW_REDUNDANT_APPEND_GE

⊢ ∀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))

PMATCH_ROW_REDUNDANT_APPEND_LT

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

PMATCH_ROW_REDUNDANT_NIL

⊢ PMATCH_ROW_REDUNDANT v [] i ⇔ F

PMATCH_ROW_REDUNDANT_SUC

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

PMATCH_ROW_REMOVE_DOUBLE_BINDS_THM

⊢ ∀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)

PMATCH_ROW_REMOVE_FUN

⊢ ∀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)

PMATCH_ROW_REMOVE_FUN_VAR

⊢ ∀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_REWRITE

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

REDUNDANT_ROWS_INFOS_CONJ_THM

⊢ ∀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')

REDUNDANT_ROWS_INFOS_DISJ_THM

⊢ ∀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')

REDUNDANT_ROWS_INFO_TO_PMATCH_EQ

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

STRONGEST_REDUNDANT_ROWS_INFO_OK

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

some_var_bool_F

⊢ (some x. ¬x) = SOME F

some_var_bool_T

⊢ (some x. x) = SOME T