src/HOL/Imperative_HOL/Array.thy

--- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 10:42:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 14:34:28 2010 +0200
@@ -28,7 +28,7 @@
   [code del]: "nth a i = (do len \<leftarrow> length a;
                  (if i < len
                      then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
-                     else raise (''array lookup: index out of range''))
+                     else raise ''array lookup: index out of range'')
               done)"
 
 definition
@@ -37,18 +37,12 @@
   [code del]: "upd i x a = (do len \<leftarrow> length a;
                       (if i < len
                            then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
-                           else raise (''array update: index out of range''))
+                           else raise ''array update: index out of range'')
                    done)" 
 
 lemma upd_return:
   "upd i x a \<guillemotright> return a = upd i x a"
-proof (rule Heap_eqI)
-  fix h
-  obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
-    by (cases "Heap_Monad.execute (Array.length a) h")
-  then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
-    by (auto simp add: upd_def bindM_def split: sum.split)
-qed
+  by (rule Heap_eqI) (simp add: upd_def bindM_def split: option.split) 
 
 
 subsection {* Derivates *}
@@ -99,14 +93,11 @@
 
 lemma array_make [code]:
   "Array.new n x = make n (\<lambda>_. x)"
-  by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
-    monad_simp array_of_list_replicate [symmetric]
-    map_replicate_trivial replicate_append_same
-    of_list_def)
+  by (rule Heap_eqI) (simp add: make_def new_def array_of_list_replicate map_replicate_trivial of_list_def)
 
 lemma array_of_list_make [code]:
   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
-  unfolding make_def map_nth ..
+  by (rule Heap_eqI) (simp add: make_def map_nth)
 
 
 subsection {* Code generator setup *}
@@ -135,13 +126,11 @@
   by (simp add: make'_def o_def)
 
 definition length' where
-  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
+  [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
 hide_const (open) length'
 lemma [code]:
-  "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
-  by (simp add: length'_def monad_simp',
-    simp add: liftM_def comp_def monad_simp,
-    simp add: monad_simp')
+  "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
+  by (simp add: length'_def)
 
 definition nth' where
   [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
@@ -155,7 +144,7 @@
 hide_const (open) upd'
 lemma [code]:
   "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
-  by (simp add: upd'_def monad_simp upd_return)
+  by (simp add: upd'_def upd_return)
 
 
 subsubsection {* SML *}