src/HOL/List.ML
changeset 4647 42af8ae6e2c1
parent 4643 1b40fcac5a09
child 4681 a331c1f5a23e
     1.1 --- a/src/HOL/List.ML	Mon Feb 23 11:24:49 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Feb 24 10:44:53 1998 +0100
     1.3 @@ -180,6 +180,18 @@
     1.4  AddSDs
     1.5   [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
     1.6  
     1.7 +goal thy "(xs @ ys = ys) = (xs=[])";
     1.8 +by(cut_inst_tac [("zs","[]")] append_same_eq 1);
     1.9 +by(Asm_full_simp_tac 1);
    1.10 +qed "append_self_conv2";
    1.11 +
    1.12 +goal thy "(ys = xs @ ys) = (xs=[])";
    1.13 +by(simp_tac (simpset() addsimps
    1.14 +     [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
    1.15 +by(Blast_tac 1);
    1.16 +qed "self_append_conv2";
    1.17 +AddIffs [append_self_conv2,self_append_conv2];
    1.18 +
    1.19  goal thy "xs ~= [] --> hd xs # tl xs = xs";
    1.20  by (induct_tac "xs" 1);
    1.21  by (ALLGOALS Asm_simp_tac);