src/FOL/ex/List.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/List.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,67 @@
+(*  Title: 	FOL/ex/list
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1991  University of Cambridge
+
+For ex/list.thy.  Examples of simplification and induction on lists
+*)
+
+open List;
+
+val prems = goal List.thy "[| P([]);  !!x l. P(x.l) |] ==> All(P)";
+by (rtac list_ind 1);
+by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
+val list_exh = result();
+
+val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons,
+		     hd_eq,tl_eq,forall_nil,forall_cons,list_free,
+		     len_nil,len_cons,at_0,at_succ];
+
+val list_ss = nat_ss addsimps list_rew_thms;
+
+goal List.thy "~l=[] --> hd(l).tl(l) = l";
+by(IND_TAC list_exh (simp_tac list_ss) "l" 1);
+result();
+
+goal List.thy "(l1++l2)++l3 = l1++(l2++l3)";
+by(IND_TAC list_ind (simp_tac list_ss) "l1" 1);
+val append_assoc = result();
+
+goal List.thy "l++[] = l";
+by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
+val app_nil_right = result();
+
+goal List.thy "l1++l2=[] <-> l1=[] & l2=[]";
+by(IND_TAC list_exh (simp_tac list_ss) "l1" 1);
+val app_eq_nil_iff = result();
+
+goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
+by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
+val forall_app = result();
+
+goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
+by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
+by(fast_tac FOL_cs 1);
+val forall_conj = result();
+
+goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
+by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
+val forall_ne = result();
+
+(*** Lists with natural numbers ***)
+
+goal List.thy "len(l1++l2) = len(l1)+len(l2)";
+by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
+val len_app = result();
+
+goal List.thy "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
+by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (ALL_IND_TAC nat_exh (asm_simp_tac list_ss) 1);
+val at_app1 = result();
+
+goal List.thy "at(l1++(x.l2), len(l1)) = x";
+by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
+val at_app_hd2 = result();
+