src/HOL/Map.thy
changeset 22230 bdec4a82f385
parent 21404 eb85850d3eb7
child 22744 5cbe966d67a2
     1.1 --- a/src/HOL/Map.thy	Thu Feb 01 20:59:50 2007 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Feb 02 15:47:58 2007 +0100
     1.3 @@ -86,49 +86,12 @@
     1.4  defs
     1.5    map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
     1.6  
     1.7 -(* special purpose constants that should be defined somewhere else and
     1.8 -whose syntax is a bit odd as well:
     1.9 -
    1.10 - "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    1.11 -                                          ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    1.12 -  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    1.13 -
    1.14 -map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
    1.15 -            ('a ~=> 'b)"                         ("_/'(_{|->}_/')" [900,0,0]900)
    1.16 -map_subst::"('a ~=> 'b) => 'b => 'b =>
    1.17 -            ('a ~=> 'b)"                         ("_/'(_~>_/')"    [900,0,0]900)
    1.18 -
    1.19 -map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    1.20 -map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    1.21 -
    1.22 -  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    1.23 -                                                 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    1.24 -  map_subst :: "('a ~=> 'b) => 'b => 'b =>
    1.25 -                ('a ~=> 'b)"                     ("_/'(_\<leadsto>_/')"    [900,0,0]900)
    1.26 -
    1.27 -
    1.28 -subsection {* @{term [source] map_upd_s} *}
    1.29 -
    1.30 -lemma map_upd_s_apply [simp]:
    1.31 -  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
    1.32 -by (simp add: map_upd_s_def)
    1.33 -
    1.34 -lemma map_subst_apply [simp]:
    1.35 -  "(m(a~>b)) x = (if m x = Some a then Some b else m x)"
    1.36 -by (simp add: map_subst_def)
    1.37 -
    1.38 -*)
    1.39 -
    1.40  
    1.41  subsection {* @{term [source] empty} *}
    1.42  
    1.43  lemma empty_upd_none [simp]: "empty(x := None) = empty"
    1.44    by (rule ext) simp
    1.45  
    1.46 -(* FIXME: what is this sum_case nonsense?? *)
    1.47 -lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
    1.48 -  by (rule ext) (simp split: sum.split)
    1.49 -
    1.50  
    1.51  subsection {* @{term [source] map_upd} *}
    1.52  
    1.53 @@ -166,22 +129,6 @@
    1.54    done
    1.55  
    1.56  
    1.57 -(* FIXME: what is this sum_case nonsense?? *)
    1.58 -subsection {* @{term [source] sum_case} and @{term [source] empty}/@{term [source] map_upd} *}
    1.59 -
    1.60 -lemma sum_case_map_upd_empty [simp]:
    1.61 -    "sum_case (m(k|->y)) empty = (sum_case m empty)(Inl k|->y)"
    1.62 -  by (rule ext) (simp split: sum.split)
    1.63 -
    1.64 -lemma sum_case_empty_map_upd [simp]:
    1.65 -    "sum_case empty (m(k|->y)) = (sum_case empty m)(Inr k|->y)"
    1.66 -  by (rule ext) (simp split: sum.split)
    1.67 -
    1.68 -lemma sum_case_map_upd_map_upd [simp]:
    1.69 -    "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
    1.70 -  by (rule ext) (simp split: sum.split)
    1.71 -
    1.72 -
    1.73  subsection {* @{term [source] map_of} *}
    1.74  
    1.75  lemma map_of_eq_None_iff:
    1.76 @@ -506,6 +453,11 @@
    1.77  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
    1.78    by (rule ext) (force simp: map_add_def dom_def split: option.split)
    1.79  
    1.80 +(* Due to John Matthews - could be rephrased with dom *)
    1.81 +lemma finite_map_freshness:
    1.82 +  "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
    1.83 +   \<exists>x. f x = None"
    1.84 +by(bestsimp dest:ex_new_if_finite)
    1.85  
    1.86  subsection {* @{term [source] ran} *}
    1.87