src/HOL/List.thy
changeset 73396 8a1c6c7909c9
parent 73379 b867b436f372
child 73411 1f1366966296
equal deleted inserted replaced
73395:6a96e9406e53 73396:8a1c6c7909c9
  2384 qed auto
  2384 qed auto
  2385 
  2385 
  2386 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
  2386 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
  2387   by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
  2387   by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
  2388 
  2388 
  2389 lemma list_all_take_drop_conv:
       
  2390   "list_all P (take n xs) \<and> list_all P (drop n xs) \<longleftrightarrow> list_all P xs"
       
  2391 proof (induction xs arbitrary: n)
       
  2392   case Nil
       
  2393   then show ?case by simp
       
  2394 next
       
  2395   case (Cons a xs)
       
  2396   then show ?case
       
  2397     by (cases n) simp_all
       
  2398 qed
       
  2399 
       
  2400 lemmas list_all_takeI = list_all_take_drop_conv[THEN iffD2, THEN conjunct1]
       
  2401 lemmas list_all_dropI = list_all_take_drop_conv[THEN iffD2, THEN conjunct2]
       
  2402 lemmas list_all_take_dropD = conjI[THEN list_all_take_drop_conv[THEN iffD1]]
       
  2403 
       
  2404 
  2389 
  2405 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
  2390 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
  2406 
  2391 
  2407 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
  2392 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
  2408   by (induct xs) auto
  2393   by (induct xs) auto
  2586   by (induct xs) auto
  2571   by (induct xs) auto
  2587 
  2572 
  2588 lemma dropWhile_idem [simp]:
  2573 lemma dropWhile_idem [simp]:
  2589   "dropWhile P (dropWhile P xs) = dropWhile P xs"
  2574   "dropWhile P (dropWhile P xs) = dropWhile P xs"
  2590   by (induct xs) auto
  2575   by (induct xs) auto
  2591 
       
  2592 lemma list_all_takeWhile_dropWhile_conv:
       
  2593   "list_all P (takeWhile Q xs) \<and> list_all P (dropWhile Q xs) \<longleftrightarrow> list_all P xs"
       
  2594   by (induction xs; simp)
       
  2595 
       
  2596 lemmas list_all_takeWhileI = list_all_takeWhile_dropWhile_conv[THEN iffD2, THEN conjunct1]
       
  2597 lemmas list_all_dropWhileI = list_all_takeWhile_dropWhile_conv[THEN iffD2, THEN conjunct2]
       
  2598 lemmas list_all_takeWhile_dropWhileD = conjI[THEN list_all_takeWhile_dropWhile_conv[THEN iffD1]]
       
  2599 
  2576 
  2600 
  2577 
  2601 subsubsection \<open>\<^const>\<open>zip\<close>\<close>
  2578 subsubsection \<open>\<^const>\<open>zip\<close>\<close>
  2602 
  2579 
  2603 lemma zip_Nil [simp]: "zip [] ys = []"
  2580 lemma zip_Nil [simp]: "zip [] ys = []"