added new arithmetic lemmas and the functions take and drop.
authornipkow
Sun Nov 12 16:29:12 1995 +0100 (1995-11-12)
changeset 13276c29cfab679c
parent 1326 1fbf9407757c
child 1328 9a449a91425d
added new arithmetic lemmas and the functions take and drop.
src/HOL/Arith.ML
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Arith.ML	Sun Nov 12 13:14:13 1995 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sun Nov 12 16:29:12 1995 +0100
     1.3 @@ -94,6 +94,21 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "add_left_cancel_less";
     1.6  
     1.7 +Addsimps [add_left_cancel, add_right_cancel,
     1.8 +          add_left_cancel_le, add_left_cancel_less];
     1.9 +
    1.10 +goal Arith.thy "(m+n = 0) = (m=0 & n=0)";
    1.11 +by (nat_ind_tac "m" 1);
    1.12 +by (ALLGOALS Asm_simp_tac);
    1.13 +qed "add_is_0";
    1.14 +Addsimps [add_is_0];
    1.15 +
    1.16 +goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
    1.17 +by (nat_ind_tac "m" 1);
    1.18 +by (ALLGOALS Asm_simp_tac);
    1.19 +qed "add_pred";
    1.20 +Addsimps [add_pred];
    1.21 +
    1.22  (*** Multiplication ***)
    1.23  
    1.24  (*right annihilation in product*)
    1.25 @@ -156,8 +171,6 @@
    1.26  goal Arith.thy "!!m::nat. m - n <= m";
    1.27  by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
    1.28  by (ALLGOALS Asm_simp_tac);
    1.29 -by (etac le_trans 1);
    1.30 -by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    1.31  qed "diff_le_self";
    1.32  
    1.33  goal Arith.thy "!!n::nat. (n+m) - n = m";
     2.1 --- a/src/HOL/List.ML	Sun Nov 12 13:14:13 1995 +0100
     2.2 +++ b/src/HOL/List.ML	Sun Nov 12 16:29:12 1995 +0100
     2.3 @@ -50,6 +50,10 @@
     2.4  by (ALLGOALS Asm_simp_tac);
     2.5  qed "same_append_eq";
     2.6  
     2.7 +goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
     2.8 +by (list.induct_tac "xs" 1);
     2.9 +by (ALLGOALS Asm_simp_tac);
    2.10 +qed "hd_append";
    2.11  
    2.12  (** rev **)
    2.13  
    2.14 @@ -181,6 +185,39 @@
    2.15  bind_thm ("nth_mem",result() RS spec RS mp);
    2.16  Addsimps [nth_mem];
    2.17  
    2.18 +(** drop **)
    2.19 +
    2.20 +goalw thy [drop_def] "drop 0 xs = xs";
    2.21 +by(Simp_tac 1);
    2.22 +qed "drop_0";
    2.23 +
    2.24 +goalw thy [drop_def] "drop (Suc n) (x#xs) = drop n xs";
    2.25 +by(Simp_tac 1);
    2.26 +qed "drop_Suc";
    2.27 +
    2.28 +goalw thy [drop_def] "drop n [] = []";
    2.29 +by (nat_ind_tac "n" 1);
    2.30 +by (ALLGOALS Asm_simp_tac);
    2.31 +qed "drop_Nil";
    2.32 +
    2.33 +Addsimps [drop_0,drop_Suc,drop_Nil];
    2.34 +
    2.35 +(** take **)
    2.36 +
    2.37 +goalw thy [take_def] "take 0 xs = []";
    2.38 +by(Simp_tac 1);
    2.39 +qed "take_0";
    2.40 +
    2.41 +goalw thy [take_def] "take (Suc n) (x#xs) = x # take n xs";
    2.42 +by(Simp_tac 1);
    2.43 +qed "take_Suc";
    2.44 +
    2.45 +goalw thy [take_def] "take n [] = []";
    2.46 +by (nat_ind_tac "n" 1);
    2.47 +by (ALLGOALS Asm_simp_tac);
    2.48 +qed "take_Nil";
    2.49 +
    2.50 +Addsimps [take_0,take_Suc,take_Nil];
    2.51  
    2.52  (** Additional mapping lemmas **)
    2.53  
     3.1 --- a/src/HOL/List.thy	Sun Nov 12 13:14:13 1995 +0100
     3.2 +++ b/src/HOL/List.thy	Sun Nov 12 16:29:12 1995 +0100
     3.3 @@ -13,19 +13,20 @@
     3.4  
     3.5  consts
     3.6  
     3.7 -  null      :: "'a list => bool"
     3.8 +  "@"	    :: "['a list, 'a list] => 'a list"		(infixr 65)
     3.9 +  drop      :: "[nat, 'a list] => 'a list"
    3.10 +  filter    :: "['a => bool, 'a list] => 'a list"
    3.11 +  flat      :: "'a list list => 'a list"
    3.12 +  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
    3.13    hd        :: "'a list => 'a"
    3.14 -  tl,ttl    :: "'a list => 'a list"
    3.15 -  mem       :: "['a, 'a list] => bool"			(infixl 55)
    3.16 +  length    :: "'a list => nat"
    3.17    list_all  :: "('a => bool) => ('a list => bool)"
    3.18    map       :: "('a=>'b) => ('a list => 'b list)"
    3.19 -  "@"	    :: "['a list, 'a list] => 'a list"		(infixr 65)
    3.20 +  mem       :: "['a, 'a list] => bool"			(infixl 55)
    3.21 +  nth       :: "[nat, 'a list] => 'a"
    3.22 +  take      :: "[nat, 'a list] => 'a list"
    3.23 +  tl,ttl    :: "'a list => 'a list"
    3.24    rev       :: "'a list => 'a list"
    3.25 -  filter    :: "['a => bool, 'a list] => 'a list"
    3.26 -  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
    3.27 -  length    :: "'a list => nat"
    3.28 -  flat      :: "'a list list => 'a list"
    3.29 -  nth       :: "[nat, 'a list] => 'a"
    3.30  
    3.31  syntax
    3.32    (* list Enumeration *)
    3.33 @@ -42,9 +43,6 @@
    3.34    "[x:xs . P]"	== "filter (%x.P) xs"
    3.35    "Alls x:xs.P"	== "list_all (%x.P) xs"
    3.36  
    3.37 -primrec null list
    3.38 -  null_Nil "null([]) = True"
    3.39 -  null_Cons "null(x#xs) = False"
    3.40  primrec hd list
    3.41    hd_Nil  "hd([]) = (@x.False)"
    3.42    hd_Cons "hd(x#xs) = x"
    3.43 @@ -83,5 +81,9 @@
    3.44    flat_Nil  "flat([]) = []"
    3.45    flat_Cons "flat(x#xs) = x @ flat(xs)"
    3.46  defs
    3.47 -  nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))"
    3.48 +  drop_def "drop n == nat_rec n (%xs.xs)   \
    3.49 +\	                (%m r xs. case xs of [] => [] | y#ys => r ys)"
    3.50 +  take_def "take n == nat_rec n (%xs.[])   \
    3.51 +\	                (%m r xs. case xs of [] => [] | y#ys => y # r ys)"
    3.52 +  nth_def  "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))"
    3.53  end
     4.1 --- a/src/HOL/Nat.ML	Sun Nov 12 13:14:13 1995 +0100
     4.2 +++ b/src/HOL/Nat.ML	Sun Nov 12 16:29:12 1995 +0100
     4.3 @@ -412,6 +412,11 @@
     4.4  by(fast_tac HOL_cs 1);
     4.5  qed "Suc_leD";
     4.6  
     4.7 +goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
     4.8 +by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
     4.9 +qed "le_SucI";
    4.10 +Addsimps[le_SucI];
    4.11 +
    4.12  goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
    4.13  by (fast_tac (HOL_cs addEs [less_asym]) 1);
    4.14  qed "less_imp_le";