src/HOL/List.ML
changeset 11868 56db9f3a6b3e
parent 11770 b6bb7a853dd2
child 12486 0ed8bdd883e0
     1.1 --- a/src/HOL/List.ML	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -232,23 +232,23 @@
     1.4  local
     1.5  
     1.6  val list_eq_pattern =
     1.7 -  Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT);
     1.8 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
     1.9  
    1.10  fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
    1.11        (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
    1.12    | last (Const("List.op @",_) $ _ $ ys) = last ys
    1.13 -  | last t = t;
    1.14 +  | last t = t
    1.15  
    1.16  fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
    1.17 -  | list1 _ = false;
    1.18 +  | list1 _ = false
    1.19  
    1.20  fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
    1.21        (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
    1.22    | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    1.23 -  | butlast xs = Const("List.list.Nil",fastype_of xs);
    1.24 +  | butlast xs = Const("List.list.Nil",fastype_of xs)
    1.25  
    1.26  val rearr_tac =
    1.27 -  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
    1.28 +  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons])
    1.29  
    1.30  fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    1.31    let
    1.32 @@ -272,9 +272,9 @@
    1.33       if lastl aconv lastr
    1.34       then rearr append_same_eq
    1.35       else None
    1.36 -  end;
    1.37 +  end
    1.38  in
    1.39 -val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
    1.40 +val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq
    1.41  end;
    1.42  
    1.43  Addsimprocs [list_eq_simproc];
    1.44 @@ -1501,24 +1501,19 @@
    1.45  Addsimps [sublist_upt_eq_take];
    1.46  
    1.47  
    1.48 -(*** Versions of some theorems above using binary numerals ***)
    1.49 -
    1.50 -AddIffs (map rename_numerals
    1.51 -	  [length_0_conv, length_greater_0_conv, sum_eq_0_conv]);
    1.52 -
    1.53 -Goal "take n (x#xs) = (if n = Numeral0 then [] else x # take (n - Numeral1) xs)";
    1.54 +Goal "take n (x#xs) = (if n=0 then [] else x # take (n - 1) xs)";
    1.55  by (case_tac "n" 1);
    1.56  by (ALLGOALS 
    1.57      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
    1.58  qed "take_Cons'";
    1.59  
    1.60 -Goal "drop n (x#xs) = (if n = Numeral0 then x#xs else drop (n - Numeral1) xs)";
    1.61 +Goal "drop n (x#xs) = (if n=0 then x#xs else drop (n - 1) xs)";
    1.62  by (case_tac "n" 1);
    1.63  by (ALLGOALS
    1.64      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
    1.65  qed "drop_Cons'";
    1.66  
    1.67 -Goal "(x#xs)!n = (if n = Numeral0 then x else xs!(n - Numeral1))";
    1.68 +Goal "(x#xs)!n = (if n=0 then x else xs!(n - 1))";
    1.69  by (case_tac "n" 1);
    1.70  by (ALLGOALS
    1.71      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));