src/FOL/ex/list.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
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
For ex/list.thy.  Examples of simplification and induction on lists
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open List;
clasohm@0
    10
clasohm@0
    11
val prems = goal List.thy "[| P([]);  !!x l. P(x.l) |] ==> All(P)";
clasohm@0
    12
by (rtac list_ind 1);
clasohm@0
    13
by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
clasohm@0
    14
val list_exh = result();
clasohm@0
    15
clasohm@0
    16
val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons,
clasohm@0
    17
		     hd_eq,tl_eq,forall_nil,forall_cons,list_free,
clasohm@0
    18
		     len_nil,len_cons,at_0,at_succ];
clasohm@0
    19
clasohm@0
    20
val list_ss = nat_ss addsimps list_rew_thms;
clasohm@0
    21
clasohm@0
    22
goal List.thy "~l=[] --> hd(l).tl(l) = l";
clasohm@0
    23
by(IND_TAC list_exh (simp_tac list_ss) "l" 1);
clasohm@0
    24
result();
clasohm@0
    25
clasohm@0
    26
goal List.thy "(l1++l2)++l3 = l1++(l2++l3)";
clasohm@0
    27
by(IND_TAC list_ind (simp_tac list_ss) "l1" 1);
clasohm@0
    28
val append_assoc = result();
clasohm@0
    29
clasohm@0
    30
goal List.thy "l++[] = l";
clasohm@0
    31
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
clasohm@0
    32
val app_nil_right = result();
clasohm@0
    33
clasohm@0
    34
goal List.thy "l1++l2=[] <-> l1=[] & l2=[]";
clasohm@0
    35
by(IND_TAC list_exh (simp_tac list_ss) "l1" 1);
clasohm@0
    36
val app_eq_nil_iff = result();
clasohm@0
    37
clasohm@0
    38
goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
clasohm@0
    39
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
clasohm@0
    40
val forall_app = result();
clasohm@0
    41
clasohm@0
    42
goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
clasohm@0
    43
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
clasohm@0
    44
by(fast_tac FOL_cs 1);
clasohm@0
    45
val forall_conj = result();
clasohm@0
    46
clasohm@0
    47
goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
clasohm@0
    48
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
clasohm@0
    49
val forall_ne = result();
clasohm@0
    50
clasohm@0
    51
(*** Lists with natural numbers ***)
clasohm@0
    52
clasohm@0
    53
goal List.thy "len(l1++l2) = len(l1)+len(l2)";
clasohm@0
    54
by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
clasohm@0
    55
val len_app = result();
clasohm@0
    56
clasohm@0
    57
goal List.thy "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
clasohm@0
    58
by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
clasohm@0
    59
by (REPEAT (rtac allI 1));
clasohm@0
    60
by (rtac impI 1);
clasohm@0
    61
by (ALL_IND_TAC nat_exh (asm_simp_tac list_ss) 1);
clasohm@0
    62
val at_app1 = result();
clasohm@0
    63
clasohm@0
    64
goal List.thy "at(l1++(x.l2), len(l1)) = x";
clasohm@0
    65
by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
clasohm@0
    66
val at_app_hd2 = result();
clasohm@0
    67