src/HOL/Imperative_HOL/Array.thy
changeset 37709 70fafefbcc98
parent 36176 3fe7e97ccca8
child 37716 24bb91462892
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 10:42:27 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 14:34:28 2010 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    [code del]: "nth a i = (do len \<leftarrow> length a;
     1.5                   (if i < len
     1.6                       then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
     1.7 -                     else raise (''array lookup: index out of range''))
     1.8 +                     else raise ''array lookup: index out of range'')
     1.9                done)"
    1.10  
    1.11  definition
    1.12 @@ -37,18 +37,12 @@
    1.13    [code del]: "upd i x a = (do len \<leftarrow> length a;
    1.14                        (if i < len
    1.15                             then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
    1.16 -                           else raise (''array update: index out of range''))
    1.17 +                           else raise ''array update: index out of range'')
    1.18                     done)" 
    1.19  
    1.20  lemma upd_return:
    1.21    "upd i x a \<guillemotright> return a = upd i x a"
    1.22 -proof (rule Heap_eqI)
    1.23 -  fix h
    1.24 -  obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
    1.25 -    by (cases "Heap_Monad.execute (Array.length a) h")
    1.26 -  then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
    1.27 -    by (auto simp add: upd_def bindM_def split: sum.split)
    1.28 -qed
    1.29 +  by (rule Heap_eqI) (simp add: upd_def bindM_def split: option.split) 
    1.30  
    1.31  
    1.32  subsection {* Derivates *}
    1.33 @@ -99,14 +93,11 @@
    1.34  
    1.35  lemma array_make [code]:
    1.36    "Array.new n x = make n (\<lambda>_. x)"
    1.37 -  by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
    1.38 -    monad_simp array_of_list_replicate [symmetric]
    1.39 -    map_replicate_trivial replicate_append_same
    1.40 -    of_list_def)
    1.41 +  by (rule Heap_eqI) (simp add: make_def new_def array_of_list_replicate map_replicate_trivial of_list_def)
    1.42  
    1.43  lemma array_of_list_make [code]:
    1.44    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
    1.45 -  unfolding make_def map_nth ..
    1.46 +  by (rule Heap_eqI) (simp add: make_def map_nth)
    1.47  
    1.48  
    1.49  subsection {* Code generator setup *}
    1.50 @@ -135,13 +126,11 @@
    1.51    by (simp add: make'_def o_def)
    1.52  
    1.53  definition length' where
    1.54 -  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
    1.55 +  [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
    1.56  hide_const (open) length'
    1.57  lemma [code]:
    1.58 -  "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
    1.59 -  by (simp add: length'_def monad_simp',
    1.60 -    simp add: liftM_def comp_def monad_simp,
    1.61 -    simp add: monad_simp')
    1.62 +  "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
    1.63 +  by (simp add: length'_def)
    1.64  
    1.65  definition nth' where
    1.66    [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
    1.67 @@ -155,7 +144,7 @@
    1.68  hide_const (open) upd'
    1.69  lemma [code]:
    1.70    "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
    1.71 -  by (simp add: upd'_def monad_simp upd_return)
    1.72 +  by (simp add: upd'_def upd_return)
    1.73  
    1.74  
    1.75  subsubsection {* SML *}