added map_val, superseding map_at and substitute
authorschirmer
Tue Mar 28 12:05:45 2006 +0200 (2006-03-28)
changeset 19332bb71a64e1263
parent 19331 f5e84acd7d3f
child 19333 99dbefd7bc2e
added map_val, superseding map_at and substitute
----------------------------------------------------------------------
src/HOL/Library/AssocList.thy
     1.1 --- a/src/HOL/Library/AssocList.thy	Tue Mar 28 10:13:51 2006 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Tue Mar 28 12:05:45 2006 +0200
     1.3 @@ -11,7 +11,9 @@
     1.4  begin
     1.5  
     1.6  text {* The operations preserve distinctness of keys and 
     1.7 -        function @{term "clearjunk"} distributes over them.*}
     1.8 +        function @{term "clearjunk"} distributes over them. Since 
     1.9 +        @{term clearjunk} enforces distinctness of keys it can be used
    1.10 +        to establish the invariant, e.g. for inductive proofs.*}
    1.11  consts 
    1.12    delete     :: "'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
    1.13    update     :: "'key \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
    1.14 @@ -19,13 +21,10 @@
    1.15    merge      :: "('key * 'val)list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.16    compose    :: "('key * 'a)list \<Rightarrow> ('a * 'b)list \<Rightarrow> ('key * 'b)list"
    1.17    restrict   :: "('key set) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.18 +  map_val    :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.19  
    1.20    clearjunk  :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.21  
    1.22 -(* a bit special
    1.23 -  substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
    1.24 -  map_at     :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val) list"
    1.25 -*)
    1.26  
    1.27  defs
    1.28  delete_def: "delete k \<equiv> filter (\<lambda>p. fst p \<noteq> k)"
    1.29 @@ -41,15 +40,10 @@
    1.30  "merge xs [] = xs"
    1.31  "merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    1.32  
    1.33 -(*
    1.34  primrec
    1.35 -"substitute v v' [] = []"
    1.36 -"substitute v v' (p#ps) = (if snd p = v then (fst p,v')#substitute v v' ps
    1.37 -                          else p#substitute v v' ps)"
    1.38 -primrec
    1.39 -"map_at f k [] = []"
    1.40 -"map_at f k (p#ps) = (if fst p = k then (k,f (snd p))#ps else p # map_at f k ps)"
    1.41 -*)
    1.42 +"map_val f [] = []"
    1.43 +"map_val f (p#ps) = (fst p, f (fst p) (snd p))#map_val f ps"
    1.44 +
    1.45  
    1.46  lemma length_delete_le: "length (delete k al) \<le> length al"
    1.47  proof (induct al)
    1.48 @@ -437,68 +431,25 @@
    1.49    "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
    1.50    by (induct xs fixing: ys al) (auto split: list.splits)
    1.51  
    1.52 -(*
    1.53  (* ******************************************************************************** *)
    1.54 -subsection {* @{const substitute} *}
    1.55 +subsection {* @{const map_val} *}
    1.56  (* ******************************************************************************** *)
    1.57  
    1.58 -lemma substitute_conv: "map_of (substitute v v' al) k = ((map_of al)(v ~> v')) k"
    1.59 +lemma map_val_conv: "map_of (map_val f al) k = option_map (f k) (map_of al k)"
    1.60    by (induct al) auto
    1.61  
    1.62 -lemma substitute_conv': "map_of (substitute v v' al) = ((map_of al)(v ~> v'))"
    1.63 -  by (rule ext) (rule substitute_conv)
    1.64 -
    1.65 -lemma dom_substitute: "fst ` set (substitute v v' al) = fst ` set al"
    1.66 +lemma dom_map_val: "fst ` set (map_val f al) = fst ` set al"
    1.67    by (induct al) auto
    1.68  
    1.69 -lemma distinct_substitute: 
    1.70 -  "distinct (map fst al) \<Longrightarrow> distinct (map fst (substitute v v' al))"
    1.71 -  by (induct al) (auto simp add: dom_substitute)
    1.72 +lemma distinct_map_val: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_val f al))"
    1.73 +  by (induct al) (auto simp add: dom_map_val)
    1.74  
    1.75 -lemma substitute_filter: 
    1.76 -  "(substitute v v' [q\<in>ps . fst q \<noteq> a]) = [q\<in>substitute v v' ps . fst q \<noteq> a]"
    1.77 +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.78    by (induct ps) auto
    1.79  
    1.80 -lemma clearjunk_substitute:
    1.81 - "clearjunk (substitute v v' al) = substitute v v' (clearjunk al)"
    1.82 -  by (induct al rule: clearjunk.induct) (auto simp add: substitute_filter delete_def)
    1.83 -*)
    1.84 -(*
    1.85 -(* ******************************************************************************** *)
    1.86 -subsection {* @{const map_at} *}
    1.87 -(* ******************************************************************************** *)
    1.88 -  
    1.89 -lemma map_at_conv: "map_of (map_at f k al) k' = (chg_map f k (map_of al)) k'"
    1.90 -  by (induct al) (auto simp add: chg_map_def split: option.splits)
    1.91 -
    1.92 -lemma map_at_conv': "map_of (map_at f k al) = (chg_map f k (map_of al))"
    1.93 -  by (rule ext) (rule map_at_conv)
    1.94 -
    1.95 -lemma dom_map_at: "fst ` set (map_at f k al) = fst ` set al"
    1.96 -  by (induct al) auto
    1.97 +lemma clearjunk_map_val: "clearjunk (map_val f al) = map_val f (clearjunk al)"
    1.98 +  by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_val_filter)
    1.99  
   1.100 -lemma distinct_map_at: 
   1.101 -  assumes "distinct (map fst al)"
   1.102 -  shows "distinct (map fst (map_at f k al))"
   1.103 -using prems by (induct al) (auto simp add: dom_map_at)
   1.104 -
   1.105 -lemma map_at_notin_filter: 
   1.106 -  "a \<noteq> k \<Longrightarrow> (map_at f k [q\<in>ps . fst q \<noteq> a]) = [q\<in>map_at f k ps . fst q \<noteq> a]"
   1.107 -  by (induct ps) auto
   1.108 -
   1.109 -lemma clearjunk_map_at:
   1.110 - "clearjunk (map_at f k al) = map_at f k (clearjunk al)"
   1.111 -  by (induct al rule: clearjunk.induct) (auto simp add: map_at_notin_filter delete_def)
   1.112 -
   1.113 -lemma map_at_new[simp]: "map_of al k = None \<Longrightarrow> map_at f k al = al"
   1.114 -  by (induct al) auto
   1.115 -
   1.116 -lemma map_at_update: "map_of al k = Some v \<Longrightarrow> map_at f k al = update k (f v) al"
   1.117 -  by (induct al) auto
   1.118 -
   1.119 -lemma map_at_other [simp]: "a \<noteq> b \<Longrightarrow> map_of (map_at f a al) b = map_of al b"
   1.120 -  by (simp add: map_at_conv')
   1.121 -*)
   1.122  (* ******************************************************************************** *)
   1.123  subsection {* @{const merge} *}
   1.124  (* ******************************************************************************** *)