--- a/thys/FMap.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/FMap.thy	Fri May 30 12:04:49 2014 +0100
@@ -15,6 +15,8 @@
 
 lift_definition lookup :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value option" is "(\<lambda> x. x)" ..
 
+notation lookup (infixl "$" 999)
+
 abbreviation the_lookup (infix "f!" 55)
   where "m f! x \<equiv> the (lookup m x)"
 
@@ -23,7 +25,7 @@
 lemma fempty_fdom[simp]: "fdom f\<emptyset> = {}"
   by (transfer, auto)
 
-lemma fdomIff: "(a : fdom m) = (lookup m a \<noteq> None)"
+lemma fdomIff: "a \<in> fdom m \<longleftrightarrow> lookup m a \<noteq> None"
  by (transfer, auto)
 
 lemma lookup_not_fdom: "x \<notin> fdom m \<Longrightarrow> lookup m x = None"
@@ -345,14 +347,44 @@
       by simp
   qed
 qed
+
+fun alookup
+where
+  "alookup k [] = None"
+| "alookup k ((x, y) # xs) = (if (k = x) then Some y else alookup k xs)"
+
   
-definition fmapdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list"
+definition fdom_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)"
+  "fdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)"
+
+lemma
+  "fdom f = set (fdom_to_list f)"
+unfolding fdom_to_list_def
+apply(subgoal_tac "finite (fdom f)")
+apply(drule finite_sorted_distinct_unique)
+apply(drule theI')
+apply(simp_all)
+done
+
+
 
 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]"
+  "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fdom_to_list f]"
+
+lemma
+  shows "(f $ k) = alookup k (fmap_to_alist f)" 
+thm finite_dom_map_of
 
+apply(transfer)
+apply(simp add: fmap_to_alist_def)
+
+thm lookup_def
+
+apply(rule theI2)
+apply(induct k xs\<equiv>"fmap_to_alist f" rule: alookup.induct)
+apply(simp add: fmap_to_alist_def fmapdom_to_list_def)
+thm theD1
 
 end