src/HOL/List.thy
 changeset 15110 78b5636eabc7 parent 15072 4861bf6af0b4 child 15113 fafcd72b9d4b
1.1 --- a/src/HOL/List.thy	Wed Aug 04 19:09:58 2004 +0200
1.2 +++ b/src/HOL/List.thy	Wed Aug 04 19:10:45 2004 +0200
1.3 @@ -36,6 +36,7 @@
1.4    zip :: "'a list => 'b list => ('a * 'b) list"
1.5    upt :: "nat => nat => nat list" ("(1[_../_'(])")
1.6    remdups :: "'a list => 'a list"
1.7 +  remove1 :: "'a => 'a list => 'a list"
1.8    null:: "'a list => bool"
1.9    "distinct":: "'a list => bool"
1.10    replicate :: "nat => 'a => 'a list"
1.11 @@ -172,6 +173,9 @@
1.12  "remdups [] = []"
1.13  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
1.14  primrec
1.15 +"remove1 x [] = []"
1.16 +"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
1.17 +primrec
1.18  replicate_0: "replicate 0 x = []"
1.19  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
1.20  defs
1.21 @@ -487,6 +491,31 @@
1.22    "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
1.23  by(induct ys, auto)
1.25 +lemma map_eq_imp_length_eq:
1.26 +  "!!xs. map f xs = map f ys ==> length xs = length ys"
1.27 +apply (induct ys)
1.28 + apply simp
1.29 +apply(simp (no_asm_use))
1.30 +apply clarify
1.31 +apply(simp (no_asm_use))
1.32 +apply fast
1.33 +done
1.34 +
1.35 +lemma map_inj_on:
1.36 + "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
1.37 +  ==> xs = ys"
1.38 +apply(frule map_eq_imp_length_eq)
1.39 +apply(rotate_tac -1)
1.40 +apply(induct rule:list_induct2)
1.41 + apply simp
1.42 +apply(simp)
1.43 +apply (blast intro:sym)
1.44 +done
1.45 +
1.46 +lemma inj_on_map_eq_map:
1.47 + "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
1.48 +by(blast dest:map_inj_on)
1.49 +
1.50  lemma map_injective:
1.51   "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
1.52  by (induct ys) (auto dest!:injD)
1.53 @@ -513,6 +542,15 @@
1.54  lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
1.55  by (induct xs) auto
1.57 +lemma map_fst_zip[simp]:
1.58 +  "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
1.59 +by (induct rule:list_induct2, simp_all)
1.60 +
1.61 +lemma map_snd_zip[simp]:
1.62 +  "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
1.63 +by (induct rule:list_induct2, simp_all)
1.64 +
1.65 +
1.66  subsection {* @{text rev} *}
1.68  lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
1.69 @@ -829,6 +867,9 @@
1.71  declare take_Cons [simp del] and drop_Cons [simp del]
1.73 +lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
1.74 +by(clarsimp simp add:neq_Nil_conv)
1.75 +
1.76  lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
1.77  by(cases xs, simp_all)
1.79 @@ -899,6 +940,18 @@
1.80  apply (case_tac xs, auto)
1.81  done
1.83 +lemma take_eq_Nil[simp]: "!!n. (take n xs = []) = (n = 0 \<or> xs = [])"
1.84 +apply(induct xs)
1.85 + apply simp
1.86 +apply(simp add:take_Cons split:nat.split)
1.87 +done
1.88 +
1.89 +lemma drop_eq_Nil[simp]: "!!n. (drop n xs = []) = (length xs <= n)"
1.90 +apply(induct xs)
1.91 +apply simp
1.92 +apply(simp add:drop_Cons split:nat.split)
1.93 +done
1.94 +
1.95  lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)"
1.96  apply (induct n, auto)
1.97  apply (case_tac xs, auto)
1.98 @@ -966,6 +1019,13 @@
1.99  apply simp_all
1.100  done
1.102 +lemma take_hd_drop:
1.103 +  "!!n. n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
1.104 +apply(induct xs)
1.105 +apply simp
1.106 +apply(simp add:drop_Cons split:nat.split)
1.107 +done
1.110  subsection {* @{text takeWhile} and @{text dropWhile} *}
1.112 @@ -1367,10 +1427,10 @@
1.113  apply (erule_tac x = "Suc j" in allE, simp)
1.114  done
1.116 -lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
1.117 +lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
1.118    by (induct xs) auto
1.120 -lemma card_distinct: "card (set xs) = size xs \<Longrightarrow> distinct xs"
1.121 +lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
1.122  proof (induct xs)
1.123    case Nil thus ?case by simp
1.124  next
1.125 @@ -1388,6 +1448,44 @@
1.126    qed
1.127  qed
1.129 +lemma inj_on_setI: "distinct(map f xs) ==> inj_on f (set xs)"
1.130 +apply(induct xs)
1.131 + apply simp
1.132 +apply fastsimp
1.133 +done
1.135 +lemma inj_on_set_conv:
1.136 + "distinct xs \<Longrightarrow> inj_on f (set xs) = distinct(map f xs)"
1.137 +apply(induct xs)
1.138 + apply simp
1.139 +apply fastsimp
1.140 +done
1.143 +subsection {* @{text remove1} *}
1.145 +lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
1.146 +apply(induct xs)
1.147 + apply simp
1.148 +apply simp
1.149 +apply blast
1.150 +done
1.152 +lemma [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
1.153 +apply(induct xs)
1.154 + apply simp
1.155 +apply simp
1.156 +apply blast
1.157 +done
1.159 +lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
1.160 +apply(insert set_remove1_subset)
1.161 +apply fast
1.162 +done
1.164 +lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
1.165 +by (induct xs) simp_all
1.168  subsection {* @{text replicate} *}