src/HOL/Map.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39379 ab1b070aa412
     1.1 --- a/src/HOL/Map.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  
     1.5  lemma map_of_zip_map:
     1.6    "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
     1.7 -  by (induct xs) (simp_all add: ext_iff)
     1.8 +  by (induct xs) (simp_all add: fun_eq_iff)
     1.9  
    1.10  lemma finite_range_map_of: "finite (range (map_of xys))"
    1.11  apply (induct xys)
    1.12 @@ -245,7 +245,7 @@
    1.13  
    1.14  lemma map_of_map:
    1.15    "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
    1.16 -  by (induct xs) (auto simp add: ext_iff)
    1.17 +  by (induct xs) (auto simp add: fun_eq_iff)
    1.18  
    1.19  lemma dom_option_map:
    1.20    "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
    1.21 @@ -347,7 +347,7 @@
    1.22  
    1.23  lemma map_add_map_of_foldr:
    1.24    "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
    1.25 -  by (induct ps) (auto simp add: ext_iff map_add_def)
    1.26 +  by (induct ps) (auto simp add: fun_eq_iff map_add_def)
    1.27  
    1.28  
    1.29  subsection {* @{term [source] restrict_map} *}
    1.30 @@ -381,26 +381,26 @@
    1.31  
    1.32  lemma restrict_fun_upd [simp]:
    1.33    "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
    1.34 -by (simp add: restrict_map_def ext_iff)
    1.35 +by (simp add: restrict_map_def fun_eq_iff)
    1.36  
    1.37  lemma fun_upd_None_restrict [simp]:
    1.38    "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)"
    1.39 -by (simp add: restrict_map_def ext_iff)
    1.40 +by (simp add: restrict_map_def fun_eq_iff)
    1.41  
    1.42  lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
    1.43 -by (simp add: restrict_map_def ext_iff)
    1.44 +by (simp add: restrict_map_def fun_eq_iff)
    1.45  
    1.46  lemma fun_upd_restrict_conv [simp]:
    1.47    "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
    1.48 -by (simp add: restrict_map_def ext_iff)
    1.49 +by (simp add: restrict_map_def fun_eq_iff)
    1.50  
    1.51  lemma map_of_map_restrict:
    1.52    "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
    1.53 -  by (induct ks) (simp_all add: ext_iff restrict_map_insert)
    1.54 +  by (induct ks) (simp_all add: fun_eq_iff restrict_map_insert)
    1.55  
    1.56  lemma restrict_complement_singleton_eq:
    1.57    "f |` (- {x}) = f(x := None)"
    1.58 -  by (simp add: restrict_map_def ext_iff)
    1.59 +  by (simp add: restrict_map_def fun_eq_iff)
    1.60  
    1.61  
    1.62  subsection {* @{term [source] map_upds} *}
    1.63 @@ -641,7 +641,7 @@
    1.64  by (fastsimp simp add: map_le_def)
    1.65  
    1.66  lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
    1.67 -by(fastsimp simp: map_add_def map_le_def ext_iff split: option.splits)
    1.68 +by(fastsimp simp: map_add_def map_le_def fun_eq_iff split: option.splits)
    1.69  
    1.70  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
    1.71  by (fastsimp simp add: map_le_def map_add_def dom_def)