Structure patternMatchesTheory


Source File Identifier index Theory binding index

signature patternMatchesTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val APPLY_REDUNDANT_ROWS_INFO_def : thm
    val IS_REDUNDANT_ROWS_INFO_def : thm
    val PMATCH_EQUIV_ROWS_def : thm
    val PMATCH_EXPAND_PRED_def : thm
    val PMATCH_FLATTEN_FUN_def : thm
    val PMATCH_INCOMPLETE_def : thm
    val PMATCH_IS_EXHAUSTIVE_def : thm
    val PMATCH_ROW_COND_EX_def : thm
    val PMATCH_ROW_COND_NOT_EX_OR_EQ_def : thm
    val PMATCH_ROW_COND_def : thm
    val PMATCH_ROW_LIFT_def : thm
    val PMATCH_ROW_REDUNDANT_def : thm
    val PMATCH_ROW_def : thm
    val PMATCH_def : thm
    val REDUNDANT_ROWS_INFOS_CONJ_def : thm
    val REDUNDANT_ROWS_INFOS_DISJ_def : thm
    val STRONGEST_REDUNDANT_ROWS_INFO_AUX_def : thm
    val STRONGEST_REDUNDANT_ROWS_INFO_def : thm
  
  (*  Theorems  *)
    val APPLY_REDUNDANT_ROWS_INFO_THMS : thm
    val EL1_STRONGEST_REDUNDANT_ROWS_INFO_AUX : thm
    val EL2_STRONGEST_REDUNDANT_ROWS_INFO_AUX : thm
    val EL_STRONGEST_REDUNDANT_ROWS_INFO : thm
    val FST_STRONGEST_REDUNDANT_ROWS_INFO_AUX : thm
    val GUARDS_ELIM_THM : thm
    val IS_REDUNDANT_ROWS_INFO_CONS : thm
    val IS_REDUNDANT_ROWS_INFO_EXTRACT_IS_EXHAUSTIVE : thm
    val IS_REDUNDANT_ROWS_INFO_NIL : thm
    val IS_REDUNDANT_ROWS_INFO_SNOC : thm
    val IS_REDUNDANT_ROWS_INFO_SNOC_PMATCH_ROW : thm
    val LENGTH_STRONGEST_REDUNDANT_ROWS_INFO : thm
    val LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX : thm
    val PMATCH_APPEND_SEM : thm
    val PMATCH_COND_SELECT_UNIQUE : thm
    val PMATCH_CONG : thm
    val PMATCH_EQUIV_APPEND : thm
    val PMATCH_EQUIV_ROWS_CONS_NONE : thm
    val PMATCH_EQUIV_ROWS_EQUIV_EXPAND : thm
    val PMATCH_EQUIV_ROWS_MATCH : thm
    val PMATCH_EQUIV_ROWS_is_equiv_1 : thm
    val PMATCH_EQUIV_ROWS_is_equiv_2 : thm
    val PMATCH_EQUIV_ROWS_is_equiv_3 : thm
    val PMATCH_EVAL : thm
    val PMATCH_EVAL_MATCH : thm
    val PMATCH_EXPAND_PRED_THM : thm
    val PMATCH_EXPAND_PRED_THM_GEN : thm
    val PMATCH_EXTEND_BASE : thm
    val PMATCH_EXTEND_BOTH : thm
    val PMATCH_EXTEND_BOTH_ID : thm
    val PMATCH_EXTEND_OLD : thm
    val PMATCH_FLATTEN_FUN_PMATCH_ROW : thm
    val PMATCH_FLATTEN_THM : thm
    val PMATCH_FLATTEN_THM_SINGLE : thm
    val PMATCH_INTRO_CATCHALL : thm
    val PMATCH_IS_EXHAUSTIVE_CONTRADICT : thm
    val PMATCH_IS_EXHAUSTIVE_LIFT : thm
    val PMATCH_IS_EXHAUSTIVE_REWRITES : thm
    val PMATCH_LIFT_THM : thm
    val PMATCH_PRED_UNROLL_CONS : thm
    val PMATCH_PRED_UNROLL_NIL : thm
    val PMATCH_REMOVE_ARB : thm
    val PMATCH_REMOVE_ARB_NO_OVERLAP : thm
    val PMATCH_ROWS_DROP_REDUNDANT : thm
    val PMATCH_ROWS_DROP_REDUNDANT_PMATCH_ROWS : thm
    val PMATCH_ROWS_DROP_REDUNDANT_ROWS_INFO_EQUIV : thm
    val PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS : thm
    val PMATCH_ROWS_DROP_REDUNDANT_TRIVIAL_SOUNDNESS_EQUIV : thm
    val PMATCH_ROWS_DROP_SUBSUMED : thm
    val PMATCH_ROWS_DROP_SUBSUMED_PMATCH_ROWS : thm
    val PMATCH_ROW_COND_DEF_GSYM : thm
    val PMATCH_ROW_COND_EX_FALSE : thm
    val PMATCH_ROW_COND_EX_FULL_DEF : thm
    val PMATCH_ROW_COND_EX_IMP_REWRITE : thm
    val PMATCH_ROW_COND_EX_WEAKEN : thm
    val PMATCH_ROW_COND_NOT_EX_OR_EQ_FIRST_ROW : thm
    val PMATCH_ROW_COND_NOT_EX_OR_EQ_NIL : thm
    val PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW : thm
    val PMATCH_ROW_CONG : thm
    val PMATCH_ROW_EQ_AUX : thm
    val PMATCH_ROW_EQ_NONE : thm
    val PMATCH_ROW_EQ_SOME : thm
    val PMATCH_ROW_EVAL_COND_EX : thm
    val PMATCH_ROW_EXTEND_INPUT : thm
    val PMATCH_ROW_LIFT_THM : thm
    val PMATCH_ROW_NEQ_NONE : thm
    val PMATCH_ROW_REDUNDANT_0 : thm
    val PMATCH_ROW_REDUNDANT_APPEND_GE : thm
    val PMATCH_ROW_REDUNDANT_APPEND_LT : thm
    val PMATCH_ROW_REDUNDANT_NIL : thm
    val PMATCH_ROW_REDUNDANT_SUC : thm
    val PMATCH_ROW_REMOVE_DOUBLE_BINDS_THM : thm
    val PMATCH_ROW_REMOVE_FUN : thm
    val PMATCH_ROW_REMOVE_FUN_VAR : thm
    val REDUNDANT_ROWS_INFOS_CONJ_REWRITE : thm
    val REDUNDANT_ROWS_INFOS_CONJ_THM : thm
    val REDUNDANT_ROWS_INFOS_DISJ_THM : thm
    val REDUNDANT_ROWS_INFO_TO_PMATCH_EQ : thm
    val STRONGEST_REDUNDANT_ROWS_INFO_OK : thm
    val some_var_bool_F : thm
    val some_var_bool_T : thm
  
  val patternMatches_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [quantHeuristics] Parent theory of "patternMatches"
   
   [rich_list] Parent theory of "patternMatches"
   
   [APPLY_REDUNDANT_ROWS_INFO_def]  Definition
      
      ⊢ ∀is xs.
            APPLY_REDUNDANT_ROWS_INFO is xs =
            MAP SND (FILTER (λx. ¬FST x) (ZIP (is,xs)))
   
   [IS_REDUNDANT_ROWS_INFO_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ PMATCH_INCOMPLETE = ARB
   
   [PMATCH_IS_EXHAUSTIVE_def]  Definition
      
      ⊢ ∀v rs. PMATCH_IS_EXHAUSTIVE v rs ⇔ EXISTS (λr. IS_SOME (r v)) rs
   
   [PMATCH_ROW_COND_EX_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀pat guard inp v.
            PMATCH_ROW_COND pat guard inp v ⇔ (pat v = inp) ∧ guard v
   
   [PMATCH_ROW_LIFT_def]  Definition
      
      ⊢ ∀f r. PMATCH_ROW_LIFT f r = (λx. OPTION_MAP f (r x))
   
   [PMATCH_ROW_REDUNDANT_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀pat guard rhs i.
            PMATCH_ROW pat guard rhs i =
            OPTION_MAP rhs (some v. PMATCH_ROW_COND pat guard i v)
   
   [PMATCH_def]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ ∀ip1 ip2.
            REDUNDANT_ROWS_INFOS_CONJ ip1 ip2 =
            MAP2 (λi1 i2. i1 ∧ i2) ip1 ip2
   
   [REDUNDANT_ROWS_INFOS_DISJ_def]  Definition
      
      ⊢ ∀ip1 ip2.
            REDUNDANT_ROWS_INFOS_DISJ ip1 ip2 =
            MAP2 (λi1 i2. i1 ∨ i2) ip1 ip2
   
   [STRONGEST_REDUNDANT_ROWS_INFO_AUX_def]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ ∀v rows.
            STRONGEST_REDUNDANT_ROWS_INFO v rows =
            SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows T [])
   
   [APPLY_REDUNDANT_ROWS_INFO_THMS]  Theorem
      
      ⊢ (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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀v rows p infos.
            FST (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos) ⇔
            p ∧ EVERY (λr. r v = NONE) rows
   
   [GUARDS_ELIM_THM]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ 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]  Theorem
      
      ⊢ ∀v rows c infos.
            IS_REDUNDANT_ROWS_INFO v rows c infos ⇒
            ¬c ⇒
            PMATCH_IS_EXHAUSTIVE v rows
   
   [IS_REDUNDANT_ROWS_INFO_NIL]  Theorem
      
      ⊢ ∀v. IS_REDUNDANT_ROWS_INFO v [] T []
   
   [IS_REDUNDANT_ROWS_INFO_SNOC]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ LENGTH (STRONGEST_REDUNDANT_ROWS_INFO v rows) = LENGTH rows
   
   [LENGTH_STRONGEST_REDUNDANT_ROWS_INFO_AUX]  Theorem
      
      ⊢ ∀v rows p infos.
            LENGTH (SND (STRONGEST_REDUNDANT_ROWS_INFO_AUX v rows p infos)) =
            LENGTH rows + LENGTH infos
   
   [PMATCH_APPEND_SEM]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (row v = NONE) ⇒
        (PMATCH_EQUIV_ROWS v (row::rows) = PMATCH_EQUIV_ROWS v rows)
   
   [PMATCH_EQUIV_ROWS_EQUIV_EXPAND]  Theorem
      
      ⊢ PMATCH_EQUIV_ROWS v rows1 rows2 ⇔
        (PMATCH_EQUIV_ROWS v rows1 = PMATCH_EQUIV_ROWS v rows2)
   
   [PMATCH_EQUIV_ROWS_MATCH]  Theorem
      
      ⊢ PMATCH_EQUIV_ROWS v rows1 rows2 ⇒ (PMATCH v rows1 = PMATCH v rows2)
   
   [PMATCH_EQUIV_ROWS_is_equiv_1]  Theorem
      
      ⊢ ∀v rows. PMATCH_EQUIV_ROWS v rows rows
   
   [PMATCH_EQUIV_ROWS_is_equiv_2]  Theorem
      
      ⊢ ∀v rows1 rows2.
            PMATCH_EQUIV_ROWS v rows1 rows2 ⇔
            PMATCH_EQUIV_ROWS v rows2 rows1
   
   [PMATCH_EQUIV_ROWS_is_equiv_3]  Theorem
      
      ⊢ ∀v rows1 rows2 rows3.
            PMATCH_EQUIV_ROWS v rows1 rows2 ⇒
            PMATCH_EQUIV_ROWS v rows2 rows3 ⇒
            PMATCH_EQUIV_ROWS v rows1 rows3
   
   [PMATCH_EVAL]  Theorem
      
      ⊢ (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]  Theorem
      
      ⊢ 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]  Theorem
      
      ⊢ ∀P v rows. P (PMATCH v rows) ⇔ PMATCH_EXPAND_PRED P v [] rows
   
   [PMATCH_EXPAND_PRED_THM_GEN]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀v_old v_new. PMATCH v_old [] = PMATCH v_new []
   
   [PMATCH_EXTEND_BOTH]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ PMATCH v rows =
        PMATCH v (SNOC (PMATCH_ROW (λ_0. _0) (λ_0. T) (λ_0. ARB)) rows)
   
   [PMATCH_IS_EXHAUSTIVE_CONTRADICT]  Theorem
      
      ⊢ ∀v rs. (EVERY (λr. r v = NONE) rs ⇒ F) ⇒ PMATCH_IS_EXHAUSTIVE v rs
   
   [PMATCH_IS_EXHAUSTIVE_LIFT]  Theorem
      
      ⊢ ∀f v rows.
            PMATCH_IS_EXHAUSTIVE v rows ⇒
            PMATCH_IS_EXHAUSTIVE v (MAP (PMATCH_ROW_LIFT f) rows)
   
   [PMATCH_IS_EXHAUSTIVE_REWRITES]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀f v rows.
            PMATCH_IS_EXHAUSTIVE v rows ⇒
            (f (PMATCH v rows) = PMATCH v (MAP (PMATCH_ROW_LIFT f) rows))
   
   [PMATCH_PRED_UNROLL_CONS]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀P v. P (PMATCH v []) = P ARB
   
   [PMATCH_REMOVE_ARB]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ PMATCH_ROW_COND pat guard inp v ⇔ (inp = pat v) ∧ guard v
   
   [PMATCH_ROW_COND_EX_FALSE]  Theorem
      
      ⊢ ∀v p g. (∀x. ¬g x) ⇒ (PMATCH_ROW_COND_EX v p g ⇔ F)
   
   [PMATCH_ROW_COND_EX_FULL_DEF]  Theorem
      
      ⊢ PMATCH_ROW_COND_EX i p g ⇔ ∃x. (i = p x) ∧ g x
   
   [PMATCH_ROW_COND_EX_IMP_REWRITE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ PMATCH_ROW_COND_NOT_EX_OR_EQ i r [] ⇔ r i ≠ NONE ⇒ F
   
   [PMATCH_ROW_COND_NOT_EX_OR_EQ_NOT_FIRST_ROW]  Theorem
      
      ⊢ 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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (PMATCH_ROW p g r i = NONE) ⇔ ∀x. ¬PMATCH_ROW_COND p g i x
   
   [PMATCH_ROW_EQ_SOME]  Theorem
      
      ⊢ (PMATCH_ROW p g r i = SOME y) ⇒
        ∃x. PMATCH_ROW_COND p g i x ∧ (y = r x)
   
   [PMATCH_ROW_EVAL_COND_EX]  Theorem
      
      ⊢ 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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ PMATCH_ROW p g r i ≠ NONE ⇔ PMATCH_ROW_COND_EX i p g
   
   [PMATCH_ROW_REDUNDANT_0]  Theorem
      
      ⊢ PMATCH_ROW_REDUNDANT v (r::rs) 0 ⇔ (r v = NONE)
   
   [PMATCH_ROW_REDUNDANT_APPEND_GE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀v rs1 rs2 i.
            i < LENGTH rs1 ⇒
            (PMATCH_ROW_REDUNDANT v (rs1 ⧺ rs2) i ⇔
             PMATCH_ROW_REDUNDANT v rs1 i)
   
   [PMATCH_ROW_REDUNDANT_NIL]  Theorem
      
      ⊢ PMATCH_ROW_REDUNDANT v [] i ⇔ F
   
   [PMATCH_ROW_REDUNDANT_SUC]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ IS_REDUNDANT_ROWS_INFO v rows (EVERY (λr. r v = NONE) rows)
          (STRONGEST_REDUNDANT_ROWS_INFO v rows)
   
   [some_var_bool_F]  Theorem
      
      ⊢ (some x. ¬x) = SOME F
   
   [some_var_bool_T]  Theorem
      
      ⊢ (some x. x) = SOME T
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13