# HG changeset patch
# User wenzelm
# Date 1468429343 -7200
# Node ID ff1d86b077519ae1bd09b7c67c8e1c6fdabd0e76
# Parent  31016a88197bfee856ab3a6844a32d3e6b493f39
tuned;

diff -r 31016a88197b -r ff1d86b07751 src/HOL/Library/AList.thy
--- 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
 
diff -r 31016a88197b -r ff1d86b07751 src/HOL/Library/AList_Mapping.thy
--- 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"
diff -r 31016a88197b -r ff1d86b07751 src/HOL/Library/Mapping.thy
--- 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