Added a number of new thms and the new function remove1
authornipkow
Wed Aug 04 19:10:45 2004 +0200 (2004-08-04)
changeset 1511078b5636eabc7
parent 15109 bba563cdd997
child 15111 c108189645f8
Added a number of new thms and the new function remove1
src/HOL/List.thy
src/HOL/Map.thy
     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  
     2.1 --- a/src/HOL/Map.thy	Wed Aug 04 19:09:58 2004 +0200
     2.2 +++ b/src/HOL/Map.thy	Wed Aug 04 19:10:45 2004 +0200
     2.3 @@ -173,6 +173,18 @@
     2.4  
     2.5  subsection {* @{term map_of} *}
     2.6  
     2.7 +lemma map_of_zip_is_None[simp]:
     2.8 +  "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
     2.9 +by (induct rule:list_induct2, simp_all)
    2.10 +
    2.11 +lemma finite_range_map_of: "finite (range (map_of xys))"
    2.12 +apply (induct_tac xys)
    2.13 +apply  (simp_all (no_asm) add: image_constant)
    2.14 +apply (rule finite_subset)
    2.15 +prefer 2 apply assumption
    2.16 +apply auto
    2.17 +done
    2.18 +
    2.19  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    2.20  by (induct_tac "xs", auto)
    2.21  
    2.22 @@ -193,14 +205,6 @@
    2.23  apply (induct_tac "xs", auto)
    2.24  done
    2.25  
    2.26 -lemma finite_range_map_of: "finite (range (map_of l))"
    2.27 -apply (induct_tac "l")
    2.28 -apply  (simp_all (no_asm) add: image_constant)
    2.29 -apply (rule finite_subset)
    2.30 -prefer 2 apply assumption
    2.31 -apply auto
    2.32 -done
    2.33 -
    2.34  lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
    2.35  by (induct_tac "xs", auto)
    2.36  
    2.37 @@ -433,6 +437,10 @@
    2.38  apply(auto simp del:fun_upd_apply)
    2.39  done
    2.40  
    2.41 +lemma dom_map_of_zip[simp]: "[| length xs = length ys; distinct xs |] ==>
    2.42 +  dom(map_of(zip xs ys)) = set xs"
    2.43 +by(induct rule: list_induct2, simp_all)
    2.44 +
    2.45  lemma finite_dom_map_of: "finite (dom (map_of l))"
    2.46  apply (unfold dom_def)
    2.47  apply (induct_tac "l")