# Package list-member-def: Definition of the list member function

## Information

name | list-member-def |

version | 1.21 |

description | Definition of the list member function |

author | Joe Hurd <joe@gilith.com> |

license | HOLLight |

provenance | HOL Light theory extracted on 2011-11-27 |

requires | bool list-def |

show | Data.Bool Data.List |

## Files

- Package tarball list-member-def-1.21.tgz
- Theory file list-member-def.thy (included in the package tarball)

## Defined Constant

- Data
- List
- member

- List

## Theorems

⊦ ∀x. ¬member x []

⊦ ∀x h t. member x (h :: t) ⇔ x = h ∨ member x t

## Input Type Operators

- →
- bool
- Data
- List
- list

- List

## Input Constants

- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- F
- T

- List
- ::
- []

- Bool

## Assumptions

⊦ T

⊦ (∃) = λP. P ((select) P)

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

⊦ ∀t. (t ⇔ F) ⇔ ¬t

⊦ (⇒) = λp q. p ∧ q ⇔ p

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

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ ∀NIL' CONS'.

∃fn. fn [] = NIL' ∧ ∀a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)