src/FOL/ex/List.ML
changeset 22822 c1a6a2159e69
parent 22821 15b2e7ec1f3b
child 22823 fa9ff469247f
     1.1 --- a/src/FOL/ex/List.ML	Fri Apr 27 14:21:23 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,60 +0,0 @@
     1.4 -(*  Title:      FOL/ex/list
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -*)
     1.9 -
    1.10 -val prems = goal (the_context ()) "[| P([]);  !!x l. P(x . l) |] ==> All(P)";
    1.11 -by (rtac list_ind 1);
    1.12 -by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
    1.13 -qed "list_exh";
    1.14 -
    1.15 -Addsimps [list_distinct1, list_distinct2, app_nil, app_cons,
    1.16 -	  hd_eq, tl_eq, forall_nil, forall_cons, list_free,
    1.17 -	  len_nil, len_cons, at_0, at_succ];
    1.18 -
    1.19 -Goal "~l=[] --> hd(l).tl(l) = l";
    1.20 -by (IND_TAC list_exh Simp_tac "l" 1);
    1.21 -result();
    1.22 -
    1.23 -Goal "(l1++l2)++l3 = l1++(l2++l3)";
    1.24 -by (IND_TAC list_ind Simp_tac "l1" 1);
    1.25 -qed "append_assoc";
    1.26 -
    1.27 -Goal "l++[] = l";
    1.28 -by (IND_TAC list_ind Simp_tac "l" 1);
    1.29 -qed "app_nil_right";
    1.30 -
    1.31 -Goal "l1++l2=[] <-> l1=[] & l2=[]";
    1.32 -by (IND_TAC list_exh Simp_tac "l1" 1);
    1.33 -qed "app_eq_nil_iff";
    1.34 -
    1.35 -Goal "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
    1.36 -by (IND_TAC list_ind Simp_tac "l" 1);
    1.37 -qed "forall_app";
    1.38 -
    1.39 -Goal "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
    1.40 -by (IND_TAC list_ind Simp_tac "l" 1);
    1.41 -by (Fast_tac 1);
    1.42 -qed "forall_conj";
    1.43 -
    1.44 -Goal "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
    1.45 -by (IND_TAC list_ind Simp_tac "l" 1);
    1.46 -qed "forall_ne";
    1.47 -
    1.48 -(*** Lists with natural numbers ***)
    1.49 -
    1.50 -Goal "len(l1++l2) = len(l1)+len(l2)";
    1.51 -by (IND_TAC list_ind Simp_tac "l1" 1);
    1.52 -qed "len_app";
    1.53 -
    1.54 -Goal "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
    1.55 -by (IND_TAC list_ind Simp_tac "l1" 1);
    1.56 -by (REPEAT (rtac allI 1));
    1.57 -by (rtac impI 1);
    1.58 -by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
    1.59 -qed "at_app1";
    1.60 -
    1.61 -Goal "at(l1++(x . l2), len(l1)) = x";
    1.62 -by (IND_TAC list_ind Simp_tac "l1" 1);
    1.63 -qed "at_app_hd2";