10 theory Map |
10 theory Map |
11 imports List |
11 imports List |
12 abbrevs "(=" = "\<subseteq>\<^sub>m" |
12 abbrevs "(=" = "\<subseteq>\<^sub>m" |
13 begin |
13 begin |
14 |
14 |
15 type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0) |
15 type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr \<open>\<rightharpoonup>\<close> 0) |
16 |
16 |
17 abbreviation (input) |
17 abbreviation (input) |
18 empty :: "'a \<rightharpoonup> 'b" where |
18 empty :: "'a \<rightharpoonup> 'b" where |
19 "empty \<equiv> \<lambda>x. None" |
19 "empty \<equiv> \<lambda>x. None" |
20 |
20 |
21 definition |
21 definition |
22 map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)" (infixl "\<circ>\<^sub>m" 55) where |
22 map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)" (infixl \<open>\<circ>\<^sub>m\<close> 55) where |
23 "f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)" |
23 "f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)" |
24 |
24 |
25 definition |
25 definition |
26 map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl "++" 100) where |
26 map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl \<open>++\<close> 100) where |
27 "m1 ++ m2 = (\<lambda>x. case m2 x of None \<Rightarrow> m1 x | Some y \<Rightarrow> Some y)" |
27 "m1 ++ m2 = (\<lambda>x. case m2 x of None \<Rightarrow> m1 x | Some y \<Rightarrow> Some y)" |
28 |
28 |
29 definition |
29 definition |
30 restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl "|`" 110) where |
30 restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl \<open>|`\<close> 110) where |
31 "m|`A = (\<lambda>x. if x \<in> A then m x else None)" |
31 "m|`A = (\<lambda>x. if x \<in> A then m x else None)" |
32 |
32 |
33 notation (latex output) |
33 notation (latex output) |
34 restrict_map ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110) |
34 restrict_map (\<open>_\<restriction>\<^bsub>_\<^esub>\<close> [111,110] 110) |
35 |
35 |
36 definition |
36 definition |
37 dom :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" where |
37 dom :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" where |
38 "dom m = {a. m a \<noteq> None}" |
38 "dom m = {a. m a \<noteq> None}" |
39 |
39 |
44 definition |
44 definition |
45 graph :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where |
45 graph :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where |
46 "graph m = {(a, b) | a b. m a = Some b}" |
46 "graph m = {(a, b) | a b. m a = Some b}" |
47 |
47 |
48 definition |
48 definition |
49 map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<subseteq>\<^sub>m" 50) where |
49 map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix \<open>\<subseteq>\<^sub>m\<close> 50) where |
50 "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)" |
50 "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)" |
51 |
51 |
52 text \<open>Function update syntax \<open>f(x := y, \<dots>)\<close> is extended with \<open>x \<mapsto> y\<close>, which is short for |
52 text \<open>Function update syntax \<open>f(x := y, \<dots>)\<close> is extended with \<open>x \<mapsto> y\<close>, which is short for |
53 \<open>x := Some y\<close>. \<open>:=\<close> and \<open>\<mapsto>\<close> can be mixed freely. |
53 \<open>x := Some y\<close>. \<open>:=\<close> and \<open>\<mapsto>\<close> can be mixed freely. |
54 The syntax \<open>[x \<mapsto> y, \<dots>]\<close> is short for \<open>Map.empty(x \<mapsto> y, \<dots>)\<close> |
54 The syntax \<open>[x \<mapsto> y, \<dots>]\<close> is short for \<open>Map.empty(x \<mapsto> y, \<dots>)\<close> |
55 but must only contain \<open>\<mapsto>\<close>, not \<open>:=\<close>, because \<open>[x:=y]\<close> clashes with the list update syntax \<open>xs[i:=x]\<close>.\<close> |
55 but must only contain \<open>\<mapsto>\<close>, not \<open>:=\<close>, because \<open>[x:=y]\<close> clashes with the list update syntax \<open>xs[i:=x]\<close>.\<close> |
56 |
56 |
57 nonterminal maplet and maplets |
57 nonterminal maplet and maplets |
58 |
58 |
59 syntax |
59 syntax |
60 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /\<mapsto>/ _") |
60 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /\<mapsto>/ _\<close>) |
61 "" :: "maplet \<Rightarrow> updbind" ("_") |
61 "" :: "maplet \<Rightarrow> updbind" (\<open>_\<close>) |
62 "" :: "maplet \<Rightarrow> maplets" ("_") |
62 "" :: "maplet \<Rightarrow> maplets" (\<open>_\<close>) |
63 "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _") |
63 "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>) |
64 "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" ("(1[_])") |
64 "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" (\<open>(1[_])\<close>) |
65 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *) |
65 (* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *) |
66 |
66 |
67 syntax (ASCII) |
67 syntax (ASCII) |
68 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /|->/ _") |
68 "_maplet" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /|->/ _\<close>) |
69 |
69 |
70 syntax_consts |
70 syntax_consts |
71 "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd |
71 "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd |
72 |
72 |
73 translations |
73 translations |
95 "map_upds m xs ys = m ++ map_of (rev (zip xs ys))" |
95 "map_upds m xs ys = m ++ map_of (rev (zip xs ys))" |
96 |
96 |
97 text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close> |
97 text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close> |
98 |
98 |
99 syntax |
99 syntax |
100 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[\<mapsto>]/ _") |
100 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /[\<mapsto>]/ _\<close>) |
101 |
101 |
102 syntax (ASCII) |
102 syntax (ASCII) |
103 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[|->]/ _") |
103 "_maplets" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /[|->]/ _\<close>) |
104 |
104 |
105 syntax_consts |
105 syntax_consts |
106 "_maplets" \<rightleftharpoons> map_upds |
106 "_maplets" \<rightleftharpoons> map_upds |
107 |
107 |
108 translations |
108 translations |