src/HOL/Library/AssocList.thy
changeset 20503 503ac4c5ef91
parent 19333 99dbefd7bc2e
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 11 14:35:30 2006 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Mon Sep 11 21:35:19 2006 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4    by (induct al) auto
     1.5  
     1.6  lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v=v'"
     1.7 -proof (induct al fixing: al') 
     1.8 +proof (induct al arbitrary: al') 
     1.9    case Nil thus ?case 
    1.10      by (cases al') (auto split: split_if_asm)
    1.11  next
    1.12 @@ -364,7 +364,7 @@
    1.13  (* ******************************************************************************** *)
    1.14  
    1.15  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
    1.16 -proof (induct ks fixing: vs al)
    1.17 +proof (induct ks arbitrary: vs al)
    1.18    case Nil
    1.19    thus ?case by simp
    1.20  next
    1.21 @@ -387,11 +387,11 @@
    1.22    assumes "distinct (map fst al)"
    1.23    shows "distinct (map fst (updates ks vs al))"
    1.24    using prems
    1.25 -by (induct ks fixing: vs al) (auto simp add: distinct_update split: list.splits)
    1.26 +by (induct ks arbitrary: vs al) (auto simp add: distinct_update split: list.splits)
    1.27  
    1.28  lemma clearjunk_updates:
    1.29   "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
    1.30 -  by (induct ks fixing: vs al) (auto simp add: clearjunk_update split: list.splits)
    1.31 +  by (induct ks arbitrary: vs al) (auto simp add: clearjunk_update split: list.splits)
    1.32  
    1.33  lemma updates_empty[simp]: "updates vs [] al = al"
    1.34    by (induct vs) auto 
    1.35 @@ -401,12 +401,12 @@
    1.36  
    1.37  lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
    1.38    updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
    1.39 -  by (induct ks fixing: vs al) (auto split: list.splits)
    1.40 +  by (induct ks arbitrary: vs al) (auto split: list.splits)
    1.41  
    1.42  lemma updates_list_update_drop[simp]:
    1.43   "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
    1.44     \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
    1.45 -  by (induct ks fixing: al vs i) (auto split:list.splits nat.splits)
    1.46 +  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
    1.47  
    1.48  lemma update_updates_conv_if: "
    1.49   map_of (updates xs ys (update x y al)) =
    1.50 @@ -425,11 +425,11 @@
    1.51  
    1.52  lemma updates_append_drop[simp]:
    1.53    "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
    1.54 -  by (induct xs fixing: ys al) (auto split: list.splits)
    1.55 +  by (induct xs arbitrary: ys al) (auto split: list.splits)
    1.56  
    1.57  lemma updates_append2_drop[simp]:
    1.58    "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
    1.59 -  by (induct xs fixing: ys al) (auto split: list.splits)
    1.60 +  by (induct xs arbitrary: ys al) (auto split: list.splits)
    1.61  
    1.62  (* ******************************************************************************** *)
    1.63  subsection {* @{const map_ran} *}
    1.64 @@ -455,13 +455,13 @@
    1.65  (* ******************************************************************************** *)
    1.66  
    1.67  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
    1.68 -  by (induct ys fixing: xs) (auto simp add: dom_update)
    1.69 +  by (induct ys arbitrary: xs) (auto simp add: dom_update)
    1.70  
    1.71  lemma distinct_merge:
    1.72    assumes "distinct (map fst xs)"
    1.73    shows "distinct (map fst (merge xs ys))"
    1.74    using prems
    1.75 -by (induct ys fixing: xs) (auto simp add: dom_merge distinct_update)
    1.76 +by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
    1.77  
    1.78  lemma clearjunk_merge:
    1.79   "clearjunk (merge xs ys) = merge (clearjunk xs) ys"