src/HOL/Map.thy
changeset 14187 26dfcd0ac436
parent 14186 6d2a494e33be
child 14208 144f45277d5a
     1.1 --- a/src/HOL/Map.thy	Thu Sep 11 22:33:12 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Sun Sep 14 17:53:27 2003 +0200
     1.3 @@ -347,6 +347,24 @@
     1.4  lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
     1.5  by(simp add:map_upds_def)
     1.6  
     1.7 +lemma map_upds_append1[simp]: "\<And>ys m. size xs < size ys \<Longrightarrow>
     1.8 +  m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
     1.9 +apply(induct xs)
    1.10 + apply(clarsimp simp add:neq_Nil_conv)
    1.11 +apply(case_tac ys)
    1.12 + apply simp
    1.13 +apply simp
    1.14 +done
    1.15 +
    1.16 +lemma map_upds_list_update2_drop[simp]:
    1.17 + "\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
    1.18 +     \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
    1.19 +apply(induct xs)
    1.20 + apply simp
    1.21 +apply(case_tac ys)
    1.22 + apply simp
    1.23 +apply(simp split:nat.split)
    1.24 +done
    1.25  
    1.26  lemma map_upd_upds_conv_if: "!!x y ys f.
    1.27   (f(x|->y))(xs [|->] ys) =
    1.28 @@ -478,9 +496,15 @@
    1.29  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
    1.30  by(simp add:map_le_def)
    1.31  
    1.32 +lemma [simp]: "f(x := None) \<subseteq>\<^sub>m f"
    1.33 +by(force simp add:map_le_def)
    1.34 +
    1.35  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
    1.36  by(fastsimp simp add:map_le_def)
    1.37  
    1.38 +lemma [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    1.39 +by(force simp add:map_le_def)
    1.40 +
    1.41  lemma map_le_upds[simp]:
    1.42   "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
    1.43  apply(induct as)
    1.44 @@ -495,11 +519,8 @@
    1.45  lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
    1.46    by (simp add: map_le_def)
    1.47  
    1.48 -lemma map_le_trans: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m h"
    1.49 -  apply (clarsimp simp add: map_le_def)
    1.50 -  apply (drule_tac x="a" in bspec, fastsimp)+
    1.51 -  apply assumption
    1.52 -done
    1.53 +lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
    1.54 +by(force simp add:map_le_def)
    1.55  
    1.56  lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
    1.57    apply (unfold map_le_def)