src/HOL/List.ML
changeset 9268 4313b08b6e1b
parent 9187 68ecc04785f1
child 9336 9ae89b9ce206
     1.1 --- a/src/HOL/List.ML	Thu Jul 06 15:36:59 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Jul 06 15:38:00 2000 +0200
     1.3 @@ -48,21 +48,11 @@
     1.4  qed "lists_Int_eq";
     1.5  Addsimps [lists_Int_eq];
     1.6  
     1.7 -
     1.8 -(**  Case analysis **)
     1.9 -section "Case analysis";
    1.10 -
    1.11 -val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    1.12 -by (induct_tac "xs" 1);
    1.13 -by (REPEAT(resolve_tac prems 1));
    1.14 -qed "list_cases";
    1.15 -
    1.16 -Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    1.17 -by (induct_tac "xs" 1);
    1.18 -by (Blast_tac 1);
    1.19 -by (Blast_tac 1);
    1.20 -bind_thm("list_eq_cases",
    1.21 -  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
    1.22 +Goal "(xs@ys : lists A) = (xs : lists A & ys : lists A)";
    1.23 +by(induct_tac "xs" 1);
    1.24 +by(Auto_tac);
    1.25 +qed "append_in_lists_conv";
    1.26 +AddIffs [append_in_lists_conv];
    1.27  
    1.28  (** length **)
    1.29  (* needs to come before "@" because of thm append_eq_append_conv *)