6 *) |
6 *) |
7 |
7 |
8 theory Map imports ZF begin |
8 theory Map imports ZF begin |
9 |
9 |
10 definition |
10 definition |
11 TMap :: "[i,i] => i" where |
11 TMap :: "[i,i] \<Rightarrow> i" where |
12 "TMap(A,B) \<equiv> {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}" |
12 "TMap(A,B) \<equiv> {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}" |
13 |
13 |
14 definition |
14 definition |
15 PMap :: "[i,i] => i" where |
15 PMap :: "[i,i] \<Rightarrow> i" where |
16 "PMap(A,B) \<equiv> TMap(A,cons(0,B))" |
16 "PMap(A,B) \<equiv> TMap(A,cons(0,B))" |
17 |
17 |
18 (* Note: 0 \<in> B \<Longrightarrow> TMap(A,B) = PMap(A,B) *) |
18 (* Note: 0 \<in> B \<Longrightarrow> TMap(A,B) = PMap(A,B) *) |
19 |
19 |
20 definition |
20 definition |
21 map_emp :: i where |
21 map_emp :: i where |
22 "map_emp \<equiv> 0" |
22 "map_emp \<equiv> 0" |
23 |
23 |
24 definition |
24 definition |
25 map_owr :: "[i,i,i]=>i" where |
25 map_owr :: "[i,i,i]\<Rightarrow>i" where |
26 "map_owr(m,a,b) \<equiv> \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}" |
26 "map_owr(m,a,b) \<equiv> \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}" |
27 |
27 |
28 definition |
28 definition |
29 map_app :: "[i,i]=>i" where |
29 map_app :: "[i,i]\<Rightarrow>i" where |
30 "map_app(m,a) \<equiv> m``{a}" |
30 "map_app(m,a) \<equiv> m``{a}" |
31 |
31 |
32 lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})" |
32 lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})" |
33 by (unfold TMap_def, blast) |
33 by (unfold TMap_def, blast) |
34 |
34 |