src/FOL/ex/list.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/list.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,49 @@
+(*  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