src/HOL/Map.thy
changeset 14180 d2e550609c40
parent 14134 0fdf5708c7a8
child 14186 6d2a494e33be
     1.1 --- a/src/HOL/Map.thy	Mon Sep 01 15:07:43 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Sep 03 18:20:57 2003 +0200
     1.3 @@ -22,25 +22,31 @@
     1.4  ran	:: "('a ~=> 'b) => 'b set"
     1.5  map_of	:: "('a * 'b)list => 'a ~=> 'b"
     1.6  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
     1.7 -	    ('a ~=> 'b)"		 ("_/'(_[|->]_/')" [900,0,0]900)
     1.8 +	    ('a ~=> 'b)"
     1.9  map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    1.10  	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    1.11  map_subst::"('a ~=> 'b) => 'b => 'b => 
    1.12  	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    1.13  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.14  
    1.15 +nonterminals
    1.16 +  maplets maplet
    1.17 +
    1.18  syntax
    1.19 -empty	::  "'a ~=> 'b"
    1.20 -map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.21 -					 ("_/'(_/|->_')"   [900,0,0]900)
    1.22 +  empty	    ::  "'a ~=> 'b"
    1.23 +  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    1.24 +  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
    1.25 +  ""         :: "maplet => maplets"             ("_")
    1.26 +  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
    1.27 +  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
    1.28 +  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
    1.29  
    1.30  syntax (xsymbols)
    1.31 +  "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    1.32 +  "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    1.33 +
    1.34    "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    1.35    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
    1.36 -  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    1.37 -					  ("_/'(_/\<mapsto>/_')"  [900,0,0]900)
    1.38 -  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.39 -				         ("_/'(_/[\<mapsto>]/_')" [900,0,0]900)
    1.40    map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    1.41  				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    1.42    map_subst :: "('a ~=> 'b) => 'b => 'b => 
    1.43 @@ -52,9 +58,15 @@
    1.44    "empty"    => "_K None"
    1.45    "empty"    <= "%x. None"
    1.46  
    1.47 -  "m(a|->b)" == "m(a:=Some b)"
    1.48    "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    1.49  
    1.50 +  "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    1.51 +  "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    1.52 +  "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    1.53 +  "_Map ms"                     == "_MapUpd empty ms"
    1.54 +  "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    1.55 +  "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    1.56 +
    1.57  defs
    1.58  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.59