# HG changeset patch
# User schirmer
# Date 1126731832 -7200
# Node ID c6338ed6caf838cf823fcd32d70f03f6354a5eb3
# Parent  df2b53a669379323638e0e86122e34ba92135e80
removed syntax fun_map_comp;
introduced map_comp;

diff -r df2b53a66937 -r c6338ed6caf8 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Sep 14 23:00:03 2005 +0200
+++ b/src/HOL/Map.thy	Wed Sep 14 23:03:52 2005 +0200
@@ -30,10 +30,9 @@
 	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
 map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
 
-syntax
-  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
-translations
-  "f o_m m" == "option_map f o m"
+constdefs
+  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
+  "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
 
 nonterminals
   maplets maplet
@@ -50,7 +49,7 @@
 syntax (xsymbols)
   "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
 
-  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
+  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
 
   "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
   "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
@@ -261,6 +260,25 @@
 apply (simp (no_asm))
 done
 
+subsection {* @{term map_comp} related *}
+
+lemma map_comp_empty [simp]: 
+  "m \<circ>\<^sub>m empty = empty"
+  "empty \<circ>\<^sub>m m = empty"
+  by (auto simp add: map_comp_def intro: ext split: option.splits)
+
+lemma map_comp_simps [simp]: 
+  "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
+  "m2 k = Some k' \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = m1 k'" 
+  by (auto simp add: map_comp_def)
+
+lemma map_comp_Some_iff:
+  "((m1 \<circ>\<^sub>m m2) k = Some v) = (\<exists>k'. m2 k = Some k' \<and> m1 k' = Some v)" 
+  by (auto simp add: map_comp_def split: option.splits)
+
+lemma map_comp_None_iff:
+  "((m1 \<circ>\<^sub>m m2) k = None) = (m2 k = None \<or> (\<exists>k'. m2 k = Some k' \<and> m1 k' = None)) " 
+  by (auto simp add: map_comp_def split: option.splits)
 
 subsection {* @{text "++"} *}