# HG changeset patch
# User schirmer
# Date 1143540693 -7200
# Node ID 99dbefd7bc2e13ce2c38036472b2b684194d74f0
# Parent  bb71a64e126389bb18b07b9d912ae10403ccbf83
renamed map_val to map_ran

diff -r bb71a64e1263 -r 99dbefd7bc2e src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Tue Mar 28 12:05:45 2006 +0200
+++ b/src/HOL/Library/AssocList.thy	Tue Mar 28 12:11:33 2006 +0200
@@ -21,7 +21,7 @@
   merge      :: "('key * 'val)list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
   compose    :: "('key * 'a)list \<Rightarrow> ('a * 'b)list \<Rightarrow> ('key * 'b)list"
   restrict   :: "('key set) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
-  map_val    :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
+  map_ran    :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
 
   clearjunk  :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
 
@@ -41,8 +41,8 @@
 "merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
 
 primrec
-"map_val f [] = []"
-"map_val f (p#ps) = (fst p, f (fst p) (snd p))#map_val f ps"
+"map_ran f [] = []"
+"map_ran f (p#ps) = (fst p, f (fst p) (snd p))#map_ran f ps"
 
 
 lemma length_delete_le: "length (delete k al) \<le> length al"
@@ -432,23 +432,23 @@
   by (induct xs fixing: ys al) (auto split: list.splits)
 
 (* ******************************************************************************** *)
-subsection {* @{const map_val} *}
+subsection {* @{const map_ran} *}
 (* ******************************************************************************** *)
 
-lemma map_val_conv: "map_of (map_val f al) k = option_map (f k) (map_of al k)"
+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_val: "fst ` set (map_val f al) = fst ` set al"
+lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
   by (induct al) auto
 
-lemma distinct_map_val: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_val f al))"
-  by (induct al) (auto simp add: dom_map_val)
+lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
+  by (induct al) (auto simp add: dom_map_ran)
 
-lemma map_val_filter: "map_val f [p\<in>ps. fst p \<noteq> a] = [p\<in>map_val f ps. fst p \<noteq> a]"
+lemma map_ran_filter: "map_ran f [p\<in>ps. fst p \<noteq> a] = [p\<in>map_ran f ps. fst p \<noteq> a]"
   by (induct ps) auto
 
-lemma clearjunk_map_val: "clearjunk (map_val f al) = map_val f (clearjunk al)"
-  by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_val_filter)
+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} *}