src/HOL/Library/AssocList.thy
changeset 26152 cf2cccf17d6d
parent 25966 74f6817870f9
child 26304 02fbd0e7954a
     1.1 --- a/src/HOL/Library/AssocList.thy	Tue Feb 26 20:38:16 2008 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Tue Feb 26 20:38:17 2008 +0100
     1.3 @@ -16,29 +16,27 @@
     1.4    to establish the invariant, e.g. for inductive proofs.
     1.5  *}
     1.6  
     1.7 -fun
     1.8 +primrec
     1.9    delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.10  where
    1.11      "delete k [] = []"
    1.12    | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
    1.13  
    1.14 -fun
    1.15 +primrec
    1.16    update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.17  where
    1.18      "update k v [] = [(k, v)]"
    1.19    | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    1.20  
    1.21 -function
    1.22 +primrec
    1.23    updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.24  where
    1.25      "updates [] vs ps = ps"
    1.26    | "updates (k#ks) vs ps = (case vs
    1.27        of [] \<Rightarrow> ps
    1.28         | (v#vs') \<Rightarrow> updates ks vs' (update k v ps))"
    1.29 -by pat_completeness auto
    1.30 -termination by lexicographic_order
    1.31  
    1.32 -fun
    1.33 +primrec
    1.34    merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.35  where
    1.36      "merge qs [] = qs"
    1.37 @@ -66,23 +64,21 @@
    1.38    finally show ?thesis .
    1.39  qed
    1.40  
    1.41 -function
    1.42 +fun
    1.43    compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
    1.44  where
    1.45      "compose [] ys = []"
    1.46    | "compose (x#xs) ys = (case map_of ys (snd x)
    1.47         of None \<Rightarrow> compose (delete (fst x) xs) ys
    1.48          | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
    1.49 -by pat_completeness auto
    1.50 -termination by lexicographic_order
    1.51  
    1.52 -fun
    1.53 +primrec
    1.54    restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.55  where
    1.56      "restrict A [] = []"
    1.57    | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
    1.58  
    1.59 -fun
    1.60 +primrec
    1.61    map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.62  where
    1.63      "map_ran f [] = []"