Isar proof
authorhaftmann
Sat, 07 Feb 2009 10:03:09 +0100
changeset 29831 5dc920623bb1
parent 29830 edac6cd01310
child 29832 b4919260eaec
Isar proof
src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Sat Feb 07 09:58:24 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Sat Feb 07 10:03:09 2009 +0100
@@ -127,16 +127,9 @@
   "size (tabulate ks f) = length (remdups ks)"
   by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
 
-lemma bulkload_tabulate: (*FIXME Isar proof*)
+lemma bulkload_tabulate:
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
-  unfolding bulkload_def tabulate_def apply simp
-  apply (rule sym)
-  apply (rule ext) apply auto
-  apply (subst map_of_eq_Some_iff)
-  apply (simp add: map_compose [symmetric] comp_def)
-  apply (simp add: image_def)
-  apply (subst map_of_eq_None_iff)
-  apply (simp add: image_def)
-  done
+  by (rule sym)
+    (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
 
 end
\ No newline at end of file