src/HOL/Map.thy
changeset 18576 8d98b7711e47
parent 18447 da548623916a
child 19323 ec5cd5b1804c
     1.1 --- a/src/HOL/Map.thy	Wed Jan 04 17:04:11 2006 +0100
     1.2 +++ b/src/HOL/Map.thy	Wed Jan 04 19:22:53 2006 +0100
     1.3 @@ -530,7 +530,7 @@
     1.4  
     1.5  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
     1.6  apply(rule ext)
     1.7 -apply(force simp: map_add_def dom_def not_None_eq  split:option.split) 
     1.8 +apply(force simp: map_add_def dom_def split:option.split) 
     1.9  done
    1.10  
    1.11  subsection {* @{term [source] ran} *}
    1.12 @@ -587,13 +587,13 @@
    1.13  done
    1.14  
    1.15  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
    1.16 -  by (fastsimp simp add: map_le_def not_None_eq)
    1.17 +  by (fastsimp simp add: map_le_def)
    1.18  
    1.19  lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
    1.20  by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
    1.21  
    1.22  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
    1.23 -by (fastsimp simp add: map_le_def map_add_def dom_def not_None_eq)
    1.24 +by (fastsimp simp add: map_le_def map_add_def dom_def)
    1.25  
    1.26  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.27  by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)