src/HOL/Library/AList.thy

 (*  Title:      HOL/Library/AList.thy
     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
 *)
 
-section {* Implementation of Association Lists *}
+section \<open>Implementation of Association Lists\<close>
 
 theory AList
 imports Main
 begin
 
 context
 begin
 
-text {*
+text \<open>
   The operations preserve distinctness of keys and
   function @{term "clearjunk"} distributes over them. Since
   @{term clearjunk} enforces distinctness of keys it can be used
   to establish the invariant, e.g. for inductive proofs.
-*}
-
-subsection {* @{text update} and @{text updates} *}
+\<close>
+
+subsection \<open>@{text update} and @{text updates}\<close>
 
 qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "update k v [] = [(k, v)]"
 | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"

 qed
 
 lemma update_last [simp]: "update k v (update k v' al) = update k v al"
   by (induct al) auto
 
-text {* Note that the lists are not necessarily the same:
+text \<open>Note that the lists are not necessarily the same:
         @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and
-        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
+        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.\<close>
 
 lemma update_swap:
   "k \<noteq> k' \<Longrightarrow>
     map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
   by (simp add: update_conv' fun_eq_iff)

 lemma updates_append2_drop [simp]:
   "size xs = size ys \<Longrightarrow> updates xs (ys @ zs) al = updates xs ys al"
   by (induct xs arbitrary: ys al) (auto split: list.splits)
 
 
-subsection {* @{text delete} *}
+subsection \<open>@{text delete}\<close>
 
 qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
 
 lemma delete_simps [simp]:

 
 lemma length_delete_le: "length (delete k al) \<le> length al"
   by (simp add: delete_eq)
 
 
-subsection {* @{text update_with_aux} and @{text delete_aux}*}
+subsection \<open>@{text update_with_aux} and @{text delete_aux}\<close>
 
 qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "update_with_aux v k f [] = [(k, f v)]"
 | "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
 
-text {*
+text \<open>
   The above @{term "delete"} traverses all the list even if it has found the key.
   This one does not have to keep going because is assumes the invariant that keys are distinct.
-*}
+\<close>
 qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "delete_aux k [] = []"
 | "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
 

 
 lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
 by(cases ts)(auto split: split_if_asm)
 
 
-subsection {* @{text restrict} *}
+subsection \<open>@{text restrict}\<close>
 
 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
 
 lemma restr_simps [simp]:

 
 lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
   by (induct ps) auto
 
 
-subsection {* @{text clearjunk} *}
+subsection \<open>@{text clearjunk}\<close>
 
 qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "clearjunk [] = []"
 | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"

   shows "clearjunk (map f ps) = map f (clearjunk ps)"
   by (induct ps rule: clearjunk.induct [case_names Nil Cons])
     (simp_all add: clearjunk_delete delete_map assms)
 
 
-subsection {* @{text map_ran} *}
+subsection \<open>@{text map_ran}\<close>
 
 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
 
 lemma map_ran_simps [simp]:

 
 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   by (simp add: map_ran_def split_def clearjunk_map)
 
 
-subsection {* @{text merge} *}
+subsection \<open>@{text merge}\<close>
 
 qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
 
 lemma merge_simps [simp]:

 
 lemma merge_append: "map_of (xs @ ys) = map_of (merge ys xs)"
   by (simp add: merge_conv')
 
 
-subsection {* @{text compose} *}
+subsection \<open>@{text compose}\<close>
 
 qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
 where
   "compose [] ys = []"
 | "compose (x # xs) ys =

   "map_of (compose xs ys) k = None \<longleftrightarrow>
     (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None))"
   by (simp add: compose_conv map_comp_None_iff)
 
 
-subsection {* @{text map_entry} *}
+subsection \<open>@{text map_entry}\<close>
 
 qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "map_entry k f [] = []"
 | "map_entry k f (p # ps) =

   assumes "distinct (map fst xs)"
   shows "distinct (map fst (map_entry k f xs))"
   using assms by (induct xs) (auto simp add: dom_map_entry)
 
 
-subsection {* @{text map_default} *}
+subsection \<open>@{text map_default}\<close>
 
 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "map_default k v f [] = [(k, v)]"
 | "map_default k v f (p # ps) =