src/HOL/Map.thy
changeset 19323 ec5cd5b1804c
parent 18576 8d98b7711e47
child 19378 6cc9ac729eb5
     1.1 --- a/src/HOL/Map.thy	Thu Mar 23 18:14:06 2006 +0100
     1.2 +++ b/src/HOL/Map.thy	Thu Mar 23 20:03:53 2006 +0100
     1.3 @@ -16,29 +16,28 @@
     1.4  translations (type) "a ~=> b " <= (type) "a => b option"
     1.5  
     1.6  consts
     1.7 -chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     1.8  map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     1.9  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
    1.10  dom	:: "('a ~=> 'b) => 'a set"
    1.11  ran	:: "('a ~=> 'b) => 'b set"
    1.12  map_of	:: "('a * 'b)list => 'a ~=> 'b"
    1.13 -map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    1.14 -	    ('a ~=> 'b)"
    1.15 -map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    1.16 -	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    1.17 -map_subst::"('a ~=> 'b) => 'b => 'b => 
    1.18 -	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    1.19 +map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.20  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.21  
    1.22  constdefs
    1.23    map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    1.24    "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.25  
    1.26 +syntax
    1.27 +  empty     ::  "'a ~=> 'b"
    1.28 +translations
    1.29 +  "empty"    => "%_. None"
    1.30 +  "empty"    <= "%x. None"
    1.31 +
    1.32  nonterminals
    1.33    maplets maplet
    1.34  
    1.35  syntax
    1.36 -  empty	    ::  "'a ~=> 'b"
    1.37    "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    1.38    "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
    1.39    ""         :: "maplet => maplets"             ("_")
    1.40 @@ -54,23 +53,11 @@
    1.41    "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    1.42    "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    1.43  
    1.44 -  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    1.45 -				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    1.46 -  map_subst :: "('a ~=> 'b) => 'b => 'b => 
    1.47 -	        ('a ~=> 'b)"			 ("_/'(_\<leadsto>_/')"    [900,0,0]900)
    1.48 - "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    1.49 -					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    1.50 -
    1.51  syntax (latex output)
    1.52    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    1.53    --"requires amssymb!"
    1.54  
    1.55  translations
    1.56 -  "empty"    => "%_. None"
    1.57 -  "empty"    <= "%x. None"
    1.58 -
    1.59 -  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    1.60 -
    1.61    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    1.62    "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    1.63    "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    1.64 @@ -79,14 +66,10 @@
    1.65    "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    1.66  
    1.67  defs
    1.68 -chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.69 -
    1.70  map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.71  restrict_map_def: "m|`A == %x. if x : A then m x else None"
    1.72  
    1.73  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    1.74 -map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    1.75 -map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    1.76  
    1.77  dom_def: "dom(m) == {a. m a ~= None}"
    1.78  ran_def: "ran(m) == {b. EX a. m a = Some b}"
    1.79 @@ -97,6 +80,38 @@
    1.80    "map_of [] = empty"
    1.81    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    1.82  
    1.83 +(* special purpose constants that should be defined somewhere else and
    1.84 +whose syntax is a bit odd as well:
    1.85 +
    1.86 + "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    1.87 +					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    1.88 +  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    1.89 +
    1.90 +map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    1.91 +	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    1.92 +map_subst::"('a ~=> 'b) => 'b => 'b => 
    1.93 +	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    1.94 +
    1.95 +map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    1.96 +map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    1.97 +
    1.98 +  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    1.99 +				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
   1.100 +  map_subst :: "('a ~=> 'b) => 'b => 'b => 
   1.101 +	        ('a ~=> 'b)"			 ("_/'(_\<leadsto>_/')"    [900,0,0]900)
   1.102 +
   1.103 +
   1.104 +subsection {* @{term [source] map_upd_s} *}
   1.105 +
   1.106 +lemma map_upd_s_apply [simp]: 
   1.107 +  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
   1.108 +by (simp add: map_upd_s_def)
   1.109 +
   1.110 +lemma map_subst_apply [simp]: 
   1.111 +  "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
   1.112 +by (simp add: map_subst_def)
   1.113 +
   1.114 +*)
   1.115  
   1.116  subsection {* @{term [source] empty} *}
   1.117  
   1.118 @@ -166,18 +181,6 @@
   1.119  done
   1.120  
   1.121  
   1.122 -subsection {* @{term [source] chg_map} *}
   1.123 -
   1.124 -lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
   1.125 -by (unfold chg_map_def, auto)
   1.126 -
   1.127 -lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   1.128 -by (unfold chg_map_def, auto)
   1.129 -
   1.130 -lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
   1.131 -by (auto simp: chg_map_def split add: option.split)
   1.132 -
   1.133 -
   1.134  subsection {* @{term [source] map_of} *}
   1.135  
   1.136  lemma map_of_eq_None_iff:
   1.137 @@ -461,16 +464,6 @@
   1.138  done
   1.139  
   1.140  
   1.141 -subsection {* @{term [source] map_upd_s} *}
   1.142 -
   1.143 -lemma map_upd_s_apply [simp]: 
   1.144 -  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
   1.145 -by (simp add: map_upd_s_def)
   1.146 -
   1.147 -lemma map_subst_apply [simp]: 
   1.148 -  "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
   1.149 -by (simp add: map_subst_def)
   1.150 -
   1.151  subsection {* @{term [source] dom} *}
   1.152  
   1.153  lemma domI: "m a = Some b ==> a : dom m"