src/HOL/Library/AssocList.thy

 *}
 
 fun
   delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "delete k [] = []"
+    "delete k [] = []"
   | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
 
 fun
   update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where

 termination by lexicographic_order
 
 fun
   restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "restrict A [] = []"
+    "restrict A [] = []"
   | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
 
 fun
   map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "map_ran f [] = []"
+    "map_ran f [] = []"
   | "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
 
 fun
   clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "clearjunk [] = []"  
+    "clearjunk [] = []"  
   | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
 
 lemmas [simp del] = compose_hint
 
 
-(* ******************************************************************************** *)
 subsection {* Lookup *}
-(* ******************************************************************************** *)
 
 lemma lookup_simps [code func]: 
   "map_of [] k = None"
   "map_of (p#ps) k = (if fst p = k then Some (snd p) else map_of ps k)"
   by simp_all
 
 
-(* ******************************************************************************** *)
 subsection {* @{const delete} *}
-(* ******************************************************************************** *)
 
 lemma delete_def:
   "delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
   by (induct xs) auto
 

   by (induct al) auto
 
 lemma distinct_delete:
   assumes "distinct (map fst al)" 
   shows "distinct (map fst (delete k al))"
-using prems
+using assms
 proof (induct al)
   case Nil thus ?case by simp
 next
   case (Cons a al)
   from Cons.prems obtain 

     dist_al: "distinct (map fst al)"
     by auto
   show ?case
   proof (cases "fst a = k")
     case True
-    from True dist_al show ?thesis by simp
+    with Cons dist_al show ?thesis by simp
   next
     case False
     from dist_al
     have "distinct (map fst (delete k al))"
       by (rule Cons.hyps)

   by (induct al) auto
 
 lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
   by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
 
-(* ******************************************************************************** *)
+
 subsection {* @{const clearjunk} *}
-(* ******************************************************************************** *)
 
 lemma insert_fst_filter: 
   "insert a(fst ` {x \<in> set ps. fst x \<noteq> a}) = insert a (fst ` set ps)"
   by (induct ps) auto
 

   by (induct al rule: clearjunk.induct) (auto simp add: notin_fst_filter)
 
 lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
   by simp
 
-(* ******************************************************************************** *)
+
 subsection {* @{const dom} and @{term "ran"} *}
-(* ******************************************************************************** *)
 
 lemma dom_map_of': "fst ` set al = dom (map_of al)"
   by (induct al) auto
 
 lemmas dom_map_of = dom_map_of' [symmetric]

   also have "\<dots> = snd ` set (clearjunk al)"
     by (simp add: ran_distinct)
   finally show ?thesis .
 qed
    
-(* ******************************************************************************** *)
+
 subsection {* @{const update} *}
-(* ******************************************************************************** *)
 
 lemma update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
   by (induct al) auto
 
 lemma update_conv': "map_of (update k v al)  = ((map_of al)(k\<mapsto>v))"

   by (induct al) auto
 
 lemma distinct_update:
   assumes "distinct (map fst al)" 
   shows "distinct (map fst (update k v al))"
-using prems
+using assms
 proof (induct al)
   case Nil thus ?case by simp
 next
   case (Cons a al)
   from Cons.prems obtain 

 
 lemma image_update[simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
   by (simp add: update_conv' image_map_upd)
 
 
-(* ******************************************************************************** *)
 subsection {* @{const updates} *}
-(* ******************************************************************************** *)
 
 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
 proof (induct ks arbitrary: vs al)
   case Nil
   thus ?case by simp

   by (rule ext) (rule updates_conv)
 
 lemma distinct_updates:
   assumes "distinct (map fst al)"
   shows "distinct (map fst (updates ks vs al))"
-  using prems
+  using assms
   by (induct ks arbitrary: vs al)
    (auto simp add: distinct_update split: list.splits)
 
 lemma clearjunk_updates:
  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"

 
 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 {* @{const map_ran} *}
-(* ******************************************************************************** *)
 
 lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
   by (induct al) auto
 
 lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"

   by (induct ps) auto
 
 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
 
-(* ******************************************************************************** *)
+
 subsection {* @{const merge} *}
-(* ******************************************************************************** *)
 
 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   by (induct ys arbitrary: xs) (auto simp add: dom_update)
 
 lemma distinct_merge:
   assumes "distinct (map fst xs)"
   shows "distinct (map fst (merge xs ys))"
-  using prems
+  using assms
 by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
 
 lemma clearjunk_merge:
  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   by (induct ys) (auto simp add: clearjunk_update)

   by (simp add: updates_conv' merge_conv')
 
 lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
   by (simp add: merge_conv')
 
-(* ******************************************************************************** *)
+
 subsection {* @{const compose} *}
-(* ******************************************************************************** *)
 
 lemma compose_first_None [simp]: 
   assumes "map_of xs k = None" 
   shows "map_of (compose xs ys) k = None"
-using prems by (induct xs ys rule: compose.induct)
+using assms by (induct xs ys rule: compose.induct)
   (auto split: option.splits split_if_asm)
 
 lemma compose_conv: 
   shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
 proof (induct xs ys rule: compose.induct)

   by (rule ext) (rule compose_conv)
 
 lemma compose_first_Some [simp]:
   assumes "map_of xs k = Some v" 
   shows "map_of (compose xs ys) k = map_of ys v"
-using prems by (simp add: compose_conv)
+using assms by (simp add: compose_conv)
 
 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
 proof (induct xs ys rule: compose.induct)
   case 1 thus ?case by simp
 next

 qed
 
 lemma distinct_compose:
  assumes "distinct (map fst xs)"
  shows "distinct (map fst (compose xs ys))"
-using prems
+using assms
 proof (induct xs ys rule: compose.induct)
   case 1 thus ?case by simp
 next
   case (2 x xs ys)
   show ?case

   "(map_of (compose xs ys) k = None) = 
     (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 {* @{const restrict} *}
-(* ******************************************************************************** *)
 
 lemma restrict_def:
   "restrict A = filter (\<lambda>p. fst p \<in> A)"
 proof
   fix xs