--- 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
--- a/src/HOL/Library/AList_Mapping.thy Wed Jul 13 15:23:33 2016 +0200
+++ b/src/HOL/Library/AList_Mapping.thy Wed Jul 13 19:02:23 2016 +0200
@@ -51,8 +51,11 @@
proof -
have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs
by (auto simp add: image_def intro!: bexI)
- show ?thesis apply transfer
- by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: *)
+ show ?thesis
+ apply transfer
+ apply (auto intro!: map_of_eqI)
+ apply (auto dest!: map_of_eq_dom intro: *)
+ done
qed
lemma map_values_Mapping [code]:
@@ -72,8 +75,8 @@
apply (rule sym)
subgoal for f xs ys x
apply (cases "map_of xs x"; cases "map_of ys x"; simp)
- apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
- dest: map_of_SomeD split: option.splits)+
+ apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
+ dest: map_of_SomeD split: option.splits)+
done
done
@@ -86,8 +89,8 @@
apply (rule sym)
subgoal for f xs ys x
apply (cases "map_of xs x"; cases "map_of ys x"; simp)
- apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
- dest: map_of_SomeD split: option.splits)+
+ apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
+ dest: map_of_SomeD split: option.splits)+
done
done
@@ -106,7 +109,7 @@
apply transfer
apply (rule ext)
apply (subst map_of_filter_distinct)
- apply (simp_all add: map_of_clearjunk split: option.split)
+ apply (simp_all add: map_of_clearjunk split: option.split)
done
lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
--- a/src/HOL/Library/Mapping.thy Wed Jul 13 15:23:33 2016 +0200
+++ b/src/HOL/Library/Mapping.thy Wed Jul 13 19:02:23 2016 +0200
@@ -74,11 +74,11 @@
(\<lambda>k. if k < length xs then Some (xs ! k) else None)
(\<lambda>k. if k < length ys then Some (ys ! k) else None)"
apply induct
- apply auto
+ apply auto
unfolding rel_fun_def
apply clarsimp
apply (case_tac xa)
- apply (auto dest: list_all2_lengthD list_all2_nthD)
+ apply (auto dest: list_all2_lengthD list_all2_nthD)
done
qed