src/HOL/Library/AssocList.thy
changeset 22740 2d8d0d61475a
parent 21404 eb85850d3eb7
child 22803 5129e02f4df2
     1.1 --- a/src/HOL/Library/AssocList.thy	Fri Apr 20 11:21:37 2007 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Fri Apr 20 11:21:38 2007 +0200
     1.3 @@ -10,44 +10,44 @@
     1.4  
     1.5  begin
     1.6  
     1.7 -text {* The operations preserve distinctness of keys and 
     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 -  updates    :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key * 'val)list \<Rightarrow>  ('key * 'val)list"
    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_ran    :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.19 +text {*
    1.20 +  The operations preserve distinctness of keys and 
    1.21 +  function @{term "clearjunk"} distributes over them. Since 
    1.22 +  @{term clearjunk} enforces distinctness of keys it can be used
    1.23 +  to establish the invariant, e.g. for inductive proofs.
    1.24 +*}
    1.25  
    1.26 -  clearjunk  :: "('key * 'val)list \<Rightarrow> ('key * 'val)list"
    1.27 -
    1.28 +fun
    1.29 +  delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.30 +where
    1.31 +  "delete k [] = []"
    1.32 +  | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
    1.33  
    1.34 -defs
    1.35 -delete_def: "delete k \<equiv> filter (\<lambda>p. fst p \<noteq> k)"
    1.36 +fun
    1.37 +  update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.38 +where
    1.39 +    "update k v [] = [(k, v)]"
    1.40 +  | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    1.41  
    1.42 -primrec
    1.43 -"update k v [] = [(k,v)]"
    1.44 -"update k v (p#ps) = (if fst p = k then (k,v)#ps else p # update k v ps)"
    1.45 -primrec
    1.46 -"updates [] vs al = al"
    1.47 -"updates (k#ks) vs al = (case vs of [] \<Rightarrow> al 
    1.48 -                         | (v#vs') \<Rightarrow> updates ks vs' (update k v al))"
    1.49 -primrec
    1.50 -"merge xs [] = xs"
    1.51 -"merge xs (p#ps) = update (fst p) (snd p) (merge xs ps)"
    1.52 +function
    1.53 +  updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.54 +where
    1.55 +    "updates [] vs ps = ps"
    1.56 +  | "updates (k#ks) vs ps = (case vs
    1.57 +      of [] \<Rightarrow> ps
    1.58 +       | (v#vs') \<Rightarrow> updates ks vs' (update k v ps))"
    1.59 +by pat_completeness auto
    1.60 +termination by lexicographic_order
    1.61  
    1.62 -primrec
    1.63 -"map_ran f [] = []"
    1.64 -"map_ran f (p#ps) = (fst p, f (fst p) (snd p))#map_ran f ps"
    1.65 -
    1.66 +fun
    1.67 +  merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.68 +where
    1.69 +    "merge qs [] = qs"
    1.70 +  | "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
    1.71  
    1.72  lemma length_delete_le: "length (delete k al) \<le> length al"
    1.73  proof (induct al)
    1.74 -  case Nil thus ?case by (simp add: delete_def)
    1.75 +  case Nil thus ?case by simp
    1.76  next
    1.77    case (Cons a al)
    1.78    note length_filter_le [of "\<lambda>p. fst p \<noteq> fst a" al] 
    1.79 @@ -55,10 +55,11 @@
    1.80      by simp
    1.81    finally have "length [p\<in>al . fst p \<noteq> fst a] \<le> Suc (length al)" .
    1.82    with Cons show ?case
    1.83 -    by (auto simp add: delete_def)
    1.84 +    by auto
    1.85  qed
    1.86  
    1.87 -lemma compose_hint: "length (delete k al) < Suc (length al)"
    1.88 +lemma compose_hint [simp]:
    1.89 +  "length (delete k al) < Suc (length al)"
    1.90  proof -
    1.91    note length_delete_le
    1.92    also have "\<And>n. n < Suc n"
    1.93 @@ -66,41 +67,56 @@
    1.94    finally show ?thesis .
    1.95  qed
    1.96  
    1.97 -recdef compose "measure size"
    1.98 -"compose [] = (\<lambda>ys. [])"
    1.99 -"compose (x#xs) = (\<lambda>ys. (case (map_of ys (snd x)) of
   1.100 -                          None \<Rightarrow> compose (delete (fst x) xs) ys
   1.101 -                         | Some v \<Rightarrow> (fst x,v)#compose xs ys))"
   1.102 -(hints intro: compose_hint)
   1.103 +function
   1.104 +  compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
   1.105 +where
   1.106 +    "compose [] ys = []"
   1.107 +  | "compose (x#xs) ys = (case map_of ys (snd x)
   1.108 +       of None \<Rightarrow> compose (delete (fst x) xs) ys
   1.109 +        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   1.110 +by pat_completeness auto
   1.111 +termination by lexicographic_order
   1.112  
   1.113 -defs  
   1.114 -restrict_def: "restrict A \<equiv> filter (\<lambda>(k,v). k \<in> A)"
   1.115 +fun
   1.116 +  restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   1.117 +where
   1.118 +  "restrict A [] = []"
   1.119 +  | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
   1.120  
   1.121 -recdef clearjunk "measure size"
   1.122 -"clearjunk [] = []"
   1.123 -"clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   1.124 -(hints intro: compose_hint)
   1.125 +fun
   1.126 +  map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   1.127 +where
   1.128 +  "map_ran f [] = []"
   1.129 +  | "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
   1.130 +
   1.131 +fun
   1.132 +  clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   1.133 +where
   1.134 +  "clearjunk [] = []"  
   1.135 +  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   1.136 +
   1.137 +lemmas [simp del] = compose_hint
   1.138  
   1.139  
   1.140  (* ******************************************************************************** *)
   1.141  subsection {* Lookup *}
   1.142  (* ******************************************************************************** *)
   1.143  
   1.144 -lemma lookup_simps: 
   1.145 +lemma lookup_simps [code func]: 
   1.146    "map_of [] k = None"
   1.147    "map_of (p#ps) k = (if fst p = k then Some (snd p) else map_of ps k)"
   1.148    by simp_all
   1.149  
   1.150 +
   1.151  (* ******************************************************************************** *)
   1.152  subsection {* @{const delete} *}
   1.153  (* ******************************************************************************** *)
   1.154  
   1.155 -lemma delete_simps [simp]:
   1.156 -    "delete k [] = []"
   1.157 -    "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
   1.158 -  by (simp_all add: delete_def)
   1.159 +lemma delete_def:
   1.160 +  "delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
   1.161 +  by (induct xs) auto
   1.162  
   1.163 -lemma delete_id[simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   1.164 +lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
   1.165    by (induct al) auto
   1.166  
   1.167  lemma delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   1.168 @@ -188,8 +204,8 @@
   1.169  proof (induct al rule: clearjunk.induct [case_names Nil Cons])
   1.170    case Nil thus ?case by simp
   1.171  next
   1.172 -  case (Cons k v ps)
   1.173 -  from Cons have "length (clearjunk [q\<in>ps . fst q \<noteq> k]) \<le> length [q\<in>ps . fst q \<noteq> k]" 
   1.174 +  case (Cons p ps)
   1.175 +  from Cons have "length (clearjunk [q\<in>ps . fst q \<noteq> fst p]) \<le> length [q\<in>ps . fst q \<noteq> fst p]" 
   1.176      by (simp add: delete_def)
   1.177    also have "\<dots> \<le> length ps"
   1.178      by simp
   1.179 @@ -387,7 +403,8 @@
   1.180    assumes "distinct (map fst al)"
   1.181    shows "distinct (map fst (updates ks vs al))"
   1.182    using prems
   1.183 -by (induct ks arbitrary: vs al) (auto simp add: distinct_update split: list.splits)
   1.184 +  by (induct ks arbitrary: vs al)
   1.185 +   (auto simp add: distinct_update split: list.splits)
   1.186  
   1.187  lemma clearjunk_updates:
   1.188   "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   1.189 @@ -525,26 +542,21 @@
   1.190  (* ******************************************************************************** *)
   1.191  
   1.192  lemma compose_induct [case_names Nil Cons]: 
   1.193 +  fixes xs ys
   1.194    assumes Nil: "P [] ys"
   1.195    assumes Cons: "\<And>x xs.
   1.196 -     \<lbrakk>\<And>v. map_of ys (snd x) = Some v \<Longrightarrow> P xs ys;
   1.197 -      map_of ys (snd x) = None \<Longrightarrow> P (delete (fst x) xs) ys\<rbrakk>
   1.198 +     (\<And>v. map_of ys (snd x) = Some v \<Longrightarrow> P xs ys)
   1.199 +     \<Longrightarrow> (map_of ys (snd x) = None \<Longrightarrow> P (delete (fst x) xs) ys)
   1.200       \<Longrightarrow> P (x # xs) ys"
   1.201    shows "P xs ys"
   1.202 -apply (rule compose.induct [where ?P="\<lambda>xs. P xs ys"])
   1.203 -apply (rule Nil)
   1.204 -apply  (rule Cons)
   1.205 -apply (erule allE, erule allE, erule impE, assumption,assumption)
   1.206 -apply (erule allE, erule impE,assumption,assumption)
   1.207 -done
   1.208 -
   1.209 +by (induct xs rule: compose.induct [where ?P="\<lambda>xs zs. P xs ys"])
   1.210 +  (auto intro: Nil Cons)
   1.211  lemma compose_first_None [simp]: 
   1.212    assumes "map_of xs k = None" 
   1.213    shows "map_of (compose xs ys) k = None"
   1.214  using prems
   1.215  by (induct xs ys rule: compose_induct) (auto split: option.splits split_if_asm)
   1.216  
   1.217 -
   1.218  lemma compose_conv: 
   1.219    shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   1.220  proof (induct xs ys rule: compose_induct)
   1.221 @@ -701,10 +713,13 @@
   1.222  subsection {* @{const restrict} *}
   1.223  (* ******************************************************************************** *)
   1.224  
   1.225 -lemma restrict_simps [simp]: 
   1.226 -  "restrict A [] = []"
   1.227 -  "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
   1.228 -  by (auto simp add: restrict_def)
   1.229 +lemma restrict_def:
   1.230 +  "restrict A = filter (\<lambda>p. fst p \<in> A)"
   1.231 +proof
   1.232 +  fix xs
   1.233 +  show "restrict A xs = filter (\<lambda>p. fst p \<in> A) xs"
   1.234 +  by (induct xs) auto
   1.235 +qed
   1.236  
   1.237  lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   1.238    by (induct al) (auto simp add: restrict_def)