9 |
9 |
10 theory Map |
10 theory Map |
11 imports List |
11 imports List |
12 begin |
12 begin |
13 |
13 |
14 types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0) |
14 types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0) |
15 translations (type) "'a ~=> 'b" <= (type) "'a => 'b option" |
15 translations (type) "'a ~=> 'b" <= (type) "'a => 'b option" |
16 |
16 |
17 type_notation (xsymbols) |
17 type_notation (xsymbols) |
18 "~=>" (infixr "\<rightharpoonup>" 0) |
18 "map" (infixr "\<rightharpoonup>" 0) |
19 |
19 |
20 abbreviation |
20 abbreviation |
21 empty :: "'a ~=> 'b" where |
21 empty :: "'a ~=> 'b" where |
22 "empty == %x. None" |
22 "empty == %x. None" |
23 |
23 |
648 by(auto simp add: map_le_def) |
648 by(auto simp add: map_le_def) |
649 ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym) |
649 ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym) |
650 thus "\<exists>v. f = [x \<mapsto> v]" by blast |
650 thus "\<exists>v. f = [x \<mapsto> v]" by blast |
651 qed |
651 qed |
652 |
652 |
|
653 |
|
654 subsection {* Various *} |
|
655 |
|
656 lemma set_map_of_compr: |
|
657 assumes distinct: "distinct (map fst xs)" |
|
658 shows "set xs = {(k, v). map_of xs k = Some v}" |
|
659 using assms proof (induct xs) |
|
660 case Nil then show ?case by simp |
|
661 next |
|
662 case (Cons x xs) |
|
663 obtain k v where "x = (k, v)" by (cases x) blast |
|
664 with Cons.prems have "k \<notin> dom (map_of xs)" |
|
665 by (simp add: dom_map_of_conv_image_fst) |
|
666 then have *: "insert (k, v) {(k, v). map_of xs k = Some v} = |
|
667 {(k', v'). (map_of xs(k \<mapsto> v)) k' = Some v'}" |
|
668 by (auto split: if_splits) |
|
669 from Cons have "set xs = {(k, v). map_of xs k = Some v}" by simp |
|
670 with * `x = (k, v)` show ?case by simp |
|
671 qed |
|
672 |
|
673 lemma map_of_inject_set: |
|
674 assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)" |
|
675 shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs") |
|
676 proof |
|
677 assume ?lhs |
|
678 moreover from `distinct (map fst xs)` have "set xs = {(k, v). map_of xs k = Some v}" |
|
679 by (rule set_map_of_compr) |
|
680 moreover from `distinct (map fst ys)` have "set ys = {(k, v). map_of ys k = Some v}" |
|
681 by (rule set_map_of_compr) |
|
682 ultimately show ?rhs by simp |
|
683 next |
|
684 assume ?rhs show ?lhs proof |
|
685 fix k |
|
686 show "map_of xs k = map_of ys k" proof (cases "map_of xs k") |
|
687 case None |
|
688 moreover with `?rhs` have "map_of ys k = None" |
|
689 by (simp add: map_of_eq_None_iff) |
|
690 ultimately show ?thesis by simp |
|
691 next |
|
692 case (Some v) |
|
693 moreover with distinct `?rhs` have "map_of ys k = Some v" |
|
694 by simp |
|
695 ultimately show ?thesis by simp |
|
696 qed |
|
697 qed |
|
698 qed |
|
699 |
653 end |
700 end |
654 |
701 |