src/HOL/List.ML
changeset 7032 d6efb3b8e669
parent 7028 6ea3b385e731
child 7224 e41e64476f9b
equal deleted inserted replaced
7031:972b5f62f476 7032:d6efb3b8e669
   409 
   409 
   410 (** set **)
   410 (** set **)
   411 
   411 
   412 section "set";
   412 section "set";
   413 
   413 
   414 qed_goal "finite_set" thy "finite (set xs)" 
   414 Goal "finite (set xs)";
   415 	(K [induct_tac "xs" 1, Auto_tac]);
   415 by (induct_tac "xs" 1);
   416 Addsimps[finite_set];
   416 by Auto_tac;
   417 AddSIs[finite_set];
   417 qed "finite_set";
       
   418 AddIffs [finite_set];
   418 
   419 
   419 Goal "set (xs@ys) = (set xs Un set ys)";
   420 Goal "set (xs@ys) = (set xs Un set ys)";
   420 by (induct_tac "xs" 1);
   421 by (induct_tac "xs" 1);
   421 by Auto_tac;
   422 by Auto_tac;
   422 qed "set_append";
   423 qed "set_append";
  1225 by (Asm_full_simp_tac 1);
  1226 by (Asm_full_simp_tac 1);
  1226 by (Asm_full_simp_tac 1);
  1227 by (Asm_full_simp_tac 1);
  1227 by (Blast_tac 1);
  1228 by (Blast_tac 1);
  1228 qed "Cons_in_lex";
  1229 qed "Cons_in_lex";
  1229 AddIffs [Cons_in_lex];
  1230 AddIffs [Cons_in_lex];
       
  1231 
       
  1232 
       
  1233 (*** Versions of some theorems above using binary numerals ***)
       
  1234 
       
  1235 AddIffs (map (rename_numerals thy) 
       
  1236 	  [length_0_conv, zero_length_conv, length_greater_0_conv,
       
  1237 	   sum_eq_0_conv]);
       
  1238 
       
  1239 Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
       
  1240 by (exhaust_tac "n" 1);
       
  1241 by (ALLGOALS 
       
  1242     (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
       
  1243 qed "take_Cons'";
       
  1244 
       
  1245 Goal "drop n (x#xs) = (if n = #0 then x#xs else drop (n-#1) xs)";
       
  1246 by (exhaust_tac "n" 1);
       
  1247 by (ALLGOALS
       
  1248     (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
       
  1249 qed "drop_Cons'";
       
  1250 
       
  1251 Goal "(x#xs)!n = (if n = #0 then x else xs!(n-#1))";
       
  1252 by (exhaust_tac "n" 1);
       
  1253 by (ALLGOALS
       
  1254     (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
       
  1255 qed "nth_Cons'";
       
  1256 
       
  1257 Addsimps (map (inst "n" "number_of ?v") [take_Cons', drop_Cons', nth_Cons']);
       
  1258