Package list-filter-thm: list-filter-thm

Information

namelist-filter-thm
version1.11
descriptionlist-filter-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-25
showData.Bool

Files

Theorems

p l.
    Number.Natural.≤ (Data.List.length (Data.List.filter p l))
      (Data.List.length l)

p l. Set.⊆ (Data.List.toSet (Data.List.filter p l)) (Data.List.toSet l)

P l1 l2.
    Data.List.filter P (Data.List.@ l1 l2) =
    Data.List.@ (Data.List.filter P l1) (Data.List.filter P l2)

P f l.
    Data.List.filter P (Data.List.map f l) =
    Data.List.map f (Data.List.filter (Function.o P f) l)

Input Type Operators

Input Constants

Assumptions

T

n. Number.Natural.≤ n n

s. Set.⊆ s s

F p. p

n. Number.Natural.≤ n (Number.Natural.suc n)

(~) = λp. p F

t. (x. t) t

() = λp. p = λx. T

x. x = x T

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f T T

() = λP. q. (x. P x q) q

x s. Set.∪ (Set.insert x Set.∅) s = Set.insert x s

m n.
    Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n)
    Number.Natural.≤ m n

f g x. Function.o f g x = f (g x)

m n p.
    Number.Natural.≤ m n Number.Natural.≤ n p Number.Natural.≤ m p

s t u. Set.⊆ s t Set.⊆ t u Set.⊆ s u

t1 t2. (if T then t1 else t2) = t1 (if F then t1 else t2) = t2

Data.List.length Data.List.[] = 0
  h t.
    Data.List.length (Data.List.:: h t) =
    Number.Natural.suc (Data.List.length t)

Data.List.toSet Data.List.[] = Set.∅
  h t.
    Data.List.toSet (Data.List.:: h t) = Set.insert h (Data.List.toSet t)

(s t. Set.⊆ s (Set.∪ s t)) s t. Set.⊆ s (Set.∪ t s)

s t u. Set.⊆ (Set.∪ s t) u Set.⊆ s u Set.⊆ t u

P. P Data.List.[] (a0 a1. P a1 P (Data.List.:: a0 a1)) x. P x

P c x y. P (if c then x else y) (c P x) (¬c P y)

(l. Data.List.@ Data.List.[] l = l)
  l h t.
    Data.List.@ (Data.List.:: h t) l = Data.List.:: h (Data.List.@ t l)

(f. Data.List.map f Data.List.[] = Data.List.[])
  f h t.
    Data.List.map f (Data.List.:: h t) =
    Data.List.:: (f h) (Data.List.map f t)

(P. Data.List.filter P Data.List.[] = Data.List.[])
  P h t.
    Data.List.filter P (Data.List.:: h t) =
    if P h then Data.List.:: h (Data.List.filter P t)
    else Data.List.filter P t

t. (T t t) (t T t) (F t F) (t F F) (t t t)