src/HOL/Imperative_HOL/Array.thy
changeset 37758 bf86a65403a8
parent 37756 59caa6180fff
child 37771 1bec64044b5e
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 10:08:10 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 16:58:44 2010 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
     1.5  
     1.6  definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
     1.7 -  [code del]: "len a = Heap_Monad.heap (\<lambda>h. (length a h, h))"
     1.8 +  [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
     1.9  
    1.10  definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
    1.11    [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.12 @@ -75,7 +75,7 @@
    1.13      (\<lambda>h. (get_array a h ! i, change a i x h))"
    1.14  
    1.15  definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
    1.16 -  [code del]: "freeze a = Heap_Monad.heap (\<lambda>h. (get_array a h, h))"
    1.17 +  [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
    1.18  
    1.19  
    1.20  subsection {* Properties *}
    1.21 @@ -83,6 +83,8 @@
    1.22  text {* FIXME: Does there exist a "canonical" array axiomatisation in
    1.23  the literature?  *}
    1.24  
    1.25 +text {* Primitives *}
    1.26 +
    1.27  lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
    1.28    and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
    1.29    unfolding noteq_arrs_def by auto
    1.30 @@ -153,50 +155,89 @@
    1.31    "array_present a (change b i v h) = array_present a h"
    1.32    by (simp add: change_def array_present_def set_array_def get_array_def)
    1.33  
    1.34 -lemma execute_new [simp]:
    1.35 -  "Heap_Monad.execute (new n x) h = Some (array (replicate n x) h)"
    1.36 +
    1.37 +text {* Monad operations *}
    1.38 +
    1.39 +lemma execute_new [simp, execute_simps]:
    1.40 +  "execute (new n x) h = Some (array (replicate n x) h)"
    1.41 +  by (simp add: new_def)
    1.42 +
    1.43 +lemma success_newI [iff, success_intros]:
    1.44 +  "success (new n x) h"
    1.45    by (simp add: new_def)
    1.46  
    1.47 -lemma execute_of_list [simp]:
    1.48 -  "Heap_Monad.execute (of_list xs) h = Some (array xs h)"
    1.49 +lemma execute_of_list [simp, execute_simps]:
    1.50 +  "execute (of_list xs) h = Some (array xs h)"
    1.51 +  by (simp add: of_list_def)
    1.52 +
    1.53 +lemma success_of_listI [iff, success_intros]:
    1.54 +  "success (of_list xs) h"
    1.55    by (simp add: of_list_def)
    1.56  
    1.57 -lemma execute_make [simp]:
    1.58 -  "Heap_Monad.execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.59 +lemma execute_make [simp, execute_simps]:
    1.60 +  "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.61    by (simp add: make_def)
    1.62  
    1.63 -lemma execute_len [simp]:
    1.64 -  "Heap_Monad.execute (len a) h = Some (length a h, h)"
    1.65 +lemma success_makeI [iff, success_intros]:
    1.66 +  "success (make n f) h"
    1.67 +  by (simp add: make_def)
    1.68 +
    1.69 +lemma execute_len [simp, execute_simps]:
    1.70 +  "execute (len a) h = Some (length a h, h)"
    1.71 +  by (simp add: len_def)
    1.72 +
    1.73 +lemma success_lenI [iff, success_intros]:
    1.74 +  "success (len a) h"
    1.75    by (simp add: len_def)
    1.76  
    1.77 -lemma execute_nth [simp]:
    1.78 +lemma execute_nth [execute_simps]:
    1.79    "i < length a h \<Longrightarrow>
    1.80 -    Heap_Monad.execute (nth a i) h = Some (get_array a h ! i, h)"
    1.81 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
    1.82 -  by (simp_all add: nth_def)
    1.83 +    execute (nth a i) h = Some (get_array a h ! i, h)"
    1.84 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
    1.85 +  by (simp_all add: nth_def execute_simps)
    1.86 +
    1.87 +lemma success_nthI [success_intros]:
    1.88 +  "i < length a h \<Longrightarrow> success (nth a i) h"
    1.89 +  by (auto intro: success_intros simp add: nth_def)
    1.90  
    1.91 -lemma execute_upd [simp]:
    1.92 +lemma execute_upd [execute_simps]:
    1.93    "i < length a h \<Longrightarrow>
    1.94 -    Heap_Monad.execute (upd i x a) h = Some (a, change a i x h)"
    1.95 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
    1.96 -  by (simp_all add: upd_def)
    1.97 +    execute (upd i x a) h = Some (a, change a i x h)"
    1.98 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
    1.99 +  by (simp_all add: upd_def execute_simps)
   1.100  
   1.101 -lemma execute_map_entry [simp]:
   1.102 +lemma success_updI [success_intros]:
   1.103 +  "i < length a h \<Longrightarrow> success (upd i x a) h"
   1.104 +  by (auto intro: success_intros simp add: upd_def)
   1.105 +
   1.106 +lemma execute_map_entry [execute_simps]:
   1.107    "i < length a h \<Longrightarrow>
   1.108 -   Heap_Monad.execute (map_entry i f a) h =
   1.109 +   execute (map_entry i f a) h =
   1.110        Some (a, change a i (f (get_array a h ! i)) h)"
   1.111 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
   1.112 -  by (simp_all add: map_entry_def)
   1.113 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.114 +  by (simp_all add: map_entry_def execute_simps)
   1.115  
   1.116 -lemma execute_swap [simp]:
   1.117 +lemma success_map_entryI [success_intros]:
   1.118 +  "i < length a h \<Longrightarrow> success (map_entry i f a) h"
   1.119 +  by (auto intro: success_intros simp add: map_entry_def)
   1.120 +
   1.121 +lemma execute_swap [execute_simps]:
   1.122    "i < length a h \<Longrightarrow>
   1.123 -   Heap_Monad.execute (swap i x a) h =
   1.124 +   execute (swap i x a) h =
   1.125        Some (get_array a h ! i, change a i x h)"
   1.126 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
   1.127 -  by (simp_all add: swap_def)
   1.128 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.129 +  by (simp_all add: swap_def execute_simps)
   1.130 +
   1.131 +lemma success_swapI [success_intros]:
   1.132 +  "i < length a h \<Longrightarrow> success (swap i x a) h"
   1.133 +  by (auto intro: success_intros simp add: swap_def)
   1.134  
   1.135 -lemma execute_freeze [simp]:
   1.136 -  "Heap_Monad.execute (freeze a) h = Some (get_array a h, h)"
   1.137 +lemma execute_freeze [simp, execute_simps]:
   1.138 +  "execute (freeze a) h = Some (get_array a h, h)"
   1.139 +  by (simp add: freeze_def)
   1.140 +
   1.141 +lemma success_freezeI [iff, success_intros]:
   1.142 +  "success (freeze a) h"
   1.143    by (simp add: freeze_def)
   1.144  
   1.145  lemma upd_return:
   1.146 @@ -265,7 +306,7 @@
   1.147       x \<leftarrow> nth a i;
   1.148       upd i (f x) a
   1.149     done)"
   1.150 -  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def)
   1.151 +  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
   1.152  
   1.153  lemma [code]:
   1.154    "swap i x a = (do
   1.155 @@ -273,7 +314,7 @@
   1.156       upd i x a;
   1.157       return y
   1.158     done)"
   1.159 -  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def)
   1.160 +  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
   1.161  
   1.162  lemma [code]:
   1.163    "freeze a = (do
   1.164 @@ -288,18 +329,18 @@
   1.165       [0..<length a h] =
   1.166         List.map (List.nth (get_array a h)) [0..<length a h]"
   1.167      by simp
   1.168 -  have "Heap_Monad.execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
   1.169 +  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
   1.170      Some (get_array a h, h)"
   1.171      apply (subst execute_fold_map_unchanged_heap)
   1.172      apply (simp_all add: nth_def guard_def *)
   1.173      apply (simp add: length_def map_nth)
   1.174      done
   1.175 -  then have "Heap_Monad.execute (do
   1.176 +  then have "execute (do
   1.177        n \<leftarrow> len a;
   1.178        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.179      done) h = Some (get_array a h, h)"
   1.180      by (auto intro: execute_eq_SomeI)
   1.181 -  then show "Heap_Monad.execute (freeze a) h = Heap_Monad.execute (do
   1.182 +  then show "execute (freeze a) h = execute (do
   1.183        n \<leftarrow> len a;
   1.184        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.185      done) h" by simp