src/FOL/ex/List.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 352 fd3ab8bcb69d
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	FOL/ex/list
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Tobias Nipkow
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Examples of simplification and induction on lists
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
List = Nat2 +
clasohm@0
    10
clasohm@0
    11
types list 1
clasohm@0
    12
arities list :: (term)term
clasohm@0
    13
clasohm@0
    14
consts
clasohm@0
    15
   hd		:: "'a list => 'a"
clasohm@0
    16
   tl		:: "'a list => 'a list"
clasohm@0
    17
   forall	:: "['a list, 'a => o] => o"
clasohm@0
    18
   len		:: "'a list => nat"
clasohm@0
    19
   at		:: "['a list, nat] => 'a"
clasohm@0
    20
   "[]"		:: "'a list"	("[]")
clasohm@0
    21
   "."		:: "['a, 'a list] => 'a list"  (infixr 80)
clasohm@0
    22
   "++"		:: "['a list, 'a list] => 'a list" (infixr 70)
clasohm@0
    23
clasohm@0
    24
rules
clasohm@0
    25
 list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"
clasohm@0
    26
clasohm@0
    27
 forall_cong 
clasohm@0
    28
  "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
clasohm@0
    29
clasohm@0
    30
 list_distinct1 "~[] = x.l"
clasohm@0
    31
 list_distinct2 "~x.l = []"
clasohm@0
    32
clasohm@0
    33
 list_free 	"x.l = x'.l' <-> x=x' & l=l'"
clasohm@0
    34
clasohm@0
    35
 app_nil 	"[]++l = l"
clasohm@0
    36
 app_cons 	"(x.l)++l' = x.(l++l')"
clasohm@0
    37
 tl_eq 	"tl(m.q) = q"
clasohm@0
    38
 hd_eq 	"hd(m.q) = m"
clasohm@0
    39
clasohm@0
    40
 forall_nil "forall([],P)"
clasohm@0
    41
 forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
clasohm@0
    42
clasohm@0
    43
 len_nil "len([]) = 0"
clasohm@0
    44
 len_cons "len(m.q) = succ(len(q))"
clasohm@0
    45
clasohm@0
    46
 at_0 "at(m.q,0) = m"
clasohm@0
    47
 at_succ "at(m.q,succ(n)) = at(q,n)"
clasohm@0
    48
clasohm@0
    49
end