List.ML: added lemmas by Stefan Merz.
authornipkow
Thu Jul 24 11:12:18 1997 +0200 (1997-07-24)
changeset 3571f1c8fa0f0bf9
parent 3570 d3662f90c453
child 3572 5ec1589eac1b
List.ML: added lemmas by Stefan Merz.
simpodata.ML: removed rules about ? now subsumed by simplification proc.
src/HOL/List.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/List.ML	Thu Jul 24 10:46:32 1997 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Jul 24 11:12:18 1997 +0200
     1.3 @@ -112,6 +112,16 @@
     1.4  qed_spec_mp "append1_eq_conv";
     1.5  AddIffs [append1_eq_conv];
     1.6  
     1.7 +goal thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
     1.8 +by (induct_tac "xs" 1);
     1.9 +by (Simp_tac 1);
    1.10 +by (strip_tac 1);
    1.11 +by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
    1.12 +by (Asm_full_simp_tac 1);
    1.13 +by (Blast_tac 1);
    1.14 +qed_spec_mp "append_same_eq";
    1.15 +AddIffs [append_same_eq];
    1.16 +
    1.17  goal thy "xs ~= [] --> hd xs # tl xs = xs";
    1.18  by (induct_tac "xs" 1);
    1.19  by (ALLGOALS Asm_simp_tac);
    1.20 @@ -123,10 +133,22 @@
    1.21  by (ALLGOALS Asm_simp_tac);
    1.22  qed "hd_append";
    1.23  
    1.24 +goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
    1.25 +by (asm_simp_tac (!simpset addsimps [hd_append]
    1.26 +                           setloop (split_tac [expand_list_case])) 1);
    1.27 +qed "hd_append2";
    1.28 +Addsimps [hd_append2];
    1.29 +
    1.30  goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
    1.31  by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
    1.32  qed "tl_append";
    1.33  
    1.34 +goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
    1.35 +by (asm_simp_tac (!simpset addsimps [tl_append]
    1.36 +                           setloop (split_tac [expand_list_case])) 1);
    1.37 +qed "tl_append2";
    1.38 +Addsimps [tl_append2];
    1.39 +
    1.40  (** map **)
    1.41  
    1.42  section "map";
     2.1 --- a/src/HOL/simpdata.ML	Thu Jul 24 10:46:32 1997 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Thu Jul 24 11:12:18 1997 +0200
     2.3 @@ -103,7 +103,7 @@
     2.4     "(P | P) = P", "(P | (P | Q)) = (P | Q)",
     2.5     "((~P) = (~Q)) = (P=Q)",
     2.6     "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
     2.7 -   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
     2.8 +   "(? x. x=t & P(x)) = P(t)", (*"(? x. t=x & P(x)) = P(t)",*)
     2.9     "(! x. t=x --> P(x)) = P(t)" ];
    2.10  
    2.11  (*Add congruence rules for = (instead of ==) *)