Nat: added zero_neq_conv
List: added nth/update lemmas.
--- a/src/HOL/List.ML Tue Oct 13 14:25:01 1998 +0200
+++ b/src/HOL/List.ML Wed Oct 14 11:50:48 1998 +0200
@@ -570,6 +570,10 @@
section "nth";
+Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
+by(simp_tac (simpset() addsplits [nat.split]) 1);
+qed "nth_Cons";
+
Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
@@ -625,9 +629,17 @@
qed_spec_mp "length_list_update";
Addsimps [length_list_update];
+Goal "!i j. i < length xs --> (xs[i:=x])!j = (if i=j then x else xs!j)";
+by(induct_tac "xs" 1);
+ by(Simp_tac 1);
+by(auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
+qed_spec_mp "nth_list_update";
+
(** last & butlast **)
+section "last / butlast";
+
Goal "last(xs@[x]) = x";
by (induct_tac "xs" 1);
by Auto_tac;
--- a/src/HOL/Nat.ML Tue Oct 13 14:25:01 1998 +0200
+++ b/src/HOL/Nat.ML Wed Oct 14 11:50:48 1998 +0200
@@ -38,6 +38,12 @@
qed "neq0_conv";
AddIffs [neq0_conv];
+Goal "(0 ~= n) = (0 < n)";
+by(exhaust_tac "n" 1);
+by(Auto_tac);
+qed "zero_neq_conv";
+AddIffs [zero_neq_conv];
+
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);