src/HOL/Map.thy
changeset 17391 c6338ed6caf8
parent 15695 f072119afa4e
child 17399 56a3a4affedc
     1.1 --- a/src/HOL/Map.thy	Wed Sep 14 23:00:03 2005 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Sep 14 23:03:52 2005 +0200
     1.3 @@ -30,10 +30,9 @@
     1.4  	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
     1.5  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
     1.6  
     1.7 -syntax
     1.8 -  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
     1.9 -translations
    1.10 -  "f o_m m" == "option_map f o m"
    1.11 +constdefs
    1.12 +  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    1.13 +  "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.14  
    1.15  nonterminals
    1.16    maplets maplet
    1.17 @@ -50,7 +49,7 @@
    1.18  syntax (xsymbols)
    1.19    "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    1.20  
    1.21 -  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
    1.22 +  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
    1.23  
    1.24    "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    1.25    "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    1.26 @@ -261,6 +260,25 @@
    1.27  apply (simp (no_asm))
    1.28  done
    1.29  
    1.30 +subsection {* @{term map_comp} related *}
    1.31 +
    1.32 +lemma map_comp_empty [simp]: 
    1.33 +  "m \<circ>\<^sub>m empty = empty"
    1.34 +  "empty \<circ>\<^sub>m m = empty"
    1.35 +  by (auto simp add: map_comp_def intro: ext split: option.splits)
    1.36 +
    1.37 +lemma map_comp_simps [simp]: 
    1.38 +  "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
    1.39 +  "m2 k = Some k' \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = m1 k'" 
    1.40 +  by (auto simp add: map_comp_def)
    1.41 +
    1.42 +lemma map_comp_Some_iff:
    1.43 +  "((m1 \<circ>\<^sub>m m2) k = Some v) = (\<exists>k'. m2 k = Some k' \<and> m1 k' = Some v)" 
    1.44 +  by (auto simp add: map_comp_def split: option.splits)
    1.45 +
    1.46 +lemma map_comp_None_iff:
    1.47 +  "((m1 \<circ>\<^sub>m m2) k = None) = (m2 k = None \<or> (\<exists>k'. m2 k = Some k' \<and> m1 k' = None)) " 
    1.48 +  by (auto simp add: map_comp_def split: option.splits)
    1.49  
    1.50  subsection {* @{text "++"} *}
    1.51