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.24  
    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.56  
    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.67  
    1.68  lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
    1.69 @@ -829,6 +867,9 @@
    1.70  
    1.71  declare take_Cons [simp del] and drop_Cons [simp del]
    1.72  
    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.78  
    1.79 @@ -899,6 +940,18 @@
    1.80  apply (case_tac xs, auto)
    1.81  done
    1.82  
    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.101  
   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.108 +
   1.109  
   1.110  subsection {* @{text takeWhile} and @{text dropWhile} *}
   1.111  
   1.112 @@ -1367,10 +1427,10 @@
   1.113  apply (erule_tac x = "Suc j" in allE, simp)
   1.114  done
   1.115  
   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.119  
   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.128  
   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.134 +
   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.141 +
   1.142 +
   1.143 +subsection {* @{text remove1} *}
   1.144 +
   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.151 +
   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.158 +
   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.163 +
   1.164 +lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
   1.165 +by (induct xs) simp_all
   1.166 +
   1.167  
   1.168  subsection {* @{text replicate} *}
   1.169