renamed map_val to map_ran
authorschirmer
Tue Mar 28 12:11:33 2006 +0200 (2006-03-28)
changeset 1933399dbefd7bc2e
parent 19332 bb71a64e1263
child 19334 96ca738055a6
renamed map_val to map_ran
src/HOL/Library/AssocList.thy
     1.1 --- a/src/HOL/Library/AssocList.thy	Tue Mar 28 12:05:45 2006 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Tue Mar 28 12:11:33 2006 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    merge      :: "('key * 'val)list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
     1.5    compose    :: "('key * 'a)list \<Rightarrow> ('a * 'b)list \<Rightarrow> ('key * 'b)list"
     1.6    restrict   :: "('key set) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
     1.7 -  map_val    :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
     1.8 +  map_ran    :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
     1.9  
    1.10    clearjunk  :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.11  
    1.12 @@ -41,8 +41,8 @@
    1.13  "merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    1.14  
    1.15  primrec
    1.16 -"map_val f [] = []"
    1.17 -"map_val f (p#ps) = (fst p, f (fst p) (snd p))#map_val f ps"
    1.18 +"map_ran f [] = []"
    1.19 +"map_ran f (p#ps) = (fst p, f (fst p) (snd p))#map_ran f ps"
    1.20  
    1.21  
    1.22  lemma length_delete_le: "length (delete k al) \<le> length al"
    1.23 @@ -432,23 +432,23 @@
    1.24    by (induct xs fixing: ys al) (auto split: list.splits)
    1.25  
    1.26  (* ******************************************************************************** *)
    1.27 -subsection {* @{const map_val} *}
    1.28 +subsection {* @{const map_ran} *}
    1.29  (* ******************************************************************************** *)
    1.30  
    1.31 -lemma map_val_conv: "map_of (map_val f al) k = option_map (f k) (map_of al k)"
    1.32 +lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
    1.33    by (induct al) auto
    1.34  
    1.35 -lemma dom_map_val: "fst ` set (map_val f al) = fst ` set al"
    1.36 +lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"
    1.37    by (induct al) auto
    1.38  
    1.39 -lemma distinct_map_val: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_val f al))"
    1.40 -  by (induct al) (auto simp add: dom_map_val)
    1.41 +lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
    1.42 +  by (induct al) (auto simp add: dom_map_ran)
    1.43  
    1.44 -lemma map_val_filter: "map_val f [p\<in>ps. fst p \<noteq> a] = [p\<in>map_val f ps. fst p \<noteq> a]"
    1.45 +lemma map_ran_filter: "map_ran f [p\<in>ps. fst p \<noteq> a] = [p\<in>map_ran f ps. fst p \<noteq> a]"
    1.46    by (induct ps) auto
    1.47  
    1.48 -lemma clearjunk_map_val: "clearjunk (map_val f al) = map_val f (clearjunk al)"
    1.49 -  by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_val_filter)
    1.50 +lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
    1.51 +  by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
    1.52  
    1.53  (* ******************************************************************************** *)
    1.54  subsection {* @{const merge} *}