src/HOL/Library/AssocList.thy
changeset 19323 ec5cd5b1804c
parent 19234 054332e39e0a
child 19332 bb71a64e1263
     1.1 --- a/src/HOL/Library/AssocList.thy	Thu Mar 23 18:14:06 2006 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Thu Mar 23 20:03:53 2006 +0100
     1.3 @@ -16,14 +16,17 @@
     1.4    delete     :: "'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     1.5    update     :: "'key \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     1.6    updates    :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     1.7 -  substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
     1.8 -  map_at     :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val) list"
     1.9    merge      :: "('key * 'val)list \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.10    compose    :: "('key * 'a)list \<Rightarrow> ('a * 'b)list \<Rightarrow> ('key * 'b)list"
    1.11    restrict   :: "('key set) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.12  
    1.13    clearjunk  :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.14  
    1.15 +(* a bit special
    1.16 +  substitute :: "'val \<Rightarrow> 'val \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
    1.17 +  map_at     :: "('val \<Rightarrow> 'val) \<Rightarrow> 'key \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val) list"
    1.18 +*)
    1.19 +
    1.20  defs
    1.21  delete_def: "delete k \<equiv> filter (\<lambda>p. fst p \<noteq> k)"
    1.22  
    1.23 @@ -35,15 +38,18 @@
    1.24  "updates (k#ks) vs al = (case vs of [] \<Rightarrow> al 
    1.25                           | (v#vs') \<Rightarrow> updates ks vs' (update k v al))"
    1.26  primrec
    1.27 +"merge xs [] = xs"
    1.28 +"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    1.29 +
    1.30 +(*
    1.31 +primrec
    1.32  "substitute v v' [] = []"
    1.33  "substitute v v' (p#ps) = (if snd p = v then (fst p,v')#substitute v v' ps
    1.34                            else p#substitute v v' ps)"
    1.35  primrec
    1.36  "map_at f k [] = []"
    1.37  "map_at f k (p#ps) = (if fst p = k then (k,f (snd p))#ps else p # map_at f k ps)"
    1.38 -primrec
    1.39 -"merge xs [] = xs"
    1.40 -"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    1.41 +*)
    1.42  
    1.43  lemma length_delete_le: "length (delete k al) \<le> length al"
    1.44  proof (induct al)
    1.45 @@ -431,7 +437,7 @@
    1.46    "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
    1.47    by (induct xs fixing: ys al) (auto split: list.splits)
    1.48  
    1.49 -
    1.50 +(*
    1.51  (* ******************************************************************************** *)
    1.52  subsection {* @{const substitute} *}
    1.53  (* ******************************************************************************** *)
    1.54 @@ -456,7 +462,8 @@
    1.55  lemma clearjunk_substitute:
    1.56   "clearjunk (substitute v v' al) = substitute v v' (clearjunk al)"
    1.57    by (induct al rule: clearjunk.induct) (auto simp add: substitute_filter delete_def)
    1.58 -
    1.59 +*)
    1.60 +(*
    1.61  (* ******************************************************************************** *)
    1.62  subsection {* @{const map_at} *}
    1.63  (* ******************************************************************************** *)
    1.64 @@ -491,7 +498,7 @@
    1.65  
    1.66  lemma map_at_other [simp]: "a \<noteq> b \<Longrightarrow> map_of (map_at f a al) b = map_of al b"
    1.67    by (simp add: map_at_conv')
    1.68 -
    1.69 +*)
    1.70  (* ******************************************************************************** *)
    1.71  subsection {* @{const merge} *}
    1.72  (* ******************************************************************************** *)