List.ML: added lemmas by Stefan Merz.
simpodata.ML: removed rules about ? now subsumed by simplification proc.

--- a/src/HOL/List.ML	Thu Jul 24 10:46:32 1997 +0200
+++ b/src/HOL/List.ML	Thu Jul 24 11:12:18 1997 +0200
@@ -112,6 +112,16 @@
 qed_spec_mp "append1_eq_conv";
 AddIffs [append1_eq_conv];
 
+goal thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "append_same_eq";
+AddIffs [append_same_eq];
+
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -123,10 +133,22 @@
 by (ALLGOALS Asm_simp_tac);
 qed "hd_append";
 
+goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
+by (asm_simp_tac (!simpset addsimps [hd_append]
+                           setloop (split_tac [expand_list_case])) 1);
+qed "hd_append2";
+Addsimps [hd_append2];
+
 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
 by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
 qed "tl_append";
 
+goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
+by (asm_simp_tac (!simpset addsimps [tl_append]
+                           setloop (split_tac [expand_list_case])) 1);
+qed "tl_append2";
+Addsimps [tl_append2];
+
 (** map **)
 
 section "map";

--- a/src/HOL/simpdata.ML	Thu Jul 24 10:46:32 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Jul 24 11:12:18 1997 +0200
@@ -103,7 +103,7 @@
    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    "((~P) = (~Q)) = (P=Q)",
    "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
-   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
+   "(? x. x=t & P(x)) = P(t)", (*"(? x. t=x & P(x)) = P(t)",*)
    "(! x. t=x --> P(x)) = P(t)" ];
 
 (*Add congruence rules for = (instead of ==) *)