src/HOL/List.ML
changeset 5183 89f162de39cf
parent 5162 53e505c6019c
child 5200 a23c23af335f
     1.1 --- a/src/HOL/List.ML	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -208,17 +208,17 @@
     1.4  
     1.5  Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
     1.6  by (asm_simp_tac (simpset() addsimps [hd_append]
     1.7 -                           addsplits [split_list_case]) 1);
     1.8 +                           addsplits [list.split]) 1);
     1.9  qed "hd_append2";
    1.10  Addsimps [hd_append2];
    1.11  
    1.12  Goal "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
    1.13 -by (simp_tac (simpset() addsplits [split_list_case]) 1);
    1.14 +by (simp_tac (simpset() addsplits [list.split]) 1);
    1.15  qed "tl_append";
    1.16  
    1.17  Goal "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
    1.18  by (asm_simp_tac (simpset() addsimps [tl_append]
    1.19 -                           addsplits [split_list_case]) 1);
    1.20 +                           addsplits [list.split]) 1);
    1.21  qed "tl_append2";
    1.22  Addsimps [tl_append2];
    1.23  
    1.24 @@ -482,7 +482,7 @@
    1.25  
    1.26  Goal
    1.27    "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
    1.28 -by (nat_ind_tac "n" 1);
    1.29 +by (induct_tac "n" 1);
    1.30   by (Asm_simp_tac 1);
    1.31   by (rtac allI 1);
    1.32   by (exhaust_tac "xs" 1);
    1.33 @@ -495,7 +495,7 @@
    1.34  by (Asm_full_simp_tac 1);
    1.35  (* case x#xl *)
    1.36  by (rtac allI 1);
    1.37 -by (nat_ind_tac "n" 1);
    1.38 +by (induct_tac "n" 1);
    1.39  by (Auto_tac);
    1.40  qed_spec_mp "nth_map";
    1.41  Addsimps [nth_map];
    1.42 @@ -506,7 +506,7 @@
    1.43  by (Simp_tac 1);
    1.44  (* case x#xl *)
    1.45  by (rtac allI 1);
    1.46 -by (nat_ind_tac "n" 1);
    1.47 +by (induct_tac "n" 1);
    1.48  by (Auto_tac);
    1.49  qed_spec_mp "list_all_nth";
    1.50  
    1.51 @@ -516,7 +516,7 @@
    1.52  by (Simp_tac 1);
    1.53  (* case x#xl *)
    1.54  by (rtac allI 1);
    1.55 -by (nat_ind_tac "n" 1);
    1.56 +by (induct_tac "n" 1);
    1.57  (* case 0 *)
    1.58  by (Asm_full_simp_tac 1);
    1.59  (* case Suc x *)
    1.60 @@ -531,7 +531,7 @@
    1.61  Goal "!i. length(xs[i:=x]) = length xs";
    1.62  by (induct_tac "xs" 1);
    1.63  by (Simp_tac 1);
    1.64 -by (asm_full_simp_tac (simpset() addsplits [split_nat_case]) 1);
    1.65 +by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
    1.66  qed_spec_mp "length_list_update";
    1.67  Addsimps [length_list_update];
    1.68  
    1.69 @@ -603,7 +603,7 @@
    1.70  Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
    1.71  
    1.72  Goal "!xs. length(take n xs) = min (length xs) n";
    1.73 -by (nat_ind_tac "n" 1);
    1.74 +by (induct_tac "n" 1);
    1.75   by (Auto_tac);
    1.76  by (exhaust_tac "xs" 1);
    1.77   by (Auto_tac);
    1.78 @@ -611,7 +611,7 @@
    1.79  Addsimps [length_take];
    1.80  
    1.81  Goal "!xs. length(drop n xs) = (length xs - n)";
    1.82 -by (nat_ind_tac "n" 1);
    1.83 +by (induct_tac "n" 1);
    1.84   by (Auto_tac);
    1.85  by (exhaust_tac "xs" 1);
    1.86   by (Auto_tac);
    1.87 @@ -619,14 +619,14 @@
    1.88  Addsimps [length_drop];
    1.89  
    1.90  Goal "!xs. length xs <= n --> take n xs = xs";
    1.91 -by (nat_ind_tac "n" 1);
    1.92 +by (induct_tac "n" 1);
    1.93   by (Auto_tac);
    1.94  by (exhaust_tac "xs" 1);
    1.95   by (Auto_tac);
    1.96  qed_spec_mp "take_all";
    1.97  
    1.98  Goal "!xs. length xs <= n --> drop n xs = []";
    1.99 -by (nat_ind_tac "n" 1);
   1.100 +by (induct_tac "n" 1);
   1.101   by (Auto_tac);
   1.102  by (exhaust_tac "xs" 1);
   1.103   by (Auto_tac);
   1.104 @@ -634,7 +634,7 @@
   1.105  
   1.106  Goal 
   1.107    "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   1.108 -by (nat_ind_tac "n" 1);
   1.109 +by (induct_tac "n" 1);
   1.110   by (Auto_tac);
   1.111  by (exhaust_tac "xs" 1);
   1.112   by (Auto_tac);
   1.113 @@ -642,7 +642,7 @@
   1.114  Addsimps [take_append];
   1.115  
   1.116  Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   1.117 -by (nat_ind_tac "n" 1);
   1.118 +by (induct_tac "n" 1);
   1.119   by (Auto_tac);
   1.120  by (exhaust_tac "xs" 1);
   1.121   by (Auto_tac);
   1.122 @@ -650,37 +650,37 @@
   1.123  Addsimps [drop_append];
   1.124  
   1.125  Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
   1.126 -by (nat_ind_tac "m" 1);
   1.127 +by (induct_tac "m" 1);
   1.128   by (Auto_tac);
   1.129  by (exhaust_tac "xs" 1);
   1.130   by (Auto_tac);
   1.131 -by (exhaust_tac "n" 1);
   1.132 +by (exhaust_tac "na" 1);
   1.133   by (Auto_tac);
   1.134  qed_spec_mp "take_take";
   1.135  
   1.136  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   1.137 -by (nat_ind_tac "m" 1);
   1.138 +by (induct_tac "m" 1);
   1.139   by (Auto_tac);
   1.140  by (exhaust_tac "xs" 1);
   1.141   by (Auto_tac);
   1.142  qed_spec_mp "drop_drop";
   1.143  
   1.144  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   1.145 -by (nat_ind_tac "m" 1);
   1.146 +by (induct_tac "m" 1);
   1.147   by (Auto_tac);
   1.148  by (exhaust_tac "xs" 1);
   1.149   by (Auto_tac);
   1.150  qed_spec_mp "take_drop";
   1.151  
   1.152  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
   1.153 -by (nat_ind_tac "n" 1);
   1.154 +by (induct_tac "n" 1);
   1.155   by (Auto_tac);
   1.156  by (exhaust_tac "xs" 1);
   1.157   by (Auto_tac);
   1.158  qed_spec_mp "take_map"; 
   1.159  
   1.160  Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
   1.161 -by (nat_ind_tac "n" 1);
   1.162 +by (induct_tac "n" 1);
   1.163   by (Auto_tac);
   1.164  by (exhaust_tac "xs" 1);
   1.165   by (Auto_tac);
   1.166 @@ -697,7 +697,7 @@
   1.167  Addsimps [nth_take];
   1.168  
   1.169  Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
   1.170 -by (nat_ind_tac "n" 1);
   1.171 +by (induct_tac "n" 1);
   1.172   by (Auto_tac);
   1.173  by (exhaust_tac "xs" 1);
   1.174   by (Auto_tac);
   1.175 @@ -792,18 +792,18 @@
   1.176  val list_eq_pattern =
   1.177    read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
   1.178  
   1.179 -fun last (cons as Const("List.op #",_) $ _ $ xs) =
   1.180 -      (case xs of Const("List.[]",_) => cons | _ => last xs)
   1.181 -  | last (Const("List.op @",_) $ _ $ ys) = last ys
   1.182 +fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
   1.183 +      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
   1.184 +  | last (Const("List.list.op @",_) $ _ $ ys) = last ys
   1.185    | last t = t;
   1.186  
   1.187 -fun list1 (Const("List.op #",_) $ _ $ Const("List.[]",_)) = true
   1.188 +fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
   1.189    | list1 _ = false;
   1.190  
   1.191 -fun butlast ((cons as Const("List.op #",_) $ x) $ xs) =
   1.192 -      (case xs of Const("List.[]",_) => xs | _ => cons $ butlast xs)
   1.193 -  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
   1.194 -  | butlast xs = Const("List.[]",fastype_of xs);
   1.195 +fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
   1.196 +      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
   1.197 +  | butlast ((app as Const("List.list.op @",_) $ xs) $ ys) = app $ butlast ys
   1.198 +  | butlast xs = Const("List.list.[]",fastype_of xs);
   1.199  
   1.200  val rearr_tac =
   1.201    simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
   1.202 @@ -815,7 +815,7 @@
   1.203        let val lhs1 = butlast lhs and rhs1 = butlast rhs
   1.204            val Type(_,listT::_) = eqT
   1.205            val appT = [listT,listT] ---> listT
   1.206 -          val app = Const("List.op @",appT)
   1.207 +          val app = Const("List.list.op @",appT)
   1.208            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
   1.209            val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
   1.210            val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])