Nat: added zero_neq_conv
authornipkow
Wed Oct 14 11:50:48 1998 +0200 (1998-10-14)
changeset 564485fd64148873
parent 5643 983ce1421211
child 5645 b872b209db69
Nat: added zero_neq_conv
List: added nth/update lemmas.
src/HOL/List.ML
src/HOL/Nat.ML
     1.1 --- a/src/HOL/List.ML	Tue Oct 13 14:25:01 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Oct 14 11:50:48 1998 +0200
     1.3 @@ -570,6 +570,10 @@
     1.4  
     1.5  section "nth";
     1.6  
     1.7 +Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
     1.8 +by(simp_tac (simpset() addsplits [nat.split]) 1);
     1.9 +qed "nth_Cons";
    1.10 +
    1.11  Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.12  by (induct_tac "n" 1);
    1.13   by (Asm_simp_tac 1);
    1.14 @@ -625,9 +629,17 @@
    1.15  qed_spec_mp "length_list_update";
    1.16  Addsimps [length_list_update];
    1.17  
    1.18 +Goal "!i j. i < length xs  --> (xs[i:=x])!j = (if i=j then x else xs!j)";
    1.19 +by(induct_tac "xs" 1);
    1.20 + by(Simp_tac 1);
    1.21 +by(auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
    1.22 +qed_spec_mp "nth_list_update";
    1.23 +
    1.24  
    1.25  (** last & butlast **)
    1.26  
    1.27 +section "last / butlast";
    1.28 +
    1.29  Goal "last(xs@[x]) = x";
    1.30  by (induct_tac "xs" 1);
    1.31  by Auto_tac;
     2.1 --- a/src/HOL/Nat.ML	Tue Oct 13 14:25:01 1998 +0200
     2.2 +++ b/src/HOL/Nat.ML	Wed Oct 14 11:50:48 1998 +0200
     2.3 @@ -38,6 +38,12 @@
     2.4  qed "neq0_conv";
     2.5  AddIffs [neq0_conv];
     2.6  
     2.7 +Goal "(0 ~= n) = (0 < n)";
     2.8 +by(exhaust_tac "n" 1);
     2.9 +by(Auto_tac);
    2.10 +qed "zero_neq_conv";
    2.11 +AddIffs [zero_neq_conv];
    2.12 +
    2.13  (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    2.14  bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    2.15