# HG changeset patch # User wenzelm # Date 1396207499 -7200 # Node ID 3e62e68fb342cce5d42dc266d3d3741322e375ea # Parent c3d7b3bb2708e17d2a0abd695e2cb97467814830 tuned proofs; diff -r c3d7b3bb2708 -r 3e62e68fb342 src/HOL/Library/AList.thy --- a/src/HOL/Library/AList.thy Sun Mar 30 21:03:40 2014 +0200 +++ b/src/HOL/Library/AList.thy Sun Mar 30 21:24:59 2014 +0200 @@ -9,17 +9,18 @@ begin text {* - The operations preserve distinctness of keys and - function @{term "clearjunk"} distributes over them. Since + The operations preserve distinctness of keys and + function @{term "clearjunk"} distributes over them. Since @{term clearjunk} enforces distinctness of keys it can be used to establish the invariant, e.g. for inductive proofs. *} subsection {* @{text update} and @{text updates} *} -primrec update :: "'key \ 'val \ ('key \ 'val) list \ ('key \ 'val) list" where - "update k v [] = [(k, v)]" - | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)" +primrec update :: "'key \ 'val \ ('key \ 'val) list \ ('key \ 'val) list" +where + "update k v [] = [(k, v)]" +| "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)" lemma update_conv': "map_of (update k v al) = (map_of al)(k\v)" by (induct al) (auto simp add: fun_eq_iff) @@ -36,12 +37,12 @@ by (induct al) simp_all lemma distinct_update: - assumes "distinct (map fst al)" + assumes "distinct (map fst al)" shows "distinct (map fst (update k v al))" using assms by (simp add: update_keys) -lemma update_filter: - "a\k \ update k v [q\ps . fst q \ a] = [q\update k v ps . fst q \ a]" +lemma update_filter: + "a \ k \ update k v [q\ps. fst q \ a] = [q\update k v ps. fst q \ a]" by (induct ps) auto lemma update_triv: "map_of al k = Some v \ update k v al = al" @@ -51,11 +52,13 @@ by (induct al) auto lemma update_eqD: "update k v al = update k v' al' \ v = v'" -proof (induct al arbitrary: al') - case Nil thus ?case +proof (induct al arbitrary: al') + case Nil + then show ?case by (cases al') (auto split: split_if_asm) next - case Cons thus ?case + case Cons + then show ?case by (cases al') (auto split: split_if_asm) qed @@ -63,13 +66,15 @@ by (induct al) auto text {* Note that the lists are not necessarily the same: - @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and + @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*} -lemma update_swap: "k\k' - \ map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))" + +lemma update_swap: + "k \ k' \ + map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))" by (simp add: update_conv' fun_eq_iff) -lemma update_Some_unfold: +lemma update_Some_unfold: "map_of (update k v al) x = Some y \ x = k \ v = y \ x \ k \ map_of al x = Some y" by (simp add: update_conv' map_upd_Some_unfold) @@ -78,8 +83,8 @@ "x \ A \ map_of (update x y al) ` A = map_of al ` A" by (simp add: update_conv') -definition updates :: "'key list \ 'val list \ ('key \ 'val) list \ ('key \ 'val) list" where - "updates ks vs = fold (case_prod update) (zip ks vs)" +definition updates :: "'key list \ 'val list \ ('key \ 'val) list \ ('key \ 'val) list" + where "updates ks vs = fold (case_prod update) (zip ks vs)" lemma updates_simps [simp]: "updates [] vs ps = ps" @@ -95,9 +100,10 @@ lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\]vs)" proof - have "map_of \ fold (case_prod update) (zip ks vs) = - fold (\(k, v) f. f(k \ v)) (zip ks vs) \ map_of" + fold (\(k, v) f. f(k \ v)) (zip ks vs) \ map_of" by (rule fold_commute) (auto simp add: fun_eq_iff update_conv') - then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def) + then show ?thesis + by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def) qed lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\]vs)) k" @@ -112,52 +118,55 @@ (zip ks vs) (map fst al))" by (rule fold_invariant [of "zip ks vs" "\_. True"]) (auto intro: assms) moreover have "map fst \ fold (case_prod update) (zip ks vs) = - fold (\(k, v) al. if k \ set al then al else al @ [k]) (zip ks vs) \ map fst" + fold (\(k, v) al. if k \ set al then al else al @ [k]) (zip ks vs) \ map fst" by (rule fold_commute) (simp add: update_keys split_def case_prod_beta comp_def) - ultimately show ?thesis by (simp add: updates_def fun_eq_iff) + ultimately show ?thesis + by (simp add: updates_def fun_eq_iff) qed lemma updates_append1[simp]: "size ks < size vs \ - updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)" + updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)" by (induct ks arbitrary: vs al) (auto split: list.splits) lemma updates_list_update_drop[simp]: - "\size ks \ i; i < size vs\ - \ updates ks (vs[i:=v]) al = updates ks vs al" - by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits) + "size ks \ i \ i < size vs \ + updates ks (vs[i:=v]) al = updates ks vs al" + by (induct ks arbitrary: al vs i) (auto split: list.splits nat.splits) -lemma update_updates_conv_if: " - map_of (updates xs ys (update x y al)) = - map_of (if x \ set(take (length ys) xs) then updates xs ys al - else (update x y (updates xs ys al)))" +lemma update_updates_conv_if: + "map_of (updates xs ys (update x y al)) = + map_of + (if x \ set (take (length ys) xs) + then updates xs ys al + else (update x y (updates xs ys al)))" by (simp add: updates_conv' update_conv' map_upd_upds_conv_if) lemma updates_twist [simp]: - "k \ set ks \ - map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))" + "k \ set ks \ + map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))" by (simp add: updates_conv' update_conv') -lemma updates_apply_notin[simp]: - "k \ set ks ==> map_of (updates ks vs al) k = map_of al k" +lemma updates_apply_notin [simp]: + "k \ set ks \ map_of (updates ks vs al) k = map_of al k" by (simp add: updates_conv) -lemma updates_append_drop[simp]: - "size xs = size ys \ updates (xs@zs) ys al = updates xs ys al" +lemma updates_append_drop [simp]: + "size xs = size ys \ updates (xs @ zs) ys al = updates xs ys al" by (induct xs arbitrary: ys al) (auto split: list.splits) -lemma updates_append2_drop[simp]: - "size xs = size ys \ updates xs (ys@zs) al = updates xs ys al" +lemma updates_append2_drop [simp]: + "size xs = size ys \ updates xs (ys @ zs) al = updates xs ys al" by (induct xs arbitrary: ys al) (auto split: list.splits) subsection {* @{text delete} *} -definition delete :: "'key \ ('key \ 'val) list \ ('key \ 'val) list" where - delete_eq: "delete k = filter (\(k', _). k \ k')" +definition delete :: "'key \ ('key \ 'val) list \ ('key \ 'val) list" + where delete_eq: "delete k = filter (\(k', _). k \ k')" lemma delete_simps [simp]: "delete k [] = []" - "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)" + "delete k (p # ps) = (if fst p = k then delete k ps else p # delete k ps)" by (auto simp add: delete_eq) lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)" @@ -166,12 +175,11 @@ corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'" by (simp add: delete_conv') -lemma delete_keys: - "map fst (delete k al) = removeAll k (map fst al)" +lemma delete_keys: "map fst (delete k al) = removeAll k (map fst al)" by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def) lemma distinct_delete: - assumes "distinct (map fst al)" + assumes "distinct (map fst al)" shows "distinct (map fst (delete k al))" using assms by (simp add: delete_keys distinct_removeAll) @@ -181,8 +189,7 @@ lemma delete_idem: "delete k (delete k al) = delete k al" by (simp add: delete_eq) -lemma map_of_delete [simp]: - "k' \ k \ map_of (delete k al) k' = map_of al k'" +lemma map_of_delete [simp]: "k' \ k \ map_of (delete k al) k' = map_of al k'" by (simp add: delete_conv') lemma delete_notin_dom: "k \ fst ` set (delete k al)" @@ -191,12 +198,10 @@ lemma dom_delete_subset: "fst ` set (delete k al) \ fst ` set al" by (auto simp add: delete_eq) -lemma delete_update_same: - "delete k (update k v al) = delete k al" +lemma delete_update_same: "delete k (update k v al) = delete k al" by (induct al) simp_all -lemma delete_update: - "k \ l \ delete l (update k v al) = update k v (delete l al)" +lemma delete_update: "k \ l \ delete l (update k v al) = update k v (delete l al)" by (induct al) simp_all lemma delete_twist: "delete x (delete y al) = delete y (delete x al)" @@ -208,8 +213,8 @@ subsection {* @{text restrict} *} -definition restrict :: "'key set \ ('key \ 'val) list \ ('key \ 'val) list" where - restrict_eq: "restrict A = filter (\(k, v). k \ A)" +definition restrict :: "'key set \ ('key \ 'val) list \ ('key \ 'val) list" + where restrict_eq: "restrict A = filter (\(k, v). k \ A)" lemma restr_simps [simp]: "restrict A [] = []" @@ -230,8 +235,8 @@ "distinct (map fst al) \ distinct (map fst (restrict A al))" by (induct al) (auto simp add: restrict_eq) -lemma restr_empty [simp]: - "restrict {} al = []" +lemma restr_empty [simp]: + "restrict {} al = []" "restrict A [] = []" by (induct al) (auto simp add: restrict_eq) @@ -251,38 +256,39 @@ by (induct al) (auto simp add: restrict_eq) lemma restr_update[simp]: - "map_of (restrict D (update x y al)) = + "map_of (restrict D (update x y al)) = map_of ((if x \ D then (update x y (restrict (D-{x}) al)) else restrict D al))" by (simp add: restr_conv' update_conv') lemma restr_delete [simp]: - "(delete x (restrict D al)) = - (if x \ D then restrict (D - {x}) al else restrict D al)" -apply (simp add: delete_eq restrict_eq) -apply (auto simp add: split_def) + "delete x (restrict D al) = (if x \ D then restrict (D - {x}) al else restrict D al)" + apply (simp add: delete_eq restrict_eq) + apply (auto simp add: split_def) proof - - have "\y. y \ x \ x \ y" by auto + have "\y. y \ x \ x \ y" + by auto then show "[p \ al. fst p \ D \ x \ fst p] = [p \ al. fst p \ D \ fst p \ x]" by simp assume "x \ D" - then have "\y. y \ D \ y \ D \ x \ y" by auto + then have "\y. y \ D \ y \ D \ x \ y" + by auto then show "[p \ al . fst p \ D \ x \ fst p] = [p \ al . fst p \ D]" by simp qed lemma update_restr: - "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))" + "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))" by (simp add: update_conv' restr_conv') (rule fun_upd_restrict) lemma update_restr_conv [simp]: - "x \ D \ - map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))" + "x \ D \ + map_of (update x y (restrict D al)) = map_of (update x y (restrict (D - {x}) al))" by (simp add: update_conv' restr_conv') -lemma restr_updates [simp]: " - \ length xs = length ys; set xs \ D \ - \ map_of (restrict D (updates xs ys al)) = - map_of (updates xs ys (restrict (D - set xs) al))" +lemma restr_updates [simp]: + "length xs = length ys \ set xs \ D \ + map_of (restrict D (updates xs ys al)) = + map_of (updates xs ys (restrict (D - set xs) al))" by (simp add: updates_conv' restr_conv') lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)" @@ -291,38 +297,30 @@ subsection {* @{text clearjunk} *} -function clearjunk :: "('key \ 'val) list \ ('key \ 'val) list" where - "clearjunk [] = []" - | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)" +function clearjunk :: "('key \ 'val) list \ ('key \ 'val) list" +where + "clearjunk [] = []" +| "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)" by pat_completeness auto -termination by (relation "measure length") - (simp_all add: less_Suc_eq_le length_delete_le) +termination + by (relation "measure length") (simp_all add: less_Suc_eq_le length_delete_le) -lemma map_of_clearjunk: - "map_of (clearjunk al) = map_of al" - by (induct al rule: clearjunk.induct) - (simp_all add: fun_eq_iff) +lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al" + by (induct al rule: clearjunk.induct) (simp_all add: fun_eq_iff) -lemma clearjunk_keys_set: - "set (map fst (clearjunk al)) = set (map fst al)" - by (induct al rule: clearjunk.induct) - (simp_all add: delete_keys) +lemma clearjunk_keys_set: "set (map fst (clearjunk al)) = set (map fst al)" + by (induct al rule: clearjunk.induct) (simp_all add: delete_keys) -lemma dom_clearjunk: - "fst ` set (clearjunk al) = fst ` set al" +lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al" using clearjunk_keys_set by simp -lemma distinct_clearjunk [simp]: - "distinct (map fst (clearjunk al))" - by (induct al rule: clearjunk.induct) - (simp_all del: set_map add: clearjunk_keys_set delete_keys) +lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))" + by (induct al rule: clearjunk.induct) (simp_all del: set_map add: clearjunk_keys_set delete_keys) -lemma ran_clearjunk: - "ran (map_of (clearjunk al)) = ran (map_of al)" +lemma ran_clearjunk: "ran (map_of (clearjunk al)) = ran (map_of al)" by (simp add: map_of_clearjunk) -lemma ran_map_of: - "ran (map_of al) = snd ` set (clearjunk al)" +lemma ran_map_of: "ran (map_of al) = snd ` set (clearjunk al)" proof - have "ran (map_of al) = ran (map_of (clearjunk al))" by (simp add: ran_clearjunk) @@ -331,45 +329,42 @@ finally show ?thesis . qed -lemma clearjunk_update: - "clearjunk (update k v al) = update k v (clearjunk al)" - by (induct al rule: clearjunk.induct) - (simp_all add: delete_update) +lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)" + by (induct al rule: clearjunk.induct) (simp_all add: delete_update) -lemma clearjunk_updates: - "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)" +lemma clearjunk_updates: "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)" proof - have "clearjunk \ fold (case_prod update) (zip ks vs) = fold (case_prod update) (zip ks vs) \ clearjunk" by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def) - then show ?thesis by (simp add: updates_def fun_eq_iff) + then show ?thesis + by (simp add: updates_def fun_eq_iff) qed -lemma clearjunk_delete: - "clearjunk (delete x al) = delete x (clearjunk al)" +lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)" by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist) -lemma clearjunk_restrict: - "clearjunk (restrict A al) = restrict A (clearjunk al)" +lemma clearjunk_restrict: "clearjunk (restrict A al) = restrict A (clearjunk al)" by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist) -lemma distinct_clearjunk_id [simp]: - "distinct (map fst al) \ clearjunk al = al" +lemma distinct_clearjunk_id [simp]: "distinct (map fst al) \ clearjunk al = al" by (induct al rule: clearjunk.induct) auto -lemma clearjunk_idem: - "clearjunk (clearjunk al) = clearjunk al" +lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al" by simp -lemma length_clearjunk: - "length (clearjunk al) \ length al" +lemma length_clearjunk: "length (clearjunk al) \ length al" proof (induct al rule: clearjunk.induct [case_names Nil Cons]) - case Nil then show ?case by simp + case Nil + then show ?case by simp next case (Cons kv al) - moreover have "length (delete (fst kv) al) \ length al" by (fact length_delete_le) - ultimately have "length (clearjunk (delete (fst kv) al)) \ length al" by (rule order_trans) - then show ?case by simp + moreover have "length (delete (fst kv) al) \ length al" + by (fact length_delete_le) + ultimately have "length (clearjunk (delete (fst kv) al)) \ length al" + by (rule order_trans) + then show ?case + by simp qed lemma delete_map: @@ -386,47 +381,41 @@ subsection {* @{text map_ran} *} -definition map_ran :: "('key \ 'val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" where - "map_ran f = map (\(k, v). (k, f k v))" +definition map_ran :: "('key \ 'val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" + where "map_ran f = map (\(k, v). (k, f k v))" lemma map_ran_simps [simp]: "map_ran f [] = []" "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps" by (simp_all add: map_ran_def) -lemma dom_map_ran: - "fst ` set (map_ran f al) = fst ` set al" +lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al" by (simp add: map_ran_def image_image split_def) - -lemma map_ran_conv: - "map_of (map_ran f al) k = map_option (f k) (map_of al k)" + +lemma map_ran_conv: "map_of (map_ran f al) k = map_option (f k) (map_of al k)" by (induct al) auto -lemma distinct_map_ran: - "distinct (map fst al) \ distinct (map fst (map_ran f al))" +lemma distinct_map_ran: "distinct (map fst al) \ distinct (map fst (map_ran f al))" by (simp add: map_ran_def split_def comp_def) -lemma map_ran_filter: - "map_ran f [p\ps. fst p \ a] = [p\map_ran f ps. fst p \ a]" +lemma map_ran_filter: "map_ran f [p\ps. fst p \ a] = [p\map_ran f ps. fst p \ a]" by (simp add: map_ran_def filter_map split_def comp_def) -lemma clearjunk_map_ran: - "clearjunk (map_ran f al) = map_ran f (clearjunk al)" +lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)" by (simp add: map_ran_def split_def clearjunk_map) subsection {* @{text merge} *} -definition merge :: "('key \ 'val) list \ ('key \ 'val) list \ ('key \ 'val) list" where - "merge qs ps = foldr (\(k, v). update k v) ps qs" +definition merge :: "('key \ 'val) list \ ('key \ 'val) list \ ('key \ 'val) list" + where "merge qs ps = foldr (\(k, v). update k v) ps qs" lemma merge_simps [simp]: "merge qs [] = qs" "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)" by (simp_all add: merge_def split_def) -lemma merge_updates: - "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs" +lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs" by (simp add: merge_def updates_def foldr_conv_fold zip_rev zip_map_fst_snd) lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \ fst ` set ys" @@ -435,86 +424,84 @@ lemma distinct_merge: assumes "distinct (map fst xs)" shows "distinct (map fst (merge xs ys))" -using assms by (simp add: merge_updates distinct_updates) + using assms by (simp add: merge_updates distinct_updates) -lemma clearjunk_merge: - "clearjunk (merge xs ys) = merge (clearjunk xs) ys" +lemma clearjunk_merge: "clearjunk (merge xs ys) = merge (clearjunk xs) ys" by (simp add: merge_updates clearjunk_updates) -lemma merge_conv': - "map_of (merge xs ys) = map_of xs ++ map_of ys" +lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys" proof - have "map_of \ fold (case_prod update) (rev ys) = - fold (\(k, v) m. m(k \ v)) (rev ys) \ map_of" + fold (\(k, v) m. m(k \ v)) (rev ys) \ map_of" by (rule fold_commute) (simp add: update_conv' case_prod_beta split_def fun_eq_iff) then show ?thesis by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff) qed -corollary merge_conv: - "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k" +corollary merge_conv: "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k" by (simp add: merge_conv') lemma merge_empty: "map_of (merge [] ys) = map_of ys" by (simp add: merge_conv') -lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = - map_of (merge (merge m1 m2) m3)" +lemma merge_assoc [simp]: "map_of (merge m1 (merge m2 m3)) = map_of (merge (merge m1 m2) m3)" by (simp add: merge_conv') -lemma merge_Some_iff: - "(map_of (merge m n) k = Some x) = - (map_of n k = Some x \ map_of n k = None \ map_of m k = Some x)" +lemma merge_Some_iff: + "map_of (merge m n) k = Some x \ + map_of n k = Some x \ map_of n k = None \ map_of m k = Some x" by (simp add: merge_conv' map_add_Some_iff) lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1] -lemma merge_find_right[simp]: "map_of n k = Some v \ map_of (merge m n) k = Some v" +lemma merge_find_right [simp]: "map_of n k = Some v \ map_of (merge m n) k = Some v" by (simp add: merge_conv') -lemma merge_None [iff]: +lemma merge_None [iff]: "(map_of (merge m n) k = None) = (map_of n k = None \ map_of m k = None)" by (simp add: merge_conv') -lemma merge_upd[simp]: +lemma merge_upd [simp]: "map_of (merge m (update k v n)) = map_of (update k v (merge m n))" by (simp add: update_conv' merge_conv') -lemma merge_updatess[simp]: +lemma merge_updatess [simp]: "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))" by (simp add: updates_conv' merge_conv') -lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)" +lemma merge_append: "map_of (xs @ ys) = map_of (merge ys xs)" by (simp add: merge_conv') subsection {* @{text compose} *} -function compose :: "('key \ 'a) list \ ('a \ 'b) list \ ('key \ 'b) list" where - "compose [] ys = []" - | "compose (x#xs) ys = (case map_of ys (snd x) - of None \ compose (delete (fst x) xs) ys - | Some v \ (fst x, v) # compose xs ys)" +function compose :: "('key \ 'a) list \ ('a \ 'b) list \ ('key \ 'b) list" +where + "compose [] ys = []" +| "compose (x # xs) ys = + (case map_of ys (snd x) of + None \ compose (delete (fst x) xs) ys + | Some v \ (fst x, v) # compose xs ys)" by pat_completeness auto -termination by (relation "measure (length \ fst)") - (simp_all add: less_Suc_eq_le length_delete_le) +termination + by (relation "measure (length \ fst)") (simp_all add: less_Suc_eq_le length_delete_le) -lemma compose_first_None [simp]: - assumes "map_of xs k = None" +lemma compose_first_None [simp]: + assumes "map_of xs k = None" shows "map_of (compose xs ys) k = None" -using assms by (induct xs ys rule: compose.induct) - (auto split: option.splits split_if_asm) + using assms by (induct xs ys rule: compose.induct) (auto split: option.splits split_if_asm) -lemma compose_conv: - shows "map_of (compose xs ys) k = (map_of ys \\<^sub>m map_of xs) k" +lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \\<^sub>m map_of xs) k" proof (induct xs ys rule: compose.induct) - case 1 then show ?case by simp + case 1 + then show ?case by simp next - case (2 x xs ys) show ?case + case (2 x xs ys) + show ?case proof (cases "map_of ys (snd x)") - case None with 2 - have hyp: "map_of (compose (delete (fst x) xs) ys) k = - (map_of ys \\<^sub>m map_of (delete (fst x) xs)) k" + case None + with 2 have hyp: "map_of (compose (delete (fst x) xs) ys) k = + (map_of ys \\<^sub>m map_of (delete (fst x) xs)) k" by simp show ?thesis proof (cases "fst x = k") @@ -530,8 +517,7 @@ from False have "map_of (delete (fst x) xs) k = map_of xs k" by simp with hyp show ?thesis - using False None - by (simp add: map_comp_def) + using False None by (simp add: map_comp_def) qed next case (Some v) @@ -542,19 +528,19 @@ by (auto simp add: map_comp_def) qed qed - -lemma compose_conv': - shows "map_of (compose xs ys) = (map_of ys \\<^sub>m map_of xs)" + +lemma compose_conv': "map_of (compose xs ys) = (map_of ys \\<^sub>m map_of xs)" by (rule ext) (rule compose_conv) lemma compose_first_Some [simp]: - assumes "map_of xs k = Some v" + assumes "map_of xs k = Some v" shows "map_of (compose xs ys) k = map_of ys v" -using assms by (simp add: compose_conv) + using assms by (simp add: compose_conv) lemma dom_compose: "fst ` set (compose xs ys) \ fst ` set xs" proof (induct xs ys rule: compose.induct) - case 1 thus ?case by simp + case 1 + then show ?case by simp next case (2 x xs ys) show ?case @@ -580,11 +566,12 @@ qed lemma distinct_compose: - assumes "distinct (map fst xs)" - shows "distinct (map fst (compose xs ys))" -using assms + assumes "distinct (map fst xs)" + shows "distinct (map fst (compose xs ys))" + using assms proof (induct xs ys rule: compose.induct) - case 1 thus ?case by simp + case 1 + then show ?case by simp next case (2 x xs ys) show ?case @@ -593,105 +580,106 @@ with 2 show ?thesis by simp next case (Some v) - with 2 dom_compose [of xs ys] show ?thesis - by (auto) + with 2 dom_compose [of xs ys] show ?thesis + by auto qed qed -lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)" +lemma compose_delete_twist: "compose (delete k xs) ys = delete k (compose xs ys)" proof (induct xs ys rule: compose.induct) - case 1 thus ?case by simp + case 1 + then show ?case by simp next case (2 x xs ys) show ?case proof (cases "map_of ys (snd x)") case None - with 2 have - hyp: "compose (delete k (delete (fst x) xs)) ys = - delete k (compose (delete (fst x) xs) ys)" + with 2 have hyp: "compose (delete k (delete (fst x) xs)) ys = + delete k (compose (delete (fst x) xs) ys)" by simp show ?thesis proof (cases "fst x = k") case True - with None hyp - show ?thesis + with None hyp show ?thesis by (simp add: delete_idem) next case False - from None False hyp - show ?thesis + from None False hyp show ?thesis by (simp add: delete_twist) qed next case (Some v) - with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp + with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" + by simp with Some show ?thesis by simp qed qed lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys" - by (induct xs ys rule: compose.induct) - (auto simp add: map_of_clearjunk split: option.splits) - + by (induct xs ys rule: compose.induct) + (auto simp add: map_of_clearjunk split: option.splits) + lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys" by (induct xs rule: clearjunk.induct) - (auto split: option.splits simp add: clearjunk_delete delete_idem - compose_delete_twist) - -lemma compose_empty [simp]: - "compose xs [] = []" + (auto split: option.splits simp add: clearjunk_delete delete_idem compose_delete_twist) + +lemma compose_empty [simp]: "compose xs [] = []" by (induct xs) (auto simp add: compose_delete_twist) lemma compose_Some_iff: - "(map_of (compose xs ys) k = Some v) = - (\k'. map_of xs k = Some k' \ map_of ys k' = Some v)" + "(map_of (compose xs ys) k = Some v) \ + (\k'. map_of xs k = Some k' \ map_of ys k' = Some v)" by (simp add: compose_conv map_comp_Some_iff) lemma map_comp_None_iff: - "(map_of (compose xs ys) k = None) = - (map_of xs k = None \ (\k'. map_of xs k = Some k' \ map_of ys k' = None)) " + "map_of (compose xs ys) k = None \ + (map_of xs k = None \ (\k'. map_of xs k = Some k' \ map_of ys k' = None))" by (simp add: compose_conv map_comp_None_iff) + subsection {* @{text map_entry} *} fun map_entry :: "'key \ ('val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" where "map_entry k f [] = []" -| "map_entry k f (p # ps) = (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)" +| "map_entry k f (p # ps) = + (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)" lemma map_of_map_entry: - "map_of (map_entry k f xs) = (map_of xs)(k := case map_of xs k of None => None | Some v' => Some (f v'))" -by (induct xs) auto + "map_of (map_entry k f xs) = + (map_of xs)(k := case map_of xs k of None \ None | Some v' \ Some (f v'))" + by (induct xs) auto -lemma dom_map_entry: - "fst ` set (map_entry k f xs) = fst ` set xs" -by (induct xs) auto +lemma dom_map_entry: "fst ` set (map_entry k f xs) = fst ` set xs" + by (induct xs) auto lemma distinct_map_entry: assumes "distinct (map fst xs)" shows "distinct (map fst (map_entry k f xs))" -using assms by (induct xs) (auto simp add: dom_map_entry) + using assms by (induct xs) (auto simp add: dom_map_entry) + subsection {* @{text map_default} *} fun map_default :: "'key \ 'val \ ('val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" where "map_default k v f [] = [(k, v)]" -| "map_default k v f (p # ps) = (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)" +| "map_default k v f (p # ps) = + (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)" lemma map_of_map_default: - "map_of (map_default k v f xs) = (map_of xs)(k := case map_of xs k of None => Some v | Some v' => Some (f v'))" -by (induct xs) auto + "map_of (map_default k v f xs) = + (map_of xs)(k := case map_of xs k of None \ Some v | Some v' \ Some (f v'))" + by (induct xs) auto -lemma dom_map_default: - "fst ` set (map_default k v f xs) = insert k (fst ` set xs)" -by (induct xs) auto +lemma dom_map_default: "fst ` set (map_default k v f xs) = insert k (fst ` set xs)" + by (induct xs) auto lemma distinct_map_default: assumes "distinct (map fst xs)" shows "distinct (map fst (map_default k v f xs))" -using assms by (induct xs) (auto simp add: dom_map_default) + using assms by (induct xs) (auto simp add: dom_map_default) hide_const (open) update updates delete restrict clearjunk merge compose map_entry