equal
deleted
inserted
replaced
13 |
13 |
14 lift_definition fran :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'value set" is "ran" .. |
14 lift_definition fran :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'value set" is "ran" .. |
15 |
15 |
16 lift_definition lookup :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value option" is "(\<lambda> x. x)" .. |
16 lift_definition lookup :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value option" is "(\<lambda> x. x)" .. |
17 |
17 |
|
18 notation lookup (infixl "$" 999) |
|
19 |
18 abbreviation the_lookup (infix "f!" 55) |
20 abbreviation the_lookup (infix "f!" 55) |
19 where "m f! x \<equiv> the (lookup m x)" |
21 where "m f! x \<equiv> the (lookup m x)" |
20 |
22 |
21 lift_definition fempty :: "'key f\<rightharpoonup> 'value" ("f\<emptyset>") is Map.empty by simp |
23 lift_definition fempty :: "'key f\<rightharpoonup> 'value" ("f\<emptyset>") is Map.empty by simp |
22 |
24 |
23 lemma fempty_fdom[simp]: "fdom f\<emptyset> = {}" |
25 lemma fempty_fdom[simp]: "fdom f\<emptyset> = {}" |
24 by (transfer, auto) |
26 by (transfer, auto) |
25 |
27 |
26 lemma fdomIff: "(a : fdom m) = (lookup m a \<noteq> None)" |
28 lemma fdomIff: "a \<in> fdom m \<longleftrightarrow> lookup m a \<noteq> None" |
27 by (transfer, auto) |
29 by (transfer, auto) |
28 |
30 |
29 lemma lookup_not_fdom: "x \<notin> fdom m \<Longrightarrow> lookup m x = None" |
31 lemma lookup_not_fdom: "x \<notin> fdom m \<Longrightarrow> lookup m x = None" |
30 by (auto iff:fdomIff) |
32 by (auto iff:fdomIff) |
31 |
33 |
343 by (metis `x \<in> fdom \<rho>1` assms(1) less_eq_fmap_def) |
345 by (metis `x \<in> fdom \<rho>1` assms(1) less_eq_fmap_def) |
344 thus "(fmap_restr S1 \<rho>1) f! x = (fmap_restr S2 \<rho>2) f! x" |
346 thus "(fmap_restr S1 \<rho>1) f! x = (fmap_restr S2 \<rho>2) f! x" |
345 by simp |
347 by simp |
346 qed |
348 qed |
347 qed |
349 qed |
348 |
350 |
349 definition fmapdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list" |
351 fun alookup |
350 where |
352 where |
351 "fmapdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)" |
353 "alookup k [] = None" |
|
354 | "alookup k ((x, y) # xs) = (if (k = x) then Some y else alookup k xs)" |
|
355 |
|
356 |
|
357 definition fdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list" |
|
358 where |
|
359 "fdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)" |
|
360 |
|
361 lemma |
|
362 "fdom f = set (fdom_to_list f)" |
|
363 unfolding fdom_to_list_def |
|
364 apply(subgoal_tac "finite (fdom f)") |
|
365 apply(drule finite_sorted_distinct_unique) |
|
366 apply(drule theI') |
|
367 apply(simp_all) |
|
368 done |
|
369 |
|
370 |
352 |
371 |
353 definition fmap_to_alist :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> ('a \<times> 'b) list" |
372 definition fmap_to_alist :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> ('a \<times> 'b) list" |
354 where |
373 where |
355 "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fmapdom_to_list f]" |
374 "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fdom_to_list f]" |
356 |
375 |
|
376 lemma |
|
377 shows "(f $ k) = alookup k (fmap_to_alist f)" |
|
378 thm finite_dom_map_of |
|
379 |
|
380 apply(transfer) |
|
381 apply(simp add: fmap_to_alist_def) |
|
382 |
|
383 thm lookup_def |
|
384 |
|
385 apply(rule theI2) |
|
386 apply(induct k xs\<equiv>"fmap_to_alist f" rule: alookup.induct) |
|
387 apply(simp add: fmap_to_alist_def fmapdom_to_list_def) |
|
388 thm theD1 |
357 |
389 |
358 end |
390 end |