Structure patternMatchesTheory
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
HOL 4, Kananaskis-13