src/HOL/Map.thy
changeset 44890 22f665a2e91c
parent 42163 392fd6c4669c
child 44921 58eef4843641
     1.1 --- a/src/HOL/Map.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4  
     1.5  lemma inj_on_map_add_dom [iff]:
     1.6    "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
     1.7 -by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits)
     1.8 +by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
     1.9  
    1.10  lemma map_upds_fold_map_upd:
    1.11    "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
    1.12 @@ -443,7 +443,7 @@
    1.13  
    1.14  lemma map_upds_twist [simp]:
    1.15    "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
    1.16 -using set_take_subset by (fastsimp simp add: map_upd_upds_conv_if)
    1.17 +using set_take_subset by (fastforce simp add: map_upd_upds_conv_if)
    1.18  
    1.19  lemma map_upds_apply_nontin [simp]:
    1.20    "x ~: set xs ==> (f(xs[|->]ys)) x = f x"
    1.21 @@ -631,7 +631,7 @@
    1.22  by (force simp add: map_le_def)
    1.23  
    1.24  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
    1.25 -by (fastsimp simp add: map_le_def)
    1.26 +by (fastforce simp add: map_le_def)
    1.27  
    1.28  lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    1.29  by (force simp add: map_le_def)
    1.30 @@ -645,7 +645,7 @@
    1.31  done
    1.32  
    1.33  lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
    1.34 -by (fastsimp simp add: map_le_def dom_def)
    1.35 +by (fastforce simp add: map_le_def dom_def)
    1.36  
    1.37  lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
    1.38  by (simp add: map_le_def)
    1.39 @@ -657,17 +657,17 @@
    1.40  unfolding map_le_def
    1.41  apply (rule ext)
    1.42  apply (case_tac "x \<in> dom f", simp)
    1.43 -apply (case_tac "x \<in> dom g", simp, fastsimp)
    1.44 +apply (case_tac "x \<in> dom g", simp, fastforce)
    1.45  done
    1.46  
    1.47  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
    1.48 -by (fastsimp simp add: map_le_def)
    1.49 +by (fastforce simp add: map_le_def)
    1.50  
    1.51  lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
    1.52 -by(fastsimp simp: map_add_def map_le_def fun_eq_iff split: option.splits)
    1.53 +by(fastforce simp: map_add_def map_le_def fun_eq_iff split: option.splits)
    1.54  
    1.55  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
    1.56 -by (fastsimp simp add: map_le_def map_add_def dom_def)
    1.57 +by (fastforce simp add: map_le_def map_add_def dom_def)
    1.58  
    1.59  lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
    1.60  by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)