src/HOL/Map.thy
changeset 15110 78b5636eabc7
parent 14739 86c6f272ef79
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Map.thy	Wed Aug 04 19:09:58 2004 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Aug 04 19:10:45 2004 +0200
     1.3 @@ -173,6 +173,18 @@
     1.4  
     1.5  subsection {* @{term map_of} *}
     1.6  
     1.7 +lemma map_of_zip_is_None[simp]:
     1.8 +  "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
     1.9 +by (induct rule:list_induct2, simp_all)
    1.10 +
    1.11 +lemma finite_range_map_of: "finite (range (map_of xys))"
    1.12 +apply (induct_tac xys)
    1.13 +apply  (simp_all (no_asm) add: image_constant)
    1.14 +apply (rule finite_subset)
    1.15 +prefer 2 apply assumption
    1.16 +apply auto
    1.17 +done
    1.18 +
    1.19  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    1.20  by (induct_tac "xs", auto)
    1.21  
    1.22 @@ -193,14 +205,6 @@
    1.23  apply (induct_tac "xs", auto)
    1.24  done
    1.25  
    1.26 -lemma finite_range_map_of: "finite (range (map_of l))"
    1.27 -apply (induct_tac "l")
    1.28 -apply  (simp_all (no_asm) add: image_constant)
    1.29 -apply (rule finite_subset)
    1.30 -prefer 2 apply assumption
    1.31 -apply auto
    1.32 -done
    1.33 -
    1.34  lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
    1.35  by (induct_tac "xs", auto)
    1.36  
    1.37 @@ -433,6 +437,10 @@
    1.38  apply(auto simp del:fun_upd_apply)
    1.39  done
    1.40  
    1.41 +lemma dom_map_of_zip[simp]: "[| length xs = length ys; distinct xs |] ==>
    1.42 +  dom(map_of(zip xs ys)) = set xs"
    1.43 +by(induct rule: list_induct2, simp_all)
    1.44 +
    1.45  lemma finite_dom_map_of: "finite (dom (map_of l))"
    1.46  apply (unfold dom_def)
    1.47  apply (induct_tac "l")