(* Title: FOL/ex/list
ID: $Id$
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Examples of simplification and induction on lists
*)
List = Nat2 +
types list 1
arities list :: (term)term
consts
hd :: "'a list => 'a"
tl :: "'a list => 'a list"
forall :: "['a list, 'a => o] => o"
len :: "'a list => nat"
at :: "['a list, nat] => 'a"
"[]" :: "'a list" ("[]")
"." :: "['a, 'a list] => 'a list" (infixr 80)
"++" :: "['a list, 'a list] => 'a list" (infixr 70)
rules
list_ind "[| P([]); ALL x l. P(l)-->P(x.l) |] ==> All(P)"
forall_cong
"[| l = l'; !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
list_distinct1 "~[] = x.l"
list_distinct2 "~x.l = []"
list_free "x.l = x'.l' <-> x=x' & l=l'"
app_nil "[]++l = l"
app_cons "(x.l)++l' = x.(l++l')"
tl_eq "tl(m.q) = q"
hd_eq "hd(m.q) = m"
forall_nil "forall([],P)"
forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
len_nil "len([]) = 0"
len_cons "len(m.q) = succ(len(q))"
at_0 "at(m.q,0) = m"
at_succ "at(m.q,succ(n)) = at(q,n)"
end