summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.thy

changeset 15110 | 78b5636eabc7 |

parent 15072 | 4861bf6af0b4 |

child 15113 | fafcd72b9d4b |

--- a/src/HOL/List.thy Wed Aug 04 19:09:58 2004 +0200 +++ b/src/HOL/List.thy Wed Aug 04 19:10:45 2004 +0200 @@ -36,6 +36,7 @@ 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" @@ -172,6 +173,9 @@ "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 @@ -487,6 +491,31 @@ "(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) @@ -513,6 +542,15 @@ 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" @@ -829,6 +867,9 @@ 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) @@ -899,6 +940,18 @@ 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) @@ -966,6 +1019,13 @@ 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} *} @@ -1367,10 +1427,10 @@ 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 @@ -1388,6 +1448,44 @@ 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} *}