The Theory list
Parents

Children
char
Constants
IsListRep
(ℕ → 'a) × ℕ → BOOL
[]
'a LIST
Cons
'a → 'a LIST → 'a LIST
Length
'a LIST → ℕ
Hd
'a LIST → 'a
Tl
'a LIST → 'a LIST
Append
'a LIST → 'a LIST → 'a LIST
Rev
'a LIST → 'a LIST
Split
('a × 'b) LIST → 'a LIST × 'b LIST
Combine
'a LIST → 'b LIST → ('a × 'b) LIST
Map
('a → 'b) → 'a LIST → 'b LIST
Fold
('a → 'b → 'b) → 'a LIST → 'b → 'b
Aliases
@
Append : 'a LIST → 'a LIST → 'a LIST
Types
'1 LIST
Fixity
Right Infix 300:
@
Definitions
IsListRep
is_list_rep_def
⊢ ∃ nil cons
fill• IsListRep nil
fill∧ (∀ x• IsListRep x ⇒ (∀ h• ¬ cons h x = nil))
fill∧ (∀ x y
fill• IsListRep x ∧ IsListRep y
fill⇒ (∀ a b
fill• cons a x = cons b y ⇔ a = b ∧ x = y))
fill∧ (∀ x
fill• IsListRep x ⇒ (∀ h• IsListRep (cons h x)))
fill∧ (∀ p
fill• p nil ∧ (∀ m• p m ⇒ (∀ h• p (cons h m)))
fill⇒ (∀ n• IsListRep n ⇒ p n))
LIST
list_def
⊢ ∃ f• TypeDefn IsListRep f
Nil
Cons
nil_cons_def
⊢ (∀ x list• ¬ Cons x list = [])
fill∧ (∀ x1 x2 list1 list2
fill• Cons x1 list1 = Cons x2 list2
fill⇔ x1 = x2 ∧ list1 = list2)
fill∧ (∀ p
fill• p [] ∧ (∀ list• p list ⇒ (∀ x• p (Cons x list)))
fill⇒ (∀ list• p list))
Length
length_def
⊢ # [] = 0 ∧ (∀ h list• # (Cons h list) = # list + 1)
Hd
hd_def
⊢ ∀ h list• Head (Cons h list) = h
Tl
tl_def
⊢ ∀ h list• Tail (Cons h list) = list
Append
append_def
⊢ (∀ list• [] @ list = list)
fill∧ (∀ h list list'
fill• Cons h list @ list' = Cons h (list @ list'))
Rev
rev_def
⊢ Rev [] = []
fill∧ (∀ h list• Rev (Cons h list) = Rev list @ [h])
Split
split_def
⊢ Split [] = ([], [])
fill∧ (∀ list h1 h2
fill• Split (Cons (h1, h2) list)
fill= (Cons h1 (Fst (Split list)),
fillCons h2 (Snd (Split list))))
Combine
combine_def
⊢ Combine [] [] = []
fill∧ (∀ h1 h2 list1 list2
fill• Combine (Cons h1 list1) (Cons h2 list2)
fill= Cons (h1, h2) (Combine list1 list2))
Map
map_def
⊢ (∀ g• Map g [] = [])
fill∧ (∀ h g list
fill• Map g (Cons h list) = Cons (g h) (Map g list))
Fold
fold_def
⊢ (∀ g x• Fold g [] x = x)
fill∧ (∀ h g x list
fill• Fold g (Cons h list) x = g h (Fold g list x))
Theorems
list_induction_thm
⊢ ∀ p
fill• p [] ∧ (∀ list• p list ⇒ (∀ x• p (Cons x list)))
fill⇒ (∀ list• p list)
list_prim_rec_thm
⊢ ∀ n c
fill• ∃1 f
fill• f [] = n
fill∧ (∀ list a
fill• f (Cons a list) = c a (f list) list)
list_clauses
⊢ ∀ x1 x2 list1 list2
fill• ¬ Cons x1 list1 = []
fill∧ ¬ [] = Cons x1 list1
fill∧ (Cons x1 list1 = Cons x2 list2
fill⇔ x1 = x2 ∧ list1 = list2)
fill∧ Head (Cons x1 list1) = x1
fill∧ Tail (Cons x1 list1) = list1
list_cases_thm
⊢ ∀ list1
fill• list1 = [] ∨ (∃ x list2• list1 = Cons x list2)

up quick index

privacy policy

Created:

V