--- a/src/HOL/Library/AList.thy Wed Jul 13 15:23:33 2016 +0200
+++ b/src/HOL/Library/AList.thy Wed Jul 13 19:02:23 2016 +0200
@@ -73,8 +73,7 @@
@{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.\<close>
lemma update_swap:
- "k \<noteq> k' \<Longrightarrow>
- map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
+ "k \<noteq> k' \<Longrightarrow> 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:
@@ -85,8 +84,8 @@
lemma image_update [simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
by (simp add: update_conv')
-qualified definition updates
- :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition updates ::
+ "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where "updates ks vs = fold (case_prod update) (zip ks vs)"
lemma updates_simps [simp]:
@@ -216,8 +215,8 @@
subsection \<open>\<open>update_with_aux\<close> and \<open>delete_aux\<close>\<close>
-qualified primrec update_with_aux
- :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified primrec update_with_aux ::
+ "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
"update_with_aux v k f [] = [(k, f v)]"
| "update_with_aux v k f (p # ps) =
@@ -257,7 +256,7 @@
lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
apply (induct xs)
- apply simp_all
+ apply simp_all
apply clarsimp
apply (fastforce intro: rev_image_eqI)
done
@@ -291,7 +290,7 @@
lemma map_of_delete_aux':
"distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
apply (induct xs)
- apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
+ apply (fastforce simp add: map_of_eq_None_iff fun_upd_twist)
apply (auto intro!: ext)
apply (simp add: map_of_eq_None_iff)
done
@@ -318,9 +317,9 @@
proof
show "map_of (restrict A al) k = ((map_of al)|` A) k" for k
apply (induct al)
- apply simp
+ apply simp
apply (cases "k \<in> A")
- apply auto
+ apply auto
done
qed