--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/FMap.thy Tue Apr 29 15:26:48 2014 +0100
@@ -0,0 +1,358 @@
+theory FMap
+ imports Main "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/DAList"
+begin
+
+subsubsection {* The type of finite maps *}
+
+typedef ('a, 'b) fmap (infixr "f\<rightharpoonup>" 1) = "{x :: 'a \<rightharpoonup> 'b. finite (dom x) }"
+ proof show "empty \<in> {x. finite (dom x)}" by simp qed
+
+setup_lifting type_definition_fmap
+
+lift_definition fdom :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key set" is "dom" ..
+
+lift_definition fran :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'value set" is "ran" ..
+
+lift_definition lookup :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value option" is "(\<lambda> x. x)" ..
+
+abbreviation the_lookup (infix "f!" 55)
+ where "m f! x \<equiv> the (lookup m x)"
+
+lift_definition fempty :: "'key f\<rightharpoonup> 'value" ("f\<emptyset>") is Map.empty by simp
+
+lemma fempty_fdom[simp]: "fdom f\<emptyset> = {}"
+ by (transfer, auto)
+
+lemma fdomIff: "(a : fdom m) = (lookup m a \<noteq> None)"
+ by (transfer, auto)
+
+lemma lookup_not_fdom: "x \<notin> fdom m \<Longrightarrow> lookup m x = None"
+ by (auto iff:fdomIff)
+
+lemma finite_range:
+ assumes "finite (dom m)"
+ shows "finite (ran m)"
+ apply (rule finite_subset[OF _ finite_imageI[OF assms, of "\<lambda> x . the (m x)"]])
+ by (auto simp add: ran_def dom_def image_def)
+
+lemma finite_fdom[simp]: "finite (fdom m)"
+ by transfer
+
+lemma finite_fran[simp]: "finite (fran m)"
+ by (transfer, rule finite_range)
+
+lemma fmap_eqI[intro]:
+ assumes "fdom a = fdom b"
+ and "\<And> x. x \<in> fdom a \<Longrightarrow> a f! x = b f! x"
+ shows "a = b"
+using assms
+proof(transfer)
+ fix a b :: "'a \<rightharpoonup> 'b"
+ assume d: "dom a = dom b"
+ assume eq: "\<And> x. x \<in> dom a \<Longrightarrow> the (a x) = the (b x)"
+ show "a = b"
+ proof
+ fix x
+ show "a x = b x"
+ proof(cases "a x")
+ case None
+ hence "x \<notin> dom a" by (simp add: dom_def)
+ hence "x \<notin> dom b" using d by simp
+ hence " b x = None" by (simp add: dom_def)
+ thus ?thesis using None by simp
+ next
+ case (Some y)
+ hence d': "x \<in> dom ( a)" by (simp add: dom_def)
+ hence "the ( a x) = the ( b x)" using eq by auto
+ moreover
+ have "x \<in> dom ( b)" using Some d' d by simp
+ then obtain y' where " b x = Some y'" by (auto simp add: dom_def)
+ ultimately
+ show " a x = b x" using Some by auto
+ qed
+ qed
+qed
+
+subsubsection {* Updates *}
+
+lift_definition
+ fmap_upd :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value \<Rightarrow> 'key f\<rightharpoonup> 'value" ("_'(_ f\<mapsto> _')" [900,900]900)
+ is "\<lambda> m x v. m( x \<mapsto> v)" by simp
+
+lemma fmap_upd_fdom[simp]: "fdom (h (x f\<mapsto> v)) = insert x (fdom h)"
+ by (transfer, auto)
+
+lemma the_lookup_fmap_upd[simp]: "lookup (h (x f\<mapsto> v)) x = Some v"
+ by (transfer, auto)
+
+lemma the_lookup_fmap_upd_other[simp]: "x' \<noteq> x \<Longrightarrow> lookup (h (x f\<mapsto> v)) x' = lookup h x'"
+ by (transfer, auto)
+
+lemma fmap_upd_overwrite[simp]: "f (x f\<mapsto> y) (x f\<mapsto> z) = f (x f\<mapsto> z)"
+ by (transfer, auto)
+
+lemma fmap_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a f\<mapsto> b))(c f\<mapsto> d) = (m(c f\<mapsto> d))(a f\<mapsto> b)"
+ apply (rule fmap_eqI)
+ apply auto[1]
+ apply (case_tac "x = a", auto)
+ apply (case_tac "x = c", auto)
+ done
+
+subsubsection {* Restriction *}
+
+lift_definition fmap_restr :: "'a set \<Rightarrow> 'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b"
+ is "\<lambda> S m. (if finite S then (restrict_map m S) else empty)" by auto
+
+lemma lookup_fmap_restr[simp]: "finite S \<Longrightarrow> x \<in> S \<Longrightarrow> lookup (fmap_restr S m) x = lookup m x"
+ by (transfer, auto)
+
+lemma fdom_fmap_restr[simp]: "finite S \<Longrightarrow> fdom (fmap_restr S m) = fdom m \<inter> S"
+ by (transfer, simp)
+
+lemma fmap_restr_fmap_restr[simp]:
+ "finite d1 \<Longrightarrow> finite d2 \<Longrightarrow> fmap_restr d1 (fmap_restr d2 x) = fmap_restr (d1 \<inter> d2) x"
+ by (transfer, auto simp add: restrict_map_def)
+
+lemma fmap_restr_fmap_restr_subset:
+ "finite d2 \<Longrightarrow> d1 \<subseteq> d2 \<Longrightarrow> fmap_restr d1 (fmap_restr d2 x) = fmap_restr d1 x"
+ by (metis Int_absorb2 finite_subset fmap_restr_fmap_restr)
+
+lemma fmap_restr_useless: "finite S \<Longrightarrow> fdom m \<subseteq> S \<Longrightarrow> fmap_restr S m = m"
+ by (rule fmap_eqI, auto)
+
+lemma fmap_restr_not_finite:
+ "\<not> finite S \<Longrightarrow> fmap_restr S \<rho> = f\<emptyset>"
+ by (transfer, simp)
+
+lemma fmap_restr_fmap_upd: "x \<in> S \<Longrightarrow> finite S \<Longrightarrow> fmap_restr S (m1(x f\<mapsto> v)) = (fmap_restr S m1)(x f\<mapsto> v)"
+ apply (rule fmap_eqI)
+ apply auto[1]
+ apply (case_tac "xa = x")
+ apply auto
+ done
+
+subsubsection {* Deleting *}
+
+lift_definition fmap_delete :: "'a \<Rightarrow> 'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b"
+ is "\<lambda> x m. m(x := None)" by auto
+
+lemma fdom_fmap_delete[simp]:
+ "fdom (fmap_delete x m) = fdom m - {x}"
+ by (transfer, auto)
+
+lemma fmap_delete_fmap_upd[simp]:
+ "fmap_delete x (m(x f\<mapsto> v)) = fmap_delete x m"
+ by (transfer, simp)
+
+lemma fmap_delete_noop:
+ "x \<notin> fdom m \<Longrightarrow> fmap_delete x m = m"
+ by (transfer, auto)
+
+lemma fmap_upd_fmap_delete[simp]: "x \<in> fdom \<Gamma> \<Longrightarrow> (fmap_delete x \<Gamma>)(x f\<mapsto> \<Gamma> f! x) = \<Gamma>"
+ by (transfer, auto)
+
+lemma fran_fmap_upd[simp]:
+ "fran (m(x f\<mapsto> v)) = insert v (fran (fmap_delete x m))"
+by (transfer, auto simp add: ran_def)
+
+subsubsection {* Addition (merging) of finite maps *}
+
+lift_definition fmap_add :: "'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b" (infixl "f++" 100)
+ is "map_add" by auto
+
+lemma fdom_fmap_add[simp]: "fdom (m1 f++ m2) = fdom m1 \<union> fdom m2"
+ by (transfer, auto)
+
+lemma lookup_fmap_add1[simp]: "x \<in> fdom m2 \<Longrightarrow> lookup (m1 f++ m2) x = lookup m2 x"
+ by (transfer, auto)
+
+lemma lookup_fmap_add2[simp]: "x \<notin> fdom m2 \<Longrightarrow> lookup (m1 f++ m2) x = lookup m1 x"
+ apply transfer
+ by (metis map_add_dom_app_simps(3))
+
+lemma [simp]: "\<rho> f++ f\<emptyset> = \<rho>"
+ by (transfer, auto)
+
+lemma fmap_add_overwrite: "fdom m1 \<subseteq> fdom m2 \<Longrightarrow> m1 f++ m2 = m2"
+ apply transfer
+ apply rule
+ apply (case_tac "x \<in> dom m2")
+ apply (auto simp add: map_add_dom_app_simps(1))
+ done
+
+lemma fmap_add_upd_swap:
+ "x \<notin> fdom \<rho>' \<Longrightarrow> \<rho>(x f\<mapsto> z) f++ \<rho>' = (\<rho> f++ \<rho>')(x f\<mapsto> z)"
+ apply transfer
+ by (metis map_add_upd_left)
+
+lemma fmap_add_upd:
+ "\<rho> f++ (\<rho>'(x f\<mapsto> z)) = (\<rho> f++ \<rho>')(x f\<mapsto> z)"
+ apply transfer
+ by (metis map_add_upd)
+
+lemma fmap_restr_add: "fmap_restr S (m1 f++ m2) = fmap_restr S m1 f++ fmap_restr S m2"
+ apply (cases "finite S")
+ apply (rule fmap_eqI)
+ apply auto[1]
+ apply (case_tac "x \<in> fdom m2")
+ apply auto
+ apply (simp add: fmap_restr_not_finite)
+ done
+
+subsubsection {* Conversion from associative lists *}
+
+lift_definition fmap_of :: "('a \<times> 'b) list \<Rightarrow> 'a f\<rightharpoonup> 'b"
+ is map_of by (rule finite_dom_map_of)
+
+lemma fmap_of_Nil[simp]: "fmap_of [] = f\<emptyset>"
+ by (transfer, simp)
+
+lemma fmap_of_Cons[simp]: "fmap_of (p # l) = (fmap_of l)(fst p f\<mapsto> snd p)"
+ by (transfer, simp)
+
+lemma fmap_of_append[simp]: "fmap_of (l1 @ l2) = fmap_of l2 f++ fmap_of l1"
+ by (transfer, simp)
+
+lemma lookup_fmap_of[simp]:
+ "lookup (fmap_of m) x = map_of m x"
+ by (transfer, auto)
+
+lemma fmap_delete_fmap_of[simp]:
+ "fmap_delete x (fmap_of m) = fmap_of (AList.delete x m)"
+ by (transfer, metis delete_conv')
+
+subsubsection {* Less-than-relation for extending finite maps *}
+
+instantiation fmap :: (type,type) order
+begin
+ definition "\<rho> \<le> \<rho>' = ((fdom \<rho> \<subseteq> fdom \<rho>') \<and> (\<forall>x \<in> fdom \<rho>. lookup \<rho> x = lookup \<rho>' x))"
+ definition "(\<rho>::'a f\<rightharpoonup> 'b) < \<rho>' = (\<rho> \<noteq> \<rho>' \<and> \<rho> \<le> \<rho>')"
+
+ lemma fmap_less_eqI[intro]:
+ assumes assm1: "fdom \<rho> \<subseteq> fdom \<rho>'"
+ and assm2: "\<And> x. \<lbrakk> x \<in> fdom \<rho> ; x \<in> fdom \<rho>' \<rbrakk> \<Longrightarrow> \<rho> f! x = \<rho>' f! x "
+ shows "\<rho> \<le> \<rho>'"
+ unfolding less_eq_fmap_def
+ apply rule
+ apply fact
+ apply rule+
+ apply (frule subsetD[OF `_ \<subseteq> _`])
+ apply (frule assm2)
+ apply (auto iff: fdomIff)
+ done
+
+ lemma fmap_less_eqD:
+ assumes "\<rho> \<le> \<rho>'"
+ assumes "x \<in> fdom \<rho>"
+ shows "lookup \<rho> x = lookup \<rho>' x"
+ using assms
+ unfolding less_eq_fmap_def by auto
+
+ lemma fmap_antisym: assumes "(x:: 'a f\<rightharpoonup> 'b) \<le> y" and "y \<le> x" shows "x = y "
+ proof(rule fmap_eqI[rule_format])
+ show "fdom x = fdom y" using `x \<le> y` and `y \<le> x` unfolding less_eq_fmap_def by auto
+
+ fix v
+ assume "v \<in> fdom x"
+ hence "v \<in> fdom y" using `fdom _ = _` by simp
+
+ thus "x f! v = y f! v"
+ using `x \<le> y` `v \<in> fdom x` unfolding less_eq_fmap_def by simp
+ qed
+
+ lemma fmap_trans: assumes "(x:: 'a f\<rightharpoonup> 'b) \<le> y" and "y \<le> z" shows "x \<le> z"
+ proof
+ show "fdom x \<subseteq> fdom z" using `x \<le> y` and `y \<le> z` unfolding less_eq_fmap_def
+ by -(rule order_trans [of _ "fdom y"], auto)
+
+ fix v
+ assume "v \<in> fdom x" and "v \<in> fdom z"
+ hence "v \<in> fdom y" using `x \<le> y` unfolding less_eq_fmap_def by auto
+ hence "lookup y v = lookup x v"
+ using `x \<le> y` `v \<in> fdom x` unfolding less_eq_fmap_def by auto
+ moreover
+ have "lookup y v = lookup z v"
+ by (rule fmap_less_eqD[OF `y \<le> z` `v \<in> fdom y`])
+ ultimately
+ show "x f! v = z f! v" by auto
+ qed
+
+ instance
+ apply default
+ using fmap_antisym apply (auto simp add: less_fmap_def)[1]
+ apply (auto simp add: less_eq_fmap_def)[1]
+ using fmap_trans apply assumption
+ using fmap_antisym apply assumption
+ done
+end
+
+lemma fmap_less_fdom:
+ "\<rho>1 \<le> \<rho>2 \<Longrightarrow> fdom \<rho>1 \<subseteq> fdom \<rho>2"
+ by (metis less_eq_fmap_def)
+
+lemma fmap_less_restrict:
+ "\<rho>1 \<le> \<rho>2 \<longleftrightarrow> \<rho>1 = fmap_restr (fdom \<rho>1) \<rho>2"
+ unfolding less_eq_fmap_def
+ apply transfer
+ apply (auto simp add:restrict_map_def split:option.split_asm)
+ by (metis option.simps(3))+
+
+lemma fmap_restr_less:
+ "fmap_restr S \<rho> \<le> \<rho>"
+ unfolding less_eq_fmap_def
+ by (transfer, auto)
+
+lemma fmap_upd_less[simp, intro]:
+ "\<rho>1 \<le> \<rho>2 \<Longrightarrow> v1 = v2 \<Longrightarrow> \<rho>1(x f\<mapsto> v1) \<le> \<rho>2(x f\<mapsto> v2)"
+ apply (rule fmap_less_eqI)
+ apply (auto dest: fmap_less_fdom)[1]
+ apply (case_tac "xa = x")
+ apply (auto dest: fmap_less_eqD)
+ done
+
+lemma fmap_update_less[simp, intro]:
+ "\<rho>1 \<le> \<rho>1' \<Longrightarrow> \<rho>2 \<le> \<rho>2' \<Longrightarrow> (fdom \<rho>2' - fdom \<rho>2) \<inter> fdom \<rho>1 = {} \<Longrightarrow> \<rho>1 f++ \<rho>2 \<le> \<rho>1' f++ \<rho>2'"
+ apply (rule fmap_less_eqI)
+ apply (auto dest: fmap_less_fdom)[1]
+ apply (case_tac "x \<in> fdom \<rho>2")
+ apply (auto dest: fmap_less_eqD fmap_less_fdom)
+ apply (metis fmap_less_eqD fmap_less_fdom lookup_fmap_add1 set_mp)
+ by (metis Diff_iff Diff_triv fmap_less_eqD lookup_fmap_add2)
+
+lemma fmap_restr_le:
+ assumes "\<rho>1 \<le> \<rho>2"
+ assumes "S1 \<subseteq> S2"
+ assumes [simp]:"finite S2"
+ shows "fmap_restr S1 \<rho>1 \<le> fmap_restr S2 \<rho>2"
+proof-
+ have [simp]: "finite S1"
+ by (rule finite_subset[OF `S1 \<subseteq> S2` `finite S2`])
+ show ?thesis
+ proof (rule fmap_less_eqI)
+ have "fdom \<rho>1 \<subseteq> fdom \<rho>2"
+ by (metis assms(1) less_eq_fmap_def)
+ thus "fdom (fmap_restr S1 \<rho>1) \<subseteq> fdom (fmap_restr S2 \<rho>2)"
+ using `S1 \<subseteq> S2`
+ by auto
+ next
+ fix x
+ assume "x \<in> fdom (fmap_restr S1 \<rho>1) "
+ hence [simp]:"x \<in> fdom \<rho>1" and [simp]:"x \<in> S1" and [simp]: "x \<in> S2"
+ by (auto intro: set_mp[OF `S1 \<subseteq> S2`])
+ have "\<rho>1 f! x = \<rho>2 f! x"
+ by (metis `x \<in> fdom \<rho>1` assms(1) less_eq_fmap_def)
+ thus "(fmap_restr S1 \<rho>1) f! x = (fmap_restr S2 \<rho>2) f! x"
+ by simp
+ qed
+qed
+
+definition fmapdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list"
+where
+ "fmapdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)"
+
+definition fmap_to_alist :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> ('a \<times> 'b) list"
+where
+ "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fmapdom_to_list f]"
+
+
+end