src/HOL/List.thy

   dropWhile :: "('a => bool) => 'a list => 'a list"
   rev :: "'a list => 'a list"
   zip :: "'a list => 'b list => ('a * 'b) list"
   upt :: "nat => nat => nat list" ("(1[_../_'(])")
   remdups :: "'a list => 'a list"
+  remove1 :: "'a => 'a list => 'a list"
   null:: "'a list => bool"
   "distinct":: "'a list => bool"
   replicate :: "nat => 'a => 'a list"
 
 nonterminals lupdbinds lupdbind

 "distinct [] = True"
 "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
 primrec
 "remdups [] = []"
 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
+primrec
+"remove1 x [] = []"
+"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
 primrec
 replicate_0: "replicate 0 x = []"
 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 defs
  list_all2_def:

 
 lemma ex_map_conv:
   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
 by(induct ys, auto)
 
+lemma map_eq_imp_length_eq:
+  "!!xs. map f xs = map f ys ==> length xs = length ys"
+apply (induct ys)
+ apply simp
+apply(simp (no_asm_use))
+apply clarify
+apply(simp (no_asm_use))
+apply fast
+done
+
+lemma map_inj_on:
+ "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
+  ==> xs = ys"
+apply(frule map_eq_imp_length_eq)
+apply(rotate_tac -1)
+apply(induct rule:list_induct2)
+ apply simp
+apply(simp)
+apply (blast intro:sym)
+done
+
+lemma inj_on_map_eq_map:
+ "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
+by(blast dest:map_inj_on)
+
 lemma map_injective:
  "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
 by (induct ys) (auto dest!:injD)
 
 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"

 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
 by (induct xs, auto)
 
 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
 by (induct xs) auto
+
+lemma map_fst_zip[simp]:
+  "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
+by (induct rule:list_induct2, simp_all)
+
+lemma map_snd_zip[simp]:
+  "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
+by (induct rule:list_induct2, simp_all)
+
 
 subsection {* @{text rev} *}
 
 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
 by (induct xs) auto

 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
 by simp
 
 declare take_Cons [simp del] and drop_Cons [simp del]
 
+lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
+by(clarsimp simp add:neq_Nil_conv)
+
 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
 by(cases xs, simp_all)
 
 lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)"
 by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)

 done
 
 lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs"
 apply (induct n, auto)
 apply (case_tac xs, auto)
+done
+
+lemma take_eq_Nil[simp]: "!!n. (take n xs = []) = (n = 0 \<or> xs = [])"
+apply(induct xs)
+ apply simp
+apply(simp add:take_Cons split:nat.split)
+done
+
+lemma drop_eq_Nil[simp]: "!!n. (drop n xs = []) = (length xs <= n)"
+apply(induct xs)
+apply simp
+apply(simp add:drop_Cons split:nat.split)
 done
 
 lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)"
 apply (induct n, auto)
 apply (case_tac xs, auto)

    else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
 apply(induct xs\<^isub>1)
  apply simp
 apply(case_tac ys\<^isub>1)
 apply simp_all
+done
+
+lemma take_hd_drop:
+  "!!n. n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
+apply(induct xs)
+apply simp
+apply(simp add:drop_Cons split:nat.split)
 done
 
 
 subsection {* @{text takeWhile} and @{text dropWhile} *}
 

  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
 apply (erule_tac x = "Suc i" in allE)
 apply (erule_tac x = "Suc j" in allE, simp)
 done
 
-lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
+lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
   by (induct xs) auto
 
-lemma card_distinct: "card (set xs) = size xs \<Longrightarrow> distinct xs"
+lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
 proof (induct xs)
   case Nil thus ?case by simp
 next
   case (Cons x xs)
   show ?case

     moreover have "card (set xs) \<le> length xs" by (rule card_length)
     ultimately have False by simp
     thus ?thesis ..
   qed
 qed
+
+lemma inj_on_setI: "distinct(map f xs) ==> inj_on f (set xs)"
+apply(induct xs)
+ apply simp
+apply fastsimp
+done
+
+lemma inj_on_set_conv:
+ "distinct xs \<Longrightarrow> inj_on f (set xs) = distinct(map f xs)"
+apply(induct xs)
+ apply simp
+apply fastsimp
+done
+
+
+subsection {* @{text remove1} *}
+
+lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
+apply(induct xs)
+ apply simp
+apply simp
+apply blast
+done
+
+lemma [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
+apply(induct xs)
+ apply simp
+apply simp
+apply blast
+done
+
+lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
+apply(insert set_remove1_subset)
+apply fast
+done
+
+lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
+by (induct xs) simp_all
 
 
 subsection {* @{text replicate} *}
 
 lemma length_replicate [simp]: "length (replicate n x) = n"