699 |
699 |
700 lemma bulkload_Mapping [code]: |
700 lemma bulkload_Mapping [code]: |
701 "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])" |
701 "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])" |
702 by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff) |
702 by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff) |
703 |
703 |
704 lemma map_of_eqI: (*FIXME move to Map.thy*) |
|
705 assumes set_eq: "set (map fst xs) = set (map fst ys)" |
|
706 assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k" |
|
707 shows "map_of xs = map_of ys" |
|
708 proof (rule ext) |
|
709 fix k show "map_of xs k = map_of ys k" |
|
710 proof (cases "map_of xs k") |
|
711 case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff) |
|
712 with set_eq have "k \<notin> set (map fst ys)" by simp |
|
713 then have "map_of ys k = None" by (simp add: map_of_eq_None_iff) |
|
714 with None show ?thesis by simp |
|
715 next |
|
716 case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric]) |
|
717 with map_eq show ?thesis by auto |
|
718 qed |
|
719 qed |
|
720 |
|
721 lemma map_of_eq_dom: (*FIXME move to Map.thy*) |
|
722 assumes "map_of xs = map_of ys" |
|
723 shows "fst ` set xs = fst ` set ys" |
|
724 proof - |
|
725 from assms have "dom (map_of xs) = dom (map_of ys)" by simp |
|
726 then show ?thesis by (simp add: dom_map_of_conv_image_fst) |
|
727 qed |
|
728 |
|
729 lemma equal_Mapping [code]: |
704 lemma equal_Mapping [code]: |
730 "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow> |
705 "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow> |
731 (let ks = map fst xs; ls = map fst ys |
706 (let ks = map fst xs; ls = map fst ys |
732 in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))" |
707 in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))" |
733 proof - |
708 proof - |
734 have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI) |
709 have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" |
|
710 by (auto simp add: image_def intro!: bexI) |
735 show ?thesis |
711 show ?thesis |
736 by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def) |
712 by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def) |
737 (auto dest!: map_of_eq_dom intro: aux) |
713 (auto dest!: map_of_eq_dom intro: aux) |
738 qed |
714 qed |
739 |
715 |